add basic built-in consequence finding

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_solver.cpp

@@ -413,4 +413,42 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);
     }
 
+    Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, 
+                                        Z3_solver s,
+                                        Z3_ast_vector assumptions,
+                                        Z3_ast_vector variables,
+                                        Z3_ast_vector consequences) {
+        Z3_TRY;
+        LOG_Z3_solver_get_consequences(c, s, assumptions, variables, consequences);
+        ast_manager& m = mk_c(c)->m();
+        RESET_ERROR_CODE();
+        CHECK_SEARCHING(c);
+        init_solver(c, s);
+        expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
+        ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
+        unsigned sz = __assumptions.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            if (!is_expr(__assumptions[i])) {
+                SET_ERROR_CODE(Z3_INVALID_USAGE);
+                return Z3_L_UNDEF;
+            }
+            _assumptions.push_back(to_expr(__assumptions[i]));
+        }
+        ast_ref_vector const& __variables = to_ast_vector_ref(variables);
+        sz = __variables.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            if (!is_expr(__variables[i])) {
+                SET_ERROR_CODE(Z3_INVALID_USAGE);
+                return Z3_L_UNDEF;
+            }
+            _variables.push_back(to_expr(__variables[i]));
+        }
+        lbool result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
+        for (unsigned i = 0; i < _consequences.size(); ++i) {
+            to_ast_vector_ref(consequences).push_back(_consequences[i].get());
+        }
+        return static_cast<Z3_lbool>(result); 
+        Z3_CATCH_RETURN(Z3_L_UNDEF);        
+    }
+
 };

src/api/dotnet/Solver.cs

@@ -18,6 +18,7 @@ Notes:
 --*/
 
 using System;
+using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Z3
@@ -212,12 +213,34 @@ namespace Microsoft.Z3
                 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
-            switch (r)
+            return lboolToStatus(r);
-            {
+        }
-                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
+
-                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
+        /// <summary>
-                default: return Status.UNKNOWN;
+        /// Retrieve fixed assignments to the set of variables in the form of consequences.
-            }
+        /// Each consequence is an implication of the form 
+        ///
+        ///       relevant-assumptions Implies variable = value
+        /// 
+        /// where the relevant assumptions is a subset of the assumptions that are passed in
+        /// and the equality on the right side of the implication indicates how a variable
+        /// is fixed.
+        /// </summary>
+        /// <remarks>
+        /// <seealso cref="Model"/>
+        /// <seealso cref="UnsatCore"/>
+        /// <seealso cref="Proof"/>    
+        /// </remarks>    
+        public Status Consequences(IEnumerable<BoolExpr> assumptions, IEnumerable<Expr> variables, out BoolExpr[] consequences) 
+        {
+            ASTVector result = new ASTVector(Context);
+            ASTVector asms = new ASTVector(Context);
+            ASTVector vars = new ASTVector(Context);
+            foreach (var asm in assumptions) asms.Push(asm);
+            foreach (var v in variables) vars.Push(v);
+            Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
+            consequences = result.ToBoolExprArray();
+            return lboolToStatus(r);
         }
 
         /// <summary>
@@ -295,7 +318,7 @@ namespace Microsoft.Z3
         /// </summary>
         public Solver Translate(Context ctx) 
         {
-	     Contract.Requires(ctx != null);
+             Contract.Requires(ctx != null);
              Contract.Ensures(Contract.Result<Solver>() != null);
              return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
         }
@@ -355,6 +378,17 @@ namespace Microsoft.Z3
             Context.Solver_DRQ.Add(o);
             base.DecRef(o);
         }
+
+        private Status lboolToStatus(Z3_lbool r) 
+        {
+            switch (r)
+            {
+                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
+                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
+                default: return Status.UNKNOWN;
+            }
+        }
+
         #endregion
     }
 }

src/api/python/z3.py

@@ -6123,6 +6123,28 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
 
+    def consequences(self, assumptions, variables):
+        """Determine fixed values for the variables based on the solver state and assumptions.
+        documentation TBD
+        """
+        if isinstance(assumptions, list):
+            _asms = AstVector(None, self.ctx)
+            for a in assumptions:
+                _asms.push(a)
+            assumptions = _asms
+        if isinstance(variables, list):
+            _vars = AstVector(None, self.ctx)
+            for a in variables:
+                _vars.push(a)
+            variables = _vars            
+        _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
+        _z3_assert(isinstance(variables, AstVector), "ast vector expected")
+        consequences = AstVector(None, self.ctx)
+        r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
+        sz = len(consequences)
+        consequences = [ consequences[i] for i in range(sz) ]
+        return CheckSatResult(r), consequences
+    
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""
         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)

