Support consequences API (#302)

z3/src/solver.rs

@@ -242,6 +242,43 @@ 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);
+            });
+
+            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);
+            });
+            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.

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)");
+}