Add plain version of fuel, not using datatype

moves-rwth · Feb 7, 2025 · ca9b5a4 · ca9b5a4
1 parent 932eedb
commit ca9b5a4
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 7 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -13,9 +13,10 @@ edition = "2021"
 build = "build.rs" # LALRPOP preprocessing
 
 [features]
-default = ["static-link-z3"]
+default = ["static-link-z3", "datatype-fuel"]
 datatype-eureal = ["z3rro/datatype-eureal"]
 datatype-eureal-funcs = ["z3rro/datatype-eureal-funcs"]
+datatype-fuel=["z3rro/datatype-fuel"]
 static-link-z3 = ["z3/static-link-z3"]
 # Emit log messages to stderr without timing information. This is useful to diff logs.
 log-print-timeless = []

diff --git a/z3rro/Cargo.toml b/z3rro/Cargo.toml
@@ -17,3 +17,4 @@ im-rc = "15"
 [features]
 datatype-eureal = []
 datatype-eureal-funcs = ["datatype-eureal"]
+datatype-fuel = []
diff --git a/z3rro/src/fuel.rs b/z3rro/src/fuel.rs
@@ -13,6 +13,7 @@ pub struct FuelFactory<'ctx> {
 }
 
 impl<'ctx> FuelFactory<'ctx> {
+    #[cfg(feature = "datatype-fuel")]
     pub fn new(ctx: &'ctx Context) -> Rc<Self> {
         // Clashes with user defined code are avoided by `$` in names
         let datatype = DatatypeBuilder::new(ctx, "$Fuel")
@@ -36,6 +37,22 @@ impl<'ctx> FuelFactory<'ctx> {
         Rc::new(factory)
     }
 
+    #[cfg(not(feature = "datatype-fuel"))]
+    pub fn new(ctx: &'ctx Context) -> Rc<Self> {
+        // Clashes with user defined code are avoided by `$` in names
+        let fuel_sort = Sort::uninterpreted(ctx, Symbol::from("$Fuel"));
+        let zero = FuncDecl::new(ctx, "$Z", &[], &fuel_sort);
+        let succ = FuncDecl::new(ctx, "$S", &[&fuel_sort], &fuel_sort);
+
+        let factory = Self {
+            ctx,
+            sort: fuel_sort,
+            zero,
+            succ,
+        };
+        Rc::new(factory)
+    }
+
     pub fn sort(&self) -> &Sort<'ctx> {
         &self.sort
     }
@@ -52,7 +69,7 @@ impl<'ctx> FuelFactory<'ctx> {
 #[derive(Debug, Clone)]
 pub struct Fuel<'ctx> {
     factory: Rc<FuelFactory<'ctx>>,
-    value: Datatype<'ctx>,
+    value: Dynamic<'ctx>,
 }
 
 impl<'ctx> Fuel<'ctx> {
@@ -65,7 +82,7 @@ impl<'ctx> Fuel<'ctx> {
     }
 
     pub fn zero(factory: Factory<'ctx, Self>) -> Self {
-        let value = factory.zero.apply(&[]).as_datatype().unwrap();
+        let value = factory.zero.apply(&[]);
 
         Self { factory, value }
     }
@@ -74,9 +91,7 @@ impl<'ctx> Fuel<'ctx> {
         let factory = fuel.factory;
         let value = factory
             .succ
-            .apply(&[&fuel.value as &dyn Ast<'ctx>])
-            .as_datatype()
-            .unwrap();
+            .apply(&[&fuel.value as &dyn Ast<'ctx>]);
 
         Self { factory, value }
     }
@@ -109,7 +124,18 @@ impl<'ctx> SmtFresh<'ctx> for Fuel<'ctx> {
         let datatype_factory = (factory.ctx, factory.sort.clone());
         Fuel {
             factory: factory.clone(),
-            value: Datatype::allocate(&datatype_factory, alloc, prefix),
+            value: Dynamic::allocate(&datatype_factory, alloc, prefix),
         }
+        /*cfg_if::cfg_if! {
+            if #[cfg(feature="datatype-fuel")] {
+                let datatype_factory = (factory.ctx, factory.sort.clone());
+                Fuel {
+                    factory: factory.clone(),
+                    value: Datatype::allocate(&datatype_factory, alloc, prefix),
+                }
+            } else {
+
+            }
+        }*/
     }
 }