expose parameters to control behavior for #5660

src/sat/sat_solver/sat_smt_preprocess.cpp

@@ -46,9 +46,9 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
     smt_params smtp(p);
     if (sp.euf() || sp.smt()) {
         s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
-        s.add_simplifier(alloc(propagate_values, m, p, st));
-        s.add_simplifier(alloc(euf::solve_eqs, m, st));
-        s.add_simplifier(alloc(elim_unconstrained, m, st));
+        if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
+        if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st));
+        if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
         if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
         if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
         if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));

src/sat/smt/euf_solver.cpp

@@ -540,6 +540,7 @@ namespace euf {
     sat::check_result solver::check() { 
         ++m_stats.m_final_checks;
         TRACE("euf", s().display(tout););
+        TRACE("final_check", s().display(tout););
         bool give_up = false;
         bool cont = false;
 

src/sat/smt/q_ematch.cpp

@@ -69,9 +69,12 @@ namespace q {
             [&](euf::enode* n) {
             m_mam->add_node(n, false);
         };
-        ctx.get_egraph().set_on_merge(_on_merge);
-        if (!ctx.relevancy_enabled())
-            ctx.get_egraph().set_on_make(_on_make);
+
+        if (ctx.get_config().m_ematching) {
+            ctx.get_egraph().set_on_merge(_on_merge);
+            if (!ctx.relevancy_enabled())
+                ctx.get_egraph().set_on_make(_on_make);
+        }
         m_mam = mam::mk(ctx, *this);
     }
 

src/smt/params/preprocessor_params.cpp

@@ -26,6 +26,9 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
     m_refine_inj_axiom        = p.refine_inj_axioms();
+    m_propagate_values        = p.propagate_values();
+    m_elim_unconstrained      = p.elim_unconstrained();
+    m_solve_eqs               = p.solve_eqs();
     m_ng_lift_ite             = static_cast<lift_ite_kind>(p.q_lift_ite());
 }
 
@@ -47,6 +50,8 @@ void preprocessor_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_eliminate_term_ite);
     DISPLAY_PARAM(m_macro_finder);
     DISPLAY_PARAM(m_propagate_values);
+    DISPLAY_PARAM(m_solve_eqs);
+    DISPLAY_PARAM(m_elim_unconstrained);
     DISPLAY_PARAM(m_refine_inj_axiom);
     DISPLAY_PARAM(m_eliminate_bounds);
     DISPLAY_PARAM(m_simplify_bit2int);

src/smt/params/preprocessor_params.h

@@ -31,43 +31,29 @@ struct preprocessor_params : public pattern_inference_params,
                              public bit_blaster_params {
     lift_ite_kind   m_lift_ite;
     lift_ite_kind   m_ng_lift_ite;  // lift ite for non ground terms
-    bool            m_pull_cheap_ite;
-    bool            m_pull_nested_quantifiers;
-    bool            m_eliminate_term_ite;
-    bool            m_macro_finder;
-    bool            m_propagate_values;
-    bool            m_refine_inj_axiom;
-    bool            m_eliminate_bounds;
-    bool            m_simplify_bit2int;
-    bool            m_nnf_cnf;
-    bool            m_distribute_forall;
-    bool            m_reduce_args;
-    bool            m_quasi_macros;
-    bool            m_restricted_quasi_macros;
-    bool            m_max_bv_sharing;
-    bool            m_pre_simplifier;
-    bool            m_nlquant_elim;
+    bool            m_pull_cheap_ite = false;
+    bool            m_pull_nested_quantifiers = false;
+    bool            m_eliminate_term_ite = false;
+    bool            m_macro_finder = false;
+    bool            m_propagate_values = true;
+    bool            m_elim_unconstrained = true;
+    bool            m_solve_eqs = true;
+    bool            m_refine_inj_axiom = true;
+    bool            m_eliminate_bounds = false;
+    bool            m_simplify_bit2int = false;
+    bool            m_nnf_cnf = true;
+    bool            m_distribute_forall = false;
+    bool            m_reduce_args = false;
+    bool            m_quasi_macros = false;
+    bool            m_restricted_quasi_macros = false;
+    bool            m_max_bv_sharing = true;
+    bool            m_pre_simplifier = true;
+    bool            m_nlquant_elim = false;
 
 public:
     preprocessor_params(params_ref const & p = params_ref()):
         m_lift_ite(lift_ite_kind::LI_NONE),
-        m_ng_lift_ite(lift_ite_kind::LI_NONE),
-        m_pull_cheap_ite(false),
-        m_pull_nested_quantifiers(false),
-        m_eliminate_term_ite(false),
-        m_macro_finder(false),
-        m_propagate_values(true),
-        m_refine_inj_axiom(true),
-        m_eliminate_bounds(false),
-        m_simplify_bit2int(false),
-        m_nnf_cnf(true),
-        m_distribute_forall(false),
-        m_reduce_args(false),
-        m_quasi_macros(false),
-        m_restricted_quasi_macros(false),
-        m_max_bv_sharing(true),
-        m_pre_simplifier(true),
-        m_nlquant_elim(false) {
+        m_ng_lift_ite(lift_ite_kind::LI_NONE) {
         updt_local_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -18,8 +18,11 @@ def_module_params(module_name='smt',
                           ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
-                          ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
-                          ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
+                          ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'),
+                          ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'),
+                          ('propagate_values', BOOL, True, 'pre-processing: propagate values'),
+                          ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),
+                          ('refine_inj_axioms', BOOL, True, 'pre-processing: refine injectivity axioms'),
 	                  ('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
@@ -50,7 +53,7 @@ def_module_params(module_name='smt',
                           ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
                           ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
                           ('bv.eq_axioms', BOOL, True, 'enable redundant equality axioms for bit-vectors'),
-                          ('bv.size_reduce', BOOL, False, 'turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
+                          ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),