add facility to add lemmas

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

src/api/api_solver.cpp

@@ -258,6 +258,16 @@ extern "C" {
         to_solver_ref(s)->assert_expr(to_expr(a), to_expr(p));
         Z3_CATCH;
     }
+
+    void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_solver_assert_lemma(c, s, a);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        CHECK_FORMULA(a,);
+        to_solver_ref(s)->assert_lemma(to_expr(a));
+        Z3_CATCH;
+    }
     
     Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) {
         Z3_TRY;

src/api/dotnet/Solver.cs

@@ -181,6 +181,21 @@ namespace Microsoft.Z3
             Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
         }
 
+        /// <summary>
+        /// Assert a lemma (or multiple) into the solver.
+        /// </summary>        
+        public void AssertLemma(params BoolExpr[] constraints)
+        {
+            Contract.Requires(constraints != null);
+            Contract.Requires(Contract.ForAll(constraints, c => c != null));
+
+            Context.CheckContextMatch<BoolExpr>(constraints);
+            foreach (BoolExpr a in constraints)
+            {
+                Native.Z3_solver_assert_lemma(Context.nCtx, NativeObject, a.NativeObject);
+            }
+        }
+
         /// <summary>
         /// The number of assertions in the solver.
         /// </summary>

src/api/z3_api.h

@@ -5949,6 +5949,16 @@ extern "C" {
     */
     void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
 
+    /**
+       \brief add a lemma. A lemma is a assumed to be a consequence of the current assertions.
+       Adding a lemma should therefore be a logical no-op. Solvers are free to ignore lemmas.
+
+       \pre \c a must be a Boolean expression
+
+       def_API('Z3_solver_assert_lemma', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST)))
+     */
+    void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a);
+
     /**
        \brief Return the set of asserted formulas on the solver.
 

src/opt/opt_solver.h

@@ -92,6 +92,7 @@ namespace opt {
         virtual void collect_param_descrs(param_descrs & r);
         virtual void collect_statistics(statistics & st) const;
         virtual void assert_expr(expr * t);
+        virtual void assert_lemma(expr* t) {}
         virtual void push_core();
         virtual void pop_core(unsigned n);
         virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);        

src/sat/sat_solver.cpp

@@ -209,7 +209,7 @@ namespace sat {
         }
     }
 
-    void solver::mk_clause(unsigned num_lits, literal * lits) {
+    void solver::mk_clause(unsigned num_lits, literal * lits, bool learned) {
         m_model_is_current = false;
         DEBUG_CODE({
             for (unsigned i = 0; i < num_lits; i++)
@@ -217,24 +217,24 @@ namespace sat {
         });
 
         if (m_user_scope_literals.empty()) {
-            mk_clause_core(num_lits, lits, false);
+            mk_clause_core(num_lits, lits, learned);
         }
         else {
             m_aux_literals.reset();
             m_aux_literals.append(num_lits, lits);
             m_aux_literals.append(m_user_scope_literals);
-            mk_clause_core(m_aux_literals.size(), m_aux_literals.c_ptr(), false);
+            mk_clause_core(m_aux_literals.size(), m_aux_literals.c_ptr(), learned);
         }
     }
 
-    void solver::mk_clause(literal l1, literal l2) {
+    void solver::mk_clause(literal l1, literal l2, bool learned) {
         literal ls[2] = { l1, l2 };
-        mk_clause(2, ls);
+        mk_clause(2, ls, learned);
     }
 
-    void solver::mk_clause(literal l1, literal l2, literal l3) {
+    void solver::mk_clause(literal l1, literal l2, literal l3, bool learned) {
         literal ls[3] = { l1, l2, l3 };
-        mk_clause(3, ls);
+        mk_clause(3, ls, learned);
     }
 
     void solver::del_clause(clause& c) {

src/sat/sat_solver.h

@@ -203,10 +203,10 @@ namespace sat {
         //
         // -----------------------
         bool_var mk_var(bool ext = false, bool dvar = true);
-        void mk_clause(literal_vector const& lits) { mk_clause(lits.size(), lits.c_ptr()); }
-        void mk_clause(unsigned num_lits, literal * lits);
-        void mk_clause(literal l1, literal l2);
-        void mk_clause(literal l1, literal l2, literal l3);
+        void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); }
+        void mk_clause(unsigned num_lits, literal * lits, bool learned = false);
+        void mk_clause(literal l1, literal l2, bool learned = false);
+        void mk_clause(literal l1, literal l2, literal l3, bool learned = false);
 
     protected:
         void del_clause(clause & c);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -241,6 +241,16 @@ public:
             assert_expr(t);
         }
     }
+
+    virtual void assert_lemma(expr* e) {
+        dep2asm_t dep2asm;
+        goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
+        for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
+            g->assert_expr(m_fmls[i].get());
+        }
+        VERIFY(l_undef != internalize_goal(g, dep2asm, true));        
+    }
+
     virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr(expr * t) {
         m_internalized = false;
@@ -501,7 +511,7 @@ public:
 private:
 
 
-    lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
+    lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_mc.reset();
         m_pc.reset();
         m_dep_core.reset();
@@ -527,7 +537,7 @@ private:
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         TRACE("sat", g->display_with_dependencies(tout););
-        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
+        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true, is_lemma);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
             std::stringstream strm;
@@ -552,7 +562,7 @@ private:
         for (unsigned i = 0; i < get_num_assumptions(); ++i) {
             g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
         }
-        lbool res = internalize_goal(g, dep2asm);
+        lbool res = internalize_goal(g, dep2asm, false);
         if (res == l_true) {
             extract_assumptions(sz, asms, dep2asm);
         }
@@ -673,7 +683,7 @@ private:
         for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
             g->assert_expr(m_fmls[i].get());
         }
-        lbool res = internalize_goal(g, dep2asm);
+        lbool res = internalize_goal(g, dep2asm, false);
         if (res != l_undef) {
             m_fmls_head = m_fmls.size();
         }

src/sat/tactic/goal2sat.cpp

@@ -67,6 +67,7 @@ struct goal2sat::imp {
     expr_ref_vector             m_interpreted_atoms;
     bool                        m_default_external;
     bool                        m_xor_solver;
+    bool                        m_is_lemma;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
         m(_m),
@@ -77,7 +78,8 @@ struct goal2sat::imp {
         m_dep2asm(dep2asm),
         m_trail(m),
         m_interpreted_atoms(m),
-        m_default_external(default_external) {
+        m_default_external(default_external),
+        m_is_lemma(false) {
         updt_params(p);
         m_true = sat::null_bool_var;
     }
@@ -98,19 +100,21 @@ struct goal2sat::imp {
         m_solver.mk_clause(1, &l);
     }
 
+    void set_lemma_mode(bool f) { m_is_lemma = f; }
+
     void mk_clause(sat::literal l1, sat::literal l2) {
         TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
-        m_solver.mk_clause(l1, l2);
+        m_solver.mk_clause(l1, l2, m_is_lemma);
     }
 
     void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
         TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
-        m_solver.mk_clause(l1, l2, l3);
+        m_solver.mk_clause(l1, l2, l3, m_is_lemma);
     }
 
     void mk_clause(unsigned num, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
-        m_solver.mk_clause(num, lits);
+        m_solver.mk_clause(num, lits, m_is_lemma);
     }
 
     sat::bool_var mk_true() {
@@ -863,9 +867,10 @@ struct goal2sat::scoped_set_imp {
 };
 
 
-void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
+void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external, bool is_lemma) {
     imp proc(g.m(), p, t, m, dep2asm, default_external);
     scoped_set_imp set(this, &proc);
+    proc.set_lemma_mode(is_lemma);
     proc(g);
     dealloc(m_interpreted_atoms);
     m_interpreted_atoms = alloc(expr_ref_vector, g.m());

src/sat/tactic/goal2sat.h

@@ -50,6 +50,7 @@ public:
 
     static bool has_unsupported_bool(goal const & s);
 
+
     /**
        \brief "Compile" the goal into the given sat solver.
        Store a mapping from atoms to boolean variables into m.
@@ -60,7 +61,7 @@ public:
        \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
        an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
     */
