Xor (#6448)

* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int

* Fixed missing assignment for binary clauses

* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Update (not compiling yet)

* #6429

* remove ternary clause optimization

Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.

* Update: Missing data-structures (still not compiling)

* Nearly compiling

* Some missing arguments

* Polishing

* Only conflicts/propagations/justifications are missing for making it compile

* Added propagation (justifications for them are still missing)

* Use the right deallocation

* Use Z3's memory allocation system

* Ported "seen"

* Polishing

* Added 64-bit "1" counting

* More polishing

* minor fixes

- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.

* adding simplifiers layer

simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.

* Create bv_slice_tactic.cpp

missing file

* adding virtual destructor

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

* Added 64-bit "1" counting (#6434)

* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added 64-bit "1" counting

* remove incorrect assertion

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

* Added limit to "visit" to allow detecting multiple visits (#6435)

* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added limit to "visit" to allow detecting multiple visits

* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)

* Bugfix

* init solve_eqs

* working on solve_eqs

* Update .gitignore

* wip - converting the equation solver as a simplifier

* make visited_helper independent of literals

re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.

* build fix

* move model and proof converters to self-contained module

* Create solve_eqs2_tactic.h

* add converters module to python build

* move tactic_params to params

* move more converters

* move horn_subsume_model_converter to ast/converters

* add initial stubs for model reconstruction trail

* fixing build

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

* fixes #6439 #6436

* It's compiling (However, two important functions are commented out)

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

src/CMakeLists.txt

@@ -49,9 +49,11 @@ add_subdirectory(ast/rewriter)
 add_subdirectory(ast/normal_forms)
 add_subdirectory(ast/macros)
 add_subdirectory(model)
+add_subdirectory(ast/euf)
+add_subdirectory(ast/converters)
+add_subdirectory(ast/simplifiers)
 add_subdirectory(tactic)
 add_subdirectory(ast/substitution)
-add_subdirectory(ast/euf)
 add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)

src/ackermannization/ackermannize_bv_model_converter.h

@@ -16,7 +16,7 @@
  --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info);

src/ackermannization/ackr_model_converter.h

@@ -15,7 +15,7 @@ Revision History:
 --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref & info, model_ref & abstr_model);

src/ackermannization/lackr_model_converter_lazy.h

@@ -16,7 +16,7 @@
  --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ackermannization/ackr_info.h"
 
 model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);

src/api/api_ast.cpp

@@ -137,7 +137,7 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
         if (!p.has_def(d)) {
-            std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
+            std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
             SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
             return;
         }
@@ -158,6 +158,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return;
         }
+        if (!pd.get_def()->get_cases().empty()) {
+            std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
+            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            return;            
+        }
+                
         if (abs_body->get_sort() != d->get_range()) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);            
             return;

src/ast/arith_decl_plugin.h

@@ -453,6 +453,9 @@ public:
     app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2); }
     app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_MUL, arg1, arg2, arg3); }
     app * mk_mul(unsigned num_args, expr * const * args) const { return num_args == 1 && is_app(args[0]) ? to_app(args[0]) : m_manager.mk_app(arith_family_id, OP_MUL, num_args, args); }
+    app * mk_mul(ptr_buffer<expr> const& args) const { return mk_mul(args.size(), args.data()); }
+    app * mk_mul(ptr_vector<expr> const& args) const { return mk_mul(args.size(), args.data()); }
+    app * mk_mul(expr_ref_vector const& args) const { return mk_mul(args.size(), args.data()); }
     app * mk_uminus(expr * arg) const { return m_manager.mk_app(arith_family_id, OP_UMINUS, arg); }
     app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_DIV, arg1, arg2); }
     app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(arith_family_id, OP_IDIV, arg1, arg2); }

src/ast/ast.h

@@ -1387,6 +1387,7 @@ inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->ge
 inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); }
 inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; }
 inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; }
+inline bool is_uninterp(func_decl const * n) { return n->get_family_id() == null_family_id; }
 inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; }
 inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); }
 inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); }

src/ast/converters/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(converters
+  SOURCES
+    equiv_proof_converter.cpp
+    generic_model_converter.cpp
+    horn_subsume_model_converter.cpp
+    model_converter.cpp
+    proof_converter.cpp
+    replace_proof_converter.cpp
+  COMPONENT_DEPENDENCIES
+    model
+)

src/ast/converters/equiv_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 #include "ast/ast_pp.h"
 #include "ast/scoped_proof.h"
 

src/ast/converters/equiv_proof_converter.h

@@ -23,7 +23,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 
 class equiv_proof_converter : public proof_converter {
     ast_manager&            m;

src/ast/converters/generic_model_converter.cpp

@@ -24,7 +24,7 @@ Notes:
 #include "ast/occurs.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
 

src/ast/converters/generic_model_converter.h

@@ -19,7 +19,7 @@ Notes:
 --*/
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 
 class generic_model_converter : public model_converter {
     enum instruction { HIDE, ADD };

src/ast/converters/horn_subsume_model_converter.cpp

@@ -18,14 +18,14 @@ Revision History:
 --*/
 
 
-#include "tactic/horn_subsume_model_converter.h"
-#include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
-#include "model/model_smt2_pp.h"
-#include "ast/rewriter/bool_rewriter.h"
-#include "ast/rewriter/th_rewriter.h"
 #include "ast/for_each_expr.h"
 #include "ast/well_sorted.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "model/model_smt2_pp.h"
+#include "ast/converters/horn_subsume_model_converter.h"
 
 void horn_subsume_model_converter::insert(app* head, expr* body) {
     m_delay_head.push_back(head);

src/ast/converters/horn_subsume_model_converter.h

@@ -34,7 +34,7 @@ Subsumption transformation (remove Horn clause):
 
 #pragma once
 
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ast/rewriter/th_rewriter.h"
 
 class horn_subsume_model_converter : public model_converter {

src/ast/converters/model_converter.cpp

@@ -16,7 +16,7 @@ Author:
 Notes:
 
 --*/
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "model/model_v2_pp.h"
 #include "ast/ast_smt2_pp.h"
 

src/ast/converters/model_converter.h

@@ -57,7 +57,7 @@ Notes:
 #include "util/ref.h"
 #include "ast/ast_pp_util.h"
 #include "model/model.h"
-#include "tactic/converter.h"
+#include "ast/converters/converter.h"
 
 class labels_vec : public svector<symbol> {};
 class smt2_pp_environment; 

src/ast/converters/proof_converter.cpp

@@ -16,8 +16,7 @@ Author:
 Notes:
 
 --*/
-#include "tactic/proof_converter.h"
-#include "tactic/goal.h"
+#include "ast/converters/proof_converter.h"
 #include "ast/ast_smt2_pp.h"
 
 class concat_proof_converter : public concat_converter<proof_converter> {
@@ -46,41 +45,6 @@ proof_converter * concat(proof_converter * pc1, proof_converter * pc2) {
     return alloc(concat_proof_converter, pc1, pc2);
 }
 
-class subgoal_proof_converter : public proof_converter {
-    proof_converter_ref m_pc;
-    goal_ref_buffer     m_goals;
-public:
-    subgoal_proof_converter(proof_converter* pc, unsigned n, goal * const* goals):
-        m_pc(pc)
-    {
-        for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]);
-    }
-
-    proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
-        // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals.
-        SASSERT(num_source == 0);
-        proof_converter_ref_buffer pc_buffer;          
-        for (goal_ref g : m_goals) {
-            pc_buffer.push_back(g->pc());
-
-        }
-        return apply(m, m_pc, pc_buffer);
-    }
-
-    proof_converter* translate(ast_translation& tr) override {
-        proof_converter_ref pc1 = m_pc->translate(tr);
-        goal_ref_buffer goals;
-        for (goal_ref g : m_goals) goals.push_back(g->translate(tr));
-        return alloc(subgoal_proof_converter, pc1.get(), goals.size(), goals.data());
-    }
-
-    void display(std::ostream& out) override {}
-    
-};
-
-proof_converter * concat(proof_converter *pc, unsigned n, goal* const* goals) {
-    return alloc(subgoal_proof_converter, pc, n, goals);
-}
 
 class proof2pc : public proof_converter {
     proof_ref m_pr;

src/ast/converters/proof_converter.h

@@ -20,8 +20,7 @@ Notes:
 
 #include "ast/ast.h"
 #include "util/ref.h"
-#include "tactic/converter.h"
-class goal;
+#include "ast/converters/converter.h"
 
 class proof_converter : public converter {
 public:
@@ -36,12 +35,6 @@ typedef sref_buffer<proof_converter> proof_converter_ref_buffer;
 
 proof_converter * concat(proof_converter * pc1, proof_converter * pc2);
 
-/**
-   \brief create a proof converter that takes a set of subgoals and converts their proofs to a proof of 
-   the goal they were derived from.
- */
-proof_converter * concat(proof_converter *pc1, unsigned n, goal* const* goals);
-
 proof_converter * proof2proof_converter(ast_manager & m, proof * pr);
 
 void apply(ast_manager & m, proof_converter * pc, proof_ref & pr);

src/ast/converters/replace_proof_converter.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/expr_functors.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"

src/ast/converters/replace_proof_converter.h

@@ -22,7 +22,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/proof_converter.h"
+#include "ast/converters/proof_converter.h"
 
 class replace_proof_converter : public proof_converter {
     ast_manager&    m;

src/ast/euf/euf_egraph.cpp

@@ -904,6 +904,10 @@ template void euf::egraph::explain_todo(ptr_vector<size_t>& justifications, cc_j
 template void euf::egraph::explain_eq(ptr_vector<size_t>& justifications, cc_justification*, enode* a, enode* b);
 template unsigned euf::egraph::explain_diseq(ptr_vector<size_t>& justifications, cc_justification*, enode* a, enode* b);
 
+template void euf::egraph::explain(ptr_vector<expr_dependency>& justifications, cc_justification*);
+template void euf::egraph::explain_todo(ptr_vector<expr_dependency>& justifications, cc_justification*);
+template void euf::egraph::explain_eq(ptr_vector<expr_dependency>& justifications, cc_justification*, enode* a, enode* b);
+template unsigned euf::egraph::explain_diseq(ptr_vector<expr_dependency>& justifications, cc_justification*, enode* a, enode* b);
 
 
 #if 0

src/ast/euf/euf_etable.cpp

@@ -201,8 +201,6 @@ namespace euf {
     enode_bool_pair etable::insert(enode * n) {
         // it doesn't make sense to insert a constant.
         SASSERT(n->num_args() > 0);
-        SASSERT(!m_manager.is_and(n->get_expr()));
-        SASSERT(!m_manager.is_or(n->get_expr()));
         enode * n_prime;
         void * t = get_table(n); 
         switch (static_cast<table_kind>(GET_TAG(t))) {

src/ast/expr_substitution.h

@@ -45,6 +45,7 @@ public:
     unsigned size() const { return m_subst.size(); }
     void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
     void erase(expr * s);
+    expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; }
     bool find(expr * s, expr * & def, proof * & def_pr);
     bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
     bool contains(expr * s);

src/ast/justified_expr.h

@@ -33,8 +33,7 @@ public:
     justified_expr(justified_expr const& other):
         m(other.m),
         m_fml(other.m_fml),
-        m_proof(other.m_proof)
-    {
+        m_proof(other.m_proof) {
         m.inc_ref(m_fml);
         m.inc_ref(m_proof);
     }
@@ -42,8 +41,7 @@ public:
     justified_expr(justified_expr && other) noexcept :
         m(other.m),
         m_fml(nullptr),
-        m_proof(nullptr)
-    {
+        m_proof(nullptr) {
         std::swap(m_fml, other.m_fml);
         std::swap(m_proof, other.m_proof);
     }
@@ -51,10 +49,11 @@ public:
     ~justified_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_proof);
-		m_fml = nullptr;
-		m_proof = nullptr;
+        m_fml = nullptr;
+        m_proof = nullptr;
     }
     
     expr* get_fml() const { return m_fml; }
+
     proof* get_proof() const { return m_proof; }        
 };

src/ast/recfun_decl_plugin.h

@@ -203,8 +203,9 @@ namespace recfun {
             def const& get_def(func_decl* f) const { return *(m_defs[f]); }
             promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); }
             def& get_def(func_decl* f) { return *(m_defs[f]); }
-            bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); }
+            bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); }            
             case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); }
+            bool is_defined(func_decl* f) {return has_case_def(f) && !get_def(f).get_cases().empty(); }
 
             func_decl_ref_vector get_rec_funs() {
                 func_decl_ref_vector result(m());

src/ast/rewriter/bool_rewriter.cpp

@@ -290,7 +290,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
                 ast_lt lt;
                 std::sort(flat_args.begin(), flat_args.end(), lt);
             }
-            result = m().mk_or(flat_args);
+            result = mk_or_app(flat_args.size(), flat_args.data());
         }
         return BR_DONE;
     }

src/ast/rewriter/mk_extract_proc.cpp

@@ -32,8 +32,15 @@ mk_extract_proc::~mk_extract_proc() {
 }
 
 app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
+    unsigned l, h;
+    while (m_util.is_extract(arg, l, h, arg)) {
+        low += l;
+        high += l;
+    }
     ast_manager & m = m_util.get_manager();
     sort * s = arg->get_sort();
+    if (low == 0 && high + 1 == m_util.get_bv_size(arg) && is_app(arg))
+        return to_app(arg);
     if (m_low == low && m_high == high && m_domain == s)
         return m.mk_app(m_f_cached, arg);
     // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain

src/ast/rewriter/th_rewriter.h

@@ -47,6 +47,7 @@ public:
     expr_ref operator()(expr * n, unsigned num_bindings, expr * const * bindings);
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
+    expr_ref mk_app(func_decl* f, ptr_vector<expr> const& args) { return mk_app(f, args.size(), args.data()); }
 
     bool reduce_quantifier(quantifier * old_q, 
                            expr * new_body, 

src/ast/simplifiers/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(simplifiers
+  SOURCES
+    bv_slice.cpp
+    euf_completion.cpp
+    extract_eqs.cpp
+    model_reconstruction_trail.cpp
+    solve_eqs.cpp
+  COMPONENT_DEPENDENCIES
+    euf
+    rewriter
+)

src/ast/simplifiers/bv_slice.cpp

@@ -0,0 +1,207 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_slice.cpp
+
+Abstract:
+
+    simplifier for extracting bit-vector ranges
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/simplifiers/bv_slice.h"
+
+namespace bv {
+
+    void slice::reduce() {
+        process_eqs();
+        apply_subst();
+        advance_qhead(m_fmls.size());
+    }
+
+    void slice::process_eqs() {
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto const [f, d] = m_fmls[i]();
+            process_eq(f);
+        }  
+    }
+
+    void slice::process_eq(expr* e) {
+        expr* x, * y;
+        if (!m.is_eq(e, x, y))
+            return;
+        if (!m_bv.is_bv(x))
+            return;
+        m_xs.reset();
+        m_ys.reset();
+        get_concats(x, m_xs);
+        get_concats(y, m_ys);
+        slice_eq();
+    }
+
+    void slice::slice_eq() {
+        unsigned i = m_xs.size(), j = m_ys.size();
+        unsigned offx = 0, offy = 0;
+        while (0 < i) {
+            SASSERT(0 < j);
+            expr* x = m_xs[i - 1]; // least significant bits are last 
+            expr* y = m_ys[j - 1];
+            SASSERT(offx == 0 || offy == 0);
+            unsigned szx = m_bv.get_bv_size(x);
+            unsigned szy = m_bv.get_bv_size(y);
+            SASSERT(offx < szx);
+            SASSERT(offy < szy);
+            if (szx - offx == szy - offy) {
+                register_slice(offx, szx - 1, x);
+                register_slice(offy, szy - 1, y);
+                --i;
+                --j;
+                offx = 0;
+                offy = 0;
+            }
+            else if (szx - offx < szy - offy) {
+                register_slice(offx, szx - 1, x);
+                register_slice(offy, offy + szx - offx - 1, y);
+                offy += szx - offx;
+                offx = 0;
+                --i;
+            }
+            else {
+                register_slice(offy, szy - 1, y);
+                register_slice(offx, offx + szy - offy - 1, x);
+                offx += szy - offy;
+                offy = 0;
+                --j;
+            }
+        }
+    }
+
+    void slice::register_slice(unsigned lo, unsigned hi, expr* x) {
+        SASSERT(lo <= hi && hi < m_bv.get_bv_size(x));
+        unsigned l, h;
+        while (m_bv.is_extract(x, l, h, x)) {
+            // x[l:h][lo:hi] = x[l+lo:l+hi]
+            hi += l;
+            lo += l;
+            SASSERT(lo <= hi && hi < m_bv.get_bv_size(x));
+        }
+        unsigned sz = m_bv.get_bv_size(x);
+        if (hi - lo + 1 == sz)
+            return;
+        SASSERT(0 < lo || hi + 1 < sz);
+        auto& b = m_boundaries.insert_if_not_there(x, uint_set());
+
+        struct remove_set : public trail {
+            uint_set& b;
+            unsigned i;
+            remove_set(uint_set& b, unsigned i) :b(b), i(i) {}
+            void undo() override {
+                b.remove(i);
+            }
+        };
+        if (lo > 0 && !b.contains(lo)) {
+            b.insert(lo); 
+            if (m_num_scopes > 0)
+                m_trail.push(remove_set(b, lo));
+        }
+        if (hi + 1 < sz && !b.contains(hi + 1)) {
+            b.insert(hi + 1); 
+            if (m_num_scopes > 0)
+                m_trail.push(remove_set(b, hi+ 1));
+        }
+    }
+
+    expr* slice::mk_extract(unsigned hi, unsigned lo, expr* x) {
+        unsigned l, h;
+        while (m_bv.is_extract(x, l, h, x)) {
+            lo += l;
+            hi += l;
+        }
+        if (lo == 0 && hi + 1 == m_bv.get_bv_size(x))
+            return x;
+        else
+            return m_bv.mk_extract(hi, lo, x);
+    }
+
+    void slice::apply_subst() {
+        if (m_boundaries.empty())
+            return;            
+        expr_ref_vector cache(m), pin(m);
+        ptr_vector<expr> todo, args;
+        expr* c;
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto const [f, d] = m_fmls[i]();
+            todo.push_back(f);
+            pin.push_back(f);
+            while (!todo.empty()) {
+                expr* e = todo.back();
+                c = cache.get(e->get_id(), nullptr);
+                if (c) {
+                    todo.pop_back();
+                    continue;
+                }
+                if (!is_app(e)) {
+                    cache.setx(e->get_id(), e);
+                    todo.pop_back();
+                    continue;
+                }
+                args.reset();
+                unsigned sz = todo.size();
+                bool change = false;
+                for (expr* arg : *to_app(e)) {
+                    c = cache.get(arg->get_id(), nullptr);
+                    if (c) {
+                        args.push_back(c);
+                        change |= c != arg;
+                        SASSERT(c->get_sort() == arg->get_sort());
+                    }
+                    else
+                        todo.push_back(arg);
+                }
+                if (sz == todo.size()) {
+                    todo.pop_back();
+                    if (change)
+                        cache.setx(e->get_id(), m_rewriter.mk_app(to_app(e)->get_decl(), args));
+                    else
+                        cache.setx(e->get_id(), e);
+                    SASSERT(e->get_sort() == cache.get(e->get_id())->get_sort());
+                    uint_set b;
+                    if (m_boundaries.find(e, b)) {
+                        expr* r = cache.get(e->get_id());
+                        expr_ref_vector xs(m);
+                        unsigned lo = 0;
+                        for (unsigned hi : b) {
+                            xs.push_back(mk_extract(hi - 1, lo, r));
+                            lo = hi;
+                        }
+                        xs.push_back(mk_extract(m_bv.get_bv_size(r) - 1, lo, r));
+                        xs.reverse();
+                        expr_ref xc(m_bv.mk_concat(xs), m);
+                        cache.setx(e->get_id(), xc);    
+                        SASSERT(e->get_sort() == xc->get_sort());
+                    }
+                }
+            }
+            c = cache.get(f->get_id());
+            if (c != f)                 
+                m_fmls.update(i, dependent_expr(m, c, d));            
+        }
+    }
+
+    void slice::get_concats(expr* x, ptr_vector<expr>& xs) {
+        while (m_bv.is_concat(x)) {
+            xs.append(to_app(x)->get_num_args(), to_app(x)->get_args()); 
+            x = xs.back();
+            xs.pop_back();
+        }
+        xs.push_back(x);
+    }
+}