src/api/z3_api.h

@@ -5887,6 +5887,17 @@ extern "C" {
                                               Z3_ast const terms[],
                                               unsigned class_ids[]);
 
+    /**
+       \brief retrieve consequences from solver that determine values of the supplied function symbols.
+       
+       def_API('Z3_solver_get_consequences', INT, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))
+     */
+
+    Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, 
+                                               Z3_solver s,
+                                               Z3_ast_vector assumptions,
+                                               Z3_ast_vector variables,
+                                               Z3_ast_vector consequences);
     /**
        \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions
 

src/solver/solver.cpp

@@ -17,6 +17,8 @@ Notes:
 
 --*/
 #include"solver.h"
+#include"model_evaluator.h"
+#include"ast_util.h"
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();
@@ -38,3 +40,82 @@ void solver::get_assertions(expr_ref_vector& fmls) const {
         fmls.push_back(get_assertion(i));
     }
 }
+
+struct scoped_assumption_push {
+    expr_ref_vector& m_vec;
+    scoped_assumption_push(expr_ref_vector& v, expr* e): m_vec(v) { v.push_back(e); }
+    ~scoped_assumption_push() { m_vec.pop_back(); }
+};
+
+lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
+    ast_manager& m = asms.get_manager();
+    lbool is_sat = check_sat(asms);
+    if (is_sat != l_true) {
+        return is_sat;
+    }
+    model_ref model;
+    get_model(model);
+    expr_ref tmp(m), nlit(m), lit(m), val(m);
+    expr_ref_vector asms1(asms);
+    model_evaluator eval(*model.get());
+    unsigned k = 0;
+    for (unsigned i = 0; i < vars.size(); ++i) {
+        expr_ref_vector core(m);
+        tmp = vars[i];
+        val = eval(tmp);
+        if (!m.is_value(val)) {
+            continue;
+        }
+        if (m.is_bool(tmp) && is_uninterp_const(tmp)) {
+            if (m.is_true(val)) {
+                nlit = m.mk_not(tmp);
+                lit = tmp;
+            }
+            else if (m.is_false(val)) {
+                nlit = tmp;
+                lit = m.mk_not(tmp);
+            }
+            else {
+                continue;
+            }
+            scoped_assumption_push _scoped_push(asms1, nlit);
+            is_sat = check_sat(asms1);
+            switch (is_sat) {
+            case l_undef: 
+                return is_sat;
+            case l_true:
+                break;
+            case l_false:
+                get_unsat_core(core);
+                k = 0;
+                for (unsigned j = 0; j < core.size(); ++j) {
+                    if (core[j].get() != nlit) {
+                        core[k] = core[j].get();
+                        ++k;
+                    }
+                }
+                core.resize(k);
+                consequences.push_back(m.mk_implies(mk_and(core), lit));
+                break;
+            }
+        }
+        else {
+            lit = m.mk_eq(tmp, val);
+            nlit = m.mk_not(lit);
+            scoped_push _scoped_push(*this);
+            assert_expr(nlit);
+            is_sat = check_sat(asms);            
+            switch (is_sat) {
+            case l_undef: 
+                return is_sat;
+            case l_true:
+                break;
+            case l_false:
+                get_unsat_core(core);
+                consequences.push_back(m.mk_implies(mk_and(core), lit));
+                break;
+            }            
+        }
+    }
+    return l_true;
+}

src/solver/solver.h

@@ -150,12 +150,13 @@ public:
     virtual expr * get_assumption(unsigned idx) const = 0;
 
     /**
-    \brief under assumptions, asms, retrieve set of consequences that fix values for expressions that can be 
+    \brief under assumptions, asms, retrieve set of consequences that 
-      built from fns. For functions that take 0 arguments, we require that the function returns all consequences
+    fix values for expressions that can be built from vars. 
-      that mention these functions. The consequences are clauses whose first literal constrain one of the 
+    The consequences are clauses whose first literal constrain one of the 
-      functions from fns and the other literals are negations of literals from asms.
+    functions from vars and the other literals are negations of literals from asms.
-     */
+    */
-    //virtual lbool get_consequences(expr_ref_vector const& asms, func_ref_vector const& fns, expr_ref_vector& consequences);
+    
+    virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
 
     /**
        \brief Display the content of this solver.