-    void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
+    void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false, bool is_lemma = false);
 
     void get_interpreted_atoms(expr_ref_vector& atoms);
 

src/smt/smt_solver.cpp

@@ -116,6 +116,10 @@ namespace smt {
             m_name2assertion.insert(a, t);
         }
 
+        virtual void assert_lemma(expr* t) {
+            // no-op
+        }
+
         virtual void push_core() {
             m_context.push();
         }

src/solver/combined_solver.cpp

@@ -179,6 +179,12 @@ public:
         m_solver2->assert_expr(t, a);
     }
 
+    virtual void assert_lemma(expr* t) {
+        m_solver1->assert_lemma(t);
+        if (m_solver2_initialized)
+            m_solver2->assert_lemma(t);
+    }
+
     virtual void push() {
         switch_inc_mode();
         m_solver1->push();

src/solver/solver.h

@@ -90,6 +90,12 @@ public:
     */
     virtual void assert_expr(expr * t, expr * a) = 0;
 
+    /**
+       \brief Add a lemma to the assertion stack. A lemma is assumed to be a consequence of already
+       asserted formulas. The solver is free to ignore lemmas.
+    */
+    virtual void assert_lemma(expr * t) = 0;
+
     /**
        \brief Create a backtracking point.
     */

src/solver/tactic2solver.cpp

@@ -55,6 +55,7 @@ public:
     virtual void set_produce_models(bool f) { m_produce_models = f; }
 
     virtual void assert_expr(expr * t);
+    virtual void assert_lemma(expr * t);
 
     virtual void push_core();
     virtual void pop_core(unsigned n);
@@ -115,6 +116,9 @@ void tactic2solver::assert_expr(expr * t) {
     m_result = 0;
 }
 
+void tactic2solver::assert_lemma(expr * t) {    
+}
+
 void tactic2solver::push_core() {
     m_scopes.push_back(m_assertions.size());
     m_result = 0;

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -93,6 +93,10 @@ public:
         }
     }
 
+    virtual void assert_lemma(expr * t) {
+        m_solver->assert_lemma(t);
+    }
+
     virtual void push_core() {
         flush_assertions();
         m_solver->push();

src/tactic/portfolio/enum2bv_solver.cpp

@@ -64,6 +64,16 @@ public:
         m_solver->assert_expr(bounds);
     }
 
+    virtual void assert_lemma(expr* t) {
+        expr_ref tmp(t, m);
+        expr_ref_vector bounds(m);
+        proof_ref tmp_proof(m);
+        m_rewriter(t, tmp, tmp_proof);
+        m_solver->assert_lemma(tmp);
+        m_rewriter.flush_side_constraints(bounds);
+        m_solver->assert_expr(bounds);        
+    }  
+
     virtual void push_core() {
         m_rewriter.push();
         m_solver->push();

src/tactic/portfolio/pb2bv_solver.cpp

@@ -56,6 +56,10 @@ public:
         m_assertions.push_back(t);
     }
 
+    virtual void assert_lemma(expr * t) {
+        m_solver->assert_lemma(t);
+    }
+
     virtual void push_core() {
         flush_assertions();
         m_rewriter.push();