src/ast/simplifiers/bv_slice.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_slice.h
+
+Abstract:
+
+    simplifier for extracting bit-vector ranges
+    It rewrites a state using bit-vector slices. 
+    Slices are extracted from bit-vector equality assertions 
+    in the style of (but not fully implementing a full slicing) 
+    Bjorner & Pichora, TACAS 1998 and Brutomesso et al 2008.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "util/uint_set.h"
+#include "ast/bv_decl_plugin.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+
+
+namespace bv {
+
+    class slice : public dependent_expr_simplifier {
+        bv_util                 m_bv;
+        th_rewriter             m_rewriter;
+        obj_map<expr, uint_set> m_boundaries;
+        ptr_vector<expr>        m_xs, m_ys;
+        
+        expr* mk_extract(unsigned hi, unsigned lo, expr* x);
+        void process_eqs();
+        void process_eq(expr* e);
+        void slice_eq();
+        void register_slice(unsigned lo, unsigned hi, expr* x);     
+        void apply_subst();
+        void get_concats(expr* x, ptr_vector<expr>& xs);
+        
+    public:
+
+        slice(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_bv(m), m_rewriter(m) {}
+
+        void push() override { dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); }
+        void reduce() override;
+    };
+}

src/ast/simplifiers/dependent_expr.h

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    dependent_expr.h
+
+Abstract:
+
+    Container class for dependent expressions.
+    They represent how assertions are tracked in goals.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+
+class dependent_expr {
+    ast_manager& m;
+    expr*            m_fml;
+    expr_dependency* m_dep;
+public:
+    dependent_expr(ast_manager& m, expr* fml, expr_dependency* d):
+        m(m),
+        m_fml(fml),
+        m_dep(d) {
+        SASSERT(fml);
+        m.inc_ref(fml);
+        m.inc_ref(d);
+    }
+    
+    dependent_expr& operator=(dependent_expr const& other) {
+        SASSERT(&m == &other.m);
+        if (this != &other) {
+            m.inc_ref(other.m_fml);
+            m.inc_ref(other.m_dep);
+            m.dec_ref(m_fml);
+            m.dec_ref(m_dep);
+            m_fml = other.m_fml;
+            m_dep = other.m_dep;
+        }
+        return *this;
+    }
+    
+    dependent_expr(dependent_expr const& other):
+        m(other.m),
+        m_fml(other.m_fml),
+        m_dep(other.m_dep) {
+        m.inc_ref(m_fml);
+        m.inc_ref(m_dep);
+    }
+
+    dependent_expr(dependent_expr && other) noexcept :
+        m(other.m),
+        m_fml(nullptr),
+        m_dep(nullptr) {
+        std::swap(m_fml, other.m_fml);
+        std::swap(m_dep, other.m_dep);
+    }
+
+    ~dependent_expr() {
+        m.dec_ref(m_fml);
+        m.dec_ref(m_dep);
+        m_fml = nullptr;
+        m_dep = nullptr;
+    }
+    
+    std::tuple<expr*, expr_dependency*> operator()() const { 
+        return { m_fml, m_dep }; 
+    }
+};

src/ast/simplifiers/dependent_expr_state.h

@@ -0,0 +1,90 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    dependent_expr_state.h
+
+Abstract:
+
+    abstraction for simplification of depenent expression states.
+    A dependent_expr_state is an interface to a set of dependent expressions.
+    Dependent expressions are formulas together with a set of dependencies that are coarse grained 
+    proof hints or justifications for them. Input assumptions can be self-justified.
+
+    The dependent_expr_simplifier implements main services:
+    - push, pop - that scope the local state
+    - reduce - to process formulas in a dependent_expr_state between the current value of m_qhead and the size() 
+      of the depdenent_expr_state
+
+    A dependent expr_simplifier can be used to:
+    - to build a tactic
+    - for incremental pre-processing
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+    
+--*/
+
+#pragma once
+
+#include "util/trail.h"
+#include "util/statistics.h"
+#include "util/params.h"
+#include "ast/converters/model_converter.h"
+#include "ast/simplifiers/dependent_expr.h"
+
+
+/**
+   abstract interface to state updated by simplifiers.
+ */
+class dependent_expr_state {
+public:
+    virtual ~dependent_expr_state() {}
+    virtual unsigned size() const = 0;
+    virtual dependent_expr const& operator[](unsigned i) = 0;
+    virtual void update(unsigned i, dependent_expr const& j) = 0;
+    virtual bool inconsistent() = 0;
+};
+
+/**
+   Shared interface of simplifiers. 
+ */
+class dependent_expr_simplifier {
+protected:
+    ast_manager&          m;
+    dependent_expr_state& m_fmls;
+    unsigned       m_qhead = 0;          // pointer into last processed formula in m_fmls
+    unsigned       m_num_scopes = 0;
+    trail_stack    m_trail;    
+    void advance_qhead(unsigned sz) { if (m_num_scopes > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; }
+public:
+    dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s) {}
+    virtual ~dependent_expr_simplifier() {}
+    virtual void push() { m_num_scopes++; m_trail.push_scope(); }
+    virtual void pop(unsigned n) { m_num_scopes -= n; m_trail.pop_scope(n); }
+    virtual void reduce() = 0;
+    virtual void collect_statistics(statistics& st) const {}
+    virtual void reset_statistics() {}
+    virtual void updt_params(params_ref const& p) {}
+    virtual model_converter_ref get_model_converter() { return model_converter_ref(); }
+};
+
+/**
+   Factory interface for creating simplifiers. 
+   The use of a factory allows delaying the creation of the dependent_expr_state
+   argument until the point where the expression simplifier is created.
+   This is used in tactics where the dependent_expr_state is a reference to the
+   new tactic. 
+
+   Alternatively have a clone method on dependent_expr_simplifier.
+ */
+class dependent_expr_simplifier_factory {
+    unsigned m_ref = 0;
+public:
+    virtual dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) = 0;
+    virtual ~dependent_expr_simplifier_factory() {}
+    void inc_ref() { ++m_ref; }
+    void dec_ref() { if (--m_ref == 0) dealloc(this); }
+};

src/ast/simplifiers/euf_completion.cpp

@@ -0,0 +1,328 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion.cpp
+
+Abstract:
+
+    Ground completion for equalities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+Notes:
+
+Create a congruence closure of E.
+Select _simplest_ term in each equivalence class. A term is _simplest_
+if it is smallest in a well-order, such as a ground Knuth-Bendix order.
+A basic approach is terms that are of smallest depth, are values can be chosen as simplest.
+Ties between equal-depth terms can be resolved arbitrarily.
+
+
+Algorithm for extracting canonical form from an E-graph:
+
+* Compute function canon(t) that maps every term in E to a canonical, least with respect to well-order relative to the congruence closure.
+  That is, terms that are equal modulo the congruence closure have the same canonical representative.
+
+* Each f(t) = g(s) in E:
+  * add f(canon(t)) = canon(f(t)), g(canon(s)) = canon(g(s)) where canon(f(t)) = canon(g(s)) by construction.
+  
+* Each other g(t) in E:
+  * add g(canon(t)) to E.
+  * Note that canon(g(t)) = true because g(t) = true is added to congruence closure of E.
+* We claim the new formula is equivalent.
+* The dependencies for each rewrite can be computed by following the equality justification data-structure.
+
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/simplifiers/euf_completion.h"
+
+namespace euf {
+
+    completion::completion(ast_manager& m, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_egraph(m),
+        m_canonical(m),
+        m_eargs(m),
+        m_deps(m),
+        m_rewriter(m) {
+        m_tt = m_egraph.mk(m.mk_true(), 0, 0, nullptr);
+        m_ff = m_egraph.mk(m.mk_false(), 0, 0, nullptr);
+    }
+
+    void completion::reduce() {
+        ++m_epoch;
+        add_egraph();
+        map_canonical();
+        read_egraph();
+    }
+
+    void completion::add_egraph() {
+        m_nodes.reset();
+        unsigned sz = m_fmls.size();
+        expr* x, *y;
+        for (unsigned i = m_qhead; i < sz; ++i) {
+            auto [f,d] = m_fmls[i]();
+            auto* n = mk_enode(f);
+            if (m.is_eq(f, x, y)) 
+                m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
+            if (m.is_not(f, x)) 
+                m_egraph.merge(n->get_arg(0), m_ff, d);
+            else 
+                m_egraph.merge(n, m_tt, d);
+        }
+        m_egraph.propagate();
+    }
+
+    void completion::read_egraph() {
+
+        if (m_egraph.inconsistent()) {
+            auto* d = explain_conflict();
+            dependent_expr de(m, m.mk_false(), d);
+            m_fmls.update(0, de);
+            return;
+        }
+
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto [f, d] = m_fmls[i]();
+            
+            expr_dependency_ref dep(d, m);
+            expr_ref g = canonize_fml(f, dep);
+            if (g != f) {
+                m_fmls.update(i, dependent_expr(m, g, dep));
+                m_stats.m_num_rewrites++;
+                IF_VERBOSE(10, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
+            }
+            CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
+        }
+        advance_qhead(m_fmls.size());
+    }
+
+    enode* completion::mk_enode(expr* e) {
+        m_todo.push_back(e);
+        enode* n;
+        while (!m_todo.empty()) {
+            e = m_todo.back();
+            if (m_egraph.find(e)) {
+                m_todo.pop_back();
+                continue;
+            }
+            if (!is_app(e)) {
+                m_nodes.push_back(m_egraph.mk(e, 0, 0, nullptr));
+                m_todo.pop_back();
+                continue;
+            }
+            m_args.reset();
+            unsigned sz = m_todo.size();
+            for (expr* arg : *to_app(e)) {
+                n = m_egraph.find(arg);
+                if (n)
+                    m_args.push_back(n);
+                else 
+                    m_todo.push_back(arg);
+            }
+            if (sz == m_todo.size()) {
+                m_nodes.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data()));
+                m_todo.pop_back();
+            }
+        }
+        return m_egraph.find(e);
+    }
+
+    expr_ref completion::canonize_fml(expr* f, expr_dependency_ref& d) {
+
+        expr* x, * y;
+        if (m.is_eq(f, x, y)) {
+            expr_ref x1 = canonize(x, d);
+            expr_ref y1 = canonize(y, d);
+
+            if (x == x1 && y == y1)
+                return expr_ref(f, m);
+            if (x1 == y1)
+                return expr_ref(m.mk_true(), m);
+            else {
+                expr* c = get_canonical(x, d);
+                if (c == x1)
+                    return expr_ref(m.mk_eq(y1, c), m);
+                else if (c == y1)
+                    return expr_ref(m.mk_eq(x1, c), m);
+                else
+                    return expr_ref(m.mk_and(m.mk_eq(x1, c), m.mk_eq(y1, c)), m);
+            }
+        }
+
+        if (m.is_not(f, x)) {
+            expr_ref x1 = canonize(x, d);
+            return expr_ref(mk_not(m, x1), m);
+        }
+
+        return canonize(f, d);
+    }
+
+    expr_ref completion::canonize(expr* f, expr_dependency_ref& d) {
+        if (!is_app(f))
+            return expr_ref(f, m); // todo could normalize ground expressions under quantifiers
+
+        m_eargs.reset();
+        bool change = false;
+        for (expr* arg : *to_app(f)) {
+            m_eargs.push_back(get_canonical(arg, d));
+            change = arg != m_eargs.back();
+        }
+
+        if (!change) 
+            return expr_ref(f, m);        
+        else
+            return expr_ref(m_rewriter.mk_app(to_app(f)->get_decl(), m_eargs.size(), m_eargs.data()), m);
+    }
+
+    expr* completion::get_canonical(expr* f, expr_dependency_ref& d) {
+        enode* n = m_egraph.find(f);
+        enode* r = n->get_root();
+        d = m.mk_join(d, explain_eq(n, r));
+        d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));        
+        return m_canonical.get(r->get_id());
+    }
+    
+    expr* completion::get_canonical(enode* n) {
+        if (m_epochs.get(n->get_id(), 0) == m_epoch)
+            return m_canonical.get(n->get_id());
+        else
+            return nullptr;
+    }
+
+    void completion::set_canonical(enode* n, expr* e) {
+        class vtrail : public trail {
+            expr_ref_vector& c;
+            unsigned idx;
+            expr_ref old_value;
+        public:
+            vtrail(expr_ref_vector& c, unsigned idx) : 
+                c(c), idx(idx), old_value(c.get(idx), c.m()) {
+            }
+        
+            void undo() override {
+                c[idx] = old_value;
+                old_value = nullptr;
+            }
+        };
+        if (m_num_scopes > 0)
+            m_trail.push(vtrail(m_canonical, n->get_id()));
+        m_canonical.setx(n->get_id(), e);
+        m_epochs.setx(n->get_id(), m_epoch, 0);
+    }
+
+    expr_dependency* completion::explain_eq(enode* a, enode* b) {
+        if (a == b)
+            return nullptr;
+        ptr_vector<expr_dependency> just;
+        m_egraph.begin_explain();
+        m_egraph.explain_eq(just, nullptr, a, b);
+        m_egraph.end_explain();
+        expr_dependency* d = nullptr;
+        for (expr_dependency* d2 : just)
+            d = m.mk_join(d, d2);
+        return d;
+    }
+
+    expr_dependency* completion::explain_conflict() {
+        ptr_vector<expr_dependency> just;
+        m_egraph.begin_explain();
+        m_egraph.explain(just, nullptr);
+        m_egraph.end_explain();
+        expr_dependency* d = nullptr;
+        for (expr_dependency* d2 : just)
+            d = m.mk_join(d, d2);
+        return d;
+    }
+
+    void completion::collect_statistics(statistics& st) const {
+        st.update("euf-completion-rewrites", m_stats.m_num_rewrites);        
+    }
+
+    void completion::map_canonical() {
+        m_todo.reset();
+        enode_vector roots;
+        for (unsigned i = 0; i < m_nodes.size(); ++i) {
+            enode* n = m_nodes[i]->get_root();
+            if (n->is_marked1())
+                continue;
+            n->mark1();
+            roots.push_back(n);
+            enode* rep = nullptr;
+            for (enode* k : enode_class(n)) 
+                if (!rep || m.is_value(k->get_expr()) || get_depth(rep->get_expr()) > get_depth(k->get_expr()))
+                    rep = k;
+            m_reps.setx(n->get_id(), rep, nullptr);
+
+            TRACE("euf_completion", tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n";
+                         for (enode* k : enode_class(n)) tout << m_egraph.bpp(k) << "\n";);
+            m_todo.push_back(n->get_expr());
+            for (enode* arg : enode_args(n)) {
+                arg = arg->get_root();
+                if (!arg->is_marked1())
+                    m_nodes.push_back(arg);
+            }
+        }
+        for (enode* r : roots)
+            r->unmark1();
+
+        // explain dependencies when no nodes are marked.
+        // explain_eq uses both mark1 and mark2 on e-nodes so 
+        // we cannot call it inside the previous loop where mark1 is used
+        // to track which roots have been processed.
+        for (enode* r : roots) {
+            enode* rep = m_reps[r->get_id()];
+            auto* d = explain_eq(r, rep);
+            m_deps.setx(r->get_id(), d);
+        }
+        expr_ref new_expr(m);
+        while (!m_todo.empty()) {
+            expr* e = m_todo.back();
+            enode* n = m_egraph.find(e);
+            SASSERT(n->is_root());
+            enode* rep = m_reps[n->get_id()];
+            if (get_canonical(n)) 
+                m_todo.pop_back();
+            else if (get_depth(rep->get_expr()) == 0 || !is_app(rep->get_expr())) {
+                set_canonical(n, rep->get_expr());
+                m_todo.pop_back();
+            }
+            else {
+                m_eargs.reset();
+                unsigned sz = m_todo.size();
+                bool new_arg = false;
+                expr_dependency* d = m_deps.get(n->get_id(), nullptr);
+                for (enode* arg : enode_args(rep)) {
+                    enode* rarg = arg->get_root();
+                    expr* c = get_canonical(rarg);
+                    if (c) {
+                        m_eargs.push_back(c);
+                        new_arg |= c != arg->get_expr();
+                        d = m.mk_join(d, m_deps.get(rarg->get_id(), nullptr));
+                    }
+                    else
+                        m_todo.push_back(rarg->get_expr());
+                }
+                if (sz == m_todo.size()) {
+                    m_todo.pop_back();
+                    if (new_arg) 
+                        new_expr = m_rewriter.mk_app(to_app(rep->get_expr())->get_decl(), m_eargs.size(), m_eargs.data());                    
+                    else
+                        new_expr = rep->get_expr();                        
+                    set_canonical(n, new_expr);
+                    m_deps.setx(n->get_id(), d);
+                }
+            }
+        }
+    }        
+}
+
+

src/ast/simplifiers/euf_completion.h

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion.h
+
+Abstract:
+
+    Ground completion for equalities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/rewriter/th_rewriter.h"
+
+namespace euf {
+
+    class completion : public dependent_expr_simplifier {
+
+        struct stats {
+            unsigned m_num_rewrites = 0;
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        egraph                 m_egraph;
+        enode*                 m_tt, *m_ff;
+        ptr_vector<expr>       m_todo;
+        enode_vector           m_args, m_reps, m_nodes;
+        expr_ref_vector        m_canonical, m_eargs;
+        expr_dependency_ref_vector m_deps;
+        unsigned               m_epoch = 0;
+        unsigned_vector        m_epochs;
+        th_rewriter            m_rewriter;
+        stats                  m_stats;
+
+        enode* mk_enode(expr* e);
+        void add_egraph();
+        void map_canonical();
+        void read_egraph();
+        expr_ref canonize(expr* f, expr_dependency_ref& dep);
+        expr_ref canonize_fml(expr* f, expr_dependency_ref& dep);
+        expr* get_canonical(expr* f, expr_dependency_ref& d);
+        expr* get_canonical(enode* n);
+        void set_canonical(enode* n, expr* e);
+        expr_dependency* explain_eq(enode* a, enode* b);
+        expr_dependency* explain_conflict();
+    public:
+        completion(ast_manager& m, dependent_expr_state& fmls);
+        void push() override { m_egraph.push(); dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); }
+        void reduce() override;
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override { m_stats.reset(); }
+    };
+}

src/ast/simplifiers/extract_eqs.cpp

@@ -0,0 +1,257 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    extract_eqs.cpp
+
+Abstract:
+
+    simplifier for solving equations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
+#include "ast/ast_pp.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/simplifiers/extract_eqs.h"
+#include "params/tactic_params.hpp"
+
+
+namespace euf {
+
+    class basic_extract_eq : public extract_eq {
+        ast_manager& m;
+        bool m_ite_solver = true;
+
+    public:
+        basic_extract_eq(ast_manager& m) : m(m) {}
+
+        void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
+            auto [f, d] = e();
+            expr* x, * y;
+            if (m.is_eq(f, x, y)) {
+                if (is_uninterp_const(x))
+                    eqs.push_back(dependent_eq(to_app(x), expr_ref(y, m), d));
+                if (is_uninterp_const(y))
+                    eqs.push_back(dependent_eq(to_app(y), expr_ref(x, m), d));
+            }
+            expr* c, * th, * el, * x1, * y1, * x2, * y2;
+            if (m_ite_solver && m.is_ite(f, c, th, el)) {
+                if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) {
+                    if (x1 == y2 && is_uninterp_const(x1))
+                        std::swap(x2, y2);
+                    if (x2 == y2 && is_uninterp_const(x2))
+                        std::swap(x2, y2), std::swap(x1, y1);
+                    if (x2 == y1 && is_uninterp_const(x2))
+                        std::swap(x1, y1);
+                    if (x1 == x2 && is_uninterp_const(x1)) 
+                        eqs.push_back(dependent_eq(to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d));                    
+                }
+            }
+            if (is_uninterp_const(f))
+                eqs.push_back(dependent_eq(to_app(f), expr_ref(m.mk_true(), m), d));
+            if (m.is_not(f, x) && is_uninterp_const(x))
+                eqs.push_back(dependent_eq(to_app(x), expr_ref(m.mk_false(), m), d));
+        }
+
+        void updt_params(params_ref const& p) {
+            tactic_params tp(p);
+            m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
+        }
+    };
+
+    class arith_extract_eq : public extract_eq {
+        ast_manager&       m;
+        arith_util         a;
+        expr_ref_vector    m_args;
+        expr_sparse_mark   m_nonzero;
+        bool               m_enabled = true;
+
+
+        // solve u mod r1 = y -> u = r1*mod!1 + y
+        void solve_mod(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            expr* u, * z;
+            rational r1, r2;
+            if (!a.is_mod(x, u, z))
+                return;
+            if (!a.is_numeral(z, r1))
+                return;
+            if (r1 <= 0)
+                return;
+            expr_ref term(m);
+            term = a.mk_add(a.mk_mul(z, m.mk_fresh_const("mod", a.mk_int())), y);
+            solve_eq(u, term, d, eqs);
+        }
+
+        /***
+        * Solve
+        *    x + Y = Z    -> x = Z - Y
+        *    -1*x + Y = Z -> x = Y - Z
+        *    a*x + Y = Z  -> x = (Z - Y)/a for is-real(x)        
+        */
+        void solve_add(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            if (!a.is_add(x))
+                return;
+            expr* u, * z;
+            rational r;
+            expr_ref term(m);
+            unsigned i = 0;
+            auto mk_term = [&](unsigned i) {
+                term = y;
+                unsigned j = 0;
+                for (expr* arg2 : *to_app(x)) {
+                    if (i != j)
+                        term = a.mk_sub(term, arg2);
+                    ++j;
+                }
+            };
+            for (expr* arg : *to_app(x)) {
+                if (is_uninterp_const(arg)) {
+                    mk_term(i);
+                    eqs.push_back(dependent_eq(to_app(arg), term, d));
+                }
+                else if (a.is_mul(arg, u, z) && a.is_numeral(u, r) && is_uninterp_const(z)) {
+                    if (r == -1) {
+                        mk_term(i);
+                        term = a.mk_uminus(term);
+                        eqs.push_back(dependent_eq(to_app(z), term, d));
+                    }
+                    else if (a.is_real(arg) && r != 0) {
+                        mk_term(i);
+                        term = a.mk_div(term, u);
+                        eqs.push_back(dependent_eq(to_app(z), term, d));
+                    }
+                }
+                else if (a.is_real(arg) && a.is_mul(arg)) {
+                    unsigned j = 0;
+                    for (expr* xarg : *to_app(arg)) {
+                        ++j;
+                        if (!is_uninterp_const(xarg))
+                            continue;
+                        unsigned k = 0;
+                        bool nonzero = true;
+                        for (expr* yarg : *to_app(arg)) {
+                            ++k;
+                            nonzero = k == j || m_nonzero.is_marked(yarg) || (a.is_numeral(yarg, r) && r != 0);                           
+                            if (!nonzero)
+                                break;
+                        }
+                        if (!nonzero)
+                            continue;
+
+                        k = 0;
+                        ptr_buffer<expr> args;
+                        for (expr* yarg : *to_app(arg)) {
+                            ++k;
+                            if (k != j)
+                                args.push_back(yarg);
+                        }
+                        mk_term(i);
+                        term = a.mk_div(term, a.mk_mul(args.size(), args.data()));
+                        eqs.push_back(dependent_eq(to_app(xarg), term, d));
+                    }
+                }
+                ++i;
+            }
+        }
+
+        /***
+        * Solve for x * Y = Z, where Y != 0 -> x = Z / Y
+        */
+        void solve_mul(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            if (!a.is_mul(x))
+                return;
+            rational r;
+            expr_ref term(m);
+            unsigned i = 0;
+            for (expr* arg : *to_app(x)) {
+                ++i;
+                if (!is_uninterp_const(arg))
+                    continue;
+                unsigned j = 0;
+                bool nonzero = true;
+                for (expr* arg2 : *to_app(x)) {
+                    ++j;
+                    nonzero = j == i || m_nonzero.is_marked(arg2) || (a.is_numeral(arg2, r) && r != 0);
+                    if (!nonzero)
+                        break;
+                }
+                if (!nonzero)
+                    continue;
+                ptr_buffer<expr> args;
+                j = 0;
+                for (expr* arg2 : *to_app(x)) {
+                    ++j;
+                    if (j != i)
+                        args.push_back(arg2);
+                }
+                term = a.mk_div(y, a.mk_mul(args));
+                eqs.push_back(dependent_eq(to_app(arg), term, d));
+            }
+        }
+
+        void add_pos(expr* f) {
+            expr* lhs = nullptr, * rhs = nullptr;
+            rational val;
+            if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_neg()) 
+                m_nonzero.mark(lhs);            
+            else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_pos())
+                m_nonzero.mark(lhs);            
+            else if (m.is_not(f, f)) {
+                if (a.is_le(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_neg())
+                    m_nonzero.mark(lhs);
+                else if (a.is_ge(f, lhs, rhs) && a.is_numeral(rhs, val) && !val.is_pos())
+                    m_nonzero.mark(lhs);
+                else if (m.is_eq(f, lhs, rhs) && a.is_numeral(rhs, val) && val.is_zero())
+                    m_nonzero.mark(lhs);
+            }
+        }
+
+        void solve_eq(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            solve_add(x, y, d, eqs);
+            solve_mod(x, y, d, eqs);
+            solve_mul(x, y, d, eqs);
+        }
+
+    public:
+        arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m) {}
+        void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
+            if (!m_enabled)
+                return;
+            auto [f, d] = e();
+            expr* x, * y;
+            if (m.is_eq(f, x, y) && a.is_int_real(x)) {
+                solve_eq(x, y, d, eqs);
+                solve_eq(y, x, d, eqs);
+            }
+        }
+
+        void pre_process(dependent_expr_state& fmls) override {
+            if (!m_enabled)
+                return;
+            m_nonzero.reset();
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                auto [f, d] = fmls[i]();
+                add_pos(f);
+            }
+        }
+
+
+        void updt_params(params_ref const& p) {
+            tactic_params tp(p);
+            m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver());
+        }
+    };
+
+    void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex) {
+        ex.push_back(alloc(arith_extract_eq, m));
+        ex.push_back(alloc(basic_extract_eq, m));
+    }
+}

src/ast/simplifiers/extract_eqs.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    extract_eqs.h
+
+Abstract:
+
+    simplifier for solving equations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/expr_substitution.h"
+#include "util/scoped_ptr_vector.h"
+
+
+namespace euf {
+
+    struct dependent_eq {
+        app* var;
+        expr_ref term;
+        expr_dependency* dep;
+        dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {}
+    };
+
+    typedef vector<dependent_eq> dep_eq_vector;
+
+    class extract_eq {
+    public:
+        virtual ~extract_eq() {}
+        virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0;
+        virtual void pre_process(dependent_expr_state& fmls) {}
+        virtual void updt_params(params_ref const& p) {}
+    };
+
+    void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex);
+
+}

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    model_reconstruction_trail.cpp
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-3.
+    
+--*/
+
+
+#include "ast/for_each_expr.h"
+#include "ast/simplifiers/model_reconstruction_trail.h"
+#include "ast/converters/generic_model_converter.h"
+
+
+void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependent_expr>& added) {
+    // accumulate a set of dependent exprs, updating m_trail to exclude loose 
+    // substitutions that use variables from the dependent expressions.
+    ast_mark free_vars;
+    auto [f, dep] = d();
+    for (expr* t : subterms::all(expr_ref(f, m))) 
+        free_vars.mark(t, true);
+    
+    NOT_IMPLEMENTED_YET();
+}
+
+/**
+ * retrieve the current model converter corresponding to chaining substitutions from the trail.
+ */
+model_converter_ref model_reconstruction_trail::get_model_converter() {
+    model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+    // walk the trail from the back
+    // add substitutions from the back to the generic model converter
+    // after they have been normalized using a global replace that replaces 
+    // substituted variables by their terms.
+    NOT_IMPLEMENTED_YET();
+    return mc;
+
+}
+

src/ast/simplifiers/model_reconstruction_trail.h

@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    model_reconstruction_trail.h
+
+Abstract:
+
+   Model reconstruction trail
+   A model reconstruction trail comprises of a sequence of assignments 
+   together with assertions that were removed in favor of the assignments. 
+   The assignments satisfy the removed assertions but are not (necessarily) 
+   equivalent to the removed assertions. For the case where assignments 
+   are equivalent to removed assertions, we squash the removed assertions 
+   and don't track them.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-3.
+    
+--*/
+
+#pragma once
+
+#include "util/scoped_ptr_vector.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/simplifiers/dependent_expr.h"
+#include "ast/converters/model_converter.h"
+
+class model_reconstruction_trail {
+
+    ast_manager& m;
+
+    struct model_reconstruction_trail_entry {
+        scoped_ptr<expr_replacer> m_replace;
+        vector<dependent_expr>    m_removed;
+        model_reconstruction_trail_entry(expr_replacer* r, vector<dependent_expr> const& rem) :
+            m_replace(r), m_removed(rem) {}
+    };
+
+    scoped_ptr_vector<model_reconstruction_trail_entry> m_trail;
+    unsigned_vector m_limit;
+
+public:
+
+    model_reconstruction_trail(ast_manager& m) : m(m) {}
+
+    /**
+    * add a new substitution to the stack
+    */
+    void push(expr_replacer* r, vector<dependent_expr> const& removed) {
+        m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed));
+    }
+
+    /**
+    * register a new depedent expression, update the trail 
+    * by removing substitutions that are not equivalence preserving.
+    */
+    void replay(dependent_expr const& d, vector<dependent_expr>& added);
+
+    /**
+    * retrieve the current model converter corresponding to chaining substitutions from the trail.
+    */
+    model_converter_ref get_model_converter();
+
+    /**
+    * push a context. Portions of the trail added within a context are removed after a context pop.
+    */
+    void push() {
+        m_limit.push_back(m_trail.size());
+    }
+
+    void pop(unsigned n) {
+        unsigned old_sz = m_limit[m_limit.size() - n];
+        m_trail.resize(old_sz);
+        m_limit.shrink(m_limit.size() - n);
+    }
+};
+

src/ast/simplifiers/solve_eqs.cpp

@@ -0,0 +1,215 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    solve_eqs.cpp
+
+Abstract:
+
+    simplifier for solving equations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#include "util/trace.h"
+#include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
+#include "ast/ast_pp.h"
+#include "ast/recfun_decl_plugin.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/simplifiers/solve_eqs.h"
+#include "ast/converters/generic_model_converter.h"
+#include "params/tactic_params.hpp"
+
+
+namespace euf {
+
+    // initialize graph that maps variable ids to next ids
+    void solve_eqs::extract_dep_graph(dep_eq_vector& eqs) {
+        m_var2id.reset();
+        m_id2var.reset();
+        m_next.reset();
+        unsigned sz = 0;
+        for (auto const& [v, t, d] : eqs)
+            sz = std::max(sz, v->get_id());
+        m_var2id.resize(sz + 1, UINT_MAX);
+        for (auto const& [v, t, d] : eqs) {
+            if (is_var(v) || !can_be_var(v))
+                continue;
+            m_var2id[v->get_id()] = m_id2var.size();
+            m_id2var.push_back(v);
+        }
+        m_next.resize(m_id2var.size());
+
+        for (auto const& eq : eqs)
+            if (can_be_var(eq.var))
+                m_next[var2id(eq.var)].push_back(eq);
+    }
+
+    /**
+    * Build a substitution while assigning levels to terms.
+    * The substitution is well-formed when variables are replaced with terms whose
+    * Free variables have higher levels.
+    */
+    void solve_eqs::extract_subst() {
+        m_id2level.reset();
+        m_id2level.resize(m_id2var.size(), UINT_MAX);
+        m_subst_ids.reset();
+        m_subst = alloc(expr_substitution, m, false, false);
+
+        auto is_explored = [&](unsigned id) {
+            return m_id2level[id] != UINT_MAX;
+        };
+
+        auto is_safe = [&](unsigned lvl, expr* t) {
+            for (auto* e : subterms::all(expr_ref(t, m)))
+                if (is_var(e) && m_id2level[var2id(e)] < lvl)
+                    return false;
+            return true;
+        };
+
+        unsigned init_level = UINT_MAX;
+        unsigned_vector todo;
+        for (unsigned id = 0; id < m_id2var.size(); ++id) {
+            if (is_explored(id))
+                continue;
+            // initialize current level to have enough room to assign different levels to all variables.
+            if (init_level < m_id2var.size() + 1)
+                return;
+            init_level -= m_id2var.size() + 1;
+            unsigned curr_level = init_level;
+            todo.push_back(id);
+            while (!todo.empty()) {
+                unsigned j = todo.back();
+                todo.pop_back();
+                if (is_explored(j))
+                    continue;
+                m_id2level[id] = curr_level++;
+                for (auto const& eq : m_next[j]) {
+                    auto const& [v, t, d] = eq;
+                    if (!is_safe(curr_level, t))
+                        continue;
+                    m_next[j][0] = eq;
+                    m_subst_ids.push_back(id);                   
+                    for (expr* e : subterms::all(expr_ref(t, m))) 
+                        if (is_var(e) && !is_explored(var2id(e))) 
+                            todo.push_back(var2id(e));   
+                    break;
+                }
+            }            
+        }
+    }
+
+    void solve_eqs::add_subst(dependent_eq const& eq) {
+        SASSERT(can_be_var(eq.var));
+        m_subst->insert(eq.var, eq.term, nullptr, eq.dep);
+        ++m_stats.m_num_elim_vars;
+    }
+
+    void solve_eqs::normalize() {
+        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+        m_subst->reset();
+        rp->set_substitution(m_subst.get());
+
+        std::sort(m_subst_ids.begin(), m_subst_ids.end(), [&](unsigned u, unsigned v) { return m_id2level[u] > m_id2level[v]; });
+
+        expr_dependency_ref new_dep(m);
+        expr_ref new_def(m);
+        proof_ref new_pr(m);
+
+        for (unsigned id : m_subst_ids) {
+            if (!m.inc())
+                break;
+            auto const& [v, def, dep] = m_next[id][0];
+            rp->operator()(def, new_def, new_pr, new_dep);
+            m_stats.m_num_steps += rp->get_num_steps() + 1;
+            new_dep = m.mk_join(dep, new_dep);
+            m_subst->insert(v, new_def, new_pr, new_dep);
+            // we updated the substitution, but we don't need to reset rp
+            // because all cached values there do not depend on v.
+        }
+
+        TRACE("solve_eqs",
+            tout << "after normalizing variables\n";
+        for (unsigned id : m_subst_ids) {
+            auto const& eq = m_next[id][0];
+            expr* def = m_subst->find(eq.var);
+            tout << mk_pp(eq.var, m) << "\n----->\n" << mk_pp(def, m) << "\n\n";
+        });
+    }
+
+    void solve_eqs::apply_subst() {
+        if (!m.inc())
+            return;
+        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+        rp->set_substitution(m_subst.get());
+        expr_ref new_f(m);
+        proof_ref new_pr(m);
+        expr_dependency_ref new_dep(m);
+        for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) {
+            auto [f, d] = m_fmls[i]();
+            rp->operator()(f, new_f, new_pr, new_dep);
+            if (new_f == f)
+                continue;
+            new_dep = m.mk_join(d, new_dep);
+            m_fmls.update(i, dependent_expr(m, new_f, new_dep));
+        }
+    }
+    
+    void solve_eqs::reduce() {
+
+        for (extract_eq* ex : m_extract_plugins)
+            ex->pre_process(m_fmls);
+
+        // TODO add a loop.
+        dep_eq_vector eqs;
+        get_eqs(eqs);
+        extract_dep_graph(eqs);
+        extract_subst();
+        apply_subst();
+        advance_qhead(m_fmls.size());
+    }
+
+    void solve_eqs::filter_unsafe_vars() {
+        m_unsafe_vars.reset();
+        recfun::util rec(m);
+        for (func_decl* f : rec.get_rec_funs())
+            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m)))
+                m_unsafe_vars.mark(term);
+    }
+
+    typedef generic_model_converter gmc;
+
+    model_converter_ref solve_eqs::get_model_converter() {
+        model_converter_ref mc = alloc(gmc, m, "solve-eqs");
+        for (unsigned id : m_subst_ids) {
+            auto* v = m_id2var[id];
+            static_cast<gmc*>(mc.get())->add(v, m_subst->find(v));
+        }
+        return mc;
+    }
+
+    solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : 
+        dependent_expr_simplifier(m, fmls), m_rewriter(m) {
+        register_extract_eqs(m, m_extract_plugins);
+    }
+
+    void solve_eqs::updt_params(params_ref const& p) {
+        tactic_params tp(p);
+        m_config.m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
+        m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
+        for (auto* ex : m_extract_plugins)
+            ex->updt_params(p);
+    }
+
+    void solve_eqs::collect_statistics(statistics& st) const {
+        st.update("solve-eqs-steps", m_stats.m_num_steps);
+        st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars);
+    }
+
+}

src/ast/simplifiers/solve_eqs.h

@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    solve_eqs.h
+
+Abstract:
+
+    simplifier for solving equations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "util/scoped_ptr_vector.h"
+#include "ast/expr_substitution.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/simplifiers/extract_eqs.h"
+
+namespace euf {
+
+    class solve_eqs : public dependent_expr_simplifier {
+        struct stats {
+            unsigned m_num_steps = 0;
+            unsigned m_num_elim_vars = 0;
+        };
+        struct config {
+            bool m_context_solve = true;
+            unsigned m_max_occs = UINT_MAX;
+        };
+
+        th_rewriter                   m_rewriter;
+        scoped_ptr_vector<extract_eq> m_extract_plugins;
+        unsigned_vector               m_var2id, m_id2level, m_subst_ids;
+        ptr_vector<app>               m_id2var;
+        vector<dep_eq_vector>         m_next;  
+        scoped_ptr<expr_substitution> m_subst;
+
+        expr_mark                     m_unsafe_vars;   // expressions that cannot be replaced
+        stats                         m_stats;
+        config                        m_config;
+
+        void add_subst(dependent_eq const& eq);
+
+        bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; }
+        unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; }
+
+        void get_eqs(dep_eq_vector& eqs) {
+            for (unsigned i = m_qhead; i < m_fmls.size(); ++i) 
+                get_eqs(m_fmls[i], eqs);            
+        }
+
+        void get_eqs(dependent_expr const& f, dep_eq_vector& eqs) {
+            for (extract_eq* ex : m_extract_plugins)
+                ex->get_eqs(f, eqs);
+        }
+
+        void filter_unsafe_vars();
+        bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); }
+        void extract_subst();
+        void extract_dep_graph(dep_eq_vector& eqs);
+        void normalize();
+        void apply_subst();
+
+    public:
+
+        solve_eqs(ast_manager& m, dependent_expr_state& fmls);
+
+        void push() override { dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); }
+        void reduce() override;
+
+        void updt_params(params_ref const& p) override;
+        void collect_statistics(statistics& st) const override;
+
+        model_converter_ref get_model_converter() override;
+    };
+}

src/cmd_context/cmd_context.cpp

@@ -47,7 +47,7 @@ Notes:
 #include "model/model_v2_pp.h"
 #include "model/model_params.hpp"
 #include "tactic/tactic_exception.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "solver/smt_logics.h"
 #include "cmd_context/basic_cmds.h"
 #include "cmd_context/cmd_context.h"

src/cmd_context/cmd_context.h

@@ -33,7 +33,7 @@ Notes:
 #include "ast/datatype_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "solver/solver.h"
 #include "solver/check_logic.h"
 #include "solver/progress_callback.h"

src/math/simplex/model_based_opt.cpp

