merge

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>

src/api/api_solver.cpp

@@ -323,15 +323,6 @@ extern "C" {
         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

@@ -239,29 +239,6 @@ namespace Microsoft.Z3
 	     Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);	
 	}
 
-        /// <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>
-        /// Assert a lemma (or multiple) into the solver.
-        /// </summary>        
-        public void AddLemma(IEnumerable<BoolExpr> constraints)
-        {
-            AssertLemma(constraints.ToArray());
-        }
-
         /// <summary>
         /// The number of assertions in the solver.
         /// </summary>
@@ -325,6 +302,7 @@ namespace Microsoft.Z3
             return lboolToStatus(r);
         }
 
+
         /// <summary>
         /// Retrieve fixed assignments to the set of variables in the form of consequences.
         /// Each consequence is an implication of the form 

src/api/z3_api.h

@@ -6135,16 +6135,6 @@ 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 load solver assertions from a file.
 

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -319,9 +319,8 @@ struct pb2bv_rewriter::imp {
                     sums.insert(sum);                        
                 }
             }
-            uint_set::iterator it = sums.begin(), end = sums.end();
+            for (unsigned u : sums) {
-            for (; it != end; ++it) {
+                oc.push_back(u);
-                oc.push_back(*it);
             }            
             std::sort(oc.begin(), oc.end());
             DEBUG_CODE(                

src/sat/sat_config.cpp

@@ -24,24 +24,8 @@ Revision History:
 
 namespace sat {
 
-    config::config(params_ref const & p):
+    config::config(params_ref const & p) {
-        m_restart_max(0),
+        m_incremental = false; // ad-hoc parameter
-        m_always_true("always_true"),
-        m_always_false("always_false"),
-        m_caching("caching"),
-        m_random("random"),
-        m_geometric("geometric"),
-        m_luby("luby"),
-        m_dyn_psm("dyn_psm"),
-        m_psm("psm"),
-        m_glue("glue"),
-        m_glue_psm("glue_psm"),
-        m_psm_glue("psm_glue") {
-        m_num_threads = 1;
-        m_lookahead_simplify = false;
-        m_lookahead_simplify_bca = false;
-        m_elim_vars = false;
-        m_incremental = false;
         updt_params(p); 
     }
 
@@ -50,21 +34,21 @@ namespace sat {
         m_max_memory  = megabytes_to_bytes(p.max_memory());
 
         symbol s = p.restart();
-        if (s == m_luby)
+        if (s == symbol("luby"))
             m_restart = RS_LUBY;
-        else if (s == m_geometric)
+        else if (s == symbol("geometric"))
             m_restart = RS_GEOMETRIC;
         else
             throw sat_param_exception("invalid restart strategy");
 
         s = p.phase();
-        if (s == m_always_false) 
+        if (s == symbol("always_false")) 
             m_phase = PS_ALWAYS_FALSE;
-        else if (s == m_always_true)
+        else if (s == symbol("always_true"))
             m_phase = PS_ALWAYS_TRUE;
-        else if (s == m_caching)
+        else if (s == symbol("caching"))
             m_phase = PS_CACHING;
-        else if (s == m_random)
+        else if (s == symbol("random"))
             m_phase = PS_RANDOM;
         else
             throw sat_param_exception("invalid phase selection strategy");
@@ -90,24 +74,18 @@ namespace sat {
         m_local_search_threads = p.local_search_threads();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
-        if (p.lookahead_reward() == symbol("heule_schur")) {
+        if (p.lookahead_reward() == symbol("heule_schur")) 
             m_lookahead_reward = heule_schur_reward;
-        }
+        else if (p.lookahead_reward() == symbol("heuleu")) 
-        else if (p.lookahead_reward() == symbol("heuleu")) {
             m_lookahead_reward = heule_unit_reward;
-        }
+        else if (p.lookahead_reward() == symbol("ternary")) 
-        else if (p.lookahead_reward() == symbol("ternary")) {
             m_lookahead_reward = ternary_reward;
-        }
+        else if (p.lookahead_reward() == symbol("unit")) 
-        else if (p.lookahead_reward() == symbol("unit")) {
             m_lookahead_reward = unit_literal_reward;
-        }
+        else if (p.lookahead_reward() == symbol("march_cu")) 
-        else if (p.lookahead_reward() == symbol("march_cu")) {
             m_lookahead_reward = march_cu_reward;
-        }
+        else  
-        else { 
             throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
-        }
 
         if (p.lookahead_cube_cutoff() == symbol("depth")) {
             m_lookahead_cube_cutoff = depth_cutoff;
@@ -142,29 +120,23 @@ namespace sat {
         // --------------------------------
 
         s = p.gc();
-        if (s == m_dyn_psm) {
+        if (s == symbol("dyn_psm")) 
-            m_gc_strategy     = GC_DYN_PSM;
+            m_gc_strategy = GC_DYN_PSM;
-            m_gc_initial      = p.gc_initial();
+        else if (s == symbol("glue_psm"))
-            m_gc_increment    = p.gc_increment();
+            m_gc_strategy = GC_GLUE_PSM;
-            m_gc_small_lbd    = p.gc_small_lbd();
+        else if (s == symbol("glue"))
-            m_gc_k            = p.gc_k();
+            m_gc_strategy = GC_GLUE;
-            if (m_gc_k > 255)
+        else if (s == symbol("psm"))
-                m_gc_k = 255;
+            m_gc_strategy = GC_PSM;
-        }
+        else if (s == symbol("psm_glue"))
-        else {
+            m_gc_strategy = GC_PSM_GLUE;
-            if (s == m_glue_psm)
+        else 
-                m_gc_strategy = GC_GLUE_PSM;
+            throw sat_param_exception("invalid gc strategy");
-            else if (s == m_glue)
+        m_gc_initial      = p.gc_initial();
-                m_gc_strategy = GC_GLUE;
+        m_gc_increment    = p.gc_increment();
-            else if (s == m_psm)
+        m_gc_small_lbd    = p.gc_small_lbd();
-                m_gc_strategy = GC_PSM;
+        m_gc_k            = std::min(255u, p.gc_k());
-            else if (s == m_psm_glue)
+
-                m_gc_strategy = GC_PSM_GLUE;
-            else 
-                throw sat_param_exception("invalid gc strategy");
-            m_gc_initial      = p.gc_initial();
-            m_gc_increment    = p.gc_increment();
-        }
         m_minimize_lemmas = p.minimize_lemmas();
         m_core_minimize   = p.core_minimize();
         m_core_minimize_partial   = p.core_minimize_partial();
@@ -176,18 +148,15 @@ namespace sat {
 
         // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.
         m_branching_heuristic = BH_VSIDS;
-        if (p.branching_heuristic() == symbol("vsids")) {
+        if (p.branching_heuristic() == symbol("vsids")) 
             m_branching_heuristic = BH_VSIDS;
-        }
+        else if (p.branching_heuristic() == symbol("chb")) 
-        else if (p.branching_heuristic() == symbol("chb")) {
             m_branching_heuristic = BH_CHB;
-        }
+        else if (p.branching_heuristic() == symbol("lrb")) 
-        else if (p.branching_heuristic() == symbol("lrb")) {
             m_branching_heuristic = BH_LRB;
-        }
+        else 
-        else {
             throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
-        }
+
         m_anti_exploration = p.branching_anti_exploration();
         m_step_size_init = 0.40;
         m_step_size_dec  = 0.000001;
@@ -199,21 +168,16 @@ namespace sat {
 
         // PB parameters
         s = p.pb_solver();
-        if (s == symbol("circuit")) {
+        if (s == symbol("circuit")) 
             m_pb_solver = PB_CIRCUIT;
-        }
+        else if (s == symbol("sorting")) 
-        else if (s == symbol("sorting")) {
             m_pb_solver = PB_SORTING;
-        }
+        else if (s == symbol("totalizer")) 
-        else if (s == symbol("totalizer")) {
             m_pb_solver = PB_TOTALIZER;
-        }
+        else if (s == symbol("solver")) 
-        else if (s == symbol("solver")) {
             m_pb_solver = PB_SOLVER;
-        }
+        else 
-        else {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
-        }
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();

src/sat/sat_config.h

@@ -114,6 +114,7 @@ namespace sat {
         unsigned           m_gc_increment;
         unsigned           m_gc_small_lbd;
         unsigned           m_gc_k;
+        bool               m_gc_burst;
 
         bool               m_minimize_lemmas;
         bool               m_dyn_sub_res;
@@ -123,20 +124,7 @@ namespace sat {
         symbol             m_drat_file;
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
-
-        symbol             m_always_true;
-        symbol             m_always_false;
-        symbol             m_caching;
-        symbol             m_random;
-        symbol             m_geometric;
-        symbol             m_luby;
         
-        symbol             m_dyn_psm;
-        symbol             m_psm;        
-        symbol             m_glue;        
-        symbol             m_glue_psm;        
-        symbol             m_psm_glue;      
-
         pb_solver          m_pb_solver;
         
         // branching heuristic settings.

src/sat/sat_elim_vars.cpp

@@ -87,6 +87,7 @@ namespace sat{
         simp.m_neg_cls.reset();
         simp.collect_clauses(pos_l, simp.m_pos_cls, false);
         simp.collect_clauses(neg_l, simp.m_neg_cls, false);
+        VERIFY(!s.is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         simp.save_clauses(mc_entry, simp.m_pos_cls);
         simp.save_clauses(mc_entry, simp.m_neg_cls);
@@ -99,7 +100,7 @@ namespace sat{
         pos_occs.reset();
         neg_occs.reset();
         literal_vector lits;
-        add_clauses(b, lits);        
+        add_clauses(b, lits); 
         return true;
     }
 

src/sat/sat_local_search.cpp

@@ -301,12 +301,10 @@ namespace sat {
             for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
                 literal l1 = ~to_literal(l_idx);
                 watch_list const & wlist = s.m_watches[l_idx];
-                watch_list::const_iterator it  = wlist.begin();
+                for (watched const& w : wlist) {
-                watch_list::const_iterator end = wlist.end();
+                    if (!w.is_binary_unblocked_clause())
-                for (; it != end; ++it) {
-                    if (!it->is_binary_unblocked_clause())
                         continue;
-                    literal l2 = it->get_literal();
+                    literal l2 = w.get_literal();
                     if (l1.index() > l2.index()) 
                         continue;
                     literal ls[2] = { l1, l2 };
@@ -316,11 +314,8 @@ namespace sat {
         }
 
         // copy clauses
-        clause_vector::const_iterator it =  s.m_clauses.begin();
+        for (clause* c : s.m_clauses) {
-        clause_vector::const_iterator end = s.m_clauses.end();
+            add_clause(c->size(), c->begin());
-        for (; it != end; ++it) {
-            clause& c = *(*it);
-            add_clause(c.size(), c.begin());
         }
         m_num_non_binary_clauses = s.m_clauses.size();
 
@@ -568,12 +563,11 @@ namespace sat {
             best_var = v = l.var();
             bool tt = cur_solution(v);
             coeff_vector const& falsep = m_vars[v].m_watch[!tt];
-            coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
+            for (pbcoeff const& pbc : falsep) {
-            for (; it != end; ++it) {
+                int slack = constraint_slack(pbc.m_constraint_id);
-                int slack = constraint_slack(it->m_constraint_id);
                 if (slack < 0)
                     ++best_bsb;
-                else if (slack < static_cast<int>(it->m_coeff))
+                else if (slack < static_cast<int>(pbc.m_coeff))
                     best_bsb += num_unsat;
             }
             ++cit;
@@ -583,7 +577,7 @@ namespace sat {
                     v = l.var();                    
                     unsigned bsb = 0;
                     coeff_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)];
-                    coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
+                    auto it = falsep.begin(), end = falsep.end();
                     for (; it != end; ++it) {
                         int slack = constraint_slack(it->m_constraint_id);
                         if (slack < 0) {
@@ -637,22 +631,20 @@ namespace sat {
         coeff_vector const& truep = m_vars[flipvar].m_watch[flip_is_true];
         coeff_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true];
 
-        coeff_vector::const_iterator it = truep.begin(), end = truep.end();
+        for (auto const& pbc : truep) {
-        for (; it != end; ++it) {
+            unsigned ci = pbc.m_constraint_id;
-            unsigned ci = it->m_constraint_id;
             constraint& c = m_constraints[ci];
             int old_slack = c.m_slack;
-            c.m_slack -= it->m_coeff;
+            c.m_slack -= pbc.m_coeff;
             if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat
                 unsat(ci);
             }
         }
-        it = falsep.begin(), end = falsep.end();
+        for (auto const& pbc : falsep) {
-        for (; it != end; ++it) {
+            unsigned ci = pbc.m_constraint_id;
-            unsigned ci = it->m_constraint_id;
             constraint& c = m_constraints[ci];
             int old_slack = c.m_slack;
-            c.m_slack += it->m_coeff;
+            c.m_slack += pbc.m_coeff;
             if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat
                 sat(ci);
             }

src/sat/sat_lookahead.cpp

@@ -683,7 +683,7 @@ namespace sat {
             // NB. u.index() > l.index() iff u.index() > (~l).index().
             // since indices for the same boolean variables occupy
             // two adjacent numbers.
-            if (u.index() > l.index() && is_stamped(u)) {                
+            if (u.index() > l.index() && is_stamped(u) && ~l != u) {                
                 add_arc(~l, ~u);
                 add_arc( u,  l);
             }
@@ -692,7 +692,8 @@ namespace sat {
             lits.reset();
             if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { 
                 for (literal u : lits) {
-                    if (u.index() > l.index() && is_stamped(u)) {
+                    // u is positive in lits, l is negative:                    
+                    if (~l != u && u.index() > l.index() && is_stamped(u)) {
                         add_arc(~l, ~u);
                         add_arc( u,  l);
                     }
@@ -2293,7 +2294,7 @@ namespace sat {
         init();                
         if (inconsistent()) return;
         inc_istamp();            
-        literal l = choose();
+        literal l = choose();        
         if (inconsistent()) return;
         SASSERT(m_trail_lim.empty());
         unsigned num_units = 0;
@@ -2305,7 +2306,7 @@ namespace sat {
                 ++num_units;
             }
         }        
-        IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";);
+        IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << " :propagations " << m_stats.m_propagations << ")\n";);
          
         if (m_s.inconsistent()) return;
 
@@ -2354,16 +2355,8 @@ namespace sat {
     void lookahead::add_hyper_binary() {
 
         unsigned num_lits = m_s.num_vars() * 2;
+        unsigned num_bins = 0;
 
-#if 0
-        std::cout << "binary trail size: " << m_binary_trail.size() << "\n";
-        std::cout << "Are windfalls still on the trail at base level?\n";
-#endif   
-
-        unsigned disconnected1 = 0;
-        unsigned disconnected2 = 0;
-
-#if 1
         typedef std::pair<unsigned, unsigned> u_pair;
         hashtable<u_pair, pair_hash<unsigned_hash, unsigned_hash>, default_eq<u_pair> > imp;
         for (unsigned idx = 0; idx < num_lits; ++idx) {
@@ -2394,14 +2387,16 @@ namespace sat {
             literal_vector const& lits = m_binary[idx];
             for (unsigned sz = bin_size[idx]; sz > 0; --sz) {
                 literal v = lits[lits.size() - sz];
-                if (v != get_parent(v)) continue;
+                if (v == get_parent(v) && 
-                if (m_s.was_eliminated(v.var())) continue;
+                    !m_s.was_eliminated(v.var()) && 
-                if (imp.contains(std::make_pair(u.index(), v.index()))) continue;
+                    !imp.contains(std::make_pair(u.index(), v.index())) && 
-                if (scc.reaches(u, v)) continue;
+                    !scc.reaches(u, v)) {
-                candidates.push_back(std::make_pair(u, v));
+                    candidates.push_back(std::make_pair(u, v));
+                }
             }
         }
-        for (unsigned i = 0; i < 5; ++i) {
+
+        for (unsigned count = 0; count < 5; ++count) {
             scc.init_big(true);
             unsigned k = 0;
             union_find_default_ctx ufctx;
@@ -2412,7 +2407,7 @@ namespace sat {
                 literal v = candidates[j].second;
                 if (!scc.reaches(u, v)) {
                     if (uf.find(u.index()) != uf.find(v.index())) {
-                        ++disconnected1;
+                        ++num_bins;
                         uf.merge(u.index(), v.index());
                         uf.merge((~u).index(), (~v).index());
                         VERIFY(!m_s.was_eliminated(u.var()));
@@ -2425,51 +2420,14 @@ namespace sat {
                     }
                 }
             }
-            //std::cout << candidates.size() << " -> " << k << "\n";
+            std::cout << candidates.size() << " -> " << k << "\n";
             if (k == candidates.size()) break;
             candidates.shrink(k);
+            if (k == 0) break;
         }
-
-        //std::cout << "candidates: " << candidates.size() << "\n";
-
-#endif
-
-#if 0
-        union_find_default_ctx ufctx;
-        union_find<union_find_default_ctx> uf(ufctx);
-        for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
-        for (unsigned idx = 0; idx < num_lits; ++idx) {
-            literal u = get_parent(to_literal(idx));
-            if (null_literal != u) {
-                for (watched const& w : m_s.m_watches[idx]) {
-                    if (!w.is_binary_clause()) continue;
-                    literal v = get_parent(w.get_literal());
-                    if (null_literal != v) {
-                        uf.merge(u.index(), v.index());
-                    }
-                }
-            }
-        }
-
-        for (unsigned i = 0; i < m_binary.size(); ++i) {
-            literal u = to_literal(i);
-            if (u == get_parent(u) && !m_s.was_eliminated(u.var())) {
-                for (literal v : m_binary[i]) {
-                    if (v == get_parent(v) && 
-                        !m_s.was_eliminated(v.var()) && 
-                        uf.find(u.index()) != uf.find(v.index())) {
-                        ++disconnected2;
-                        uf.merge(u.index(), v.index());
-                        // m_s.mk_clause(~u, v, true);
-                    }
-                }
-            }
-        }
-#endif
         
-        IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";);
+        IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << num_bins << ")\n";);
-        //IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";);
+        m_stats.m_bca += num_bins;
-        //m_stats.m_bca += disconnected;
     }
 
     void lookahead::normalize_parents() {

src/sat/sat_params.pyg

@@ -18,10 +18,11 @@ def_module_params('sat',
                           ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
                           ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
-                          ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequence'),
+                          ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequency'),
                           ('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
                           ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
                           ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
+                          ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'),
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
                           ('core.minimize', BOOL, False, 'minimize computed core'),
@@ -37,14 +38,8 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
-                          ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
+                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
-                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'),
+                          ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
-                          ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),
-                          ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'),
-                          ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'),
-                          ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'),
-                          ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'),
-                          ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),

src/sat/sat_scc.h

@@ -51,6 +51,8 @@ namespace sat {
 
         struct pframe;
 
+        bool reaches_aux(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } 
+
     public:
 
         scc(solver & s, params_ref const & p);
@@ -66,11 +68,12 @@ namespace sat {
           \brief create binary implication graph and associated data-structures to check transitivity.
          */
         void init_big(bool learned);
+        void ensure_big(bool learned) { if (m_left.empty()) init_big(learned); }
         int get_left(literal l) const { return m_left[l.index()]; }
         int get_right(literal l) const { return m_right[l.index()]; }
         literal get_parent(literal l) const { return m_parent[l.index()]; }
         literal get_root(literal l) const { return m_root[l.index()]; }
-        bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
+        bool reaches(literal u, literal v) const { return reaches_aux(u, v) || reaches_aux(~v, ~u); }        
     };
 };
 

src/sat/sat_simplifier.cpp

@@ -77,6 +77,7 @@ namespace sat {
     inline bool simplifier::is_external(bool_var v) const { 
         return 
             s.is_assumption(v) ||
+            (s.is_external(v) && s.is_incremental()) ||
             (s.is_external(v) && s.m_ext &&
              (!m_ext_use_list.get(literal(v, false)).empty() ||
               !m_ext_use_list.get(literal(v, true)).empty()));
@@ -154,6 +155,7 @@ namespace sat {
         else {
             remove_clause(c);
         }
+        
     }
 
     inline void simplifier::unblock_clause(clause & c) {
@@ -1354,6 +1356,7 @@ namespace sat {
 
         void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
             TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
+            VERIFY(!s.is_external(l));
             if (new_entry == 0 && !s.m_retain_blocked_clauses)
                 new_entry = &(mc.mk(k, l.var()));
             m_to_remove.push_back(&c);
@@ -1365,20 +1368,22 @@ namespace sat {
         }
 
         void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            SASSERT(!s.is_external(l.var()));
             prepare_block_clause(c, l, new_entry, model_converter::BLOCK_LIT);
-            if (!s.m_retain_blocked_clauses) 
+            mc.insert(*new_entry, c);
-                mc.insert(*new_entry, c);
         }
 
         void block_covered_clause(clause& c, literal l, model_converter::kind k) {
+            SASSERT(!s.is_external(l.var()));
             model_converter::entry * new_entry = 0;
             prepare_block_clause(c, l, new_entry, k);
-            if (!s.m_retain_blocked_clauses) 
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
-                mc.insert(*new_entry, m_covered_clause, m_elim_stack);
         }
         
         void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
-            if (new_entry == 0 && !s.m_retain_blocked_clauses) 
+            SASSERT(!s.is_external(blocked));
+            VERIFY(!s.is_external(blocked));
+            if (new_entry == 0) 
                 new_entry = &(mc.mk(k, blocked.var()));
             literal l2 = it->get_literal();
             TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
@@ -1394,15 +1399,13 @@ namespace sat {
         
         void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
             prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
-            if (!s.m_retain_blocked_clauses) 
+            mc.insert(*new_entry, l, it->get_literal());
-                mc.insert(*new_entry, l, it->get_literal());
         }
 
         void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
             model_converter::entry * new_entry = 0;
             prepare_block_binary(it, l, blocked, new_entry, k);
-            if (!s.m_retain_blocked_clauses) 
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
-                mc.insert(*new_entry, m_covered_clause, m_elim_stack);
         }
 
         void bca() {
@@ -1779,6 +1782,7 @@ namespace sat {
 
         // eliminate variable
         ++s.m_stats.m_elim_var_res;
+        VERIFY(!s.is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);
@@ -1867,7 +1871,10 @@ namespace sat {
             checkpoint();
             if (m_elim_counter < 0) 
                 break;
-            if (try_eliminate(v)) {
+            if (is_external(v)) {
+                // skip
+            }
+            else if (try_eliminate(v)) {
                 m_num_elim_vars++;
             }
             else if (elim_vars_bdd_enabled() && elim_bdd(v)) { 

src/sat/sat_simplifier.h

@@ -163,6 +163,7 @@ namespace sat {
         void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
 
         bool is_external(bool_var v) const;
+        bool is_external(literal l) const { return is_external(l.var()); }
         bool was_eliminated(bool_var v) const;
         lbool value(bool_var v) const;
         lbool value(literal l) const;

src/sat/sat_solver.cpp

@@ -904,6 +904,11 @@ namespace sat {
             propagate(false);
             if (check_inconsistent()) return l_false;
             cleanup();
+            if (m_config.m_gc_burst) {
+                // force gc
+                m_conflicts_since_gc = m_gc_threshold + 1;
+                gc();
+            }
             if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
                 m_restart_threshold = m_config.m_burst_search;
                 lbool r = bounded_search();
@@ -1326,6 +1331,7 @@ namespace sat {
     void solver::add_assumption(literal lit) {
         m_assumption_set.insert(lit);
         m_assumptions.push_back(lit);
+        VERIFY(is_external(lit.var()));
     }
 
     void solver::pop_assumption() {
@@ -1438,14 +1444,12 @@ namespace sat {
             CASSERT("sat_simplify_bug", check_invariant());
         }
 
-
         if (m_config.m_lookahead_simplify) {
             lookahead lh(*this);
             lh.simplify();
             lh.collect_statistics(m_aux_stats);
         }
 
-
         sort_watch_lits();
         CASSERT("sat_simplify_bug", check_invariant());
 
@@ -1585,6 +1589,8 @@ namespace sat {
         }
         for (literal l : m_assumptions) {
             if (value_at(l, m) != l_true) {
+                VERIFY(is_external(l.var()));
+                IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";);
                 TRACE("sat",
                       tout << l << " does not model check\n";
                       tout << "trail: " << m_trail << "\n";
@@ -1641,7 +1647,7 @@ namespace sat {
     void solver::gc() {
         if (m_conflicts_since_gc <= m_gc_threshold)
             return;
-        IF_VERBOSE(1, verbose_stream() << "gc\n";);
+        IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";);
         CASSERT("sat_gc_bug", check_invariant());
         switch (m_config.m_gc_strategy) {
         case GC_GLUE:
@@ -2099,6 +2105,7 @@ namespace sat {
 
         pop_reinit(m_scope_lvl - new_scope_lvl);
         TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout););
+        // unsound: m_asymm_branch.minimize(m_scc, m_lemma);
         clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
         if (lemma) {
             lemma->set_glue(glue);

src/sat/sat_solver.h

@@ -263,6 +263,7 @@ namespace sat {
         unsigned num_clauses() const;
         unsigned num_restarts() const { return m_restarts; }
         bool is_external(bool_var v) const { return m_external[v] != 0; }
+        bool is_external(literal l) const { return is_external(l.var()); }
         void set_external(bool_var v);
         void set_non_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
@@ -305,6 +306,7 @@ namespace sat {
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
         void set_incremental(bool b) { m_config.m_incremental = b; }
+        bool is_incremental() const { return m_config.m_incremental; }
         extension* get_extension() const { return m_ext.get(); }
         void       set_extension(extension* e);
         bool       set_root(literal l, literal r);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -251,15 +251,6 @@ public:
         }
     }
 
-    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_core(expr * t) {
         m_internalized = false;
@@ -526,7 +517,7 @@ private:
         m_pc = g->pc();
         m_mc = g->mc();
         TRACE("sat", g->display_with_dependencies(tout););
-        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma);
+        m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, m_solver.get_config().m_incremental, is_lemma);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
             std::stringstream strm;

src/smt/smt_solver.cpp

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

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -105,10 +105,6 @@ 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

@@ -68,16 +68,6 @@ 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

@@ -62,10 +62,6 @@ 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();