From 045bd2e0508a17c9d28681b9c9459e001c0a5597 Mon Sep 17 00:00:00 2001
From: Simon Vandevelde <s.vandevelde@kuleuven.be>
Date: Wed, 7 Aug 2024 12:31:17 +0200
Subject: [PATCH] Support consequences API (#302)

Add consequences, allowing you to derive implied propositions from a set of assumed propositions.
---
 z3/src/solver.rs | 35 +++++++++++++++++++++++++++++++++++
 z3/tests/lib.rs  | 29 +++++++++++++++++++++++++++++
 2 files changed, 64 insertions(+)

diff --git a/z3/src/solver.rs b/z3/src/solver.rs
index 13923d55..6d7d41f8 100644
--- a/z3/src/solver.rs
+++ b/z3/src/solver.rs
@@ -242,6 +242,41 @@ impl<'ctx> Solver<'ctx> {
         unsat_core
     }
 
+    /// Retrieve consequences from the solver given a set of assumptions.
+    pub fn get_consequences(&self,
+                            assumptions: &[ast::Bool<'ctx>],
+                            variables: &[ast::Bool<'ctx>],
+                            ) -> Vec<ast::Bool<'ctx>> {
+        unsafe {
+            let _assumptions = Z3_mk_ast_vector(self.ctx.z3_ctx);
+            Z3_ast_vector_inc_ref(self.ctx.z3_ctx, _assumptions);
+            assumptions.iter().for_each(|x| {
+                 Z3_ast_vector_push(self.ctx.z3_ctx, _assumptions, x.z3_ast.clone());
+            });
+
+            let _variables = Z3_mk_ast_vector(self.ctx.z3_ctx);
+            Z3_ast_vector_inc_ref(self.ctx.z3_ctx, _variables);
+            variables.iter().for_each(|x| {
+                Z3_ast_vector_push(self.ctx.z3_ctx, _variables, x.z3_ast.clone());
+            });
+            let consequences = Z3_mk_ast_vector(self.ctx.z3_ctx);
+            Z3_ast_vector_inc_ref(self.ctx.z3_ctx, consequences);
+
+            Z3_solver_get_consequences(self.ctx.z3_ctx,
+                                           self.z3_slv,
+                                           _assumptions,
+                                           _variables,
+                                           consequences);
+            let mut cons = vec!();
+            for i in 0..Z3_ast_vector_size(self.ctx.z3_ctx, consequences) {
+                let val = Z3_ast_vector_get(self.ctx.z3_ctx, consequences, i);
+                cons.push(ast::Bool::wrap(self.ctx, val));
+            }
+            cons
+        }
+    }
+
+
     /// Create a backtracking point.
     ///
     /// The solver contains a stack of assertions.
diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs
index 59b294e4..a2b53f01 100644
--- a/z3/tests/lib.rs
+++ b/z3/tests/lib.rs
@@ -1892,3 +1892,32 @@ fn get_version() {
     println!("Z3 version: {:?}", z3::version());
     println!("Z3 full version string: {}", z3::full_version());
 }
+
+#[test]
+fn test_consequences() {
+    let cfg = Config::new();
+    let ctx = &Context::new(&cfg);
+    let solver = Solver::new(ctx);
+    let a = Bool::new_const(&ctx, "a");
+    let b = Bool::new_const(&ctx, "b");
+    let c = Bool::new_const(&ctx, "c");
+    let d = Bool::new_const(&ctx, "d");
+    solver.assert(&a.implies(&b));
+    solver.assert(&b.implies(&c));
+
+    let assumptions = vec!(a.clone());
+    let variables = vec!(b.clone(), c.clone(), d.clone());
+    let mut cons = solver.get_consequences(&assumptions, &variables);
+    assert!(cons.len() == 2);
+    assert!(cons.pop().unwrap().to_string() == "(=> a c)");
+    assert!(cons.pop().unwrap().to_string() == "(=> a b)");
+
+    let assumptions = vec!(c.not(), d.clone());
+    let variables = vec!(a, b, c, d);
+    let mut cons = solver.get_consequences(&assumptions, &variables);
+    assert!(cons.len() == 4);
+    assert!(cons.pop().unwrap().to_string() == "(=> (not c) (not a))");
+    assert!(cons.pop().unwrap().to_string() == "(=> (not c) (not b))");
+    assert!(cons.pop().unwrap().to_string() == "(=> (not c) (not c))");
+    assert!(cons.pop().unwrap().to_string() == "(=> d d)");
+}