From 365f05b41a41ebab61a7af5ca906d16a49f6e2fd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 30 Jul 2014 17:49:51 -0700
Subject: [PATCH] testing inc-sat solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/inc_sat_solver.cpp  | 16 +++++++++++++---
 src/sat/sat_solver.cpp      |  7 +++++--
 src/sat/tactic/goal2sat.cpp | 12 +++++++-----
 src/sat/tactic/goal2sat.h   |  2 +-
 4 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp
index 506e3227c..d6404808e 100644
--- a/src/opt/inc_sat_solver.cpp
+++ b/src/opt/inc_sat_solver.cpp
@@ -27,6 +27,8 @@ class inc_sat_solver : public solver {
     tactic_ref      m_preprocess;
     statistics      m_stats;
     unsigned        m_num_scopes;
+    sat::literal_vector m_asms;
+
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -96,10 +98,10 @@ public:
             }
             g = result[0];
             TRACE("opt", g->display_with_dependencies(tout););
-            m_goal2sat(*g, m_params, m_solver, m_map, dep2asm);
+            m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         }
-        
-        lbool r = m_solver.check();
+        extract_assumptions(dep2asm, m_asms);
+        lbool r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         switch (r) {
         case l_true:
             extract_model();
@@ -178,6 +180,14 @@ public:
 
 private:
 
+    void extract_assumptions(dep2asm_t& dep2asm, sat::literal_vector& asms) {
+        asms.reset();
+        dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
+        for (; it != end; ++it) {
+            asms.push_back(it->m_value);
+        }
+    }
+
     void extract_core(dep2asm_t& dep2asm) {
         u_map<expr*> asm2dep;
         dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 1d3d3ce71..911c49c74 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -696,7 +696,7 @@ namespace sat {
     // -----------------------
     lbool solver::check(unsigned num_lits, literal const* lits) {
         pop_to_base_level();
-        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the efficient SAT solver)\n";);
+        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(scope_lvl() == 0);
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {
@@ -875,7 +875,10 @@ namespace sat {
         m_assumption_set.reset();        
         push();
 
-        TRACE("sat", display(tout););
+        TRACE("sat", 
+              for (unsigned i = 0; i < num_lits; ++i) 
+                  tout << lits[i] << " ";
+              tout << "\n";);
 #define _INSERT_LIT(_l_)                     \
         SASSERT(is_external((_l_).var()));   \
         m_assumption_set.insert(_l_);        \
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 7e22fca8b..636e8920f 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -59,13 +59,15 @@ struct goal2sat::imp {
     unsigned long long          m_max_memory;
     volatile bool               m_cancel;
     expr_ref_vector             m_trail;
+    bool                        m_default_external;
     
-    imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm):
+    imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
         m(_m),
         m_solver(s),
         m_map(map),
         m_dep2asm(dep2asm),
-        m_trail(m) {
+        m_trail(m),
+        m_default_external(default_external) {
         updt_params(p);
         m_cancel = false;
         m_true = sat::null_bool_var;
@@ -121,7 +123,7 @@ struct goal2sat::imp {
                 l = sat::literal(mk_true(), !sign);
             }
             else {
-                bool ext = !is_uninterp_const(t) || m_interface_vars.contains(t);
+                bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
                 sat::bool_var v = m_solver.mk_var(ext);
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
@@ -486,8 +488,8 @@ struct goal2sat::scoped_set_imp {
     }
 };
 
-void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm) {
-    imp proc(g.m(), p, t, m, dep2asm);
+void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
+    imp proc(g.m(), p, t, m, dep2asm, default_external);
     scoped_set_imp set(this, &proc);
     proc(g);
 }
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index bcc3dd52e..b4e9615a0 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -57,7 +57,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);
+    void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
     void set_cancel(bool f);
 };