local changes

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

src/muz/pdr/pdr_smt_context_manager.h

@@ -21,7 +21,6 @@ Revision History:
 #define _PDR_SMT_CONTEXT_MANAGER_H_
 
 #include "smt_kernel.h"
-#include "sat_solver.h"
 #include "func_decl_dependencies.h"
 #include "dl_util.h"
 

src/sat/sat_solver.cpp

@@ -697,6 +697,7 @@ namespace sat {
         try {
             if (inconsistent()) return l_false;
             init_search();
+            init_assumptons(num_lits, lits);
             propagate(false);
             if (inconsistent()) return l_false;
             cleanup();
@@ -851,6 +852,29 @@ namespace sat {
         }
     }
 
+    void solver::init_assumptions(unsigned num_lits, literal const* lits) {
+        if (num_lits == 0) {
+            return;
+        }
+        push();
+        m_assumptions.reset();
+        m_assumption_set.reset();
+        for (unsigned i = 0; i < num_lits; ++i) {
+            literal l = lits[i];
+            m_assumption_set.insert(l);
+            m_assumptions.push_back(l);
+            mk_clause(1, &l); 
+        }
+    }
+
+    bool solver::tracking_assumptions() const {
+        return !m_assumptions.empty();
+    }
+
+    bool solver::is_assumption(literal l) const {
+        return tracking_assumptions() && m_assumption_set.contains(l);
+    }
+
     void solver::init_search() {
         m_phase_counter           = 0;
         m_phase_cache_on          = false;
@@ -1936,7 +1960,7 @@ namespace sat {
             clause_wrapper cw = m_clauses_to_reinit[i];
             bool reinit = false;
             if (cw.is_binary()) {
-                if (propagate_bin_clause(cw[0], cw[1])) {
+o                if (propagate_bin_clause(cw[0], cw[1])) {
                     if (scope_lvl() > 0) {
                         m_clauses_to_reinit[j] = cw;
                         j++;

src/sat/sat_solver.h

@@ -118,6 +118,8 @@ namespace sat {
         stopwatch               m_stopwatch;
         params_ref              m_params;
         scoped_ptr<solver>      m_clone; // for debugging purposes
+        literal_vector          m_assumptions;
+        literal_set             m_assumption_set;
 
         void del_clauses(clause * const * begin, clause * const * end);
 
@@ -267,6 +269,9 @@ namespace sat {
         bool_var next_var();
         lbool bounded_search();
         void init_search();
+        void init_assumptions(unsigned num_lits, literal const* lits);
+        bool tracking_assumptions() const;
+        bool is_assumption(literal l) const;
         void simplify_problem();
         void mk_model();
         bool check_model(model const & m) const;