fix bugs in incremental operation of sat solver

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

src/api/dotnet/Context.cs

@@ -2266,7 +2266,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a pseudo-Boolean <= constraint.
+        /// Create a pseudo-Boolean less-or-equal constraint.
         /// </summary>
         public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) 
         {

src/api/dotnet/Fixedpoint.cs

@@ -316,6 +316,7 @@ namespace Microsoft.Z3
             }
         }
 
+	/// <summary>
         /// Parse an SMT-LIB2 file with fixedpoint rules. 
         /// Add the rules to the current fixedpoint context. 
         /// Return the set of queries in the file.

src/api/dotnet/Optimize.cs

@@ -98,7 +98,15 @@ namespace Microsoft.Z3
 	        return Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);            
         }
 
-	    public Status Check() {
+	
+	///
+	/// <summary>
+	/// Check satisfiability of asserted constraints.
+	/// Produce a model that (when the objectives are bounded and 
+	/// don't use strict inequalities) meets the objectives.
+	/// </summary>
+	///
+        public Status Check() {
 	        Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
             switch (r)
             {
@@ -150,26 +158,46 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Declare an arithmetical maximization objective.
+	/// Return a handle to the objective. The handle is used as
+	/// an argument to GetLower and GetUpper.
+        /// </summary>        	
         public uint MkMaximize(ArithExpr e) 
         {
 	        return Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
 	    }
 
+        /// <summary>
+        /// Declare an arithmetical minimization objective. 
+	/// Similar to MkMaximize.
+        /// </summary>        	
         public uint MkMinimize(ArithExpr e)
         {
 	        return Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
         }
 
+        /// <summary>
+        /// Retrieve a lower bound for the objective handle.
+        /// </summary>        	
         public ArithExpr GetLower(uint index) 
         {
             return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
         }
 
+
+        /// <summary>
+        /// Retrieve an upper bound for the objective handle.
+        /// </summary>        	
         public ArithExpr GetUpper(uint index)
         {
             return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
+
+        /// <summary>
+        /// Print the context to a string (SMT-LIB parseable benchmark).
+        /// </summary>        	
         public override string ToString() 
         {
             return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);

src/opt/inc_sat_solver.cpp

@@ -39,8 +39,9 @@ class inc_sat_solver : public solver {
     params_ref      m_params;
     bool            m_optimize_model; // parameter
     expr_ref_vector m_fmls;
-    expr_ref_vector m_current_fmls;
     unsigned_vector m_fmls_lim;
+    unsigned_vector m_fmls_head_lim;
+    unsigned            m_fmls_head;
     expr_ref_vector     m_core;
     atom2bool_var       m_map;
     model_ref           m_model;
@@ -61,7 +62,10 @@ public:
     inc_sat_solver(ast_manager& m, params_ref const& p):
         m(m), m_solver(p,0), 
         m_params(p), m_optimize_model(false), 
-        m_fmls(m), m_current_fmls(m), m_core(m), m_map(m),
+        m_fmls(m), 
+        m_fmls_head(0),
+        m_core(m), 
+        m_map(m),
         m_num_scopes(0), 
         m_dep_core(m),
         m_soft(m) {
@@ -127,9 +131,11 @@ public:
         if (f) m_preprocess->cancel(); else m_preprocess->reset_cancel();
     }
     virtual void push() {
+        internalize_formulas();
         m_solver.user_push();
         ++m_num_scopes;
-        m_fmls_lim.push_back(m_current_fmls.size());
+        m_fmls_lim.push_back(m_fmls.size());
+        m_fmls_head_lim.push_back(m_fmls_head);
     }
     virtual void pop(unsigned n) {
         if (n < m_num_scopes) {   // allow inc_sat_solver to 
@@ -139,8 +145,10 @@ public:
         m_solver.user_pop(n);        
         m_num_scopes -= n;
         while (n > 0) {
-            m_current_fmls.resize(m_fmls_lim.back());
+            m_fmls_head = m_fmls_head_lim.back();
+            m_fmls.resize(m_fmls_lim.back());
             m_fmls_lim.pop_back();
+            m_fmls_head_lim.pop_back();
             --n;
         }
     }
@@ -156,8 +164,8 @@ public:
         }
     }
     virtual void assert_expr(expr * t) {
+        TRACE("opt", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
-        m_current_fmls.push_back(t);
     }
     virtual void set_produce_models(bool f) {}
     virtual void collect_param_descrs(param_descrs & r) {
@@ -291,15 +299,14 @@ private:
     }
 
     lbool internalize_formulas() {
-        if (m_fmls.empty()) {
+        if (m_fmls_head == m_fmls.size()) {
             return l_true;
         }
         dep2asm_t dep2asm;
         goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
-        for (unsigned i = 0; i < m_fmls.size(); ++i) {
+        for (; m_fmls_head < m_fmls.size(); ++m_fmls_head) {
-            g->assert_expr(m_fmls[i].get());
+            g->assert_expr(m_fmls[m_fmls_head].get());
         }
-        m_fmls.reset();
         return internalize_goal(g, dep2asm);
     }
 

src/opt/maxres.cpp

@@ -63,7 +63,7 @@ Notes:
 #include "opt_context.h"
 #include "pb_decl_plugin.h"
 #include "opt_params.hpp"
-
+#include "ast_util.h"
 
 using namespace opt;
 
@@ -101,8 +101,8 @@ public:
            strategy_t st):
         maxsmt_solver_base(c, ws, soft),
         m_B(m), m_asms(m),
-        m_mus(m_s, m),
+        m_mus(c.get_solver(), m),
-        m_mss(m_s, m),
+        m_mss(c.get_solver(), m),
         m_trail(m),
         m_st(st),
         m_hill_climb(true),
@@ -519,7 +519,7 @@ public:
         rational w = split_core(core);
         TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
         max_resolve(core, w);
-        fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
+        fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);
         m_lower += w;
         trace_bounds("maxres");
@@ -811,7 +811,7 @@ public:
         expr_ref_vector nsoft(m);
         expr_ref fml(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            nsoft.push_back(m.mk_not(m_soft[i].get()));
+            nsoft.push_back(mk_not(m, m_soft[i].get()));
         }            
         fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
         s().assert_expr(fml);        
@@ -880,7 +880,7 @@ public:
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             n = m_soft[i].get();
             if (!m_assignment[i]) {
-                n = m.mk_not(n);
+                n = mk_not(m, n);
             }
             sat_solver->assert_expr(n);
         }

src/opt/maxsmt.cpp

@@ -29,13 +29,13 @@ Notes:
 #include "uint_set.h"
 #include "opt_context.h"
 #include "theory_wmaxsat.h"
+#include "ast_util.h"
 
 
 namespace opt {
 
     maxsmt_solver_base::maxsmt_solver_base(
         context& c, vector<rational> const& ws, expr_ref_vector const& soft):
-        m_s(c.get_solver()), 
         m(c.get_manager()), 
         m_c(c),
         m_cancel(false), m_soft(m),
@@ -50,6 +50,10 @@ namespace opt {
         m_params.copy(p);
     }       
 
+    solver& maxsmt_solver_base::s() {
+        return m_c.get_solver(); 
+    }
+
     void maxsmt_solver_base::init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
         m_weights.reset();
         m_soft.reset();
@@ -78,19 +82,10 @@ namespace opt {
               tout << "\n";);
     }
 
-    expr* maxsmt_solver_base::mk_not(expr* e) {
-        if (m.is_not(e, e)) {
-            return e;
-        }
-        else {
-            return m.mk_not(e);
-        }
-    }
-
     void maxsmt_solver_base::set_mus(bool f) {
         params_ref p;
         p.set_bool("minimize_core", f);
-        m_s.updt_params(p);
+        s().updt_params(p);
     }
 
     void maxsmt_solver_base::enable_sls(expr_ref_vector const& soft, vector<rational> const& ws) {
@@ -149,10 +144,10 @@ namespace opt {
 
 
     maxsmt::maxsmt(context& c):
-        m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false), 
+        m(c.get_manager()), m_c(c), m_cancel(false), 
         m_soft_constraints(m), m_answer(m) {}
 
-    lbool maxsmt::operator()(solver* s) {
+    lbool maxsmt::operator()() {
         lbool is_sat;
         m_msolver = 0;
         symbol const& maxsat_engine = m_c.maxsat_engine();
@@ -161,7 +156,7 @@ namespace opt {
         if (m_soft_constraints.empty()) {
             TRACE("opt", tout << "no constraints\n";);
             m_msolver = 0;
-            is_sat = m_s.check_sat(0, 0);
+            is_sat = s().check_sat(0, 0);
         }
         else if (maxsat_engine == symbol("maxres")) {            
             m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
@@ -222,9 +217,9 @@ namespace opt {
         // TBD: have to use a different solver 
         // because we don't push local scope any longer.
         return;
-        solver::scoped_push _sp(m_s);
+        solver::scoped_push _sp(s());
         commit_assignment();
-        if (l_true != m_s.check_sat(0,0)) {
+        if (l_true != s().check_sat(0,0)) {
             IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
             UNREACHABLE();
         }
@@ -274,10 +269,10 @@ namespace opt {
             expr_ref tmp(m);
             tmp = m_soft_constraints[i].get();
             if (!get_assignment(i)) {
-                tmp = m.mk_not(tmp);
+                tmp = mk_not(m, tmp);
             }
             TRACE("opt", tout << "committing: " << tmp << "\n";);
-            m_s.assert_expr(tmp);            
+            s().assert_expr(tmp);            
         }
     }
 
@@ -327,5 +322,9 @@ namespace opt {
         }
     }
 
+    solver& maxsmt::s() {
+        return m_c.get_solver(); 
+    }
+
 
 };

src/opt/maxsmt.h

@@ -58,7 +58,6 @@ namespace opt {
     // 
     class maxsmt_solver_base : public maxsmt_solver {
     protected:
-        solver&          m_s;
         ast_manager&     m;
         context&         m_c;
         volatile bool    m_cancel;
@@ -84,9 +83,8 @@ namespace opt {
         void set_model() { s().get_model(m_model); }
         virtual void updt_params(params_ref& p);
         virtual void init_soft(weights_t& weights, expr_ref_vector const& soft);
-        solver& s() { return m_s; }
+        solver& s();
         void init();
-        expr* mk_not(expr* e);
         void set_mus(bool f);
         app* mk_fresh_bool(char const* name);
 
@@ -115,7 +113,6 @@ namespace opt {
 
     class maxsmt {
         ast_manager&              m;
-        solver&                   m_s;
         context&                  m_c;
         scoped_ptr<maxsmt_solver> m_msolver;
         volatile bool    m_cancel;
@@ -129,7 +126,7 @@ namespace opt {
         params_ref       m_params;
     public:
         maxsmt(context& c);
-        lbool operator()(solver* s);
+        lbool operator()();
         void set_cancel(bool f);
         void updt_params(params_ref& p);
         void add(expr* f, rational const& w); 
@@ -150,6 +147,7 @@ namespace opt {
     private:
         bool is_maxsat_problem(weights_t& ws) const;        
         void verify_assignment();
+        solver& s();
     };
 
 };

src/opt/mus.cpp

@@ -22,6 +22,7 @@ Notes:
 #include "smt_literal.h"
 #include "mus.h"
 #include "ast_pp.h"
+#include "ast_util.h"
 
 using namespace opt;
 
@@ -61,13 +62,6 @@ struct mus::imp {
         return idx;
     }
     
-    expr* mk_not(expr* e) {
-        if (m.is_not(e, e)) {
-            return e;
-        }
-        return m.mk_not(e);
-    }
-    
     lbool get_mus(unsigned_vector& mus) {
         // SASSERT: mus does not have duplicates.
         m_model.reset();
@@ -92,7 +86,7 @@ struct mus::imp {
             core.pop_back();
             expr* cls = m_cls2expr[cls_id].get();
             expr_ref not_cls(m);
-            not_cls = mk_not(cls);
+            not_cls = mk_not(m, cls);
             unsigned sz = assumptions.size();
             assumptions.push_back(not_cls);
             add_core(core, assumptions);

src/opt/opt_context.cpp

@@ -267,7 +267,7 @@ namespace opt {
         model_ref tmp;
         maxsmt& ms = *m_maxsmts.find(id);
         if (scoped) get_solver().push();            
-        lbool result = ms(m_solver.get());
+        lbool result = ms();
         if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
         if (scoped) get_solver().pop(1);
         if (result == l_true && committed) ms.commit_assignment();

src/sat/sat_solver.cpp

@@ -911,21 +911,20 @@ namespace sat {
               }
               m_mc.display(tout);
               );
-#define _INSERT_LIT(_l_)                     \
-        SASSERT(is_external((_l_).var()));   \
-        m_assumption_set.insert(_l_);        \
-        m_assumptions.push_back(_l_);        \
-        assign(_l_, justification());        \
-//        propagate(false);                     \
 
         for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
             literal nlit = ~m_user_scope_literals[i];
-            _INSERT_LIT(nlit);
+            assign(nlit, justification());       
+            //        propagate(false);         
         }
 
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
-            _INSERT_LIT(lit);
+            SASSERT(is_external((lit).var()));  
+            m_assumption_set.insert(lit);       
+            m_assumptions.push_back(lit);       
+            assign(lit, justification());       
+            //        propagate(false);         
         }
     }