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 <leonardo@microsoft.com>

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.
+    expr qf = forall(x, f);
-    Z3_app vars[] = {(Z3_app) x};
+
-    expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars,
-                                            0, 0, // no pattern
-                                            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";

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;

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<typename T> 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<Z3_ast> _assumptions(n);

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.
         

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