Limited functions

.gitignore

@@ -1,4 +1,5 @@
 target
+.idea
 .DS_Store
 benchmark-results.csv
 vscode-ext/node_modules/

Cargo.toml

@@ -18,9 +18,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 = []
@@ -86,8 +87,8 @@ harness = false
 opt-level = 3
 
 [patch.crates-io]
-z3 = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
-z3-sys = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
+z3 = { git = 'https://github.com/prove-rs/z3.rs.git', rev = '60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf' }
+z3-sys = { git = 'https://github.com/prove-rs/z3.rs.git', rev = '60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf' }
 # to work on z3.rs locally, clone it into the main directory and use the following directive instead:
 # z3 = { path = 'z3.rs/z3' }
 

src/ast/decl.rs

@@ -444,6 +444,15 @@ pub struct DomainDecl {
     pub span: Span,
 }
 
+impl DomainDecl {
+    pub fn function_decls(&self) -> impl Iterator<Item = &DeclRef<FuncDecl>> {
+        self.body.iter().filter_map(|spec| match spec {
+            DomainSpec::Function(func_ref) => Some(func_ref),
+            _ => None,
+        })
+    }
+}
+
 impl SimplePretty for DomainDecl {
     fn pretty(&self) -> Doc {
         Doc::text("domain")
@@ -484,6 +493,7 @@ pub struct FuncDecl {
     /// The body is in a [`RefCell`] so that we can have an exclusive reference
     /// to it while still retrieving a shared reference to the declaration
     pub body: RefCell<Option<Expr>>,
+    pub computable: bool,
     pub span: Span,
 }
 

src/ast/expr.rs

@@ -66,6 +66,21 @@ pub enum ExprKind {
     Lit(Lit),
 }
 
+impl Expr {
+    pub fn children_mut(&mut self) -> Vec<&mut Expr> {
+        match &mut self.kind {
+            ExprKind::Var(_) | ExprKind::Lit(_) => vec![],
+            ExprKind::Call(_, args) => args.iter_mut().collect(),
+            ExprKind::Ite(cond, branch1, branch2) => vec![cond, branch1, branch2],
+            ExprKind::Binary(_, lhs, rhs) => vec![lhs, rhs],
+            ExprKind::Unary(_, operand) => vec![operand],
+            ExprKind::Cast(operand) => vec![operand],
+            ExprKind::Quant(_, _, _, expr) => vec![expr],
+            ExprKind::Subst(_, subst, expr) => vec![subst, expr],
+        }
+    }
+}
+
 impl SimplePretty for Expr {
     fn pretty(&self) -> Doc {
         let res = match &self.kind {

src/ast/shared.rs

@@ -1,3 +1,6 @@
+use ref_cast::RefCast;
+use std::cmp::Ordering;
+use std::hash::{Hash, Hasher};
 use std::{
     fmt,
     ops::{Deref, DerefMut},
@@ -72,3 +75,48 @@ impl<T: ?Sized + fmt::Debug> fmt::Debug for Shared<T> {
         fmt::Debug::fmt(&**self, f)
     }
 }
+
+/// [Shared] wrapper that provides pointer based [Eq] and [Hash] implementations.
+#[repr(transparent)]
+#[derive(RefCast, Clone)]
+pub struct PointerHashShared<T>(Shared<T>);
+
+impl<T> PointerHashShared<T> {
+    pub fn new(shared: Shared<T>) -> Self {
+        Self(shared)
+    }
+
+    pub fn into_shared(self) -> Shared<T> {
+        self.0
+    }
+
+    pub fn as_shared(&self) -> &Shared<T> {
+        &self.0
+    }
+}
+
+impl<T> PartialEq for PointerHashShared<T> {
+    fn eq(&self, other: &Self) -> bool {
+        Shared::as_ptr(&self.0) == Shared::as_ptr(&other.0)
+    }
+}
+
+impl<T> Eq for PointerHashShared<T> {}
+
+impl<T> Ord for PointerHashShared<T> {
+    fn cmp(&self, other: &Self) -> Ordering {
+        Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0))
+    }
+}
+
+impl<T> PartialOrd for PointerHashShared<T> {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0)))
+    }
+}
+
+impl<T> Hash for PointerHashShared<T> {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        Shared::as_ptr(&self.0).hash(state)
+    }
+}

src/driver.rs

@@ -70,6 +70,7 @@ use z3rro::{
     util::{PrefixWriter, ReasonUnknown},
 };
 
+use crate::smt::{LiteralExprCollector, SmtCtxOptions};
 use tracing::{info_span, instrument, trace};
 
 /// Human-readable name for a source unit. Used for debugging and error messages.
@@ -558,7 +559,7 @@ impl QuantVcUnit {
         let _entered = span.enter();
         if !options.opt_options.strict {
             let ctx = Context::new(&Config::default());
-            let smt_ctx = SmtCtx::new(&ctx, tcx);
+            let smt_ctx = SmtCtx::new(&ctx, tcx, SmtCtxOptions::default());
             let mut unfolder = Unfolder::new(limits_ref.clone(), &smt_ctx);
             unfolder.visit_expr(&mut self.expr)
         } else {
@@ -657,14 +658,23 @@ impl BoolVcUnit {
 
     /// Translate to SMT.
     pub fn into_smt_vc<'smt, 'ctx>(
-        self,
+        mut self,
         translate: &mut TranslateExprs<'smt, 'ctx>,
     ) -> SmtVcUnit<'ctx> {
         let span = info_span!("translation to Z3");
         let _entered = span.enter();
+
+        translate.set_literal_exprs(
+            LiteralExprCollector::new()
+                .with_computable_functions(translate.ctx.computable_functions().as_slice())
+                .collect(&mut self.vc),
+        );
+        let bool_vc = translate.t_bool(&self.vc);
+        translate.clear_literal_exprs();
+
         SmtVcUnit {
             quant_vc: self.quant_vc,
-            vc: translate.t_bool(&self.vc),
+            vc: bool_vc,
         }
     }
 }
@@ -830,6 +840,8 @@ fn mk_valid_query_prover<'smt, 'ctx>(
         prover.set_timeout(remaining);
     }
 
+    // add the definition of all used Lit marker functions
+    smt_translate.ctx.add_lit_axioms_to_prover(&mut prover);
     // add assumptions (from axioms and locals) to the prover
     smt_translate
         .ctx

src/front/parser/grammar.lalrpop

@@ -264,10 +264,10 @@ DomainDecl: DomainDecl = {
 }
 
 DomainSpec: DomainSpec = {
-    <l: @L> "func" <name: Ident> <inputs: ParamList> ":" <output: Ty> <r: @R>
-        => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), span: span(file, l, r) })),
-    <l: @L> "func" <name: Ident> <inputs: ParamList> ":" <output: Ty> "=" <body: Expr> <r: @R>
-        => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), span: span(file, l, r) })),
+    <l: @L> <comp:"@computable"?> "func" <name: Ident> <inputs: ParamList> ":" <output: Ty> <r: @R>
+        => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(None), computable: comp.is_some(), span: span(file, l, r) })),
+    <l: @L> <comp:"@computable"?> "func" <name: Ident> <inputs: ParamList> ":" <output: Ty> "=" <body: Expr> <r: @R>
+        => DomainSpec::Function(DeclRef::new(FuncDecl { name, inputs, output, body: RefCell::new(Some(body)), computable: comp.is_some(), span: span(file, l, r) })),
     <l: @L> "axiom" <name: Ident> <axiom: Expr> <r: @R>
         => DomainSpec::Axiom(DeclRef::new(AxiomDecl{ name, axiom, span: span(file, l, r) }))
 }