diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 518fa5384..799a2b56b 100644 --- a/src/api/api_solver.cpp +++ b/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(result); + Z3_CATCH_RETURN(Z3_L_UNDEF); + } + }; diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index c9e76e68e..f8f340373 100644 --- a/src/api/dotnet/Solver.cs +++ b/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) - { - case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; - default: return Status.UNKNOWN; - } + return lboolToStatus(r); + } + + /// + /// 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. + /// + /// + /// + /// + /// + /// + public Status Consequences(IEnumerable assumptions, IEnumerable 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); } /// @@ -295,7 +318,7 @@ namespace Microsoft.Z3 /// public Solver Translate(Context ctx) { - Contract.Requires(ctx != null); + Contract.Requires(ctx != null); Contract.Ensures(Contract.Result() != 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 } } diff --git a/src/api/python/z3.py b/src/api/python/z3.py index ca02975f1..7dfb95318 100644 --- a/src/api/python/z3.py +++ b/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) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 41ca923bb..3334d1617 100644 --- a/src/api/z3_api.h +++ b/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 diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 3bbe1c3fd..c587a1722 100644 --- a/src/solver/solver.cpp +++ b/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; +} diff --git a/src/solver/solver.h b/src/solver/solver.h index e4e4942d3..d55db9821 100644 --- a/src/solver/solver.h +++ b/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 - built from fns. For functions that take 0 arguments, we require that the function returns all consequences - that mention these functions. The consequences are clauses whose first literal constrain one of the - functions from fns 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); + \brief under assumptions, asms, retrieve set of consequences that + fix values for expressions that can be built from vars. + The consequences are clauses whose first literal constrain one of the + functions from vars and the other literals are negations of literals from asms. + */ + + 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.