update lookahead to include extensions

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

contrib/cmake/src/sat/CMakeLists.txt

@@ -14,6 +14,7 @@ z3_add_component(sat
     sat_iff3_finder.cpp
     sat_integrity_checker.cpp
     sat_local_search.cpp
+    sat_lookahead.cpp
     sat_model_converter.cpp
     sat_mus.cpp
     sat_parallel.cpp

src/api/api_interp.cpp

@@ -542,14 +542,15 @@ extern "C" {
     }
 
 
-    int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast *cnsts[], unsigned *parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast *theory[]){
+    int Z3_read_interpolation_problem(Z3_context ctx, Z3_ast_vector cnsts, unsigned* _num, unsigned* parents[], const char *filename, Z3_string_ptr error, Z3_ast_vector theory){
 
         hash_map<std::string, std::string> file_params;
         get_file_params(filename, file_params);
 
         unsigned num_theory = 0;
-        if (file_params.find("THEORY") != file_params.end())
+        if (file_params.find("THEORY") != file_params.end()) {
             num_theory = atoi(file_params["THEORY"].c_str());
+        }
 
         Z3_ast_vector assertions = iZ3_parse(ctx, filename, error);
         if (assertions == 0)
@@ -559,23 +560,15 @@ extern "C" {
             num_theory = Z3_ast_vector_size(ctx, assertions);
         unsigned num = Z3_ast_vector_size(ctx, assertions) - num_theory;
 
-        read_cnsts.resize(num);
         read_parents.resize(num);
-        read_theory.resize(num_theory);
 
-        for (unsigned j = 0; j < num_theory; j++)
+        for (unsigned j = 0; theory && j < num_theory; j++)
-            read_theory[j] = Z3_ast_vector_get(ctx, assertions, j);
+            Z3_ast_vector_push(ctx, theory, Z3_ast_vector_get(ctx, assertions, j));
+        
         for (unsigned j = 0; j < num; j++)
-            read_cnsts[j] = Z3_ast_vector_get(ctx, assertions, j + num_theory);
+            Z3_ast_vector_push(ctx, cnsts, Z3_ast_vector_get(ctx, assertions, j + num_theory));
-        
-        if (ret_num_theory)
-            *ret_num_theory = num_theory;
-        if (theory)
-            *theory = &read_theory[0];
         
         if (!parents){
-            *_num = num;
-            *cnsts = &read_cnsts[0];
             Z3_ast_vector_dec_ref(ctx, assertions);
             return true;
         }
@@ -586,7 +579,7 @@ extern "C" {
         hash_map<Z3_ast, int> pred_map;
 
         for (unsigned j = 0; j < num; j++){
-            Z3_ast lhs = 0, rhs = read_cnsts[j];
+            Z3_ast lhs = 0, rhs = Z3_ast_vector_get(ctx, cnsts, j);
 
             if (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, rhs))) == Z3_OP_IMPLIES){
                 Z3_app app1 = Z3_to_app(ctx, rhs);
@@ -627,7 +620,7 @@ extern "C" {
                         read_error << "formula " << j + 1 << ": should be (implies {children} fmla parent)";
                         goto fail;
                     }
-                    read_cnsts[j] = lhs;
+                    Z3_ast_vector_set(ctx, cnsts, j, lhs);
                     Z3_ast name = rhs;
                     if (pred_map.find(name) != pred_map.end()){
                         read_error << "formula " << j + 1 << ": duplicate symbol";
@@ -646,7 +639,6 @@ extern "C" {
             }
 
         *_num = num;
-        *cnsts = &read_cnsts[0];
         *parents = &read_parents[0];
         Z3_ast_vector_dec_ref(ctx, assertions);
         return true;

src/api/dotnet/InterpolationContext.cs

@@ -133,19 +133,16 @@ namespace Microsoft.Z3
         /// well documented.</remarks>
         public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
         {
-            uint num = 0, num_theory = 0;
+            uint num = 0;
-            IntPtr[] n_cnsts;
-            IntPtr[] n_theory;
             IntPtr n_err_str;
-            int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory);
+            ASTVector _cnsts = new ASTVector(this);
+            ASTVector _theory = new ASTVector(this);
+
+            int r = Native.Z3_read_interpolation_problem(nCtx, _cnsts.NativeObject, ref num, out parents, filename, out n_err_str, _theory.NativeObject);
             error = Marshal.PtrToStringAnsi(n_err_str);
-            cnsts = new Expr[num];
+            cnsts = _cnsts.ToExprArray();
             parents = new uint[num];
-            theory = new Expr[num_theory];
+            theory = _theory.ToExprArray();
-            for (int i = 0; i < num; i++)
-                cnsts[i] = Expr.Create(this, n_cnsts[i]);
-            for (int i = 0; i < num_theory; i++)
-                theory[i] = Expr.Create(this, n_theory[i]);
             return r;
         }
 

src/api/z3_interp.h

@@ -207,18 +207,17 @@ extern "C" {
        where each value is represented using the common symbols between
        the formulas in the subtree and the remainder of the formulas.
 
-       def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST)))
+       def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _in(AST_VECTOR), _out(UINT), _out_managed_array(2, UINT), _in(STRING), _out(STRING), _in(AST_VECTOR)))
 
        */
 
     int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
