From caced62f40f0d2bd61c4e7e5d7e7b69251d13424 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Nov 2012 15:54:31 -0800 Subject: [PATCH] New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 69 +++++++++++++++++++++++++++++++++++++--- src/api/api_solver.cpp | 11 +++++++ src/api/c++/z3++.h | 54 ++++++++++++++++++++++++++++++- src/api/python/z3.py | 23 ++++++++++++++ src/api/z3_api.h | 18 ++++++++++- 5 files changed, 168 insertions(+), 7 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 29c3a25b9..180117a96 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -336,6 +336,35 @@ void ite_example() { std::cout << "term: " << ite << "\n"; } +/** + \brief Small example using quantifiers. +*/ +void quantifier_example() { + std::cout << "quantifier example\n"; + context c; + + expr x = c.int_const("x"); + expr y = c.int_const("y"); + sort I = c.int_sort(); + func_decl f = function("f", I, I, I); + + solver s(c); + + // making sure model based quantifier instantiation is enabled. + params p(c); + p.set(":mbqi", true); + s.set(p); + + s.add(forall(x, y, f(x, y) >= 0)); + expr a = c.int_const("a"); + s.add(f(a, a) < a); + std::cout << s << "\n"; + std::cout << s.check() << "\n"; + std::cout << s.get_model() << "\n"; + s.add(a < 0); + std::cout << s.check() << "\n"; +} + /** \brief Unsat core example */ @@ -426,6 +455,37 @@ void unsat_core_example2() { } } +/** + \brief Unsat core example 3 +*/ +void unsat_core_example3() { + // Extract unsat core using tracked assertions + std::cout << "unsat core example 3\n"; + context c; + expr x = c.int_const("x"); + expr y = c.int_const("y"); + solver s(c); + + // enabling unsat core tracking + params p(c); + p.set(":unsat-core", true); + s.set(p); + + // The following assertion will not be tracked. + s.add(x > 0); + + // The following assertion will be tracked using Boolean variable p1. + // The C++ wrapper will automatically create the Boolean variable. + s.add(y > 0, "p1"); + + // Asserting other tracked assertions. + s.add(x < 10, "p2"); + s.add(y < 0, "p3"); + + std::cout << s.check() << "\n"; + std::cout << s.unsat_core() << "\n"; +} + void tactic_example1() { /* Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic @@ -709,11 +769,8 @@ void tactic_qe() { expr x = c.int_const("x"); expr f = implies(x <= a, x < b); - // We have to use the C API directly for creating quantified formulas. - Z3_app vars[] = {(Z3_app) x}; - expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars, - 0, 0, // no pattern - f)); + expr qf = forall(x, f); + std::cout << qf << "\n"; s.add(qf); @@ -769,8 +826,10 @@ int main() { error_example(); std::cout << "\n"; numeral_example(); std::cout << "\n"; ite_example(); std::cout << "\n"; + quantifier_example(); std::cout << "\n"; unsat_core_example1(); std::cout << "\n"; unsat_core_example2(); std::cout << "\n"; + unsat_core_example3(); std::cout << "\n"; tactic_example1(); std::cout << "\n"; tactic_example2(); std::cout << "\n"; tactic_example3(); std::cout << "\n"; diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6d1becb4d..790ca8f59 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -203,6 +203,17 @@ extern "C" { to_solver_ref(s)->assert_expr(to_expr(a)); Z3_CATCH; } + + void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p) { + Z3_TRY; + LOG_Z3_solver_assert_and_track(c, s, a, p); + RESET_ERROR_CODE(); + init_solver(c, s); + CHECK_FORMULA(a,); + CHECK_FORMULA(p,); + to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p)); + Z3_CATCH; + } Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) { Z3_TRY; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8a2499321..4130c2622 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -331,6 +331,7 @@ namespace z3 { bool is_numeral() const { return kind() == Z3_NUMERAL_AST; } bool is_app() const { return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; } + bool is_const() const { return is_app() && num_args() == 0; } bool is_quantifier() const { return kind() == Z3_QUANTIFIER_AST; } bool is_var() const { return kind() == Z3_VAR_AST; } @@ -600,7 +601,7 @@ namespace z3 { expr simplify() const { Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); } expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); } }; - + /** \brief Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file. @@ -654,6 +655,49 @@ namespace z3 { inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); } inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); } inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), a); } + + // Basic functions for creating quantified formulas. + // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. + inline expr forall(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } template class cast_ast; @@ -889,6 +933,14 @@ namespace z3 { void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); } void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } void add(expr const & e) { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); } + void add(expr const & e, expr const & p) { + assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const()); + Z3_solver_assert_and_track(ctx(), m_solver, e, p); + check_error(); + } + void add(expr const & e, char const * p) { + add(e, ctx().bool_const(p)); + } check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); } check_result check(unsigned n, expr * const assumptions) { array _assumptions(n); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 0a1eec722..f3de4258a 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5743,7 +5743,30 @@ class Solver(Z3PPObject): [x > 0, x < 2] """ self.assert_exprs(*args) + + def assert_and_track(self, a, p): + """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. + If `p` is a string, it will be automatically converted into a Boolean constant. + + >>> x = Int('x') + >>> p3 = Bool('p3') + >>> s = Solver() + >>> s.set(unsat_core=True) + >>> s.assert_and_track(x > 0, 'p1') + >>> s.assert_and_track(x != 1, 'p2') + >>> s.assert_and_track(x < 0, p3) + >>> print s.check() + unsat + >>> print s.unsat_core() + [p3, p1] + """ + if isinstance(p, str): + p = Bool(p, self.ctx) + _z3_assert(isinstance(a, BoolRef), "Boolean expression expected") + _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected") + Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast()) + def check(self, *assumptions): """Check whether the assertions in the given solver plus the optional assumptions are consistent or not. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index fe4aa8301..8d00fb044 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6609,6 +6609,22 @@ END_MLAPI_EXCLUDE def_API('Z3_solver_assert', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST))) */ void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a); + + /** + \brief Assert a constraint \c a into the solver, and track it (in the unsat) core using + the Boolean constant \c p. + + This API is an alternative to #Z3_solver_check_assumptions for extracting unsat cores. + Both APIs can be used in the same solver. The unsat core will contain a combination + of the Boolean variables provided using Z3_solver_assert_and_track and the Boolean literals + provided using #Z3_solver_check_assumptions. + + \pre \c a must be a Boolean expression + \pre \c p must be a Boolean constant (aka variable). + + def_API('Z3_solver_assert_and_track', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST))) + */ + void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p); /** \brief Return the set of asserted formulas as a goal object. @@ -6645,7 +6661,7 @@ END_MLAPI_EXCLUDE */ Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[]); - + /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions