throttle ackerman on arrays

src/ast/euf/euf_egraph.cpp

@@ -189,10 +189,10 @@ namespace euf {
             add_th_diseq(id, v1, v2, n->get_expr());
             return;
         }
-        for (auto p : euf::enode_th_vars(r1)) {
+        for (auto const& p : euf::enode_th_vars(r1)) {
             if (!th_propagates_diseqs(p.get_id()))
                 continue;
-            for (auto q : euf::enode_th_vars(r2))
+            for (auto const& q : euf::enode_th_vars(r2))
                 if (p.get_id() == q.get_id()) 
                     add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr());
         }
@@ -506,7 +506,7 @@ namespace euf {
 
     void egraph::merge_th_eq(enode* n, enode* root) {
         SASSERT(n != root);
-        for (auto iv : enode_th_vars(n)) {
+        for (auto const& iv : enode_th_vars(n)) {
             theory_id id = iv.get_id();
             theory_var v = root->get_th_var(id);
             if (v == null_theory_var) {                
@@ -789,7 +789,7 @@ namespace euf {
             out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
-            for (auto v : enode_th_vars(n))
+            for (auto const& v : enode_th_vars(n))
                 out << " " << v.get_id() << ":" << v.get_var();
             out << "] ";
         }

src/sat/smt/arith_solver.h

@@ -445,6 +445,7 @@ namespace arith {
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
         bool include_func_interp(func_decl* f) const override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }

src/sat/smt/array_solver.h

@@ -261,6 +261,7 @@ namespace array {
         bool is_shared(theory_var v) const override;
         bool enable_self_propagate() const override { return true; }
         void relevant_eh(euf::enode* n) override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); }
  
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}

src/sat/smt/euf_ackerman.cpp

@@ -99,14 +99,38 @@ namespace euf {
         m_tmp_inference->init(m_tmp_inference);
     }
 
+    bool ackerman::enable_cc(app* a, app* b) {
+        if (!s.enable_ackerman_axioms(a))
+            return false;
+        if (!s.enable_ackerman_axioms(b))
+            return false;
+        for (expr* arg : *a)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        for (expr* arg : *b)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        return true;
+    }
+
+    bool ackerman::enable_eq(expr* a, expr* b, expr* c) {
+        return s.enable_ackerman_axioms(a) && 
+            s.enable_ackerman_axioms(b) && 
+            s.enable_ackerman_axioms(c);           
+    }
+
     void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
         if (!is_app(n1) || !is_app(n2))
             return;
+        if (!s.enable_ackerman_axioms(n1))
+            return;
         SASSERT(!s.m_drating);
         app* a = to_app(n1);
         app* b = to_app(n2);
         if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args())
             return;
+        if (!enable_cc(a, b))
+            return;
         TRACE("ack", tout << "conflict eh: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         insert(a, b);
         gc();
@@ -117,6 +141,8 @@ namespace euf {
             return;
         if (s.m_drating)
             return;
+        if (!enable_eq(a, b, c))
+            return;
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
         insert(a, b, c);
         gc();
@@ -128,6 +154,8 @@ namespace euf {
         TRACE("ack", tout << "used cc: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         SASSERT(a->get_decl() == b->get_decl());
         SASSERT(a->get_num_args() == b->get_num_args());
+        if (!enable_cc(a, b))
+            return;
         insert(a, b);
         gc();
     }

src/sat/smt/euf_ackerman.h

@@ -70,6 +70,9 @@ namespace euf {
         void add_cc(expr* a, expr* b);
         void add_eq(expr* a, expr* b, expr* c);        
         void gc();
+        bool enable_cc(app* a, app* b);
+        bool enable_eq(expr* a, expr* b, expr* c);
+
 
     public:
         ackerman(solver& s, ast_manager& m);

src/sat/smt/euf_solver.cpp

@@ -751,6 +751,18 @@ namespace euf {
         }       
     }
 
+    bool solver::enable_ackerman_axioms(expr* e) const {
+        euf::enode* n = get_enode(e);
+        if (!n)
+            return false;
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && !th->enable_ackerman_axioms(n))
+                return false;
+        }
+        return true;
+    }
+
     void solver::pre_simplify() {
         for (auto* e : m_solvers)
             e->pre_simplify();

src/sat/smt/euf_solver.h

@@ -372,6 +372,7 @@ namespace euf {
         th_rewriter& get_rewriter() { return m_rewriter; }
         void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
+        bool enable_ackerman_axioms(expr* n) const;
 
         // relevancy
         bool m_relevancy_enabled = true;

src/sat/smt/sat_th.h

@@ -111,6 +111,8 @@ namespace euf {
 
         virtual void new_diseq_eh(euf::th_eq const& eq) {}
 
+        virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; }
+
         virtual void relevant_eh(euf::enode* n) {}
 
         /**