@@ -1299,7 +1299,7 @@ namespace opt {
         def result;
         unsigned_vector div_rows(_div_rows), mod_rows(_mod_rows);
         SASSERT(!div_rows.empty() || !mod_rows.empty());
-        TRACE("opt", display(tout << "solve_div " << x << "\n"));
+        TRACE("opt", display(tout << "solve_div v" << x << "\n"));
 
         rational K(1);
         for (unsigned ri : div_rows)

src/muz/base/dl_context.cpp

@@ -644,6 +644,12 @@ namespace datalog {
     }
 
     void context::add_table_fact(func_decl * pred, const table_fact & fact) {
+        if (!is_uninterp(pred)) {
+            std::stringstream strm;
+            strm << "Predicate " << pred->get_name() << " when used for facts should be uninterpreted";        
+            throw default_exception(strm.str());
+        }
+        
         if (get_engine() == DATALOG_ENGINE) {
             ensure_engine();
             m_rel->add_fact(pred, fact);

src/muz/base/dl_context.h

@@ -30,7 +30,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/params.h"
 #include "util/trail.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "model/model2expr.h"
 #include "smt/params/smt_params.h"
 #include "muz/base/dl_rule_transformer.h"

src/muz/base/dl_rule.cpp

@@ -41,7 +41,7 @@ Revision History:
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/expr_safe_replace.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "ast/scoped_proof.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/ast_util.h"

src/muz/base/dl_rule.h

@@ -23,8 +23,8 @@ Revision History:
 #include "muz/base/dl_costs.h"
 #include "muz/base/dl_util.h"
 #include "ast/used_vars.h"
-#include "tactic/proof_converter.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/proof_converter.h"
+#include "ast/converters/model_converter.h"
 #include "ast/rewriter/ast_counter.h"
 #include "ast/rewriter/rewriter.h"
 #include "muz/base/hnf.h"

src/muz/base/dl_util.h

@@ -18,13 +18,14 @@ Revision History:
 --*/
 #pragma once
 
+
 #include<vector>
 #include "ast/ast.h"
 #include "util/hashtable.h"
 #include "util/obj_hashtable.h"
 #include "util/uint_set.h"
-#include "tactic/horn_subsume_model_converter.h"
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/horn_subsume_model_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/substitution/substitution.h"
 #include "ast/rewriter/ast_counter.h"
 #include "util/statistics.h"

src/muz/base/hnf.h

@@ -27,7 +27,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/ast.h"
 #include "util/params.h"
 #include "ast/normal_forms/defined_names.h"
-#include "tactic/proof_converter.h"
+#include "ast/converters/proof_converter.h"
  
 class hnf {
     class imp;

src/muz/fp/horn_tactic.cpp

@@ -20,9 +20,9 @@ Revision History:
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "tactic/tactical.h"
-#include "tactic/model_converter.h"
-#include "tactic/proof_converter.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/model_converter.h"
+#include "ast/converters/proof_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "muz/fp/horn_tactic.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"

src/muz/spacer/spacer_manager.cpp

@@ -28,7 +28,7 @@ Revision History:
 #include "ast/expr_abstract.h"
 #include "model/model2expr.h"
 #include "model/model_smt2_pp.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 
 #include "smt/smt_solver.h"
 namespace spacer {

src/muz/transforms/dl_mk_array_blast.h

@@ -22,9 +22,9 @@ Revision History:
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
-#include "tactic/equiv_proof_converter.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
 

src/muz/transforms/dl_mk_bit_blast.cpp

@@ -22,7 +22,7 @@ Revision History:
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
 #include "muz/base/fp_params.hpp"
 #include "ast/scoped_proof.h"

src/muz/transforms/dl_mk_coi_filter.cpp

@@ -21,7 +21,7 @@ Author:
 #include "muz/dataflow/dataflow.h"
 #include "muz/dataflow/reachability.h"
 #include "ast/ast_pp.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "ast/ast_util.h"
 
 namespace datalog {

src/muz/transforms/dl_mk_elim_term_ite.h

@@ -21,7 +21,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
     class mk_elim_term_ite : public rule_transformer::plugin {

src/muz/transforms/dl_mk_subsumption_checker.cpp

@@ -25,7 +25,7 @@ Revision History:
 #include "ast/rewriter/rewriter_def.h"
 #include "muz/transforms/dl_mk_subsumption_checker.h"
 #include "muz/base/fp_params.hpp"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 
 
 namespace datalog {

src/nlsat/tactic/goal2nlsat.h

@@ -24,7 +24,7 @@ Notes:
 #pragma once
 
 #include "nlsat/nlsat_types.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 
 class goal;
 class expr2var;

src/opt/opt_context.cpp

@@ -39,7 +39,7 @@ Notes:
 #include "tactic/arith/card2bv_tactic.h"
 #include "tactic/arith/eq2bv_tactic.h"
 #include "tactic/bv/dt2bv_tactic.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "sat/sat_params.hpp"

src/opt/opt_context.h

@@ -20,7 +20,7 @@ Notes:
 #include "ast/ast.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "tactic/tactic.h"
 #include "qe/qsat.h"
 #include "opt/opt_solver.h"

src/opt/opt_solver.h

@@ -29,7 +29,7 @@ Notes:
 #include "smt/params/smt_params.h"
 #include "smt/smt_types.h"
 #include "smt/theory_opt.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 
 namespace opt {
 

src/opt/sortmax.cpp

@@ -24,7 +24,7 @@ Notes:
 #include "smt/smt_context.h"
 #include "opt/opt_context.h"
 #include "util/sorting_network.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 
 namespace opt {
 

src/params/CMakeLists.txt

@@ -16,6 +16,7 @@ z3_add_component(params
     rewriter_params.pyg
     seq_rewriter_params.pyg
     solver_params.pyg
+    tactic_params.pyg
   EXTRA_REGISTER_MODULE_HEADERS
     context_params.h
 )

src/qe/mbp/mbp_arith.cpp

@@ -421,15 +421,23 @@ namespace mbp {
             mbo.display(tout););
             vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.data(), compute_def);
 
+
             vector<row> rows;
+            u_map<row> def_vars;
             mbo.get_live_rows(rows);
-            rows2fmls(rows, index2expr, fmls);
+            for (row const& r : rows) {
+                if (r.m_type == opt::t_mod)
+                    def_vars.insert(r.m_id, r);
+                else if (r.m_type == opt::t_div)
+                    def_vars.insert(r.m_id, r);
+            }
+            rows2fmls(def_vars, rows, index2expr, fmls);
             TRACE("qe", mbo.display(tout << "mbo result\n");
             for (auto const& d : defs) tout << "def: " << d << "\n";
             tout << fmls << "\n";);
 
             if (compute_def)
-                optdefs2mbpdef(defs, index2expr, real_vars, result);
+                optdefs2mbpdef(def_vars, defs, index2expr, real_vars, result);
             if (m_apply_projection && !apply_projection(eval, result, fmls))
                 return false;
 
@@ -442,7 +450,7 @@ namespace mbp {
             return true;
         }
 
-        void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
+        void optdefs2mbpdef(u_map<row> const& def_vars, vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
             SASSERT(defs.size() == real_vars.size());
             for (unsigned i = 0; i < defs.size(); ++i) {
                 auto const& d = defs[i];
@@ -450,8 +458,12 @@ namespace mbp {
                 bool is_int = a.is_int(x);
                 expr_ref_vector ts(m);
                 expr_ref t(m);
-                for (var const& v : d.m_vars)
-                    ts.push_back(var2expr(index2expr, v));
+                for (var const& v : d.m_vars) {
+                    t = id2expr(def_vars, index2expr, v.m_id);
+                    if (v.m_coeff != 1)
+                        t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
+                    ts.push_back(t);
+                }
                 if (!d.m_coeff.is_zero())
                     ts.push_back(a.mk_numeral(d.m_coeff, is_int));
                 if (ts.empty())
@@ -492,7 +504,8 @@ namespace mbp {
                     t = a.mk_int(mod(r.m_coeff, r.m_mod));
                     return t;
                 }
-                ts.push_back(a.mk_int(r.m_coeff));
+                if (r.m_coeff != 0)
+                    ts.push_back(a.mk_int(r.m_coeff));
                 t = mk_add(ts);
                 t = a.mk_mod(t, a.mk_int(r.m_mod));
                 return t;
@@ -501,7 +514,8 @@ namespace mbp {
                     t = a.mk_int(div(r.m_coeff, r.m_mod));
                     return t;
                 }
-                ts.push_back(a.mk_int(r.m_coeff));
+                if (r.m_coeff != 0)
+                    ts.push_back(a.mk_int(r.m_coeff));
                 t = mk_add(ts);
                 t = a.mk_idiv(t, a.mk_int(r.m_mod));
                 return t;
@@ -513,15 +527,7 @@ namespace mbp {
             }
         }
 
-        void rows2fmls(vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
-
-            u_map<row> def_vars;
-            for (row const& r : rows) {
-                if (r.m_type == opt::t_mod)
-                    def_vars.insert(r.m_id, r);
-                else if (r.m_type == opt::t_div)
-                    def_vars.insert(r.m_id, r);
-            }
+        void rows2fmls(u_map<row>& def_vars, vector<row> const& rows, ptr_vector<expr> const& index2expr, expr_ref_vector& fmls) {
 
             for (row const& r : rows) {
                 expr_ref t(m), s(m), val(m);

src/qe/qsat.h

@@ -21,7 +21,7 @@ Revision History:
 #pragma once
 
 #include "tactic/tactic.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "qe/qe_mbp.h"
 
 namespace qe {

src/sat/sat_cleaner.cpp

@@ -64,9 +64,6 @@ namespace sat {
                     }
                     TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
                     break;
-#if ENABLE_TERNARY
-                case watched::TERNARY:
-#endif
                 case watched::CLAUSE:
                     // skip
                     break;

src/sat/sat_config.cpp

@@ -265,6 +265,7 @@ namespace sat {
         m_xor_gauss_max_matrix_columns = p.xor_gauss_max_matrix_columns();
         m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices();
         m_xor_gauss_force_use_all_matrices = p.xor_gauss_force_use_all_matrices();
+        m_xor_gauss_min_usefulness_cutoff = p.xor_gauss_min_usefulness_cutoff();
         
         sat_simplifier_params ssp(_p);
         m_elim_vars = ssp.elim_vars();

src/sat/sat_config.h

@@ -208,6 +208,12 @@ namespace sat {
         unsigned           m_xor_gauss_max_matrix_columns;
         unsigned           m_xor_gauss_max_num_matrices;
         bool               m_xor_gauss_force_use_all_matrices;
+        double             m_xor_gauss_min_usefulness_cutoff;
+        
+        const bool         m_xor_gauss_doMatrixFind = true;
+        const unsigned     m_xor_gauss_min_clauses = 2;
+        const unsigned     m_xor_gauss_max_clauses = 500000;
+        const unsigned     m_xor_gauss_var_per_cut = 2;
         
 
         config(params_ref const & p);

src/sat/sat_drat.cpp

@@ -445,10 +445,6 @@ namespace sat {
             return false;
         case justification::BINARY:
             return contains(c, j.get_literal());
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            return contains(c, j.get_literal1(), j.get_literal2());
-#endif
         case justification::CLAUSE:
             return contains(s.get_clause(j));
         default:

src/sat/sat_gc.cpp

@@ -178,33 +178,9 @@ namespace sat {
         IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
     }
 
-#if ENABLE_TERNARY
-    bool solver::can_delete3(literal l1, literal l2, literal l3) const {                                                           
-        if (value(l1) == l_true && 
-            value(l2) == l_false && 
-            value(l3) == l_false) {
-            justification const& j = m_justification[l1.var()];
-            if (j.is_ternary_clause()) {
-                watched w1(l2, l3);
-                watched w2(j.get_literal1(), j.get_literal2());
-                return w1 != w2;
-            }
-        }
-        return true;
-    }
-#endif
-
     bool solver::can_delete(clause const & c) const {
         if (c.on_reinit_stack())
             return false;
-#if ENABLE_TERNARY
-        if (c.size() == 3) {
-            return
-                can_delete3(c[0],c[1],c[2]) &&
-                can_delete3(c[1],c[0],c[2]) &&
-                can_delete3(c[2],c[0],c[1]);
-        }
-#endif
         literal l0 = c[0];
         if (value(l0) != l_true)
             return true;

src/sat/sat_integrity_checker.cpp

@@ -26,13 +26,6 @@ namespace sat {
     integrity_checker::integrity_checker(solver const & _s):
         s(_s) {
     }
-
-#if ENABLE_TERNARY
-    // for ternary clauses 
-    static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
-        return wlist.contains(watched(l1, l2));
-    }
-#endif
     
     // for nary clauses
     static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
@@ -65,18 +58,6 @@ namespace sat {
         if (c.frozen())
             return true;
 
-#if ENABLE_TERNARY
-        if (c.size() == 3) {
-            CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
-                   tout << "watch_list:\n";
-                   s.display_watch_list(tout, s.get_wlist(~c[0]));
-                   tout << "\n";);
-            VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
-            VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
-            VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
-            return true;
-        }
-#endif
         {
             if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
                 bool on_prop_stack = false;
@@ -174,13 +155,6 @@ namespace sat {
                        tout << "\n";);
                 VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
                 break;
-#if ENABLE_TERNARY
-            case watched::TERNARY:
-                VERIFY(!s.was_eliminated(w.get_literal1().var()));
-                VERIFY(!s.was_eliminated(w.get_literal2().var()));
-                VERIFY(w.get_literal1().index() < w.get_literal2().index());
-                break;
-#endif
             case watched::CLAUSE:
                 VERIFY(!s.get_clause(w.get_clause_offset()).was_removed());
                 break;

src/sat/sat_justification.h

@@ -22,11 +22,7 @@ namespace sat {
     
     class justification {
     public:
-        enum kind { NONE = 0, BINARY = 1, 
-#if ENABLE_TERNARY
-            TERNARY = 2, 
-#endif 
-            CLAUSE = 3, EXT_JUSTIFICATION = 4};
+        enum kind { NONE = 0, BINARY = 1, CLAUSE = 2, EXT_JUSTIFICATION = 3};
     private:
         unsigned m_level;
         size_t m_val1;
@@ -36,9 +32,7 @@ namespace sat {
     public:
         justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {}
         explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {}
-#if ENABLE_TERNARY
-        justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
-#endif
+
         explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {}
         static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); }
         
@@ -51,12 +45,6 @@ namespace sat {
         bool is_binary_clause() const { return m_val2 == BINARY; }
         literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); }
 
-#if ENABLE_TERNARY
-        bool is_ternary_clause() const { return get_kind() == TERNARY; }
-        literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); }
-        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
-#endif
-
         bool is_clause() const { return m_val2 == CLAUSE; }
         clause_offset get_clause_offset() const { return m_val1; }
         
@@ -73,11 +61,6 @@ namespace sat {
         case justification::BINARY:
             out << "binary " << j.get_literal();
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            out << "ternary " << j.get_literal1() << " " << j.get_literal2();
-            break;
-#endif
         case justification::CLAUSE:
             out << "clause";
             break;

src/sat/sat_lut_finder.cpp

@@ -124,8 +124,8 @@ namespace sat {
     }
 
     bool lut_finder::extract_lut(literal l1, literal l2) {
-        SASSERT(s.is_visited(l1.var()));
-        SASSERT(s.is_visited(l2.var()));
+        SASSERT(s.m_visited.is_visited(l1.var()));
+        SASSERT(s.m_visited.is_visited(l2.var()));
         m_missing.reset();
         unsigned mask = 0;
         for (unsigned i = 0; i < m_vars.size(); ++i) {

src/sat/sat_params.pyg

@@ -135,13 +135,13 @@ def_module_params('sat',
                           # ('xor.allow_elim_vars', BOOL, 'tbd'),
                           # ('xor.var_per_cut', UINT, 'tbd'),
                           # ('xor.force_preserve_xors', BOOL, 'tbd'),
-                          ('xor.gauss.max_matrix_columns', UINT, UINT_MAX, 'tbd'),
-                          ('xor.gauss.max_matrix_rows', UINT,  UINT_MAX, 'The maximum matrix size -- no. of rows'),
-                          ('xor.gauss.min_matrix_rows', UINT,  0, 'The minimum matrix size -- no. of rows'),
-                          ('xor.gauss.max_num_matrices', UINT,  UINT_MAX, 'Maximum number of matrices'),
+                          ('xor.gauss.max_matrix_columns', UINT, 1000, 'tbd'),
+                          ('xor.gauss.max_matrix_rows', UINT,  2000, 'The maximum matrix size -- no. of rows'),
+                          ('xor.gauss.min_matrix_rows', UINT,  3, 'The minimum matrix size -- no. of rows'),
+                          ('xor.gauss.max_num_matrices', UINT,  5, 'Maximum number of matrices'),
                           ('xor.gauss.force_use_all_matrices', BOOL, True, 'tbd'),
                           # ('xor.gauss.autodisable', BOOL, False, 'tbd'),
-                          # ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'),
+                          ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0.2, 'tbd'),
                           # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'),
                           # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'),
                           # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd')

src/sat/sat_proof_trim.cpp

@@ -125,10 +125,6 @@ namespace sat {
                     in_coi |= m_in_coi.contains(lit.index());                
             else if (js.is_binary_clause())
                 in_coi = m_in_coi.contains(js.get_literal().index());
-#if ENABLE_TERNARY
-            else if (js.is_ternary_clause())
-                in_coi = m_in_coi.contains(js.get_literal1().index()) || m_in_coi.contains(js.get_literal2().index());
-#endif
             else
                 UNREACHABLE(); // approach does not work for external justifications
             
@@ -226,12 +222,6 @@ namespace sat {
         case justification::BINARY:
             add_dependency(j.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            add_dependency(j.get_literal1());
-            add_dependency(j.get_literal2());
-            break;
-#endif
         case justification::CLAUSE: 
             for (auto lit : s.get_clause(j))
                 if (s.value(lit) == l_false)
@@ -262,13 +252,6 @@ namespace sat {
             m_clause.push_back(l);
             m_clause.push_back(j.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            m_clause.push_back(l);
-            m_clause.push_back(j.get_literal1());
-            m_clause.push_back(j.get_literal2());
-            break;
-#endif
         case justification::CLAUSE:
             s.get_clause(j).mark_used();
             IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");

src/sat/sat_simplifier.cpp

@@ -271,9 +271,6 @@ namespace sat {
             watch_list::iterator end2   = wlist.end();
             for (; it2 != end2; ++it2) {
                 switch (it2->get_kind()) {
-#if ENABLE_TERNARY
-                case watched::TERNARY:
-#endif
                 case watched::CLAUSE:
                     // consume
                     break;

src/sat/sat_solver.cpp

@@ -454,10 +454,6 @@ namespace sat {
             if (redundant && m_par) 
                 m_par->share_clause(*this, lits[0], lits[1]);
             return nullptr;
-#if ENABLE_TERNARY
-        case 3:
-                return mk_ter_clause(lits, st);
-#endif
         default:
             return mk_nary_clause(num_lits, lits, st);
         }
@@ -551,58 +547,6 @@ namespace sat {
         m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
     }
 
-#if ENABLE_TERNARY
-    clause * solver::mk_ter_clause(literal * lits, sat::status st) {
-        VERIFY(ENABLE_TERNARY);
-        m_stats.m_mk_ter_clause++;
-        clause * r = alloc_clause(3, lits, st.is_redundant());
-        bool reinit = attach_ter_clause(*r, st);
-        if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
-        if (st.is_redundant())
-            m_learned.push_back(r);
-        else
-            m_clauses.push_back(r);
-        for (literal l : *r) {
-            m_touched[l.var()] = m_touch_index;
-        }
-        return r;
-    }
-
-    bool solver::attach_ter_clause(clause & c, sat::status st) {
-        VERIFY(ENABLE_TERNARY);
-        bool reinit = false;
-        if (m_config.m_drat) m_drat.add(c, st);
-        TRACE("sat_verbose", tout << c << "\n";);
-        SASSERT(!c.was_removed());
-        m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
-        m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
-        m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
-        if (!at_base_lvl()) 
-            reinit = propagate_ter_clause(c);        
-        return reinit;
-    }
-
-    bool solver::propagate_ter_clause(clause& c) {
-        bool reinit = false;
-        if (value(c[1]) == l_false && value(c[2]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2]));
-            reinit = !c.is_learned();
-        }
-        else if (value(c[0]) == l_false && value(c[2]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2]));
-            reinit = !c.is_learned();
-        }
-        else if (value(c[0]) == l_false && value(c[1]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1]));
-            reinit = !c.is_learned();
-        }
-        return reinit;
-    }
-#endif
-
     clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_stats.m_mk_clause++;
         clause * r = alloc_clause(num_lits, lits, st.is_redundant());
@@ -669,13 +613,7 @@ namespace sat {
 
     void solver::attach_clause(clause & c, bool & reinit) {
         SASSERT(c.size() > 2);
-        reinit = false;
-#if ENABLE_TERNARY
-        if (ENABLE_TERNARY && c.size() == 3)
-            reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
-        else
-#endif
-            reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
+        reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
     }
 
     void solver::set_learned(clause& c, bool redundant) {
@@ -923,12 +861,6 @@ namespace sat {
     }
 
     void solver::detach_clause(clause& c) {
-#if ENABLE_TERNARY
-        if (c.size() == 3) {
-            detach_ter_clause(c);
-            return;
-        }
-#endif
         detach_nary_clause(c);
     }
 
@@ -938,14 +870,6 @@ namespace sat {
         erase_clause_watch(get_wlist(~c[1]), cls_off);
     }
 
-#if ENABLE_TERNARY
-    void solver::detach_ter_clause(clause & c) {
-        erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
-        erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
-        erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
-    }
-#endif
-
     // -----------------------
     //
     // Basic
@@ -1129,31 +1053,6 @@ namespace sat {
                 *it2 = *it;
                 it2++;
                 break;
-#if ENABLE_TERNARY
-            case watched::TERNARY: {
-                lbool val1, val2;
-                l1 = it->get_literal1();
-                l2 = it->get_literal2();
-                val1 = value(l1);
-                val2 = value(l2);
-                if (val1 == l_false && val2 == l_undef) {
-                    m_stats.m_ter_propagate++;
-                    assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l));
-                }
-                else if (val1 == l_undef && val2 == l_false) {
-                    m_stats.m_ter_propagate++;
-                    assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l));
-                }
-                else if (val1 == l_false && val2 == l_false) {
-                    CONFLICT_CLEANUP();
-                    set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2);
-                    return false;
-                }
-                *it2 = *it;
-                it2++;
-                break;
-            }
-#endif
             case watched::CLAUSE: {
                 if (value(it->get_blocked_literal()) == l_true) {
                     TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
@@ -2540,12 +2439,6 @@ namespace sat {
             case justification::BINARY:
                 process_antecedent(~(js.get_literal()), num_marks);
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                process_antecedent(~(js.get_literal1()), num_marks);
-                process_antecedent(~(js.get_literal2()), num_marks);
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 unsigned i = 0;
@@ -2724,13 +2617,6 @@ namespace sat {
             SASSERT(consequent != null_literal);
             process_antecedent_for_unsat_core(~(js.get_literal()));
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            SASSERT(consequent != null_literal);
-            process_antecedent_for_unsat_core(~(js.get_literal1()));
-            process_antecedent_for_unsat_core(~(js.get_literal2()));
-            break;
-#endif
         case justification::CLAUSE: {
             clause & c = get_clause(js);
             unsigned i = 0;
@@ -2867,12 +2753,6 @@ namespace sat {
         case justification::BINARY:
             level = update_max_level(js.get_literal(), level, unique_max);
             return level;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            level = update_max_level(js.get_literal1(), level, unique_max);
-            level = update_max_level(js.get_literal2(), level, unique_max);
-            return level;
-#endif
         case justification::CLAUSE: 
             for (literal l : get_clause(js)) 
                 level = update_max_level(l, level, unique_max);
@@ -3224,15 +3104,6 @@ namespace sat {
                     return false;
                 }
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                if (!process_antecedent_for_minimization(~(js.get_literal1())) ||
-                    !process_antecedent_for_minimization(~(js.get_literal2()))) {
-                    reset_unmark(old_size);
-                    return false;
-                }
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 unsigned i   = 0;
@@ -3388,12 +3259,6 @@ namespace sat {
             case justification::BINARY:
                 update_lrb_reasoned(js.get_literal());
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                update_lrb_reasoned(js.get_literal1());
-                update_lrb_reasoned(js.get_literal2());
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 for (literal l : c) {
@@ -3463,20 +3328,6 @@ namespace sat {
                         unmark_lit(~l2);
                     }
                 }
-#if ENABLE_TERNARY
-                else if (w.is_ternary_clause()) {
-                    literal l2 = w.get_literal1();
-                    literal l3 = w.get_literal2();
-                    if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) {
-                        // eliminate ~l3 from lemma because we have the clause l \/ l2 \/ l3
-                        unmark_lit(~l3);
-                    }
-                    else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) {
-                        // eliminate ~l2 from lemma because we have the clause l \/ l2 \/ l3
-                        unmark_lit(~l2);
-                    }
-                }
-#endif
                 else {
                     // May miss some binary/ternary clauses, but that is ok.
                     // I sort the watch lists at every simplification round.
@@ -3599,7 +3450,7 @@ namespace sat {
                 mark_visited(cw[j].var());
         }
         for (literal lit : m_lemma)
-            mark_visited(lit.var());
+           mark_visited(lit.var());
 
         auto is_active = [&](bool_var v) {
             return value(v) != l_undef && lvl(v) <= new_lvl;
@@ -3741,17 +3592,6 @@ namespace sat {
             }
             else {
                 clause & c = *(cw.get_clause());
-#if ENABLE_TERNARY
-                if (ENABLE_TERNARY && c.size() == 3) {
-                    if (propagate_ter_clause(c) && !at_base_lvl())
-                        m_clauses_to_reinit[j++] = cw;                
-                    else if (has_variables_to_reinit(c) && !at_base_lvl())
-                        m_clauses_to_reinit[j++] = cw;
-                    else 
-                        c.set_reinit_stack(false);
-                    continue;
-                }
-#endif
                 detach_clause(c);
                 attach_clause(c, reinit);
                 if (reinit && !at_base_lvl()) 
@@ -4018,12 +3858,6 @@ namespace sat {
         case justification::BINARY:
             out << "binary " << js.get_literal() << "@" << lvl(js.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " ";
-            out << js.get_literal2() << "@" << lvl(js.get_literal2());
-            break;
-#endif
         case justification::CLAUSE: {
             out << "(";
             bool first = true;
@@ -4683,24 +4517,14 @@ namespace sat {
             if (!check_domain(lit, ~js.get_literal())) return false;
             s |= m_antecedents.find(js.get_literal().var());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            if (!check_domain(lit, ~js.get_literal1()) ||
-                !check_domain(lit, ~js.get_literal2())) return false;
-            s |= m_antecedents.find(js.get_literal1().var());
-            s |= m_antecedents.find(js.get_literal2().var());
-            break;
-#endif
         case justification::CLAUSE: {
             clause & c = get_clause(js);
             for (literal l : c) {
                 if (l != lit) {
-                    if (check_domain(lit, ~l) && all_found) {
-                        s |= m_antecedents.find(l.var());
-                    }
-                    else {
-                        all_found = false;
-                    }
+                    if (check_domain(lit, ~l) && all_found) 
+                        s |= m_antecedents.find(l.var());                    
+                    else 
+                        all_found = false;                    
                 }
             }
             break;
@@ -4735,12 +4559,11 @@ namespace sat {
 
     bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
         index_set s;
-        if (m_antecedents.contains(lit.var())) {
+        if (m_antecedents.contains(lit.var())) 
             return true;
-        }
-        if (assumptions.contains(lit)) {
-            s.insert(lit.index());
-        }
+        
+        if (assumptions.contains(lit)) 
+            s.insert(lit.index());        
         else {
             if (!extract_assumptions(lit, s)) {
                 SASSERT(!m_todo_antecedents.empty());
@@ -4812,7 +4635,7 @@ namespace sat {
             clause_vector const & cs = *(vs[i]);
             for (clause* cp : cs) {
                 clause & c = *cp;
-                if (ENABLE_TERNARY && c.size() == 3)
+                if (c.size() == 3)
                     num_ter++;
                 else
                     num_cls++;
@@ -4899,22 +4722,4 @@ namespace sat {
         return true;
     }
 
-    void solver::init_ts(unsigned n, svector<unsigned>& v, unsigned& ts) {
-        if (v.empty()) 
-            ts = 0;
-        
-        ts++;
-        if (ts == 0) {
-            ts = 1;
-            v.reset();
-        }
-        while (v.size() < n) 
-            v.push_back(0);        
-    }
-
-    void solver::init_visited() {
-        init_ts(2 * num_vars(), m_visited, m_visited_ts);
-    }
-
-
 };

src/sat/sat_solver.h

@@ -28,6 +28,7 @@ Revision History:
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/scoped_limit_trail.h"
+#include "util/visit_helper.h"
 #include "sat/sat_types.h"
 #include "sat/sat_clause.h"
 #include "sat/sat_watched.h"
@@ -51,6 +52,10 @@ namespace pb {
     class solver;
 };
 
+namespace xr {
+    class solver;
+};
+
 namespace sat {
 
     /**
@@ -176,8 +181,7 @@ namespace sat {
         std::string             m_reason_unknown;
         bool                    m_trim = false;
 
-        svector<unsigned>       m_visited;
-        unsigned                m_visited_ts;
+        visit_helper            m_visited;
 
         struct scope {
             unsigned m_trail_lim;
@@ -221,6 +225,7 @@ namespace sat {
         friend class simplifier;
         friend class scc;
         friend class pb::solver;
+        friend class xr::solver;
         friend class anf_simplifier;
         friend class cut_simplifier;
         friend class parallel;
@@ -307,11 +312,6 @@ namespace sat {
         void mk_bin_clause(literal l1, literal l2, sat::status st);
         void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); }
         bool propagate_bin_clause(literal l1, literal l2);
-#if ENABLE_TERNARY
-        clause * mk_ter_clause(literal * lits, status st);
-        bool attach_ter_clause(clause & c, status st);
-        bool propagate_ter_clause(clause& c);
-#endif
         clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
         bool has_variables_to_reinit(clause const& c) const;
         bool has_variables_to_reinit(literal l1, literal l2) const;
@@ -347,16 +347,16 @@ namespace sat {
         void detach_bin_clause(literal l1, literal l2, bool learned);
         void detach_clause(clause & c);
         void detach_nary_clause(clause & c);
-        void detach_ter_clause(clause & c);
         void push_reinit_stack(clause & c);
         void push_reinit_stack(literal l1, literal l2);
-
-        void init_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
-        void init_visited();
-        void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
+        
+        void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); }
+        bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); }
+        bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); }
+        unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); }
+        void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); }
         void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
-        bool is_visited(bool_var v) const { return is_visited(literal(v, false)); }
-        bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; }
+        void inc_visited(bool_var v) { m_visited.inc_visited(v); }
         bool all_distinct(literal_vector const& lits);
         bool all_distinct(clause const& cl);
 

src/sat/sat_types.h

@@ -34,8 +34,6 @@ class params_ref;
 class reslimit;
 class statistics;
 
-#define ENABLE_TERNARY false
-
 namespace sat {
 #define SAT_VB_LVL 10
 

src/sat/sat_watched.cpp

@@ -71,34 +71,6 @@ namespace sat {
         VERIFY(found);
     }
 
-#if ENABLE_TERNARY
-    void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) {
-        watched w(l1, l2);
-        watch_list::iterator it = wlist.begin(), end = wlist.end();
-        watch_list::iterator it2 = it;
-        bool found = false;
-        for (; it != end; ++it) {
-            if (!found && w == *it) {
-                found = true;
-            }
-            else {
-                *it2 = *it;
-                ++it2;    
-            }    
-        }
-        wlist.set_end(it2);
-#if 0
-        VERIFY(found);
-        for (watched const& w2 : wlist) {
-            if (w2 == w) {
-                std::cout << l1 << " " << l2 << "\n";
-            }
-            //VERIFY(w2 != w);
-        }
-#endif
-    }
-#endif
-
     void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
         watch_list::iterator end = wlist.end();
         for (; it != end; ++it, ++it2) 
@@ -120,11 +92,6 @@ namespace sat {
                 if (w.is_learned())
                     out << "*";
                 break;
-#if ENABLE_TERNARY
-            case watched::TERNARY:
-                out << "(" << w.get_literal1() << " " << w.get_literal2() << ")";
-                break;
-#endif
             case watched::CLAUSE:
                 out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")";
                 break;

src/sat/sat_watched.h

@@ -40,11 +40,7 @@ namespace sat {
     class watched {
     public:
         enum kind {
-            BINARY = 0, 
-#if ENABLE_TERNARY
-            TERNARY,
-#endif
-            CLAUSE, EXT_CONSTRAINT
+            BINARY = 0, CLAUSE, EXT_CONSTRAINT
         };
     private:
         size_t   m_val1;
@@ -59,18 +55,6 @@ namespace sat {
             SASSERT(learned || is_binary_non_learned_clause());
         }
 
-#if ENABLE_TERNARY
-        watched(literal l1, literal l2) {
-            SASSERT(l1 != l2);
-            if (l1.index() > l2.index())
-                std::swap(l1, l2);
-            m_val1 = l1.to_uint();
-            m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2);
-            SASSERT(is_ternary_clause());
-            SASSERT(get_literal1() == l1);
-            SASSERT(get_literal2() == l2);
-        }
-#endif
 
         unsigned val2() const { return m_val2; }
 
@@ -101,11 +85,6 @@ namespace sat {
 
         void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); }
                 
-#if ENABLE_TERNARY
-        bool is_ternary_clause() const { return get_kind() == TERNARY; }
-        literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
-        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
-#endif
 
         bool is_clause() const { return get_kind() == CLAUSE; }
         clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }
@@ -124,21 +103,14 @@ namespace sat {
         bool operator!=(watched const & w) const { return !operator==(w); }
     };
 
-    static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
-#if ENABLE_TERNARY
-    static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
-#endif
-    static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
-    static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
+    static_assert(0 <= watched::BINARY && watched::BINARY <= 2, "");
+    static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 2, "");
+    static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 2, "");
 
     struct watched_lt {
         bool operator()(watched const & w1, watched const & w2) const {
             if (w2.is_binary_clause()) return false;
             if (w1.is_binary_clause()) return true;
-#if ENABLE_TERNARY
-            if (w2.is_ternary_clause()) return false;
-            if (w1.is_ternary_clause()) return true;
-#endif
             return false;
         }
     };
@@ -148,8 +120,6 @@ namespace sat {
     watched* find_binary_watch(watch_list & wlist, literal l);
     watched const* find_binary_watch(watch_list const & wlist, literal l);
     bool erase_clause_watch(watch_list & wlist, clause_offset c);
-    void erase_ternary_watch(watch_list & wlist, literal l1, literal l2);
-    void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned);
 
     class clause_allocator;
     std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext);

src/sat/sat_xor_finder.cpp

@@ -107,7 +107,6 @@ namespace sat {
         m_combination |= (1 << mask); 
     }
 
-
     void xor_finder::add_xor(bool parity, clause& c) {
         DEBUG_CODE(for (clause* cp : m_clauses_to_remove) VERIFY(cp->was_used()););
         m_removed_clauses.append(m_clauses_to_remove);
@@ -122,8 +121,8 @@ namespace sat {
     }
 
     bool xor_finder::extract_xor(bool parity, clause& c, literal l1, literal l2) {
-        SASSERT(s.is_visited(l1.var()));
-        SASSERT(s.is_visited(l2.var()));
+        SASSERT(s.m_visited.is_visited(l1.var()));
+        SASSERT(s.m_visited.is_visited(l2.var()));
         m_missing.reset();
         unsigned mask = 0;
         for (unsigned i = 0; i < c.size(); ++i) {

src/sat/smt/CMakeLists.txt

@@ -46,6 +46,7 @@ z3_add_component(sat_smt
     user_solver.cpp
     xor_matrix_finder.cpp
     xor_solver.cpp
+    xor_gaussian.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast

src/sat/smt/euf_solver.h

@@ -22,7 +22,7 @@ Author:
 #include "ast/ast_util.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "tactic/model_converter.h"
+#include "ast/converters/model_converter.h"
 #include "sat/sat_extension.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"

src/sat/smt/pb_solver.cpp

@@ -690,15 +690,6 @@ namespace pb {
                 inc_coeff(consequent, offset);
                 process_antecedent(js.get_literal(), offset);
                 break;
-#if ENABLE_TERNARY
-            case sat::justification::TERNARY:
-                inc_bound(offset); 
-                SASSERT (consequent != sat::null_literal);
-                inc_coeff(consequent, offset);				
-                process_antecedent(js.get_literal1(), offset);
-                process_antecedent(js.get_literal2(), offset);
-                break;
-#endif
             case sat::justification::CLAUSE: {
                 inc_bound(offset); 
                 sat::clause & c = s().get_clause(js);
@@ -1019,16 +1010,6 @@ namespace pb {
                 inc_coeff(consequent, 1);
                 process_antecedent(js.get_literal());
                 break;
-#if ENABLE_TERNARY
-            case sat::justification::TERNARY:
-                SASSERT(consequent != sat::null_literal);
-                round_to_one(consequent.var());
-                inc_bound(1);
-                inc_coeff(consequent, 1);
-                process_antecedent(js.get_literal1());
-                process_antecedent(js.get_literal2());
-                break;
-#endif
             case sat::justification::CLAUSE: {
                 sat::clause & c = s().get_clause(js);
                 unsigned i = 0;
@@ -3476,15 +3457,6 @@ namespace pb {
             ineq.push(lit, offset);
             ineq.push(js.get_literal(), offset);
             break;
-#if ENABLE_TERNARY
-        case sat::justification::TERNARY:
-            SASSERT(lit != sat::null_literal);
-            ineq.reset(offset);
-            ineq.push(lit, offset);
-            ineq.push(js.get_literal1(), offset);
-            ineq.push(js.get_literal2(), offset);
-            break;
-#endif
         case sat::justification::CLAUSE: {
             ineq.reset(offset);
             sat::clause & c = s().get_clause(js);

src/sat/smt/xor_gaussian.h

@@ -0,0 +1,706 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    xor_gaussian.h
+
+Abstract:
+
+    A roughly 1:1 port of CryptoMiniSAT's gaussian elimination datastructures/algorithms
+
+--*/
+
+#pragma once
+
+#include "sat/smt/euf_solver.h"
+
+#include "util/debug.h"
+#include "util/sat_literal.h"
+#include "util/trace.h"
+
+namespace xr {
+    
+    typedef sat::literal literal;
+    typedef sat::bool_var bool_var;
+    typedef sat::literal_vector literal_vector;
+    typedef sat::bool_var_vector bool_var_vector;
+
+
+    class solver;
+    
+#ifdef _MSC_VER
+    inline int scan_fwd_64b(int64_t value) {
+        unsigned long at;
+        unsigned char ret = _BitScanForward64(&at, value);
+        at++;
+        if (!ret) at = 0;
+        return at;
+    }
+#else
+    inline int scan_fwd_64b(uint64_t value) {
+        return  __builtin_ffsll(value);
+    }
+#endif
+
+    class justification {
+        
+        friend class solver;
+        
+        unsigned matrix_num;
+        unsigned row_num;
+    
+        //XOR
+        justification(const unsigned matrix_num, const unsigned row_num):
+            matrix_num(matrix_num),
+            row_num(row_num) { 
+            SASSERT(matrix_num != -1);
+            SASSERT(row_num != -1);
+        }
+        
+    public:
+        justification() : matrix_num(-1), row_num(-1) {}
+        
+        void deallocate(small_object_allocator& a) { a.deallocate(get_obj_size(), sat::constraint_base::mem2base_ptr(this)); }
+        sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); }
+        static justification& from_index(size_t idx) { 
+            return *reinterpret_cast<justification*>(sat::constraint_base::from_index(idx)->mem());
+        }
+        static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); }
+    
+        unsigned get_matrix_num() const {
+            return matrix_num;
+        }
+    
+        unsigned get_row_num() const {
+            return row_num;
+        }
+    
+        bool isNull() const {
+            return matrix_num == -1;
+        }
+    
+        bool operator==(const justification other) const {
+            return matrix_num == other.matrix_num && row_num == other.row_num;
+        }
+    
+        bool operator!=(const justification other) const {
+            return !(*this == other);
+        }
+    };
+    
+    inline std::ostream& operator<<(std::ostream& os, const justification& pb) {
+        if (!pb.isNull()) {
+            return os << " xor reason, matrix= " << pb.get_matrix_num() << " row: " << pb.get_row_num();
+        }
+        return os << " NULL";
+    }
+    
+    enum class gret : unsigned { confl, prop, nothing_satisfied, nothing_fnewwatch };
+    enum class gauss_res : unsigned { none, confl, prop };
+    
+    struct gauss_watched {
+        gauss_watched(unsigned r, unsigned m) : row_n(r) , matrix_num(m) { }
+    
+        unsigned row_n;        // watch row
+        unsigned matrix_num;   // watch matrix
+    
+        bool operator<(const gauss_watched& other) const {
+            if (matrix_num < other.matrix_num)
+                return true;
+            if (matrix_num > other.matrix_num)
+                return false;
+            return row_n < other.row_n;
+        }
+    };
+    
+    struct gauss_data {
+        bool do_eliminate;                                      // we do elimination when basic variable is invoked
+        unsigned new_resp_var;                                  // do elimination variable
+        unsigned new_resp_row ;                                 // do elimination row
+        sat::justification conflict = sat::justification(0);    // returning conflict
+        gauss_res status;                                       // status
+        unsigned currLevel;                                     // level at which the variable was decided on
+
+        unsigned num_props = 0;                                 // total gauss propagation time for DPLL
+        unsigned num_conflicts = 0;                             // total gauss conflict time for DPLL
+        unsigned disable_checks = 0;
+        bool disabled = false;                                  // decide to do gaussian elimination
+
+        void reset() {
+            do_eliminate = false;
+            status = gauss_res::none;
+        }
+    };
+    
+    struct reason {
+        bool m_must_recalc = true;
+        literal m_propagated = sat::null_literal;
+        unsigned m_ID = 0;
+        literal_vector m_reason;
+    };
+    
+    struct xor_clause {
+        
+        bool m_rhs = false;
+        bool_var_vector m_clash_vars;
+        bool m_detached = false;
+        bool_var_vector m_vars;
+        
+        xor_clause() = default;
+        xor_clause(const xor_clause& c) = default;        
+        xor_clause(xor_clause&& c)  noexcept : m_rhs(c.m_rhs), m_clash_vars(std::move(c.m_clash_vars)), m_detached(c.m_detached), m_vars(std::move(c.m_vars)) { }
+        
+        ~xor_clause() = default;
+        
+        xor_clause& operator=(const xor_clause& c) = default;
+    
+        explicit xor_clause(const unsigned_vector& cl, const bool _rhs, const bool_var_vector& _clash_vars) : m_rhs(_rhs), m_clash_vars(_clash_vars) {
+            for (unsigned i = 0; i < cl.size(); i++) {
+                m_vars.push_back(cl[i]);
+            }
+        }
+    
+        template<typename T>
+        explicit xor_clause(const T& cl, const bool _rhs, const bool_var_vector& _clash_vars) : m_rhs(_rhs), m_clash_vars(_clash_vars) {
+            for (unsigned i = 0; i < cl.size(); i++) {
+                m_vars.push_back(cl[i].var());
+            }
+        }
+    
+        explicit xor_clause(const bool_var_vector& cl, const bool _rhs, const unsigned clash_var) : m_rhs(_rhs) {
+            m_clash_vars.push_back(clash_var);
+            for (unsigned i = 0; i < cl.size(); i++) {
+                m_vars.push_back(cl[i]);
+            }
+        }
+        
+        unsigned_vector::const_iterator begin() const {
+            return m_vars.begin();
+        }
+    
+        unsigned_vector::const_iterator end() const {
+            return m_vars.end();
+        }
+    
+        unsigned_vector::iterator begin() {
+            return m_vars.begin();
+        }
+    
+        unsigned_vector::iterator end() {
+            return m_vars.end();
+        }
+    
+        bool operator<(const xor_clause& other) const {
+            unsigned i = 0;
+            while(i < other.size() && i < size()) {
+                if (other[i] != m_vars[i])
+                    return m_vars[i] < other[i];
+                i++;
+            }
+    
+            if (other.size() != size()) {
+                return size() < other.size();
+            }
+            return false;
+        }
+    
+        const unsigned& operator[](const unsigned at) const {
+            return m_vars[at];
+        }
+    
+        unsigned& operator[](const unsigned at) {
+            return m_vars[at];
+        }
+    
+        void shrink(const unsigned newsize) {
+            m_vars.shrink(newsize);
+        }
+    
+        bool_var_vector& get_vars() {
+            return m_vars;
+        }
+    
+        const bool_var_vector& get_vars() const {
+            return m_vars;
+        }
+    
+        unsigned size() const {
+            return m_vars.size();
+        }
+    
+        bool empty() const {
+            if (!m_vars.empty())
+                return false;
+            if (!m_clash_vars.empty())
+                return false;
+            return !m_rhs;
+        }
+    
+        // add all elements in other.m_clash_vars that are not yet in m_clash_vars:
+        void merge_clash(const xor_clause& other, visit_helper& visited) {
+            visited.init_visited(m_clash_vars.size());
+            for (const bool_var& v: m_clash_vars) {
+                visited.mark_visited(v);
+            }
+    
+            for (const auto& v: other.m_clash_vars) {
+                if (!visited.is_visited(v)) {
+                    visited.mark_visited(v);
+                    m_clash_vars.push_back(v);
+                }
+            }
+        }
+    };
+    
+    inline std::ostream& operator<<(std::ostream& os, const xor_clause& thisXor) {
+        for (unsigned i = 0; i < thisXor.size(); i++) {
+            os << literal(thisXor[i], false);
+    
+            if (i + 1 < thisXor.size())
+                os << " + ";
+        }
+        os << " =  " << std::boolalpha << thisXor.m_rhs << std::noboolalpha;
+    
+        os << " -- clash: ";
+        for (const auto& c: thisXor.m_clash_vars) {
+            os << c + 1 << ", ";
+        }
+    
+        return os;
+    }
+    
+    class PackedRow {
+        
+        friend class PackedMatrix;
+        friend class EGaussian;
+        friend std::ostream& operator<<(std::ostream& os, const PackedRow& m);
+
+        PackedRow(const unsigned _size, int64_t* const _mp) :
+            mp(_mp+1),
+            rhs_internal(*_mp), 
+            size(_size) {}
+       
+           int64_t* __restrict const mp;
+           int64_t& rhs_internal;
+           const int size;
+        
+    public:
+        
+        PackedRow() = delete;
+        
+        PackedRow& operator=(const PackedRow& b) {
+            //start from -1, because that's wher RHS is
+            for (int i = -1; i < size; i++) {
+                *(mp + i) = *(b.mp + i);
+            }
+    
+            return *this;
+        }
+    
+        PackedRow& operator^=(const PackedRow& b) {
+            //start from -1, because that's wher RHS is
+            for (int i = -1; i < size; i++) {
+                *(mp + i) ^= *(b.mp + i);
+            }
+    
+            return *this;
+        }
+        
+        void set_and(const PackedRow& a, const PackedRow& b) {
+            for (int i = 0; i < size; i++) {
+                *(mp + i) = *(a.mp + i) & *(b.mp + i);
+            }
+        }
+    
+        unsigned set_and_until_popcnt_atleast2(const PackedRow& a, const PackedRow& b) {
+            unsigned pop = 0;
+            for (int i = 0; i < size && pop < 2; i++) {
+                *(mp + i) = *(a.mp + i) & *(b.mp + i);
+                pop += get_num_1bits((uint64_t)*(mp + i));
+            }
+    
+            return pop;
+        }
+    
+        void xor_in(const PackedRow& b) {
+            rhs_internal ^= b.rhs_internal;
+            for (int i = 0; i < size; i++) {
+                *(mp + i) ^= *(b.mp + i);
+            }
+        }
+    
+        inline const int64_t& rhs() const {
+            return rhs_internal;
+        }
+    
+        inline int64_t& rhs() {
+            return rhs_internal;
+        }
+    
+        inline bool isZero() const {
+            for (int i = 0; i < size; i++) {
+                if (mp[i]) return false;
+            }
+            return true;
+        }
+    
+        inline void setZero() {
+            memset(mp, 0, sizeof(int64_t)*size);
+        }
+    
+        inline void setOne() {
+            memset(mp, 0xff, sizeof(int64_t)*size);
+        }
+    
+        inline void clearBit(const unsigned i) {
+            mp[i / 64] &= ~(1LL << (i % 64));
+        }
+    
+        inline void setBit(const unsigned i) {
+            mp[i / 64] |= (1LL << (i % 64));
+        }
+    
+        inline void invert_rhs(const bool b = true) {
+            rhs_internal ^= (int)b;
+        }
+    
+        void swapBoth(PackedRow b) {
+            int64_t* __restrict mp1 = mp - 1;
+            int64_t* __restrict mp2 = b.mp - 1;
+    
+            unsigned i = size+1;
+            while(i != 0) {
+                std::swap(*mp1, *mp2);
+                mp1++;
+                mp2++;
+                i--;
+            }
+        }
+    
+        inline bool operator[](const unsigned i) const {
+            return (mp[i / 64] >> (i % 64)) & 1;
+        }
+    
+        template<class T>
+        void set(
+            const T& v,
+            const unsigned_vector& var_to_col,
+            const unsigned num_cols) {
+            SASSERT(size == ((int)num_cols/64) + ((bool)(num_cols % 64)));
+    
+            setZero();
+            for (unsigned i = 0; i != v.size(); i++) {
+                const unsigned toset_var = var_to_col[v[i]];
+                SASSERT(toset_var != UINT32_MAX);
+    
+                setBit(toset_var);
+            }
+    
+            rhs_internal = v.m_rhs;
+        }
+    
+        // using find nonbasic and basic value
+        unsigned find_watchVar(
+            sat::literal_vector& tmp_clause,
+            const unsigned_vector& col_to_var,
+            char_vector &var_has_resp_row,
+            unsigned& non_resp_var);
+    
+        // using find nonbasic value after watch list is enter
+        gret propGause(
+            const unsigned_vector& col_to_var,
+            char_vector &var_has_resp_row,
+            unsigned& new_resp_var,
+            PackedRow& tmp_col,
+            PackedRow& tmp_col2,
+            PackedRow& cols_vals,
+            PackedRow& cols_unset,
+            literal& ret_lit_prop
+        );
+    
+        void get_reason(
+            sat::literal_vector& tmp_clause,
+            const unsigned_vector& col_to_var,
+            PackedRow& cols_vals,
+            PackedRow& tmp_col2,
+            literal prop
+        );
+    
+        unsigned popcnt() const {
+            unsigned ret = 0;
+            for (int i = 0; i < size; i++) {
+                ret += get_num_1bits((uint64_t)mp[i]);
+            }
+            return ret;
+        }
+    };
+    
+    class PackedMatrix {
+    public:
+        PackedMatrix() : mp(nullptr), numRows(0), numCols(0) { }
+    
+        ~PackedMatrix() {
+            #ifdef _WIN32
+            _aligned_free((void*)mp);
+            #else
+            free(mp);
+            #endif
+        }
+    
+        void resize(const unsigned num_rows, unsigned num_cols) {
+            num_cols = num_cols / 64 + (bool)(num_cols % 64);
+            if (numRows * (numCols + 1) < (int)num_rows * ((int)num_cols + 1)) {
+                size_t size = sizeof(int64_t) * num_rows*(num_cols+1);
+                #ifdef _WIN32
+                _aligned_free((void*)mp);
+                mp =  (int64_t*)_aligned_malloc(size, 16);
+                #else
+                free(mp);
+                posix_memalign((void**)&mp, 16,  size);
+                #endif
+            }
+    
+            numRows = num_rows;
+            numCols = num_cols;
+        }
+    
+        void resizeNumRows(const unsigned num_rows) {
+            SASSERT((int)num_rows <= numRows);
+            numRows = num_rows;
+        }
+    
+        PackedMatrix& operator=(const PackedMatrix& b) {
+            if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) {
+                size_t size = sizeof(int64_t) * b.numRows*(b.numCols+1);
+                #ifdef _WIN32
+                _aligned_free((void*)mp);
+                mp =  (int64_t*)_aligned_malloc(size, 16);
+                #else
+                free(mp);
+                posix_memalign((void**)&mp, 16,  size);
+                #endif
+            }
+            numRows = b.numRows;
+            numCols = b.numCols;
+            memcpy(mp, b.mp, sizeof(int)*numRows*(numCols+1));
+    
+            return *this;
+        }
+    
+        inline PackedRow operator[](const unsigned i) {
+            return PackedRow(numCols, mp+i*(numCols+1));
+        }
+    
+        inline PackedRow operator[](const unsigned i) const {
+            return PackedRow(numCols, mp+i*(numCols+1));
+        }
+    
+        class iterator {
+            int64_t* mp;
+            const unsigned numCols;
+            
+            iterator(int64_t* _mp, const unsigned _numCols) : mp(_mp), numCols(_numCols) { }
+                
+        public:
+            friend class PackedMatrix;
+    
+            PackedRow operator*() {
+                return PackedRow(numCols, mp);
+            }
+    
+            iterator& operator++() {
+                mp += (numCols+1);
+                return *this;
+            }
+    
+            iterator operator+(const unsigned num) const {
+                iterator ret(*this);
+                ret.mp += (numCols + 1) * num;
+                return ret;
+            }
+    
+            unsigned operator-(const iterator& b) const {
+                return (unsigned)(mp - b.mp) / (numCols + 1);
+            }
+    
+            void operator+=(const unsigned num) {
+                mp += (numCols + 1) * num;  // add by f4
+            }
+    
+            bool operator!=(const iterator& it) const {
+                return mp != it.mp;
+            }
+    
+            bool operator==(const iterator& it) const {
+                return mp == it.mp;
+            }
+        };
+    
+        inline iterator begin() {
+            return iterator(mp, numCols);
+        }
+    
+        inline iterator end() {
+            return iterator(mp+numRows*(numCols+1), numCols);
+        }
+    
+    private:
+    
+        int64_t *mp;
+        int numRows;
+        int numCols;
+    };
+    
+    class EGaussian {
+    public:
+        EGaussian(
+            solver& solver,
+            const unsigned matrix_no,
+            const vector<xor_clause>& xorclauses
+        );
+        ~EGaussian();
+        bool is_initialized() const;
+    
+        ///returns FALSE in case of conflict
+        bool find_truths(
+            gauss_watched*& i,
+            gauss_watched*& j,
+            const unsigned var,
+            const unsigned row_n,
+            gauss_data& gqd
+        );
+    
+        sat::literal_vector* get_reason(const unsigned row, int& out_ID);
+    
+        // when basic variable is touched , eliminate one col
+        void eliminate_col(
+            unsigned p,
+            gauss_data& gqd
+        );
+        void canceling();
+        bool full_init(bool& created);
+        void update_cols_vals_set(bool force = false);
+        bool must_disable(gauss_data& gqd);
+        void check_invariants();
+        void update_matrix_no(unsigned n);
+        void check_watchlist_sanity();
+        void move_back_xor_clauses();
+    
+        vector<xor_clause> m_xorclauses;
+    
+    private:
+        xr::solver& m_solver;   // original sat solver
+    
+        //Cleanup
+        void clear_gwatches(const unsigned var);
+        void delete_gauss_watch_this_matrix();
+        void delete_gausswatch(const unsigned  row_n);
+    
+        //Invariant checks, debug
+        void check_no_prop_or_unsat_rows();
+        void check_tracked_cols_only_one_set();
+        bool check_row_satisfied(const unsigned row);
+        void check_row_not_in_watch(const unsigned v, const unsigned row_num) const;
+    
+        //Reason generation
+        vector<reason> xor_reasons;
+        sat::literal_vector tmp_clause;
+        unsigned get_max_level(const gauss_data& gqd, const unsigned row_n);
+    
+        //Initialisation
+        void eliminate();
+        void fill_matrix();
+        void select_columnorder();
+        gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc.
+        double get_density();
+    
+        //Helper functions
+        void prop_lit(const gauss_data& gqd, const unsigned row_i, const sat::literal ret_lit_prop);
+        bool inconsistent() const;
+
+        ///////////////
+        // stats
+        ///////////////
+        unsigned find_truth_ret_satisfied_precheck = 0;
+        unsigned find_truth_called_propgause = 0;
+        unsigned find_truth_ret_fnewwatch = 0;
+        unsigned find_truth_ret_confl = 0;
+        unsigned find_truth_ret_satisfied = 0;
+        unsigned find_truth_ret_prop = 0;
+    
+        unsigned elim_called = 0;
+        unsigned elim_xored_rows = 0;
+        unsigned elim_called_propgause = 0;
+        unsigned elim_ret_prop = 0;
+        unsigned elim_ret_confl = 0;
+        unsigned elim_ret_satisfied = 0;
+        unsigned elim_ret_fnewwatch = 0;
+        double before_init_density = 0;
+        double after_init_density = 0;
+        
+        ///////////////
+        // Internal data
+        ///////////////
+        unsigned matrix_no;
+        bool initialized = false;
+        bool cancelled_since_val_update = true;
+        unsigned last_val_update = 0;
+    
+        //Is the clause at this ROW satisfied already?
+        //satisfied_xors[row] tells me that
+        // TODO: Are characters enough?
+        char_vector satisfied_xors;
+    
+        // Someone is responsible for this column if TRUE
+        ///we always WATCH this variable
+        char_vector var_has_resp_row;
+    
+        ///row_to_var_non_resp[ROW] gives VAR it's NOT responsible for
+        ///we always WATCH this variable
+        unsigned_vector row_to_var_non_resp;
+    
+    
+        PackedMatrix mat;
+        svector<char_vector> bdd_matrix; // TODO: we will probably not need it
+        unsigned_vector  var_to_col; ///var->col mapping. Index with VAR
+        unsigned_vector col_to_var; ///col->var mapping. Index with COL
+        unsigned num_rows = 0;
+        unsigned num_cols = 0;
+    
+        //quick lookup
+        PackedRow* cols_vals = nullptr;
+        PackedRow* cols_unset = nullptr;
+        PackedRow* tmp_col = nullptr;
+        PackedRow* tmp_col2 = nullptr;
+        void update_cols_vals_set(const sat::literal lit1);
+    
+        //Data to free (with delete[] x)
+        // TODO: This are always 4 equally sized elements; merge them into one block  
+        svector<int64_t*> tofree;
+    };
+    
+    inline void EGaussian::canceling() {
+        cancelled_since_val_update = true;
+        memset(satisfied_xors.data(), 0, satisfied_xors.size());
+    }
+    
+    inline double EGaussian::get_density() {
+        if (num_rows*num_cols == 0)
+            return 0;
+    
+        unsigned pop = 0;
+        for (const auto& row: mat) {
+            pop += row.popcnt();
+        }
+        return (double)pop/(double)(num_rows*num_cols);
+    }
+    
+    inline void EGaussian::update_matrix_no(unsigned n) {
+        matrix_no = n;
+    }
+    
+    inline bool EGaussian::is_initialized() const {
+        return initialized;
+    }
+}

src/sat/smt/xor_matrix_finder.cpp

@@ -15,6 +15,7 @@ Notes:
 --*/
 
 
+#include "sat/sat_xor_finder.h"
 #include "sat/smt/xor_matrix_finder.h"
 #include "sat/smt/xor_solver.h"
 
@@ -23,8 +24,8 @@ namespace xr {
 
     xor_matrix_finder::xor_matrix_finder(solver& s) : m_xor(s), m_sat(s.s()) { }
         
-    inline bool xor_matrix_finder::belong_same_matrix(const constraint& x) {
-        uint32_t comp_num = -1;
+    inline bool xor_matrix_finder::belong_same_matrix(const xor_clause& x) {
+        unsigned comp_num = -1;
         for (sat::bool_var v : x) {
             if (m_table[v] == l_undef) // Belongs to none, abort
                 return false;            
@@ -39,72 +40,73 @@ namespace xr {
     bool xor_matrix_finder::find_matrices(bool& can_detach) {
 
         SASSERT(!m_sat.inconsistent());
-#if 0
-        SASSERT(m_xor.gmatrices.empty());
+        SASSERT(m_xor.m_gmatrices.empty());
+        
         can_detach = true;
     
         m_table.clear();
-        m_table.resize(m_solver->nVars(), l_undef);
-        m_reverseTable.clear();
-        clash_vars_unused.clear();
+        m_table.resize(m_sat.num_vars(), l_undef);
+        m_reverseTable.reset();
+        clash_vars_unused.reset();
         m_matrix_no = 0;
         
-        XorFinder finder(NULL, solver);
+        for (auto& x: m_xor.m_xorclauses_unused) 
+            m_xor.m_xorclauses.push_back(x);
+        m_xor.m_xorclauses_unused.clear();
+        m_xor.clean_xor_clauses(m_xor.m_xorclauses); 
     
-        for (auto& x: m_solver->xorclauses_unused) 
-            m_xor.xorclauses.push_back(std::move(x));
-        m_xor.xorclauses_unused.clear();
-        m_xor.clauseCleaner->clean_xor_clauses(solver->xorclauses); 
-    
-        finder.grab_mem();
-        finder.move_xors_without_connecting_vars_to_unused();
-        if (!finder.xor_together_xors(m_solver->xorclauses)) 
+        m_xor.move_xors_without_connecting_vars_to_unused();
+        if (!m_xor.xor_together_xors(m_xor.m_xorclauses)) 
             return false;
     
-        finder.move_xors_without_connecting_vars_to_unused();
-        finder.clean_equivalent_xors(m_solver->xorclauses);
-        for (const auto& x: m_xor.xorclauses_unused)
-            clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end());
+        m_xor.move_xors_without_connecting_vars_to_unused();
+        m_xor.clean_equivalent_xors(m_xor.m_xorclauses);
+        for (const auto& c : m_xor.m_xorclauses_unused){
+            for (const auto& v : c) {
+                clash_vars_unused.insert(v);                
+            }
+        }
     
-        if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) {
+        if (m_xor.m_xorclauses.size() < m_sat.get_config().m_xor_gauss_min_clauses) {
             can_detach = false;
             return true;
         }
     
         //Just one giant matrix.
-        // if (m_sat.get_config().m_xor_gauss_do_matrix_find)
-        if (!m_sat.get_config().m_xor_doMatrixFind) {
-            m_xor.gmatrices.push_back(new EGaussian(m_xor, 0, m_xor.xorclauses));
-            m_xor.gqueuedata.resize(m_xor.gmatrices.size());
+        if (!m_sat.get_config().m_xor_gauss_doMatrixFind) {
+            m_xor.m_gmatrices.push_back(alloc(EGaussian, m_xor, 0, m_xor.m_xorclauses));
+            m_xor.m_gqueuedata.resize(m_xor.m_gmatrices.size());
             return true;
         }
     
-        std::vector<uint32_t> newSet;
-        uint_set tomerge;
-        for (const constraint& x : m_xor.m_constraints) {
+        unsigned_vector newSet;
+        unsigned_vector tomerge;
+        for (const xor_clause& x : m_xor.m_xorclauses) {
             if (belong_same_matrix(x))
                 continue;
     
-            tomerge.clear();
+            tomerge.reset();
             newSet.clear();
-            for (uint32_t v : x) {
+            for (unsigned v : x) {
                 if (m_table[v] != l_undef)
-                    tomerge.insert(m_table[v]);
+                    tomerge.push_back(m_table[v]);
                 else
                     newSet.push_back(v);
             }
             if (tomerge.size() == 1) {
-                const uint32_t into = *tomerge.begin();
-                auto intoReverse = m_reverseTable.find(into);
-                for (uint32_t i = 0; i < newSet.size(); i++) {
-                    intoReverse->second.push_back(newSet[i]);
+                const unsigned into = *tomerge.begin();
+                unsigned_vector& intoReverse = m_reverseTable.find(into);
+                for (unsigned i = 0; i < newSet.size(); i++) {
+                    intoReverse.push_back(newSet[i]);
                     m_table[newSet[i]] = into;
                 }
                 continue;
             }
     
-            for (uint32_t v: tomerge) {
-                newSet.insert(newSet.end(), m_reverseTable[v].begin(), m_reverseTable[v].end());
+            for (unsigned v: tomerge) {
+                for (const auto& v2 : m_reverseTable[v]) {
+                    newSet.insert(v2);
+                }
                 m_reverseTable.erase(v);
             }
             for (auto j : newSet)
@@ -115,14 +117,13 @@ namespace xr {
     
         set_matrixes();
 
-#endif        
         return !m_sat.inconsistent();
     }
     
     unsigned xor_matrix_finder::set_matrixes() {
 
         svector<matrix_shape> matrix_shapes;
-        svector<ptr_vector<constraint>> xors_in_matrix(m_matrix_no);
+        vector<vector<xor_clause>> xors_in_matrix(m_matrix_no);
 
         for (unsigned i = 0; i < m_matrix_no; i++) {
             matrix_shapes.push_back(matrix_shape(i));
@@ -130,18 +131,18 @@ namespace xr {
             matrix_shapes[i].m_cols = m_reverseTable[i].size();
         }
 
-        for (constraint* x : m_xor.m_constraints) {
+        for (xor_clause& x : m_xor.m_xorclauses) {
             // take 1st variable to check which matrix it's in.
-            const uint32_t matrix = m_table[(*x)[0]];
+            const unsigned matrix = m_table[x[0]];
             SASSERT(matrix < m_matrix_no);
     
             //for stats
             matrix_shapes[matrix].m_rows ++;
-            matrix_shapes[matrix].m_sum_xor_sizes += x->get_size();
+            matrix_shapes[matrix].m_sum_xor_sizes += x.size();
             xors_in_matrix[matrix].push_back(x);
         }
       
-        m_xor.m_constraints.clear();
+        m_xor.m_xorclauses.clear();
     
         for (auto& m: matrix_shapes) 
             if (m.tot_size() > 0) 
@@ -182,7 +183,7 @@ namespace xr {
                        
             // if already detached, we MUST use the matrix
             for (const auto& x: xors_in_matrix[i]) {
-                if (x->is_detached()) {
+                if (x.m_detached) {
                     use_matrix = true;
                     break;
                 }
@@ -191,23 +192,23 @@ namespace xr {
             if (m_sat.get_config().m_xor_gauss_force_use_all_matrices) 
                 use_matrix = true;            
     
-#if 0
             if (use_matrix) {
-                m_xor.gmatrices.push_back(
+                m_xor.m_gmatrices.push_back(
                     alloc(EGaussian, m_xor, realMatrixNum, xors_in_matrix[i]));
-                m_xor.gqueuedata.resize(m_solver->gmatrices.size());
+                m_xor.m_gqueuedata.resize(m_xor.m_gmatrices.size());
     
                 realMatrixNum++;
-                SASSERT(m_xor.gmatrices.size() == realMatrixNum);
+                SASSERT(m_xor.m_gmatrices.size() == realMatrixNum);
             } 
             else {
                 for (auto& x: xors_in_matrix[i]) {
-                    m_xor.xorclauses_unused.push_back(x);
-                    clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end());
+                    m_xor.m_xorclauses_unused.push_back(x);
+                    for (const auto& v : x.m_clash_vars) {
+                        clash_vars_unused.insert(v);                        
+                    }
                 }
                 unusedMatrix++;
             }
-#endif
         }
         return realMatrixNum;
     }

src/sat/smt/xor_matrix_finder.h

@@ -18,6 +18,7 @@ Abstract:
 #include "util/uint_set.h"
 #include "util/map.h"
 #include "sat/sat_solver.h"
+#include "sat/smt/xor_gaussian.h"
 
 namespace xr {
 
@@ -25,17 +26,16 @@ namespace xr {
     class constraint;
     
     class xor_matrix_finder {
-
-                        
+        
         struct matrix_shape {
             matrix_shape(uint32_t matrix_num) : m_num(matrix_num) {}
         
             matrix_shape() {}
         
-            uint32_t m_num = 0;
-            uint32_t m_rows = 0;
-            uint32_t m_cols = 0;
-            uint32_t m_sum_xor_sizes = 0;
+            unsigned m_num = 0;
+            unsigned m_rows = 0;
+            unsigned m_cols = 0;
+            unsigned m_sum_xor_sizes = 0;
             double m_density = 0;
         
             uint64_t tot_size() const {
@@ -59,7 +59,7 @@ namespace xr {
         
         unsigned set_matrixes();
         
-        inline bool belong_same_matrix(const constraint& x);
+        inline bool belong_same_matrix(const xor_clause& x);
         
     public:
         xor_matrix_finder(solver& solver);

src/sat/smt/xor_solver.cpp

@@ -12,34 +12,207 @@ Abstract:
 
 --*/
 
-
+#include "sat/smt/xor_matrix_finder.h"
 #include "sat/smt/xor_solver.h"
 #include "sat/sat_simplifier_params.hpp"
 #include "sat/sat_xor_finder.h"
 
 namespace xr {
-
-
-    solver::solver(euf::solver& ctx):
+    
+    solver::solver(euf::solver& ctx) :
         solver(ctx.get_manager(), ctx.get_manager().mk_family_id("xor")) {
         m_ctx = &ctx;
     }
 
-    solver::solver(ast_manager& m, euf::theory_id id)
-        : euf::th_solver(m, symbol("xor"), id) {
+    solver::solver(ast_manager& m, euf::theory_id id) : euf::th_solver(m, symbol("xor"), id) { }
+    
+    solver::~solver() {
+        /*for (justification* j : m_justifications) {
+            j->deallocate(m_allocator);
+        }*/
+        clear_gauss_matrices(true);
     }
 
     euf::th_solver* solver::clone(euf::solver& ctx) {
         // and relevant copy internal state
         return alloc(solver, ctx);
     }
+    
+    void solver::add_every_combination_xor(const sat::literal_vector& lits, const bool attach) {
+        unsigned at = 0, num = 0;
+        sat::literal_vector xorlits;
+        m_tmp_xor_clash_vars.clear();
+        sat::literal lastlit_added = sat::null_literal;
+        while (at != lits.size()) {
+            xorlits.clear();
+            for (unsigned last_at = at; at < last_at + s().get_config().m_xor_gauss_var_per_cut && at < lits.size(); at++) {
+                xorlits.push_back(lits[at]);
+            }
+    
+            //Connect to old cut
+            if (lastlit_added != sat::null_literal) {
+                xorlits.push_back(lastlit_added);
+            } else if (at < lits.size()) {
+                xorlits.push_back(lits[at]);
+                at++;
+            }
+    
+            if (at + 1 == lits.size()) {
+                xorlits.push_back(lits[at]);
+                at++;
+            }
+    
+            //New lit to connect to next cut
+            if (at != lits.size()) {
+                const sat::bool_var new_var = m_solver->mk_var();
+                m_tmp_xor_clash_vars.push_back(new_var);
+                const sat::literal to_add = sat::literal(new_var, false);
+                xorlits.push_back(to_add);
+                lastlit_added = to_add;
+            }
+    
+            // TODO: Implement the following function. Unfortunately, it is needed
+            // add_xor_clause_inter_cleaned_cut(xorlits, attach);
+            if (s().inconsistent())
+                break;
+    
+            num++;
+        }
+    }
+    
+    void solver::add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach) {
+        // TODO: make overload in which "lits" ==> svector<sat::bool_var>; however, first implement missing function "add_xor_clause_inter_cleaned_cut"
+        if (s().inconsistent())
+            return;
+        TRACE("xor", tout << "adding xor: " << lits << " rhs: " << rhs << "\n");
+        SASSERT(!attach || m_prop_queue_head == m_prop_queue.size());
+        SASSERT(s().at_search_lvl());
+    
+        sat::literal_vector ps(lits);
+        for (sat::literal& lit: ps) {
+            if (lit.sign()) {
+                rhs ^= true;
+                lit.neg();
+            }
+        }
+        clean_xor_no_prop(ps, rhs);
+    
+        if (ps.size() >= (0x01UL << 28)) 
+            throw default_exception("xor clause too long");
+    
+        if (ps.empty()) {
+            if (rhs)
+                m_solver->set_conflict();
+            return;
+        }
+    
+        if (rhs)
+            ps[0].neg();
+    
+        add_every_combination_xor(ps, attach);
+        if (ps.size() > 2) {
+            m_xor_clauses_updated = true;
+            m_xorclauses.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars));
+            m_xorclauses_orig.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars));
+        }
+    }
 
-    void solver::asserted(sat::literal l) {
-
+    void solver::asserted(sat::literal l) {        
+        TRACE("xor", tout << "asserted: " << l << "\n";);
+        force_push();
+        m_prop_queue.push_back(l);
     }
 
     bool solver::unit_propagate() {
-        return false;
+        if (m_prop_queue_head == m_prop_queue.size())
+            return false;
+        force_push();
+        m_ctx->push(value_trail<unsigned>(m_prop_queue_head));
+        for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
+            sat::literal const p = m_prop_queue[m_prop_queue_head];
+            sat::justification conflict = gauss_jordan_elim(p, m_num_scopes);
+            if (conflict.is_none()) {
+                m_prop_queue_head = m_prop_queue.size();
+                s().set_conflict(conflict);
+            }
+        }
+        return true;
+    }
+    
+    sat::justification solver::gauss_jordan_elim(const sat::literal p, const unsigned currLevel) {
+        if (m_gmatrices.empty()) 
+            return sat::justification(-1);
+        for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
+            if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue;
+            m_gqueuedata[i].reset();
+            m_gmatrices[i]->update_cols_vals_set();
+        }
+        
+        bool confl_in_gauss = false;
+        SASSERT(m_gwatches.size() > p.var());
+        svector<gauss_watched>& ws = m_gwatches[p.var()];
+        gauss_watched* i = ws.begin();
+        gauss_watched* j = i;
+        const gauss_watched* end = ws.end();
+        
+        for (; i != end; i++) {
+            if (m_gqueuedata[i->matrix_num].disabled || !m_gmatrices[i->matrix_num]->is_initialized())
+                continue; //remove watch and continue
+        
+            m_gqueuedata[i->matrix_num].new_resp_var = UINT_MAX;
+            m_gqueuedata[i->matrix_num].new_resp_row = UINT_MAX;
+            m_gqueuedata[i->matrix_num].do_eliminate = false;
+            m_gqueuedata[i->matrix_num].currLevel = currLevel;
+        
+            if (m_gmatrices[i->matrix_num]->find_truths(i, j, p.var(), i->row_n, m_gqueuedata[i->matrix_num])) {
+                continue;
+            } else {
+                confl_in_gauss = true;
+                i++;
+                break;
+            }
+        }
+        
+        for (; i != end; i++) 
+            *j++ = *i;
+        ws.shrink((unsigned)(i - j));
+        
+        for (unsigned g = 0; g < m_gqueuedata.size(); g++) {
+            if (m_gqueuedata[g].disabled || !m_gmatrices[g]->is_initialized())
+                continue;
+        
+            if (m_gqueuedata[g].do_eliminate) {
+                m_gmatrices[g]->eliminate_col(p.var(), m_gqueuedata[g]);
+                confl_in_gauss |= (m_gqueuedata[g].status == gauss_res::confl);
+            }
+        }
+        
+        for (gauss_data& gqd: m_gqueuedata) {
+            if (gqd.disabled) continue;
+        
+            //There was a conflict but this is not that matrix.
+            //Just skip.
+            if (confl_in_gauss && gqd.status != gauss_res::confl) 
+                continue;
+        
+            switch (gqd.status) {
+                case gauss_res::confl:
+                    gqd.num_conflicts++;
+                    return gqd.conflict;
+        
+                case gauss_res::prop:
+                    gqd.num_props++;
+                    break;
+        
+                case gauss_res::none:
+                    //nothing
+                    break;
+        
+                default:
+                    UNREACHABLE();
+            }
+        }
+        return sat::justification(-1);
     }
     
     void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx,
@@ -51,10 +224,44 @@ namespace xr {
         return sat::check_result::CR_DONE;
     }
     
+    // TODO: we should separate this parts from the euf_solver. Other non-euf theories might need it as well
+    // Similar: Attaching "theory_var"s in non-euf/enode cases  
+    void solver::force_push() {
+        for (; m_num_scopes > 0; --m_num_scopes) {
+            push_core();
+        }
+    }
+    
+    void solver::push_core() {
+        m_prop_queue_lim.push_back(m_prop_queue.size());
+        //m_justifications_lim.push_back(m_justifications.size());
+    }
+    
+    void solver::pop_core(unsigned num_scopes) {
+        SASSERT(m_num_scopes == 0);
+        unsigned old_sz = m_prop_queue_lim.size() - num_scopes;
+        m_prop_queue.shrink(m_prop_queue_lim[old_sz]);
+        m_prop_queue_lim.shrink(old_sz);
+        
+        /*old_sz = m_justifications_lim.size() - num_scopes;
+        unsigned lim = m_justifications_lim[old_sz];
+        for (unsigned i = m_justifications.size(); i > lim; i--) {
+            m_justifications[i - 1].destroy(m_allocator);
+        }
+        m_justifications_lim.shrink(old_sz);
+        m_justifications.shrink(old_sz);*/
+    }
+    
     void solver::push() {
+        m_num_scopes++; 
     }
     
     void solver::pop(unsigned n) {
+        unsigned k = std::min(m_num_scopes, n);
+        m_num_scopes -= k;
+        n -= k;
+        if (n > 0)
+            pop_core(n);
     }
 
     // inprocessing
@@ -73,6 +280,463 @@ namespace xr {
         return out;
     }
     
+    bool solver::clean_xor_clauses(vector<xor_clause>& xors) {     
+        SASSERT(!inconsistent());
+        
+        unsigned last_trail = UINT_MAX;
+        while (last_trail != s().trail_size() && !inconsistent()) {
+            last_trail = s().trail_size();
+            unsigned j = 0;
+            for (xor_clause& x : xors) {
+                if (inconsistent()) {
+                    xors[j++] = x;
+                    continue;
+                }
+        
+                const bool keep = clean_one_xor(x);
+                if (keep) {
+                    SASSERT(x.size() > 2);
+                    xors[j++] = x;
+                } 
+                else {
+                    for (const auto& v : x.m_clash_vars) {
+                        m_removed_xorclauses_clash_vars.insert(v);                    
+                    }
+                }
+            }
+            xors.shrink(j);
+            if (inconsistent()) break;
+            s().propagate(false);
+        }
+        
+        return !inconsistent();
+    }
+    
+    
+    bool solver::clean_one_xor(xor_clause& x) {
+    
+        unsigned j = 0;
+        for (auto const& v : x.m_clash_vars)
+            if (s().value(v) == l_undef)
+                x.m_clash_vars[j++] = v;
+        
+        x.m_clash_vars.shrink(j);
+    
+        j = 0;
+        for (auto const& v : x) {
+            if (s().value(v) != l_undef)
+                x.m_rhs  ^= s().value(v) == l_true;
+            else
+                x[j++] = v;
+        }
+        x.shrink(j);
+        SASSERT(!inconsistent());
+        switch (x.size()) {
+            case 0:
+                if (x.m_rhs)
+                    s().set_conflict();
+                /*TODO: Implement
+                if (inconsistent()) {
+                    SASSERT(m_solver.unsat_cl_ID == 0);
+                    m_solver.unsat_cl_ID = solver->clauseID;
+                }*/
+                return false;
+            case 1: {
+                s().assign_scoped(sat::literal(x[0], !x.m_rhs));
+                s().propagate(false);
+                return false;
+            }
+            case 2: {
+                sat::literal_vector vec(x.size());
+                for (const auto& v : x.m_vars)
+                    vec.push_back(sat::literal(v));
+                add_xor_clause(vec, x.m_rhs, true);
+                return false;
+            }
+            default:
+                return true;
+        }
+    }
+    
+    bool solver::clear_gauss_matrices(const bool destruct) {
+        // TODO: Include; ignored for now. Maybe we can ignore the detached clauses
+        /*if (!destruct) {
+            if (!fully_undo_xor_detach()) 
+                return false;
+        }*/
+        m_xor_clauses_updated = true;
+
+        for (EGaussian* g: m_gmatrices) 
+            g->move_back_xor_clauses();
+        for (EGaussian* g: m_gmatrices) 
+            dealloc(g);
+        for (auto& w: m_gwatches) 
+            w.clear();
+
+        m_gmatrices.clear();
+        m_gqueuedata.clear();
+
+        m_xorclauses.clear(); // we rely on xorclauses_orig now
+        m_xorclauses_unused.clear();
+
+        if (!destruct)
+            for (const auto& x: m_xorclauses_orig)
+                m_xorclauses.push_back(x);
+
+        return !s().inconsistent();
+    }
+    
+    bool solver::find_and_init_all_matrices() {
+        if (!m_xor_clauses_updated/* && (!m_detached_xor_clauses || !assump_contains_xor_clash())*/)
+            return true;
+        
+        bool can_detach;
+        if (!clear_gauss_matrices(false)) 
+            return false;
+        
+        xor_matrix_finder mfinder(*this);
+        mfinder.find_matrices(can_detach);
+        if (s().inconsistent()) return false;
+        if (!init_all_matrices()) return false;
+        
+        /* TODO: Make this work (ignored for now)
+        bool ret_no_irred_nonxor_contains_clash_vars;
+        if (can_detach &&
+            s().get_config().m_xor_gauss_detach_reattach &&
+            !s().get_config().autodisable &&
+            (ret_no_irred_nonxor_contains_clash_vars = no_irred_nonxor_contains_clash_vars())) {
+            detach_xor_clauses(mfinder.clash_vars_unused);
+            unset_clash_decision_vars(xorclauses);
+            rebuildOrderHeap();
+        }*/
+        m_xor_clauses_updated = false;
+        return true;
+    }
+    
+    bool solver::init_all_matrices() {
+        SASSERT(!s().inconsistent());
+        SASSERT(s().at_search_lvl());
+        SASSERT(m_gmatrices.size() == m_gqueuedata.size());
+        
+        for (unsigned i = 0; i < m_gmatrices.size(); i++) {
+            auto& g = m_gmatrices[i];
+            bool created = false;
+            if (!g->full_init(created)) 
+                return false;
+            SASSERT(!s().inconsistent());
+    
+            if (!created) {
+                m_gqueuedata[i].disabled = true;
+                memory::deallocate(g);
+                g = nullptr;
+            }
+        }
+    
+        unsigned j = 0;
+        bool modified = false;
+        for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
+            if (m_gmatrices[i] == nullptr) {
+                modified = true;
+                continue;
+            }
+            if (!modified) {
+                j++;
+                continue;
+            }
+            m_gmatrices[j] = m_gmatrices[i];
+            m_gmatrices[j]->update_matrix_no(j);
+            m_gqueuedata[j] = m_gqueuedata[i];
+            
+            for (unsigned var = 0; var < s().num_vars(); var++) {
+                for (gauss_watched& k : m_gwatches[var]) {
+                    if (k.matrix_num == i)
+                        k.matrix_num = j;
+                }
+            }
+            j++;
+        }
+        m_gqueuedata.shrink(j);
+        m_gmatrices.shrink(j);
+        
+        return !s().inconsistent();
+    }
+    
+    bool solver::xor_has_interesting_var(const xor_clause& x) {
+        return std::any_of(x.begin(), x.end(), [&](bool_var v) { return s().num_visited(v) > 1; });
+    }
+    
+    void solver::move_xors_without_connecting_vars_to_unused() {
+        if (m_xorclauses.empty()) 
+            return;
+    
+        vector<xor_clause> cleaned;
+        s().init_visited(2);
+        
+        for(const xor_clause& x: m_xorclauses) {
+            for (unsigned v : x) {
+                s().inc_visited(v);
+            }
+        }
+    
+        //has at least 1 var with occur of 2
+        for(const xor_clause& x: m_xorclauses) {
+            if (xor_has_interesting_var(x) || x.m_detached) {
+                TRACE("xor", tout << "XOR has connecting var: " << x << "\n";);
+                cleaned.push_back(x);
+            } else {
+                TRACE("xor", tout << "XOR has no connecting var: " << x << "\n";);
+                m_xorclauses_unused.push_back(x);
+            }
+        }
+        
+        m_xorclauses = cleaned;
+    }
+    
+    void solver::clean_equivalent_xors(vector<xor_clause>& txors){
+        if (!txors.empty()) {
+            size_t orig_size = txors.size();
+            for (xor_clause& x: txors) {
+                std::sort(x.begin(), x.end());
+            }
+            std::sort(txors.begin(), txors.end());
+    
+            unsigned sz = 1;
+            unsigned j = 0;
+            for (unsigned i = 1; i < txors.size(); i++) {
+                auto& jd = txors[j];
+                auto& id = txors[i];
+                if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) {
+                    jd.merge_clash(id, m_visited);
+                    jd.m_detached |= id.m_detached;
+                } else {
+                    j++;
+                    j = i;
+                    sz++;
+                }
+            }
+            txors.resize(sz);
+        }
+    }
+    
+    sat::justification solver::mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i) {
+        void* mem = m_ctx->get_region().allocate(justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(matrix_no, row_i);
+        return sat::justification::mk_ext_justification(level, constraint->to_index()); 
+    }
+    
+    void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) {
+        std::sort(ps.begin(), ps.end());
+        sat::literal p = sat::null_literal;
+        unsigned i = 0, j = 0;
+        for (; i != ps.size(); i++) {
+            SASSERT(!ps[i].sign());
+            if (ps[i].var() == p.var()) {
+                //added, but easily removed
+                j--;
+                p = sat::null_literal;
+                //Flip rhs if necessary
+                if (s().value(ps[i]) != l_undef) {
+                    rhs ^= s().value(ps[i]) == l_true;
+                }
+            } else if (s().value(ps[i]) == l_undef) {
+                //Add and remember as last one to have been added
+                ps[j++] = p = ps[i];
+            } else {
+                //modify rhs instead of adding
+                rhs ^= s().value(ps[i]) == l_true;
+            }
+        }
+        ps.resize(ps.size() - (i - j));
+    }
+    
+    bool solver::xor_together_xors(vector<xor_clause>& xors) {
+        
+        if (xors.empty())
+            return !s().inconsistent();
+        
+        if (m_occ_cnt.size() != s().num_vars()) {
+            m_occ_cnt.clear();
+            m_occ_cnt.resize(s().num_vars(), 0);
+        }
+    
+        TRACE_CODE( 
+            TRACE("xor", tout << "XOR-ing together XORs. Starting with: " << "\n";);
+            for (const auto& x: xors) {
+                TRACE("xor", tout << "XOR before xor-ing together: " << x << "\n";);
+            };
+        );
+        
+        SASSERT(!s().inconsistent());
+        SASSERT(s().at_search_lvl());
+        const size_t origsize = xors.size();
+    
+        unsigned xored = 0;
+        SASSERT(m_occurrences.empty());
+    #if 0
+        //Link in xors into watchlist
+        for (unsigned i = 0; i < xors.size(); i++) {
+            const xor_clause& x = xors[i];
+            for (bool_var v: x) {
+                if (m_occ_cnt[v] == 0) {
+                    m_occurrences.push_back(v);
+                }
+                m_occ_cnt[v]++;
+    
+                sat::literal l(v, false);
+                SASSERT(s()->watches.size() > l.toInt());
+                m_watches[l].push(Watched(i, WatchType::watch_idx_t));
+                m_watches.smudge(l);
+            }
+        }
+    
+        //Don't XOR together over variables that are in regular clauses
+        s().init_visited();
+        
+        for (unsigned i = 0; i < 2 * s().num_vars(); i++) {
+            const auto& ws = s().get_wlist(i);
+            for (const auto& w: ws) {
+                if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned()) {
+                    sat::bool_var v = w.get_literal().var();
+                    s().mark_visited(v);
+                }
+            }
+        }
+    
+        for (const auto& cl: s().clauses()) {
+            /* TODO: Do we need this? Are the xors still in the clause set?
+            if (cl->red() || cl->used_in_xor()) {
+                continue;
+            }*/
+            // TODO: maybe again instead
+            if (cl->is_learned())
+                continue;
+            for (literal l: *cl)
+                s().mark_visited(l.var());
+        }
+    
+        //until fixedpoint
+        bool changed = true;
+        while (changed) {
+            changed = false;
+            m_interesting.clear();
+            for (const unsigned l : m_occurrences) {
+                if (m_occ_cnt[l] == 2 && !s().is_visited(l)) {
+                    m_interesting.push_back(l);
+                }
+            }
+    
+            while (!m_interesting.empty()) {
+    
+                //Pop and check if it can be XOR-ed together
+                const unsigned v = m_interesting.back();
+                m_interesting.resize(m_interesting.size()-1);
+                if (m_occ_cnt[v] != 2)
+                    continue;
+    
+                unsigned indexes[2];
+                unsigned at = 0;
+                size_t i2 = 0;
+                //SASSERT(watches.size() > literal(v, false).index());
+                vector<sat::watched> ws = s().get_wlist(literal(v, false));
+    
+                //Remove the 2 indexes from the watchlist
+                for (unsigned i = 0; i < ws.size(); i++) {
+                    const sat::watched& w = ws[i];
+                    if (!w.isIdx()) {
+                        ws[i2++] = ws[i];
+                    } else if (!xors[w.get_idx()].empty()) {
+                        SASSERT(at < 2);
+                        indexes[at] = w.get_idx();
+                        at++;
+                    }
+                }
+                SASSERT(at == 2);
+                ws.resize(i2);
+    
+                xor_clause& x0 = xors[indexes[0]];
+                xor_clause& x1 = xors[indexes[1]];
+                unsigned clash_var;
+                unsigned clash_num = xor_two(&x0, &x1, clash_var);
+    
+                //If they are equivalent
+                if (x0.size() == x1.size()
+                    && x0.m_rhs == x1.m_rhs
+                    && clash_num == x0.size()
+                ) {
+                    TRACE("xor", tout 
+                    << "x1: " << x0 << " -- at idx: " << indexes[0] 
+                    << "and  x2: " << x1 << " -- at idx: " << indexes[1] 
+                    << "are equivalent.\n");
+    
+                    //Update clash values & detached values
+                    x1.merge_clash(x0, m_visited);
+                    x1.m_detached |= x0.m_detached;
+    
+                    TRACE("xor", tout << "after merge: " << x1 <<  " -- at idx: " << indexes[1] << "\n";);
+    
+                    x0 = xor_clause();
+    
+                    //Re-attach the other, remove the occur of the one we deleted
+                    s().m_watches[Lit(v, false)].push(Watched(indexes[1], WatchType::watch_idx_t));
+    
+                    for (unsigned v2: x1) {
+                        sat::literal l(v2, false);
+                        SASSERT(m_occ_cnt[l.var()] >= 2);
+                        m_occ_cnt[l.var()]--;
+                        if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) {
+                            m_interesting.push_back(l.var());
+                        }
+                    }
+                } else if (clash_num > 1 || x0.m_detached || x1.m_detached) {
+                    //add back to ws, can't do much
+                    ws.push(Watched(indexes[0], WatchType::watch_idx_t));
+                    ws.push(Watched(indexes[1], WatchType::watch_idx_t));
+                    continue;
+                } else {
+                    m_occ_cnt[v] -= 2;
+                    SASSERT(m_occ_cnt[v] == 0);
+    
+                    xor_clause x_new(m_tmp_vars_xor_two, x0.m_rhs ^ x1.m_rhs, clash_var);
+                    x_new.merge_clash(x0, m_visited);
+                    x_new.merge_clash(x1, m_visited);
+    
+                    TRACE("xor", tout 
+                    << "x1: " << x0 << " -- at idx: " << indexes[0] << "\n" 
+                    << "x2: " << x1 << " -- at idx: " << indexes[1] << "\n"
+                    << "clashed on var: " << clash_var+1 << "\n"
+                    << "final: " << x_new <<  " -- at idx: " << xors.size() << "\n";);
+    
+                    changed = true;
+                    xors.push_back(x_new);
+                    for(uint32_t v2: x_new) {
+                        sat::literal l(v2, false);
+                        s().watches[l].push(Watched(xors.size()-1, WatchType::watch_idx_t));
+                        SASSERT(m_occ_cnt[l.var()] >= 1);
+                        if (m_occ_cnt[l.var()] == 2 && !s().is_visited(l.var())) {
+                            m_interesting.push_back(l.var());
+                        }
+                    }
+                    xors[indexes[0]] = xor_clause();
+                    xors[indexes[1]] = xor_clause();
+                    xored++;
+                }
+            }
+        }
+    
+        //Clear
+        for (const bool_var l : m_occurrences) { 
+            m_occ_cnt[l] = 0;
+        }
+        m_occurrences.clear();
+    
+        clean_occur_from_idx_types_only_smudged();
+        clean_xors_from_empty(xors);
+        #endif
+    
+        return !s().inconsistent();
+    }
+    
     std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const  {
         return out;
     }
@@ -80,6 +744,5 @@ namespace xr {
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
         return out;
     }
-    
 }
 

src/sat/smt/xor_solver.h

@@ -15,178 +15,80 @@ Abstract:
 #pragma once
 
 #include "sat/smt/euf_solver.h"
+#include "sat/smt/xor_gaussian.h"
 
 namespace xr {
-
-    class constraint {
-        unsigned        m_size;
-        bool            m_detached = false;
-        size_t          m_obj_size;
-        bool            m_rhs;
-        sat::bool_var   m_vars[0];
-        
-    public:
-        static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(constraint) + num_lits * sizeof(sat::bool_var)); }
-        
-        constraint(const svector<sat::bool_var>& ids, bool expected_result) : m_size(ids.size()), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) {
-            unsigned i = 0;
-            for (auto v : ids)
-                m_vars[i++] = v;
-        }
-        sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); }
-        void deallocate(small_object_allocator& a) { a.deallocate(m_obj_size, sat::constraint_base::mem2base_ptr(this)); }
-        sat::bool_var operator[](unsigned i) const { return m_vars[i]; }
-        bool is_detached() const { return m_detached; }
-        unsigned get_size() const { return m_size; }
-        bool get_rhs() const { return m_rhs; }
-        sat::bool_var const* begin() const { return m_vars; }
-        sat::bool_var const* end() const { return m_vars + m_size; }
-        std::ostream& display(std::ostream& out) const {
-            bool first = true;
-            for (auto v : *this)
-                out << (first ? "" : " ^ ") << v, first = false;
-            return out << " = " << m_rhs;
-        }
-    };
-
-#if 0
-    class EGaussian {
-    public:
-        EGaussian(
-            solver* solver,
-            const uint32_t matrix_no,
-            const vector<constraint>& xorclauses
-        );
-        ~EGaussian();
-        bool is_initialized() const;
-
-        ///returns FALSE in case of conflict
-        bool find_truths(
-            GaussWatched*& i,
-            GaussWatched*& j,
-            const uint32_t var,
-            const uint32_t row_n,
-            gauss_data& gqd
-        );
-
-        vector<Lit>* get_reason(const uint32_t row, int32_t& out_ID);
-
-        // when basic variable is touched , eliminate one col
-        void eliminate_col(
-            uint32_t p,
-            gauss_data& gqd
-        );
-        void canceling();
-        bool full_init(bool& created);
-        void update_cols_vals_set(bool force = false);
-        void print_matrix_stats(uint32_t verbosity);
-        bool must_disable(gauss_data& gqd);
-        void check_invariants();
-        void update_matrix_no(uint32_t n);
-        void check_watchlist_sanity();
-        uint32_t get_matrix_no();
-        void finalize_frat();
-        void move_back_xor_clauses();
-
-        vector<constraint> xorclauses;
-
-    private:
-        solver* solver;   // orignal sat solver
-
-        //Cleanup
-        void clear_gwatches(const uint32_t var);
-        void delete_gauss_watch_this_matrix();
-        void delete_gausswatch(const uint32_t  row_n);
-
-        //Invariant checks, debug
-        void check_no_prop_or_unsat_rows();
-        void check_tracked_cols_only_one_set();
-        bool check_row_satisfied(const uint32_t row);
-        void print_gwatches(const uint32_t var) const;
-        void check_row_not_in_watch(const uint32_t v, const uint32_t row_num) const;
-
-        //Reason generation
-        vector<XorReason> xor_reasons;
-        vector<Lit> tmp_clause;
-        uint32_t get_max_level(const GaussQData& gqd, const uint32_t row_n);
-
-        //Initialisation
-        void eliminate();
-        void fill_matrix();
-        void select_columnorder();
-        gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc.
-        double get_density();
-
-        //Helper functions
-        void prop_lit(
-            const gauss_data& gqd, const uint32_t row_i, const Lit ret_lit_prop);
-
-        ///////////////
-        // Internal data
-        ///////////////
-        uint32_t matrix_no;
-        bool initialized = false;
-        bool cancelled_since_val_update = true;
-        uint32_t last_val_update = 0;
-
-        //Is the clause at this ROW satisfied already?
-        //satisfied_xors[decision_level][row] tells me that
-        vector<char> satisfied_xors;
-
-        // Someone is responsible for this column if TRUE
-        ///we always WATCH this variable
-        vector<char> var_has_resp_row;
-
-        ///row_to_var_non_resp[ROW] gives VAR it's NOT responsible for
-        ///we always WATCH this variable
-        vector<uint32_t> row_to_var_non_resp;
-
-
-        PackedMatrix mat;
-        vector<vector<char>> bdd_matrix;
-        vector<uint32_t>  var_to_col; ///var->col mapping. Index with VAR
-        vector<uint32_t> col_to_var; ///col->var mapping. Index with COL
-        uint32_t num_rows = 0;
-        uint32_t num_cols = 0;
-
-        //quick lookup
-        PackedRow* cols_vals = NULL;
-        PackedRow* cols_unset = NULL;
-        PackedRow* tmp_col = NULL;
-        PackedRow* tmp_col2 = NULL;
-        void update_cols_vals_set(const Lit lit1);
-
-        //Data to free (with delete[] x)
-        vector<int64_t*> tofree;
-    };
-#endif
+    
+    class solver;
 
     class solver : public euf::th_solver {
         friend class xor_matrix_finder;
+        friend class EGaussian;
 
+        euf::solver*              m_ctx = nullptr;
 
-        euf::solver* m_ctx = nullptr;
+        unsigned                  m_num_scopes = 0;
 
-        ptr_vector<constraint> m_constraints;
+        literal_vector            m_prop_queue;
+        unsigned_vector           m_prop_queue_lim;
+        unsigned                  m_prop_queue_head = 0;
+        // ptr_vector<justification> m_justifications;
+        // unsigned_vector           m_justifications_lim;
 
-//        ptr_vector<EGaussian>       gmatrices;
+        bool_var_vector                m_tmp_xor_clash_vars;
+             
+        vector<xor_clause>             m_xorclauses;
+        vector<xor_clause>             m_xorclauses_orig;
+        vector<xor_clause>             m_xorclauses_unused;
+             
+        bool_var_vector                m_removed_xorclauses_clash_vars;
+        bool                           m_detached_xor_clauses = false;
+        bool                           m_xor_clauses_updated = false;
+        
+        vector<svector<gauss_watched>> m_gwatches;
+        ptr_vector<EGaussian>          m_gmatrices;
+        svector<gauss_data>            m_gqueuedata;
+        
+        visit_helper                   m_visited;
+        
+        // tmp
+        bool_var_vector m_occurrences;
+        // unfortunately, we cannot use generic "m_visited" here, 
+        // as the number of occurrences might be quite high 
+        // and we need the list of occurrences
+        unsigned_vector m_occ_cnt; 
+        bool_var_vector m_interesting;
+        
+        void force_push();
+        void push_core();
+        void pop_core(unsigned num_scopes);
 
+        bool xor_has_interesting_var(const xor_clause& x);
+        
+        void clean_xor_no_prop(sat::literal_vector& ps, bool& rhs);
+        void add_every_combination_xor(const sat::literal_vector& lits, const bool attach);
+        
+        void add_xor_clause(const sat::literal_vector& lits, bool rhs, const bool attach);
+        
+        bool inconsistent() const { return s().inconsistent(); }
+        
     public:
         solver(euf::solver& ctx);
         solver(ast_manager& m, euf::theory_id id);
+        ~solver() override;
         th_solver* clone(euf::solver& ctx) override;
 
-
-        void add_xor(sat::literal_vector const& lits) override { NOT_IMPLEMENTED_YET(); }
-
-
+        void add_xor(const sat::literal_vector& lits) override { 
+            add_xor_clause(lits, true, true);
+        }
+        
         sat::literal internalize(expr* e, bool sign, bool root)  override { UNREACHABLE(); return sat::null_literal; }
 
         void internalize(expr* e) override { UNREACHABLE(); }
-
-
+        
         void asserted(sat::literal l) override;
         bool unit_propagate() override;
+        sat::justification gauss_jordan_elim(const sat::literal p, const unsigned currLevel);
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
 
         void pre_simplify() override;
@@ -195,11 +97,26 @@ namespace xr {
         sat::check_result check() override;
         void push() override;
         void pop(unsigned n) override;
-
+        
+        void init_search() override {
+            find_and_init_all_matrices();
+        }
+        
+        bool clean_xor_clauses(vector<xor_clause>& xors);
+        bool clean_one_xor(xor_clause& x);
+        bool clear_gauss_matrices(const bool destruct);
+        bool find_and_init_all_matrices();
+        bool init_all_matrices();
+        
+        void move_xors_without_connecting_vars_to_unused();
+        void clean_equivalent_xors(vector<xor_clause>& txors);
+        
+        bool xor_together_xors(vector<xor_clause>& xors);
+        
+        sat::justification mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i);
+        
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
-
-    };
-
+};
 }

src/sat/tactic/goal2sat.cpp

@@ -37,7 +37,7 @@ Notes:
 #include "model/model_evaluator.h"
 #include "model/model_v2_pp.h"
 #include "tactic/tactic.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "sat/sat_cut_simplifier.h"
 #include "sat/sat_drat.h"
 #include "sat/tactic/goal2sat.h"

src/sat/tactic/sat2goal.cpp

@@ -37,7 +37,7 @@ Notes:
 #include "model/model_evaluator.h"
 #include "model/model_v2_pp.h"
 #include "tactic/tactic.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "sat/sat_cut_simplifier.h"
 #include "sat/sat_drat.h"
 #include "sat/tactic/sat2goal.h"

src/sat/tactic/sat2goal.h

@@ -31,7 +31,7 @@ Notes:
 #include "tactic/goal.h"
 #include "sat/sat_model_converter.h"
 #include "sat/sat_solver.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "sat/smt/atom2bool_var.h"
 
 class sat2goal {

src/smt/smt_context_pp.cpp

@@ -166,7 +166,7 @@ namespace smt {
         unsigned num = get_num_bool_vars();
         for (unsigned v = 0; v < num; v++) {
             expr * n = m_bool_var2expr[v];
-            ast_def_ll_pp(out, m, n, get_pp_visited(), true, false);
+            ast_def_ll_pp(out << v << " ", m, n, get_pp_visited(), true, false);
         }
     }
 

src/smt/tactic/smt_tactic_core.cpp

@@ -26,7 +26,7 @@ Notes:
 #include "smt/smt_solver.h"
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "solver/solver2tactic.h"
 #include "solver/solver.h"
 #include "solver/mus.h"

src/smt/theory_arith_aux.h

@@ -22,7 +22,7 @@ Revision History:
 #include "smt/theory_arith.h"
 #include "smt/smt_farkas_util.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 
 namespace smt {
 

src/smt/theory_lra.cpp

@@ -43,7 +43,7 @@
 #include "smt/smt_model_generator.h"
 #include "smt/arith_eq_adapter.h"
 #include "util/nat_set.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "util/cancel_eh.h"