+                                             Z3_ast_vector cnsts,
                                              unsigned* num,
-                                             Z3_ast *cnsts[],
                                              unsigned* parents[],
                                              Z3_string filename,
                                              Z3_string_ptr error,
-                                             unsigned *num_theory,
+                                             Z3_ast_vector theory);
-                                             Z3_ast *theory[]);
 
 
 

src/cmd_context/basic_cmds.cpp

@@ -266,7 +266,7 @@ UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr
     ctx.regular_stream() << std::endl; 
 });
 
-UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;);
+UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;);
 
 
 class set_get_option_cmd : public cmd {

src/sat/card_extension.cpp

@@ -79,12 +79,6 @@ namespace sat {
         }
     }
 
-    void card_extension::init_watch(bool_var v) {
-        if (m_var_infos.size() <= static_cast<unsigned>(v)) {
-            m_var_infos.resize(static_cast<unsigned>(v)+100);
-        }
-    }
-
     void card_extension::init_watch(card& c, bool is_true) {
         clear_watch(c);
         if (c.lit() != null_literal && c.lit().sign() == is_true) {
@@ -94,7 +88,7 @@ namespace sat {
         SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
         unsigned j = 0, sz = c.size(), bound = c.k();
         if (bound == sz) {
-            for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
+            for (unsigned i = 0; i < sz && !inconsistent(); ++i) {
                 assign(c, c[i]);
             }
             return;
@@ -135,7 +129,7 @@ namespace sat {
             set_conflict(c, alit);
         }
         else if (j == bound) {
-            for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
+            for (unsigned i = 0; i < bound && !inconsistent(); ++i) {
                 assign(c, c[i]);                
             }
         }
@@ -149,20 +143,12 @@ namespace sat {
     void card_extension::clear_watch(card& c) {
         unsigned sz = std::min(c.k() + 1, c.size());
         for (unsigned i = 0; i < sz; ++i) {
-            unwatch_literal(c[i], &c);            
+            unwatch_literal(c[i], c);            
         }
     }
 
-    void card_extension::unwatch_literal(literal lit, card* c) {
+    void card_extension::unwatch_literal(literal lit, card& c) {
-        if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
+        get_wlist(~lit).erase(watched(c.index()));
-            return;
-        }
-        ptr_vector<card>*& cards = m_var_infos[lit.var()].m_card_watch[lit.sign()];
-        if (!is_tag_empty(cards)) {
-            if (remove(*cards, c)) {
-                cards = set_tag_empty(cards);
-            }        
-        }
     }
 
     void card_extension::assign(card& c, literal lit) {
@@ -177,7 +163,7 @@ namespace sat {
             m_num_propagations_since_pop++;
             //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
             SASSERT(validate_unit_propagation(c));
-            if (s().m_config.m_drat) {
+            if (get_config().m_drat) {
                 svector<drat::premise> ps;
                 literal_vector lits;
                 if (c.lit() != null_literal) lits.push_back(~c.lit());
@@ -186,27 +172,16 @@ namespace sat {
                 }
                 lits.push_back(lit);
                 ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
-                s().m_drat.add(lits, ps);
+                drat_add(lits, ps);
             }
-            s().assign(lit, justification::mk_ext_justification(c.index()));
+            assign(lit, justification::mk_ext_justification(c.index()));
             break;
         }
     }
 
     void card_extension::watch_literal(card& c, literal lit) {
         TRACE("sat_verbose", tout << "watch: " << lit << "\n";);
-        init_watch(lit.var());
+        get_wlist(~lit).push_back(watched(c.index()));
-        ptr_vector<card>* cards = m_var_infos[lit.var()].m_card_watch[lit.sign()];
-        if (cards == 0) {
-            cards = alloc(ptr_vector<card>);
-            m_var_infos[lit.var()].m_card_watch[lit.sign()] = cards;
-        }
-        else if (is_tag_empty(cards)) {
-            cards = set_tag_non_empty(cards);
-            m_var_infos[lit.var()].m_card_watch[lit.sign()] = cards;            
-        }
-        TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
-        cards->push_back(&c);
     }
 
     void card_extension::set_conflict(card& c, literal lit) {
@@ -214,8 +189,8 @@ namespace sat {
         TRACE("sat", display(tout, c, true); );
         SASSERT(validate_conflict(c));
         SASSERT(value(lit) == l_false);
-        s().set_conflict(justification::mk_ext_justification(c.index()), ~lit);
+        set_conflict(justification::mk_ext_justification(c.index()), ~lit);
-        SASSERT(s().inconsistent());
+        SASSERT(inconsistent());
     }
 
     // pb:
@@ -322,7 +297,7 @@ namespace sat {
     lbool card_extension::add_assign(pb& p, literal alit) {
 
         TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
-        SASSERT(!s().inconsistent());
+        SASSERT(!inconsistent());
         unsigned sz = p.size();
         unsigned bound = p.k();
         unsigned num_watch = p.num_watch();
@@ -364,7 +339,7 @@ namespace sat {
             }
         }
 
-        SASSERT(!s().inconsistent());
+        SASSERT(!inconsistent());
         DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); });
 
         if (slack < bound) {
@@ -400,7 +375,7 @@ namespace sat {
             }
 
             for (literal lit : to_assign) {
-                if (s().inconsistent()) break;
+                if (inconsistent()) break;
                 if (value(lit) == l_undef) {
                     assign(p, lit);
                 }				
@@ -415,37 +390,18 @@ namespace sat {
 
     void card_extension::watch_literal(pb& p, wliteral l) {
         literal lit = l.second;
-        init_watch(lit.var());
+        get_wlist(~lit).push_back(watched(p.index()));
-        ptr_vector<pb>* pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
-        if (pbs == 0) {
-            pbs = alloc(ptr_vector<pb>);
-            m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;
-        }
-        else if (is_tag_empty(pbs)) {
-            pbs = set_tag_non_empty(pbs);
-            m_var_infos[lit.var()].m_pb_watch[lit.sign()] = pbs;            
-        }
-        TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
-        pbs->push_back(&p);
     }
 
     void card_extension::clear_watch(pb& p) {
         unsigned sz = p.size();
         for (unsigned i = 0; i < sz; ++i) {
-            unwatch_literal(p[i].second, &p);            
+            unwatch_literal(p[i].second, p);            
         }
     }
     
-    void card_extension::unwatch_literal(literal lit, pb* p) {
+    void card_extension::unwatch_literal(literal lit, pb& p) {
-        if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
+        get_wlist(~lit).erase(watched(p.index()));        
-            return;
-        }
-        pb_watch*& pbs = m_var_infos[lit.var()].m_pb_watch[lit.sign()];
-        if (!is_tag_empty(pbs)) {
-            if (remove(*pbs, p)) {
-                pbs = set_tag_empty(pbs);
-            }        
-        }
     }
 
     void card_extension::set_conflict(pb& p, literal lit) {
@@ -453,8 +409,8 @@ namespace sat {
         TRACE("sat", display(tout, p, true); );
         // SASSERT(validate_conflict(p));
         SASSERT(value(lit) == l_false);
-        s().set_conflict(justification::mk_ext_justification(p.index()), ~lit);
+        set_conflict(justification::mk_ext_justification(p.index()), ~lit);
-        SASSERT(s().inconsistent());
+        SASSERT(inconsistent());
     }
 
     void card_extension::assign(pb& p, literal lit) {
@@ -468,15 +424,15 @@ namespace sat {
             SASSERT(validate_unit_propagation(p, lit));
             m_stats.m_num_pb_propagations++;
             m_num_propagations_since_pop++;
-            if (s().m_config.m_drat) {
+            if (get_config().m_drat) {
                 svector<drat::premise> ps;
                 literal_vector lits;
                 get_pb_antecedents(lit, p, lits);
                 lits.push_back(lit);
                 ps.push_back(drat::premise(drat::s_ext(), p.lit()));
-                s().m_drat.add(lits, ps);
+                drat_add(lits, ps);
             }
-            s().assign(lit, justification::mk_ext_justification(p.index()));
+            assign(lit, justification::mk_ext_justification(p.index()));
             break;
         }
     }
@@ -513,53 +469,6 @@ namespace sat {
         out << ">= " << p.k()  << "\n";
     }
 
-    void card_extension::asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p0) {
-        TRACE("sat", tout << "literal: " << l << " has pb: " << !is_tag_empty(pbs) << " p0 != 0: " << (p0 != 0) << "\n";);
-        if (!is_tag_empty(pbs)) {
-            ptr_vector<pb>::iterator begin = pbs->begin();
-            ptr_vector<pb>::iterator it = begin, it2 = it, end = pbs->end();
-            for (; it != end; ++it) {
-                pb& p = *(*it);
-                if (p.lit() != null_literal && value(p.lit()) != l_true) {
-                    continue;
-                }
-                switch (add_assign(p, ~l)) {
-                case l_true: // unit propagation, keep watching the literal
-                    if (it2 != it) {
-                        *it2 = *it;
-                    }
-                    ++it2;
-                    break;
-                case l_false: // conflict.
-                    SASSERT(s().inconsistent());
-                    for (; it != end; ++it, ++it2) {
-                        *it2 = *it;
-                    }
-                    pbs->set_end(it2);
-                    return;                
-                case l_undef: // watch literal was swapped
-                    if (s().inconsistent()) {
-                        ++it;
-                        for (; it != end; ++it, ++it2) {
-                            *it2 = *it;
-                        }
-                        pbs->set_end(it2);
-                        return;
-                    }
-                    break; 
-                }
-            }
-            pbs->set_end(it2);
-            if (pbs->empty()) {
-                m_var_infos[l.var()].m_pb_watch[!l.sign()] = set_tag_empty(pbs);
-            }
-        }
-
-        if (p0 != 0 && !s().inconsistent()) {
-            init_watch(*p0, !l.sign());
-        }        
-    }
-
     // xor:
 
     void card_extension::copy_xor(card_extension& result) {
@@ -575,20 +484,12 @@ namespace sat {
     }
 
     void card_extension::clear_watch(xor& x) {
-        unwatch_literal(x[0], &x);
+        unwatch_literal(x[0], x);
-        unwatch_literal(x[1], &x);         
+        unwatch_literal(x[1], x);         
     }
 
-    void card_extension::unwatch_literal(literal lit, xor* c) {
+    void card_extension::unwatch_literal(literal lit, xor& c) {
-        if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
+        get_wlist(~lit).erase(watched(c.index()));
-            return;
-        }
-        xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch;
-        if (!is_tag_empty(xors)) {
-            if (remove(*xors, c)) {
-                xors = set_tag_empty(xors);
-            }        
-        }
     }
 
     bool card_extension::parity(xor const& x, unsigned offset) const {
@@ -620,16 +521,15 @@ namespace sat {
         switch (j) {
         case 0: 
             if (!parity(x, 0)) {
-                literal_set litset;
+                unsigned l = lvl(x[0]);
-                for (unsigned i = 0; i < sz; ++i) {
+                j = 1;
-                    litset.insert(x[i]);
+                for (unsigned i = 1; i < sz; ++i) {
+                    if (lvl(x[i]) > l) {
+                        j = i;
+                        l = lvl(x[i]);
                     } 
-                literal_vector const& lits = s().m_trail;
-                unsigned idx = lits.size()-1;
-                while (!litset.contains(lits[idx])) {
-                    --idx;
                 }
-                set_conflict(x, lits[idx]);
+                set_conflict(x, x[j]);
             }
             break;
         case 1: 
@@ -644,18 +544,18 @@ namespace sat {
     }
 
     void card_extension::assign(xor& x, literal lit) {
-        SASSERT(!s().inconsistent());
+        SASSERT(!inconsistent());
         switch (value(lit)) {
         case l_true: 
             break;
         case l_false: 
             set_conflict(x, lit); 
-            SASSERT(s().inconsistent());
+            SASSERT(inconsistent());
             break;
         default:
             m_stats.m_num_xor_propagations++;
             m_num_propagations_since_pop++;
-            if (s().m_config.m_drat) {
+            if (get_config().m_drat) {
                 svector<drat::premise> ps;
                 literal_vector lits;
                 if (x.lit() != null_literal) lits.push_back(~x.lit());
@@ -664,25 +564,17 @@ namespace sat {
                 }
                 lits.push_back(lit);
                 ps.push_back(drat::premise(drat::s_ext(), x.lit()));
-                s().m_drat.add(lits, ps);
+                drat_add(lits, ps);
             }
             TRACE("sat", display(tout << lit << " ", x, true););
-            s().assign(lit, justification::mk_ext_justification(x.index()));
+            assign(lit, justification::mk_ext_justification(x.index()));
             break;
         }
     }
 
     void card_extension::watch_literal(xor& x, literal lit) {
         TRACE("sat_verbose", tout << "watch: " << lit << "\n";);
-        init_watch(lit.var());
+        get_wlist(~lit).push_back(watched(x.index()));
-        xor_watch*& xors = m_var_infos[lit.var()].m_xor_watch;
-        if (xors == 0) {
-            xors = alloc(ptr_vector<xor>);
-        }
-        else if (is_tag_empty(xors)) {
-            xors = set_tag_non_empty(xors);
-        }
-        xors->push_back(&x);
         TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
     }
 
@@ -693,8 +585,8 @@ namespace sat {
         if (value(lit) == l_true) lit.neg();
         SASSERT(validate_conflict(x));
         TRACE("sat", display(tout << lit << " ", x, true););
-        s().set_conflict(justification::mk_ext_justification(x.index()), ~lit);
+        set_conflict(justification::mk_ext_justification(x.index()), ~lit);
-        SASSERT(s().inconsistent());
+        SASSERT(inconsistent());
     }
 
     lbool card_extension::add_assign(xor& x, literal alit) {
@@ -735,49 +627,9 @@ namespace sat {
         else if (!parity(x, 0)) {
             set_conflict(x, ~x[1]);
         }      
-        return s().inconsistent() ? l_false : l_true;  
+        return inconsistent() ? l_false : l_true;  
     }
     
-    void card_extension::asserted_xor(literal l, ptr_vector<xor>* xors, xor* x) {
-        TRACE("sat", tout << l << " " << !is_tag_empty(xors) << " " << (x != 0) << "\n";);
-        if (!is_tag_empty(xors)) {
-            ptr_vector<xor>::iterator begin = xors->begin();
-            ptr_vector<xor>::iterator it = begin, it2 = it, end = xors->end();
-            for (; it != end; ++it) {
-                xor& c = *(*it);
-                if (c.lit() != null_literal && value(c.lit()) != l_true) {
-                    continue;
-                }
-                switch (add_assign(c, ~l)) {
-                case l_false: // conflict
-                    for (; it != end; ++it, ++it2) {
-                        *it2 = *it;
-                    }
-                    SASSERT(s().inconsistent());
-                    xors->set_end(it2);
-                    return;
-                case l_undef: // watch literal was swapped
-                    break;
-                case l_true: // unit propagation, keep watching the literal
-                    if (it2 != it) {
-                        *it2 = *it;
-                    }
-                    ++it2;
-                    break;
-                }
-            }
-            xors->set_end(it2);
-            if (xors->empty()) {
-                m_var_infos[l.var()].m_xor_watch = set_tag_empty(xors);
-            }
-        }
-
-        if (x != 0 && !s().inconsistent()) {
-            init_watch(*x, !l.sign());
-        }
-    }
-
-    
     void card_extension::normalize_active_coeffs() {
         while (!m_active_var_set.empty()) m_active_var_set.erase();
         unsigned i = 0, j = 0, sz = m_active_vars.size();
@@ -841,7 +693,6 @@ namespace sat {
         m_active_vars.reset();
     }
 
-
     bool card_extension::resolve_conflict() {        
         if (0 == m_num_propagations_since_pop) {
             return false;
@@ -1084,9 +935,9 @@ namespace sat {
         
         TRACE("sat", tout << m_lemma << "\n";);
 
-        if (s().m_config.m_drat) {
+        if (get_config().m_drat) {
             svector<drat::premise> ps; // TBD fill in
-            s().m_drat.add(m_lemma, ps);
+            drat_add(m_lemma, ps);
         }
 
         s().m_lemma.reset();
@@ -1155,16 +1006,11 @@ namespace sat {
         return p;        
     }
 
-    card_extension::card_extension(): m_solver(0), m_has_xor(false) {        
+    card_extension::card_extension(): m_solver(0), m_lookahead(0) {        
         TRACE("sat", tout << this << "\n";);
     }
 
     card_extension::~card_extension() {
-        for (unsigned i = 0; i < m_var_infos.size(); ++i) {
-            m_var_infos[i].reset();
-        }
-        m_var_trail.reset();
-        m_var_lim.reset();
         m_stats.reset();
     }
 
@@ -1180,9 +1026,9 @@ namespace sat {
             m_card_axioms.push_back(c);
         }
         else {
-            init_watch(v);
+            get_wlist(literal(v, false)).push_back(index);
-            m_var_infos[v].m_card = c;
+            get_wlist(literal(v, true)).push_back(index);
-            m_var_trail.push_back(v);
+            m_index_trail.push_back(index);
         }
     }
 
@@ -1197,28 +1043,58 @@ namespace sat {
             m_pb_axioms.push_back(p);
         }
         else {
-            init_watch(v);
+            get_wlist(literal(v, false)).push_back(index);
-            m_var_infos[v].m_pb = p;
+            get_wlist(literal(v, true)).push_back(index);
-            m_var_trail.push_back(v);
+            m_index_trail.push_back(index);
         }
     }
 
 
     void card_extension::add_xor(bool_var v, literal_vector const& lits) {
-        m_has_xor = true;
         unsigned index = 4*m_xors.size() + 0x1;
         SASSERT(is_xor_index(index));
+        SASSERT(v != null_bool_var);
         xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits);
         m_xors.push_back(x);
-        init_watch(v);
+        get_wlist(literal(v, false)).push_back(index);
-        m_var_infos[v].m_xor = x;
+        get_wlist(literal(v, true)).push_back(index);
-        m_var_trail.push_back(v);
+        m_index_trail.push_back(index);
     }
 
 
     void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
+        TRACE("sat", tout << l << " " << idx << "\n";);
+        if (is_pb_index(idx)) {
+            pb& p = index2pb(idx);
+            if (l.var() == p.lit().var()) {
+                init_watch(p, !l.sign());
+            }
+            else {
+                keep = l_undef != add_assign(p, ~l);
+            }
+        }
+        else if (is_card_index(idx)) {
+            card& c = index2card(idx);
+            if (l.var() == c.lit().var()) {
+                init_watch(c, !l.sign());
+            }
+            else {
+                keep = l_undef != add_assign(c, ~l);
+            }
+        }
+        else if (is_xor_index(idx)) {
+            xor& x = index2xor(idx);
+            if (l.var() == x.lit().var()) {
+                init_watch(x, !l.sign());
+            }
+            else {
+                keep = l_undef != add_assign(x, ~l);
+            }
+        }
+        else {
             UNREACHABLE();
         }
+    }
 
 
     void card_extension::ensure_parity_size(bool_var v) {
@@ -1454,100 +1330,53 @@ namespace sat {
         }
         SASSERT(validate_unit_propagation(c));
         
-        for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
+        for (unsigned i = 0; i < bound && !inconsistent(); ++i) {
             assign(c, c[i]);
         }
 
-        return s().inconsistent() ? l_false : l_true;
+        return inconsistent() ? l_false : l_true;
     }
 
     void card_extension::asserted(literal l) {
-        bool_var v = l.var();
-        if (s().inconsistent()) return;
-        if (v >= m_var_infos.size()) return;
-        var_info& vinfo = m_var_infos[v];
-        ptr_vector<card>* cards = vinfo.m_card_watch[!l.sign()];
-        ptr_vector<xor>* xors = vinfo.m_xor_watch;
-        ptr_vector<pb>* pbs = vinfo.m_pb_watch[!l.sign()];
-        pb* p = vinfo.m_pb;
-        card* crd = vinfo.m_card;
-        xor* x = vinfo.m_xor;
-
-        if (!is_tag_empty(cards)) {
-            ptr_vector<card>::iterator begin = cards->begin();
-            ptr_vector<card>::iterator it = begin, it2 = it, end = cards->end();
-            for (; it != end; ++it) {
-                card& c = *(*it);
-                if (c.lit() != null_literal && value(c.lit()) != l_true) {
-                    continue;
-                }
-                switch (add_assign(c, ~l)) {
-                case l_false: // conflict
-                    for (; it != end; ++it, ++it2) {
-                        *it2 = *it;
-                    }
-                    SASSERT(s().inconsistent());
-                    cards->set_end(it2);
-                    return;
-                case l_undef: // watch literal was swapped
-                    break;
-                case l_true: // unit propagation, keep watching the literal
-                    if (it2 != it) {
-                        *it2 = *it;
-                    }
-                    ++it2;
-                    break;
-                }
-            }
-            cards->set_end(it2);
-            if (cards->empty()) {
-                m_var_infos[v].m_card_watch[!l.sign()] = set_tag_empty(cards);
-            }
-        }
-
-        if (crd != 0 && !s().inconsistent()) {
-            init_watch(*crd, !l.sign());
-        }
-        
-        if ((!is_tag_empty(pbs) || p) && !s().inconsistent()) {
-            asserted_pb(l, pbs, p);
-        }
-
-        if (m_has_xor && !s().inconsistent()) {
-            asserted_xor(l, xors, x);
-        }
     }
 
 
     check_result card_extension::check() { return CR_DONE; }
 
     void card_extension::push() {
-        m_var_lim.push_back(m_var_trail.size());
+        m_index_lim.push_back(m_index_trail.size());
     }
 
     void card_extension::pop(unsigned n) {        
         TRACE("sat_verbose", tout << "pop:" << n << "\n";);
-        unsigned new_lim = m_var_lim.size() - n;
+        unsigned new_lim = m_index_lim.size() - n;
-        unsigned sz = m_var_lim[new_lim];
+        unsigned sz = m_index_lim[new_lim];
-        while (m_var_trail.size() > sz) {
+        while (m_index_trail.size() > sz) {
-            bool_var v = m_var_trail.back();
+            unsigned index = m_index_trail.back();
-            m_var_trail.pop_back();
+            m_index_trail.pop_back();
-            if (v != null_bool_var) {
+            if (is_card_index(index)) {
-                card* c = m_var_infos[v].m_card;
+                SASSERT(m_cards.back()->index() == index);
-                if (c) {
+                clear_watch(*m_cards.back());
-                    clear_watch(*c);
+                dealloc(m_cards.back());
-                    m_var_infos[v].m_card = 0;
+                m_cards.pop_back();
-                    dealloc(c);
             }
-                xor* x = m_var_infos[v].m_xor;
+            else if (is_pb_index(index)) {
-                if (x) {
+                SASSERT(m_pbs.back()->index() == index);
-                    clear_watch(*x);
+                clear_watch(*m_pbs.back());
-                    m_var_infos[v].m_xor = 0;
+                dealloc(m_pbs.back());
-                    dealloc(x);
+                m_pbs.pop_back();
+            }
+            else if (is_xor_index(index)) {
+                SASSERT(m_xors.back()->index() == index);
+                clear_watch(*m_xors.back());
+                dealloc(m_xors.back());
+                m_xors.pop_back();
+            }
+            else {
+                UNREACHABLE();
             }
         }
-        }
+        m_index_lim.resize(new_lim);
-        m_var_lim.resize(new_lim);
         m_num_propagations_since_pop = 0;
     }
 
@@ -1604,30 +1433,6 @@ namespace sat {
         }
     }
 
-     void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
-        card_watch const* w = m_var_infos[v].m_card_watch[sign];
-        if (!is_tag_empty(w)) {
-            card_watch const& wl = *w;
-            out << literal(v, sign) << " |-> ";
-            for (unsigned i = 0; i < wl.size(); ++i) {
-                out << wl[i]->lit() << " ";
-            }
-            out << "\n";        
-        }
-    }
-
-    void card_extension::display_watch(std::ostream& out, bool_var v) const {
-        xor_watch const* w = m_var_infos[v].m_xor_watch;
-        if (!is_tag_empty(w)) {
-            xor_watch const& wl = *w;
-            out << "v" << v << " |-> ";
-            for (unsigned i = 0; i < wl.size(); ++i) {
-                out << wl[i]->lit() << " ";
-            }
-            out << "\n";        
-        }
-    }
-
     void card_extension::display(std::ostream& out, ineq& ineq) const {
         for (unsigned i = 0; i < ineq.m_lits.size(); ++i) {
             out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " ";
@@ -1694,17 +1499,6 @@ namespace sat {
     }
 
     std::ostream& card_extension::display(std::ostream& out) const {
-        for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
-            display_watch(out, vi, false);
-            display_watch(out, vi, true);
-            display_watch(out, vi);
-        }
-        for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
-            card* c = m_var_infos[vi].m_card;
-            if (c) display(out, *c, false);
-            xor* x = m_var_infos[vi].m_xor;
-            if (x) display(out, *x, false);
-        }
         return out;
     }
 

src/sat/card_extension.h

@@ -21,8 +21,10 @@ Revision History:
 
 #include"sat_extension.h"
 #include"sat_solver.h"
+#include"sat_lookahead.h"
 #include"scoped_ptr_vector.h"
 
+
 namespace sat {
     
     class card_extension : public extension {
@@ -116,52 +118,8 @@ namespace sat {
             void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); }
         };
 
-        typedef ptr_vector<card> card_watch;
-        typedef ptr_vector<xor> xor_watch;
-        typedef ptr_vector<pb>  pb_watch;
-        struct var_info {
-            card_watch* m_card_watch[2];
-            pb_watch*   m_pb_watch[2];
-            xor_watch*  m_xor_watch;
-            card*       m_card;
-            pb*         m_pb;
-            xor*        m_xor;
-            var_info(): m_xor_watch(0), m_card(0), m_xor(0), m_pb(0) {
-                m_card_watch[0] = 0;
-                m_card_watch[1] = 0;
-                m_pb_watch[0] = 0;
-                m_pb_watch[1] = 0;
-            }
-            void reset() {
-                dealloc(m_card);
-                dealloc(m_xor);
-                dealloc(m_pb);
-                dealloc(card_extension::set_tag_non_empty(m_card_watch[0]));
-                dealloc(card_extension::set_tag_non_empty(m_card_watch[1]));
-                dealloc(card_extension::set_tag_non_empty(m_pb_watch[0]));
-                dealloc(card_extension::set_tag_non_empty(m_pb_watch[1]));
-                dealloc(card_extension::set_tag_non_empty(m_xor_watch));
-            }
-        };
-        
-        template<typename T>
-        static ptr_vector<T>* set_tag_empty(ptr_vector<T>* c) {
-            return TAG(ptr_vector<T>*, c, 1);
-        }
-
-        template<typename T>
-        static bool is_tag_empty(ptr_vector<T> const* c) {
-            return !c || GET_TAG(c) == 1;
-        }
-
-        template<typename T>
-        static ptr_vector<T>* set_tag_non_empty(ptr_vector<T>* c) {
-            return UNTAG(ptr_vector<T>*, c);
-        }
-
-
-
         solver*             m_solver;
+        lookahead*          m_lookahead;
         stats               m_stats;        
 
         ptr_vector<card>    m_cards;
@@ -172,9 +130,8 @@ namespace sat {
         scoped_ptr_vector<pb>   m_pb_axioms;
 
         // watch literals
-        svector<var_info>   m_var_infos;
+        unsigned_vector     m_index_trail;
-        unsigned_vector     m_var_trail;
+        unsigned_vector     m_index_lim;       
-        unsigned_vector     m_var_lim;       
 
         // conflict resolution
         unsigned          m_num_marks;
@@ -185,7 +142,6 @@ namespace sat {
         tracked_uint_set  m_active_var_set;
         literal_vector    m_lemma;
         unsigned          m_num_propagations_since_pop;
-        bool              m_has_xor;
         unsigned_vector   m_parity_marks;
         literal_vector    m_parity_trail;
 
@@ -206,7 +162,7 @@ namespace sat {
         void clear_watch(card& c);
         void reset_coeffs();
         void reset_marked_literals();
-        void unwatch_literal(literal w, card* c);
+        void unwatch_literal(literal w, card& c);
         void get_card_antecedents(literal l, card const& c, literal_vector & r);
 
 
@@ -214,13 +170,12 @@ namespace sat {
         void copy_xor(card_extension& result);
         void clear_watch(xor& x);
         void watch_literal(xor& x, literal lit);
-        void unwatch_literal(literal w, xor* x);
+        void unwatch_literal(literal w, xor& x);
         void init_watch(xor& x, bool is_true);
         void assign(xor& x, literal lit);
         void set_conflict(xor& x, literal lit);
         bool parity(xor const& x, unsigned offset) const;
         lbool add_assign(xor& x, literal alit);
-        void asserted_xor(literal l, ptr_vector<xor>* xors, xor* x);
         void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
         void get_xor_antecedents(literal l, xor const& x, literal_vector & r);
 
@@ -236,7 +191,6 @@ namespace sat {
         // pb functionality
         unsigned m_a_max;
         void copy_pb(card_extension& result);
-        void asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p);
         void init_watch(pb& p, bool is_true);
         lbool add_assign(pb& p, literal alit);
         void add_index(pb& p, unsigned index, literal lit);
@@ -244,28 +198,18 @@ namespace sat {
         void clear_watch(pb& p);
         void set_conflict(pb& p, literal lit);
         void assign(pb& p, literal l);
-        void unwatch_literal(literal w, pb* p);
+        void unwatch_literal(literal w, pb& p);
         void get_pb_antecedents(literal l, pb const& p, literal_vector & r);
 
-
+        inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
-        template<typename T>
-        bool remove(ptr_vector<T>& ts, T* t) {
-            unsigned sz = ts.size();
-            for (unsigned j = 0; j < sz; ++j) {
-                if (ts[j] == t) {                        
-                    std::swap(ts[j], ts[sz-1]);
-                    ts.pop_back();
-                    return sz == 1;
-                }
-            }
-            return false;
-        }
-    
-
-
-        inline lbool value(literal lit) const { return m_solver->value(lit); }
         inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }
         inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); }
+        inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); }
+        inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
+        inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else m_solver->assign(l, j); }
+        inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); else m_solver->set_conflict(j, l); }
+        inline config const& get_config() const { return m_solver->get_config(); }
+        inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { m_solver->m_drat.add(c, premises); }
 
 
         void normalize_active_coeffs();
@@ -296,13 +240,12 @@ namespace sat {
         void display(std::ostream& out, card const& c, bool values) const;
         void display(std::ostream& out, pb const& p, bool values) const;
         void display(std::ostream& out, xor const& c, bool values) const;
-        void display_watch(std::ostream& out, bool_var v) const;
-        void display_watch(std::ostream& out, bool_var v, bool sign) const;
 
     public:
         card_extension();
         virtual ~card_extension();
         virtual void set_solver(solver* s) { m_solver = s; }
+        virtual void set_lookahead(lookahead* l) { m_lookahead = l; }
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xor(bool_var v, literal_vector const& lits);

src/sat/sat_extension.h

@@ -33,6 +33,7 @@ namespace sat {
     public:
         virtual ~extension() {}
         virtual void set_solver(solver* s) = 0;
+        virtual void set_lookahead(lookahead* s) = 0;
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
         virtual void asserted(literal l) = 0;

src/sat/sat_solver.cpp

@@ -779,14 +779,14 @@ namespace sat {
                 case watched::EXT_CONSTRAINT:
                     SASSERT(m_ext);
                     m_ext->propagate(l, it->get_ext_constraint_idx(), keep);
-                    if (keep) {
-                        *it2 = *it;
-                        it2++;
-                    }
                     if (m_inconsistent) {
                         CONFLICT_CLEANUP();
                         return false;
                     }
+                    if (keep) {
+                        *it2 = *it;
+                        it2++;
+                    }
                     break;
                 default:
                     UNREACHABLE();

src/sat/sat_types.h

@@ -124,6 +124,7 @@ namespace sat {
     };
 
     class solver;
+    class lookahead;
     class clause;
     class clause_wrapper;
     class integrity_checker;

src/sat/sat_watched.h

@@ -103,7 +103,7 @@ namespace sat {
         }
 
         bool is_ext_constraint() const { return get_kind() == EXT_CONSTRAINT; }
-        ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val2; }
+        ext_constraint_idx get_ext_constraint_idx() const { SASSERT(is_ext_constraint()); return m_val1; }
         
         bool operator==(watched const & w) const { return m_val1 == w.m_val1 && m_val2 == w.m_val2; }
         bool operator!=(watched const & w) const { return !operator==(w); }