updated sat_smt

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 30, 2020 · 86310a1 · 86310a1
1 parent e9a4e48
commit 86310a1
Show file tree

Hide file tree

Showing 15 changed files with 389 additions and 437 deletions.
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
@@ -75,7 +75,6 @@ namespace sat {
         virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0;
         virtual void collect_statistics(statistics& st) const = 0;
         virtual extension* copy(solver* s) = 0;       
-        virtual extension* copy(lookahead* s, bool learned) = 0;       
         virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
         virtual void gc() = 0;
         virtual void pop_reinit() = 0;

diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
@@ -22,7 +22,6 @@ Module Name:
 
 #include <cmath>
 #include "sat/sat_solver.h"
-#include "sat/sat_extension.h"
 #include "sat/sat_lookahead.h"
 #include "sat/sat_scc.h"
 #include "util/union_find.h"
@@ -1037,9 +1036,6 @@ namespace sat {
             }
         }
 
-        if (m_s.m_ext) {
-            // m_ext = m_s.m_ext->copy(this, learned);
-        }
         propagate();
         m_qhead = m_trail.size();
         m_init_freevars = m_freevars.size();

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -126,7 +126,7 @@ class inc_sat_solver : public solver {
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext) {
             auto& si = result->m_goal2sat.si(dst_m, m_params, result->m_solver, result->m_map, result->m_dep2asm, is_incremental());
-            euf::solver::scoped_set_translate st(*ext, tr, result->m_map, si);  
+            euf::solver::scoped_set_translate st(*ext, dst_m, result->m_map, si);  
             result->m_solver.copy(m_solver);
         }        
         else {