Merge 111b82af80 into 40efe27066

src/params/smt_params.cpp

@@ -51,6 +51,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_core_validate = p.core_validate();
     m_sls_enable = p.sls_enable();
     m_sls_parallel = p.sls_parallel();
+    m_finite_set_lattice_refutation = p.finite_set_lattice_refutation();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
     m_up_persist_clauses = p.up_persist_clauses();

src/params/smt_params.h

@@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params,
     symbol           m_proof_log;
     bool             m_sls_enable = false;
     bool             m_sls_parallel = true;
+    bool             m_finite_set_lattice_refutation = true;
 
     // -----------------------------------
     //

src/params/smt_params_helper.pyg

@@ -114,6 +114,7 @@ def_module_params(module_name='smt',
                           ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'),
                           ('array.weak', BOOL, False, 'weak array theory'),
                           ('array.extensional', BOOL, True, 'extensional array theory'),
+                          ('finite_set.lattice_refutation', BOOL, True, 'enable lattice refutation for finite set theory'),
                           ('clause_proof', BOOL, False, 'record a clausal proof'),
                           ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
                           ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),

src/smt/theory_finite_set.cpp

@@ -260,7 +260,8 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_eqs));
             m_find.merge(v1, v2);  // triggers merge_eh, which triggers incremental generation of theory axioms
         }
-        m_lattice_refutation.add_equality(v1, v2);
+        if (ctx.get_fparams().m_finite_set_lattice_refutation)
+            m_lattice_refutation.add_equality(v1, v2);
 
         // Check if Z3 has a boolean variable for it
         TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";);
@@ -287,7 +288,8 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_diseqs));
             m_axioms.extensionality_axiom(e1, e2);
         }
-        m_lattice_refutation.add_disequality(v1,v2);
+        if (ctx.get_fparams().m_finite_set_lattice_refutation)
+            m_lattice_refutation.add_disequality(v1,v2);
     }
 
     //

src/smt/theory_finite_set_lattice_refutation.cpp

@@ -12,7 +12,7 @@ Module Name:
 #include "smt/smt_theory.h"
 #include "smt/theory_finite_set.h"
 #include "smt/smt_context.h"
-#include "iostream"
+#include <iostream>
 
 const int NUM_WORDS = 5;
 // some example have shown, the introduction of large conflict clauses can severely slow down refutation