Merge branch 'master' into polysat

src/smt/mam.cpp

@@ -2006,33 +2006,36 @@ namespace {
                 m_backtrack_stack.resize(t->get_num_choices());
         }
 
-        void execute(code_tree * t) {
+        bool execute(code_tree * t) {
             TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
             init(t);
+#define CLEANUP  for (enode* app : t->get_candidates()) if (app->is_marked()) app->unset_mark();
             if (t->filter_candidates()) {
                 for (enode* app : t->get_candidates()) {
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
                     if (!app->is_marked() && app->is_cgr()) {
-                        if (m_context.resource_limits_exceeded() || !execute_core(t, app))
-                            return;
+                        if (m_context.resource_limits_exceeded() || !execute_core(t, app)) {
+                            CLEANUP;
+                            return false;
+                        }
                         app->set_mark();
                     }
                 }
-                for (enode* app : t->get_candidates()) {
-                    if (app->is_marked())
-                        app->unset_mark();
-                }
+                CLEANUP;
+                
             }
             else {
                 for (enode* app : t->get_candidates()) {
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
                     if (app->is_cgr()) {
                         TRACE("trigger_bug", tout << "is_cgr\n";);
+                        // scoped_suspend_rlimit susp(m.limit(), false);
                         if (m_context.resource_limits_exceeded() || !execute_core(t, app))
-                            return;
+                            return false;
                     }
                 }
             }
+            return true;
         }
 
         // init(t) must be invoked before execute_core
@@ -3886,7 +3889,8 @@ namespace {
             TRACE("trigger_bug", tout << "match\n"; display(tout););
             for (code_tree* t : m_to_match) {
                 SASSERT(t->has_candidates());
-                m_interpreter.execute(t);
+                if (!m_interpreter.execute(t))
+                    return;
                 t->reset_candidates();
             }
             m_to_match.reset();

src/smt/params/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(smt_params
     theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     params
+    ast
   PYG_FILES
     smt_params_helper.pyg
 )

src/smt/params/dyn_ack_params.cpp

@@ -29,7 +29,7 @@ void dyn_ack_params::updt_params(params_ref const & _p) {
     m_dack_gc_inv_decay = p.dack_gc_inv_decay();
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void dyn_ack_params::display(std::ostream & out) const {
     DISPLAY_PARAM((unsigned)m_dack);

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());
 }
 
@@ -34,7 +37,7 @@ void preprocessor_params::updt_params(params_ref const & p) {
     updt_local_params(p);
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void preprocessor_params::display(std::ostream & out) const {
     pattern_inference_params::display(out);
@@ -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/qi_params.cpp

@@ -39,7 +39,7 @@ void qi_params::updt_params(params_ref const & _p) {
     m_qi_quick_checker = static_cast<quick_checker_mode>(p.qi_quick_checker());
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void qi_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_qi_cost);

src/smt/params/smt_params.cpp

@@ -64,6 +64,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_axioms2files = sp.axioms2files();
     m_lemmas2console = sp.lemmas2console();
     m_instantiations2console = sp.instantiations2console();
+    m_proof_log = sp.proof_log();
 }
 
 void smt_params::updt_params(params_ref const & p) {
@@ -84,7 +85,7 @@ void smt_params::updt_params(context_params const & p) {
     m_model          = p.m_model;
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void smt_params::display(std::ostream & out) const {
     preprocessor_params::display(out);
@@ -126,6 +127,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_ematching);
     DISPLAY_PARAM(m_induction);
     DISPLAY_PARAM(m_clause_proof);
+    DISPLAY_PARAM(m_proof_log);
 
     DISPLAY_PARAM(m_case_split_strategy);
     DISPLAY_PARAM(m_rel_case_split_order);
@@ -186,3 +188,243 @@ void smt_params::validate_string_solver(symbol const& s) const {
         return;
     throw default_exception("Invalid string solver value. Legal values are z3str3, seq, empty, auto, none");
 }
+
+void smt_params::setup_QF_UF() {
+    m_relevancy_lvl           = 0;
+    m_nnf_cnf                 = false;
+    m_restart_strategy        = RS_LUBY;
+    m_phase_selection         = PS_CACHING_CONSERVATIVE2;
+    m_random_initial_activity = IA_RANDOM;
+}
+
+void smt_params::setup_QF_RDL() {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false;
+    m_arith_propagate_eqs = false;
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_RDL(static_features & st) {
+
+}
+
+void smt_params::setup_QF_IDL() {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false;
+    m_arith_propagate_eqs = false;
+    m_arith_small_lemma_size = 30;
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_IDL(static_features & st) {
+
+}
+
+void smt_params::setup_QF_LRA() {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false;
+    m_arith_propagate_eqs = false;
+    m_eliminate_term_ite  = true;
+    m_nnf_cnf             = false;
+    m_phase_selection     = PS_THEORY;
+}
+
+void smt_params::setup_QF_LRA(static_features const& st) {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false;
+    m_arith_propagate_eqs = false;
+    m_eliminate_term_ite  = true;
+    m_nnf_cnf             = false;
+    if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) {
+        m_relevancy_lvl       = 2;
+        m_relevancy_lemma     = false;
+    }
+    m_phase_selection       = PS_THEORY;
+    if (!st.m_cnf) {
+        m_restart_strategy      = RS_GEOMETRIC;
+        m_arith_stronger_lemmas = false;
+        m_restart_adaptive      = false;
+    }
+    m_arith_small_lemma_size = 32;
+}
+
+void smt_params::setup_QF_LIA() {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false; 
+    m_arith_propagate_eqs = false; 
+    m_nnf_cnf             = false;            
+}
+
+void smt_params::setup_QF_LIA(static_features const& st) {
+    m_relevancy_lvl       = 0;
+    m_arith_eq2ineq       = true;
+    m_arith_reflect       = false; 
+    m_arith_propagate_eqs = false;
+    m_nnf_cnf             = false;
+    if (st.m_max_ite_tree_depth > 50) {
+        m_arith_eq2ineq        = false;
+        m_pull_cheap_ite       = true;
+        m_arith_propagate_eqs  = true;
+        m_relevancy_lvl        = 2; 
+        m_relevancy_lemma      = false;
+    }
+    else if (st.m_num_clauses == st.m_num_units) {
+        m_arith_gcd_test         = false;
+        m_arith_branch_cut_ratio = 4;
+        m_relevancy_lvl          = 2; 
+        m_arith_eq2ineq          = true;
+        m_eliminate_term_ite     = true;
+    } 
+    else {
+        m_eliminate_term_ite   = true;
+        m_restart_adaptive     = false;
+        m_restart_strategy     = RS_GEOMETRIC;
+        m_restart_factor       = 1.5;
+    }
+    if (st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses && st.m_cnf && st.m_arith_k_sum > rational(100000)) {
+        m_arith_bound_prop      = bound_prop_mode::BP_NONE;
+        m_arith_stronger_lemmas = false;
+    }
+}
+
+void smt_params::setup_QF_UFIDL() {
+    m_relevancy_lvl = 0;
+    m_arith_reflect = false;
+    m_nnf_cnf = false;
+    m_arith_eq_bounds = true;
+    m_arith_eq2ineq = true;
+    // m_params.m_phase_selection  = PS_THEORY;
+    m_restart_strategy = RS_GEOMETRIC;
+    m_restart_factor = 1.5;
+    m_restart_adaptive = false;
+}
+
+void smt_params::setup_QF_UFLIA() {
+    m_relevancy_lvl       = 0;
+    m_arith_reflect       = false; 
+    m_nnf_cnf             = false;
+    m_arith_propagation_threshold = 1000;
+}
+
+
+void smt_params::setup_QF_UFLRA() {
+    m_relevancy_lvl       = 0;
+    m_arith_reflect       = false; 
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_BV() {
+    m_relevancy_lvl       = 0;
+    m_arith_reflect       = false; 
+    m_bv_cc               = false;
+    m_bb_ext_gates        = true;
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_AUFBV() {
+    m_array_mode          = AR_SIMPLE;
+    m_relevancy_lvl       = 0;
+    m_bv_cc               = false;
+    m_bb_ext_gates        = true;
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_AX() {
+    m_array_mode          = AR_SIMPLE;
+    m_nnf_cnf             = false;
+}
+
+void smt_params::setup_QF_AX(static_features const& st) {
+    m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
+    m_nnf_cnf             = false;
+    if (st.m_num_clauses == st.m_num_units) {
+        m_relevancy_lvl       = 0;
+        m_phase_selection     = PS_ALWAYS_FALSE;
+    }
+    else 
+        m_relevancy_lvl       = 2;
+}
+
+void smt_params::setup_QF_AUFLIA() {
+    m_array_mode          = AR_SIMPLE;
+    m_nnf_cnf             = false;
+    m_relevancy_lvl       = 2;
+    m_restart_strategy    = RS_GEOMETRIC;
+    m_restart_factor      = 1.5;
+    m_phase_selection     = PS_CACHING_CONSERVATIVE2;
+}
+
+void smt_params::setup_QF_AUFLIA(static_features const& st) {
+    m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
+    if (st.m_has_real)
+        throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
+    m_nnf_cnf             = false;
+    if (st.m_num_clauses == st.m_num_units) {
+        TRACE("QF_AUFLIA", tout << "using relevancy: 0\n";);
+        m_relevancy_lvl       = 0;
+        m_phase_selection     = PS_ALWAYS_FALSE;
+    }
+    else {
+        m_relevancy_lvl           = 0; // it was 2, for some reason 2 doesn't work anymore TODO: investigate
+        m_restart_strategy        = RS_GEOMETRIC;
+        m_restart_factor          = 1.5;
+        m_phase_selection         = PS_CACHING_CONSERVATIVE2;
+        m_random_initial_activity = IA_ZERO;
+    }    
+}
+
+void smt_params::setup_AUFLIA(bool simple_array) {
+    m_array_mode              = simple_array ? AR_SIMPLE : AR_FULL;
+    m_pi_use_database         = true;
+    m_phase_selection         = PS_ALWAYS_FALSE;
+    m_restart_strategy        = RS_GEOMETRIC;
+    m_restart_factor          = 1.5;
+    m_eliminate_bounds        = true;
+    m_qi_quick_checker        = MC_UNSAT;
+    m_qi_lazy_threshold       = 20;
+    m_mbqi                    = true; // enabling MBQI and MACRO_FINDER by default :-)
+    
+    // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general)
+    // It destroys the existing patterns.
+    // m_macro_finder            = true; 
+    
+    if (m_ng_lift_ite == lift_ite_kind::LI_NONE)
+        m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
+}
+
+void smt_params::setup_AUFLIA(static_features const & st) {
+    m_qi_eager_threshold      = st.m_num_quantifiers_with_patterns == 0 ? 5 : 7;
+}
+
+void smt_params::setup_AUFLIRA(bool simple_array) {
+    m_array_mode              = simple_array ? AR_SIMPLE : AR_FULL;
+    m_phase_selection         = PS_ALWAYS_FALSE;
+    m_eliminate_bounds        = true;
+    m_qi_quick_checker        = MC_UNSAT;
+    m_qi_eager_threshold      = 5;
+    // Added for MBQI release
+    m_qi_lazy_threshold       = 20;
+    // 
+    m_macro_finder            = true;
+    if (m_ng_lift_ite == lift_ite_kind::LI_NONE)
+        m_ng_lift_ite         = lift_ite_kind::LI_CONSERVATIVE;
+    m_pi_max_multi_patterns   = 10; //<< it was used for SMT-COMP
+    m_array_lazy_ieq          = true;
+    m_array_lazy_ieq_delay    = 4;
+    //
+    m_mbqi                    = true; // enabling MBQI by default :-)
+    // 
+}
+
+void smt_params::setup_LRA() {
+    m_relevancy_lvl       = 0;
+    m_arith_reflect       = false;
+    m_arith_propagate_eqs = false;
+    m_eliminate_term_ite  = true;
+}
+

src/smt/params/smt_params.h

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include "ast/static_features.h"
 #include "smt/params/dyn_ack_params.h"
 #include "smt/params/qi_params.h"
 #include "smt/params/theory_arith_params.h"
@@ -112,6 +113,7 @@ struct smt_params : public preprocessor_params,
     bool             m_ematching = true;
     bool             m_induction = false;
     bool             m_clause_proof = false;
+    symbol           m_proof_log;
 
     // -----------------------------------
     //
@@ -253,6 +255,51 @@ struct smt_params : public preprocessor_params,
     void display(std::ostream & out) const;
 
     void validate_string_solver(symbol const& s) const;
+
+    void setup_QF_UF();
+
+    void setup_QF_RDL();
+
+    void setup_QF_RDL(static_features & st);
+
+    void setup_QF_IDL();
+
+    void setup_QF_IDL(static_features & st);
+
+    void setup_QF_LRA();
+
+    void setup_QF_LRA(static_features const& st);
+
+    void setup_QF_LIA();
+
+    void setup_QF_LIA(static_features const& st);
+
+    void setup_QF_UFIDL();
+
+    void setup_QF_UFLIA();
+
+    void setup_QF_UFLRA();
+
+    void setup_QF_BV();
+
+    void setup_QF_AUFBV();
+
+    void setup_QF_AX();
+
+    void setup_QF_AX(static_features const& st);
+
+    void setup_QF_AUFLIA();
+
+    void setup_QF_AUFLIA(static_features const& st);
+
+    void setup_AUFLIA(bool simple_array);
+
+    void setup_AUFLIA(static_features const & st);
+
+    void setup_AUFLIRA(bool simple_array);
+
+    void setup_LRA();
+            
 };
 
 

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.'),
@@ -51,7 +54,7 @@ def_module_params(module_name='smt',
                           ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'),
 			  ('bv.polysat', BOOL, True, 'use polysat bit-vector solver'),
                           ('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'),

src/smt/params/theory_arith_params.cpp

@@ -42,7 +42,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
 }
 
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_arith_eq2ineq);

src/smt/params/theory_array_params.cpp

@@ -25,7 +25,7 @@ void theory_array_params::updt_params(params_ref const & _p) {
     m_array_extensional = p.array_extensional();
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void theory_array_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_array_mode);

src/smt/params/theory_bv_params.cpp

@@ -32,7 +32,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
     m_bv_size_reduce = p.bv_size_reduce();
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void theory_bv_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_bv_mode);

src/smt/params/theory_datatype_params.h

@@ -32,7 +32,7 @@ struct theory_datatype_params {
         m_dt_lazy_splits = p.dt_lazy_splits(); 
     }
 
-    void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
+    void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << '\n'; }
 };
 
 

src/smt/params/theory_pb_params.cpp

@@ -25,7 +25,7 @@ void theory_pb_params::updt_params(params_ref const & _p) {
     m_pb_learn_complements = p.pb_learn_complements();
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void theory_pb_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pb_conflict_frequency);

src/smt/params/theory_str_params.cpp

@@ -37,7 +37,7 @@ void theory_str_params::updt_params(params_ref const & _p) {
     m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex();
 }
 
-#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
+#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void theory_str_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_StrongArrangements);

src/smt/qi_queue.cpp

@@ -304,6 +304,20 @@ namespace smt {
             }
             m_instances.push_back(pr1);
         }
+        else if (m_context.clause_proof_active()) {
+            expr_ref_vector bindings_e(m), args(m);
+            arith_util a(m);
+            expr_ref gen(a.mk_int(generation), m);
+            expr* gens[1] = { gen.get() };
+            for (unsigned i = 0; i < num_bindings; ++i) 
+                bindings_e.push_back(bindings[i]->get_expr());
+            args.push_back(q);
+            args.push_back(mk_not(m, instance));
+            args.push_back(m.mk_app(symbol("bind"), num_bindings, bindings_e.data(), m.mk_proof_sort()));
+            args.push_back(m.mk_app(symbol("gen"), 1, gens, m.mk_proof_sort()));
+            pr1 = m.mk_app(symbol("inst"), args.size(), args.data(), m.mk_proof_sort());
+            m_instances.push_back(pr1);            
+        }
         TRACE("qi_queue", tout << mk_pp(lemma, m) << "\n#" << lemma->get_id() << ":=\n" << mk_ll_pp(lemma, m););
         m_stats.m_num_instances++;
         unsigned gen = get_new_gen(q, generation, ent.m_cost);

src/smt/smt_clause_proof.cpp

@@ -16,9 +16,32 @@ Revision History:
 #include "smt/smt_context.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include <iostream>
 
 namespace smt {
-    clause_proof::clause_proof(context& ctx): ctx(ctx), m(ctx.get_manager()), m_lits(m) {}
+    
+    clause_proof::clause_proof(context& ctx):
+        ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m),
+        m_assumption(m), m_rup(m), m_del(m), m_smt(m) {
+        
+        auto proof_log = ctx.get_fparams().m_proof_log;
+        m_has_log = proof_log.is_non_empty_string();
+        m_enabled = ctx.get_fparams().m_clause_proof || m_has_log;        
+    }
+
+    void clause_proof::init_pp_out() {
+        if (m_has_log && !m_pp_out) {
+            static unsigned id = 0;
+            auto proof_log = ctx.get_fparams().m_proof_log;
+            std::string log_name = proof_log.str();
+            if (id > 0)
+                log_name = std::to_string(id) + log_name;
+            ++id;
+            m_pp_out = alloc(std::ofstream, log_name);
+            if (!*m_pp_out)
+                throw default_exception(std::string("Could not open file ") + proof_log.str());
+        }
+    }
 
     clause_proof::status clause_proof::kind2st(clause_kind k) {
         switch (k) {
@@ -36,119 +59,210 @@ namespace smt {
         }
     }
 
-    proof* clause_proof::justification2proof(justification* j) {
-        return (m.proofs_enabled() && j) ? j->mk_proof(ctx.get_cr()) : nullptr;
+    proof_ref clause_proof::justification2proof(status st, justification* j) {
+        proof* r = nullptr;
+        if (j)
+            r = j->mk_proof(ctx.get_cr());
+        if (r) 
+            return proof_ref(r, m);
+        if (!is_enabled())
+            return proof_ref(m);
+        switch (st) {
+        case status::assumption:
+            if (!m_assumption) 
+                m_assumption = m.mk_const("assumption", m.mk_proof_sort());
+            return m_assumption;
+        case status::lemma:
+            if (!m_rup)
+                m_rup = m.mk_const("rup", m.mk_proof_sort());
+            return m_rup;
+        case status::th_lemma:
+        case status::th_assumption:
+            if (!m_smt)
+                m_smt = m.mk_const("smt", m.mk_proof_sort());
+            return m_smt;
+        case status::deleted:
+            if (!m_del)
+                m_del = m.mk_const("del", m.mk_proof_sort());
+            return m_del;
+        }
+        UNREACHABLE();
+        return proof_ref(m);
     }
 
     void clause_proof::add(clause& c) {
-        if (ctx.get_fparams().m_clause_proof) {  
-            justification* j = c.get_justification();
-            proof_ref pr(justification2proof(j), m);
-            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-            update(c, kind2st(c.get_kind()), pr);
-        }
+        if (!is_enabled())
+            return;
+        justification* j = c.get_justification();
+        auto st = kind2st(c.get_kind());
+        auto pr = justification2proof(st, j);
+        CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
+        update(c, st, pr);        
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
-        if (ctx.get_fparams().m_clause_proof) {              
-            proof_ref pr(justification2proof(j), m);
-            CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-            m_lits.reset();
-            for (unsigned i = 0; i < n; ++i) {
-                m_lits.push_back(ctx.literal2expr(lits[i]));
-            }
-            update(kind2st(k), m_lits, pr);
-        }
+        if (!is_enabled())
+            return;
+        auto st = kind2st(k);
+        auto pr = justification2proof(st, j);
+        CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
+        m_lits.reset();
+        for (unsigned i = 0; i < n; ++i) 
+            m_lits.push_back(ctx.literal2expr(lits[i]));
+        update(st, m_lits, pr);
     }
 
 
     void clause_proof::shrink(clause& c, unsigned new_size) {
-        if (ctx.get_fparams().m_clause_proof) {            
-            m_lits.reset();
-            for (unsigned i = 0; i < new_size; ++i) {
-                m_lits.push_back(ctx.literal2expr(c[i]));
-            }
-            update(status::lemma, m_lits, nullptr);
-            for (unsigned i = new_size; i < c.get_num_literals(); ++i) {
-                m_lits.push_back(ctx.literal2expr(c[i]));
-            }
-            update(status::deleted, m_lits, nullptr);
-        }
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        for (unsigned i = 0; i < new_size; ++i) 
+            m_lits.push_back(ctx.literal2expr(c[i]));
+        auto p = justification2proof(status::lemma, nullptr);
+        update(status::lemma, m_lits, p);
+        for (unsigned i = new_size; i < c.get_num_literals(); ++i) 
+            m_lits.push_back(ctx.literal2expr(c[i]));
+        p = justification2proof(status::deleted, nullptr);
+        update(status::deleted, m_lits, p);
     }
 
     void clause_proof::add(literal lit, clause_kind k, justification* j) {
-        if (ctx.get_fparams().m_clause_proof) {
-            m_lits.reset();
-            m_lits.push_back(ctx.literal2expr(lit));
-            proof* pr = justification2proof(j);
-            update(kind2st(k), m_lits, pr);
-        }
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        m_lits.push_back(ctx.literal2expr(lit));
+        auto st = kind2st(k);
+        auto pr = justification2proof(st, j);
+        update(st, m_lits, pr);
     }
 
     void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
-        if (ctx.get_fparams().m_clause_proof) {
-            m_lits.reset();
-            m_lits.push_back(ctx.literal2expr(lit1));
-            m_lits.push_back(ctx.literal2expr(lit2));
-            proof* pr = justification2proof(j);
-            m_trail.push_back(info(kind2st(k), m_lits, pr));
-        }
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        m_lits.push_back(ctx.literal2expr(lit1));
+        m_lits.push_back(ctx.literal2expr(lit2));
+        auto st = kind2st(k);
+        auto pr = justification2proof(st, j);
+        update(st, m_lits, pr);
     }
 
+    void clause_proof::propagate(literal lit, justification const& jst, literal_vector const& ante) {
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        for (literal l : ante)
+            m_lits.push_back(ctx.literal2expr(~l));
+        m_lits.push_back(ctx.literal2expr(lit));
+        proof_ref pr(m.mk_app(symbol("smt"), 0, nullptr, m.mk_proof_sort()), m);
+        update(clause_proof::status::th_lemma, m_lits, pr);
+    }
 
     void clause_proof::del(clause& c) {
-        update(c, status::deleted, nullptr);
+        update(c, status::deleted, justification2proof(status::deleted, nullptr));
+    }
+
+    std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
+        for (expr* e : v)
+            if (m.is_not(e, e))                
+                m_pp.display_expr_def(out << " (not ", e) << ")";
+            else
+                m_pp.display_expr_def(out << " ", e);
+        return out;
+    }
+
+    std::ostream& clause_proof::display_hint(std::ostream& out, proof* p) {
+        if (p)
+            m_pp.display_expr_def(out << " ", p);
+        return out;
+    }
+
+    void clause_proof::declare(std::ostream& out, expr* e) {
+        m_pp.collect(e);
+        m_pp.display_decls(out);
+        m.is_not(e, e);
+        m_pp.define_expr(out, e);
     }
 
     void clause_proof::update(status st, expr_ref_vector& v, proof* p) {
         TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";);
-        IF_VERBOSE(3, verbose_stream() << st << " " << v << "\n");
-        m_trail.push_back(info(st, v, p));
+        if (ctx.get_fparams().m_clause_proof)
+            m_trail.push_back(info(st, v, p));
+        if (m_on_clause_eh) 
+            m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data());        
+        if (m_has_log) {
+            init_pp_out();
+            auto& out = *m_pp_out;
+            for (auto* e : v)
+                declare(out, e);
+            switch (st) {
+            case clause_proof::status::assumption:
+                if (!p || p->get_decl()->get_name() == "assumption") {
+                    display_literals(out << "(assume", v) << ")\n";
+                    break;
+                }
+                Z3_fallthrough;
+            case clause_proof::status::lemma:
+            case clause_proof::status::th_lemma:
+            case clause_proof::status::th_assumption:
+                if (p)
+                    declare(out, p);
+                display_hint(display_literals(out << "(infer", v), p) << ")\n";
+                break;
+            case clause_proof::status::deleted:
+                display_literals(out << "(del", v) << ")\n";
+                break;
+            default:
+                UNREACHABLE();
+            }
+            out.flush();
+        }
     }
 
     void clause_proof::update(clause& c, status st, proof* p) {
-        if (ctx.get_fparams().m_clause_proof) {
-            m_lits.reset();
-            for (literal lit : c) {
-                m_lits.push_back(ctx.literal2expr(lit));
-            }
-            update(st, m_lits, p);
-        }
+        if (!is_enabled())
+            return;
+        m_lits.reset();
+        for (literal lit : c) 
+            m_lits.push_back(ctx.literal2expr(lit));        
+        update(st, m_lits, p);        
     }
 
     proof_ref clause_proof::get_proof(bool inconsistent) {
         TRACE("context", tout << "get-proof " << ctx.get_fparams().m_clause_proof << "\n";);
-        if (!ctx.get_fparams().m_clause_proof) {
+        if (!ctx.get_fparams().m_clause_proof) 
             return proof_ref(m);
-        }
         proof_ref_vector ps(m);
         for (auto& info : m_trail) {
             expr_ref fact = mk_or(info.m_clause);
             proof* pr = info.m_proof;
+            expr* args[2] = { pr, fact };
+            unsigned num_args = 2, offset = 0;
+            if (!pr) 
+                offset = 1;
             switch (info.m_status) {
             case status::assumption:
-                ps.push_back(m.mk_assumption_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::lemma:
-                ps.push_back(m.mk_lemma_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::th_assumption:
-                ps.push_back(m.mk_th_assumption_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("th-assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::th_lemma:
-                ps.push_back(m.mk_th_lemma_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("th-lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::deleted:
                 ps.push_back(m.mk_redundant_del(fact));
                 break;
             }
         }
-        if (inconsistent) {
+        if (inconsistent) 
             ps.push_back(m.mk_false());
-        }
-        else {
+        else 
             ps.push_back(m.mk_const("clause-trail-end", m.mk_bool_sort()));
-        }
         return proof_ref(m.mk_clause_trail(ps.size(), ps.data()), m);
     }
 

src/smt/smt_clause_proof.h

@@ -26,8 +26,11 @@ Revision History:
 --*/
 #pragma once
 
+#include "ast/ast_pp_util.h"
 #include "smt/smt_theory.h"
 #include "smt/smt_clause.h"
+#include "smt/smt_justification.h"
+#include "tactic/user_propagator_base.h"
 
 namespace smt {
     class context;
@@ -50,14 +53,28 @@ namespace smt {
             proof_ref       m_proof;
             info(status st, expr_ref_vector& v, proof* p): m_status(st), m_clause(v), m_proof(p, m_clause.m()) {}
         };
-        context&     ctx;
-        ast_manager& m;
+        context&        ctx;
+        ast_manager&    m;
         expr_ref_vector m_lits;
-        vector<info> m_trail;
+        vector<info>    m_trail;
+        bool            m_enabled = false;
+        bool            m_has_log = false;
+        user_propagator::on_clause_eh_t m_on_clause_eh;
+        void*                           m_on_clause_ctx = nullptr;
+        ast_pp_util                     m_pp;
+        scoped_ptr<std::ofstream>       m_pp_out;
+        proof_ref m_assumption, m_rup, m_del, m_smt;
+
+        void init_pp_out();
+        
         void update(status st, expr_ref_vector& v, proof* p);
         void update(clause& c, status st, proof* p);
         status kind2st(clause_kind k);
-        proof* justification2proof(justification* j);
+        proof_ref justification2proof(status st, justification* j);
+        void log(status st, proof* p);
+        void declare(std::ostream& out, expr* e);
+        std::ostream& display_literals(std::ostream& out, expr_ref_vector const& v);
+        std::ostream& display_hint(std::ostream& out, proof* p);
     public:
         clause_proof(context& ctx);
         void shrink(clause& c, unsigned new_size);
@@ -65,8 +82,15 @@ namespace smt {
         void add(literal lit1, literal lit2, clause_kind k, justification* j);
         void add(clause& c);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
+        void propagate(literal lit, justification const& j, literal_vector const& ante);
         void del(clause& c);
         proof_ref get_proof(bool inconsistent);
+        bool is_enabled() const { return m_enabled; }
+        void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) {
+            m_on_clause_eh = on_clause;
+            m_on_clause_ctx = ctx;
+            m_enabled |= !!m_on_clause_eh;
+        }
     };
 
     std::ostream& operator<<(std::ostream& out, clause_proof::status st);

src/smt/smt_conflict_resolution.cpp

@@ -350,6 +350,7 @@ namespace smt {
         literal_vector & antecedents = m_tmp_literal_vector;
         antecedents.reset();
         justification2literals_core(js, antecedents);
+        m_ctx.get_clause_proof().propagate(consequent, *js, antecedents);
         for (literal l : antecedents)
             process_antecedent(l, num_marks);
         (void)consequent;

src/smt/smt_context.cpp

@@ -284,7 +284,7 @@ namespace smt {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
               display_literal_smt2(tout, l) << "\n";
               tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n";
-              /*display(tout, j);*/
+              display(tout, j);
               );
         TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
 
@@ -639,7 +639,6 @@ namespace smt {
                     if (val != l_true) {
                         if (val == l_false && js.get_kind() == eq_justification::CONGRUENCE)
                             m_dyn_ack_manager.cg_conflict_eh(n1->get_expr(), n2->get_expr());
-
                         assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
                     }
                     // It is not necessary to reinsert the equality to the congruence table
@@ -867,6 +866,7 @@ namespace smt {
                 SASSERT(curr != m_false_enode);
                 bool_var v = enode2bool_var(curr);
                 literal l(v, sign);
+                CTRACE("propagate", (get_assignment(l) != l_true), tout << enode_pp(curr, *this) << " " << l << "\n");
                 if (get_assignment(l) != l_true)
                     assign(l, mk_justification(eq_root_propagation_justification(curr)));
                 curr = curr->m_next;
@@ -1723,7 +1723,7 @@ namespace smt {
                     return false;
             }
             if (!get_cancel_flag()) {
-                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
+//                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
                 m_qmanager->propagate();
             }
             if (inconsistent())
@@ -2962,7 +2962,11 @@ namespace smt {
         pop_to_base_lvl();
         setup_context(false);
         bool was_consistent = !inconsistent();
-        internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
+        try {
+            internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
+        } catch (cancel_exception&) {
+            throw default_exception("Resource limits hit in push");
+        }
         if (!m.inc())
             throw default_exception("push canceled");
         scoped_suspend_rlimit _suspend_cancel(m.limit());
@@ -3028,6 +3032,10 @@ namespace smt {
         TRACE("end_assert_expr_ll", ast_mark m; m_asserted_formulas.display_ll(tout, m););
     }
 
+    void context::add_asserted(expr* e) {
+        m_asserted_formulas.assert_expr(e);
+    }
+
     void context::assert_expr(expr * e) {
         assert_expr(e, nullptr);
     }
@@ -3553,7 +3561,12 @@ namespace smt {
             return p(asms);
         }
 
-        internalize_assertions();
+        try {
+            internalize_assertions();
+        } catch (cancel_exception&) {
+            VERIFY(resource_limits_exceeded());
+            return l_undef;
+        }
         expr_ref_vector theory_assumptions(m);
         add_theory_assumptions(theory_assumptions);
         if (!theory_assumptions.empty()) {
@@ -3617,10 +3630,15 @@ namespace smt {
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(m, num_assumptions, assumptions);
-            internalize_assertions();
-            add_theory_assumptions(asms);                
-            TRACE("unsat_core_bug", tout << asms << "\n";);        
-            init_assumptions(asms);
+            try {
+                internalize_assertions();
+                add_theory_assumptions(asms);
+                TRACE("unsat_core_bug", tout << asms << '\n';);
+                init_assumptions(asms);
+            } catch (cancel_exception&) {
+                VERIFY(resource_limits_exceeded());
+                return l_undef;
+            }
             TRACE("before_search", display(tout););
             r = search();
             r = mk_unsat_core(r);        
@@ -3638,11 +3656,16 @@ namespace smt {
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(cube);
-            internalize_assertions();
-            add_theory_assumptions(asms);
-            // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
-            for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
-            init_assumptions(asms);
+            try {
+                internalize_assertions();
+                add_theory_assumptions(asms);
+                // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
+                for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
+                init_assumptions(asms);
+            } catch (cancel_exception&) {
+                VERIFY(resource_limits_exceeded());
+                return l_undef;
+            }
             for (auto const& clause : clauses) init_clause(clause);
             r = search();   
             r = mk_unsat_core(r);             
@@ -3732,6 +3755,7 @@ namespace smt {
         flet<bool> l(m_searching, true);
         TRACE("after_init_search", display(tout););
         IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);
+        log_stats();
         TRACE("search_lite", tout << "searching...\n";);
         lbool    status            = l_undef;
         unsigned curr_lvl          = m_scope_lvl;

src/smt/smt_context.h

@@ -62,6 +62,8 @@ namespace smt {
 
     class model_generator;
 
+    struct cancel_exception {};
+
     class context {
         friend class model_generator;
         friend class lookahead;
@@ -1618,6 +1620,8 @@ namespace smt {
 
         void register_plugin(theory * th);
 
+        void add_asserted(expr* e);
+
         void assert_expr(expr * e);
 
         void assert_expr(expr * e, proof * pr);
@@ -1706,6 +1710,14 @@ namespace smt {
 
         void get_units(expr_ref_vector& result);
 
+        bool clause_proof_active() const { return m_clause_proof.is_enabled(); }
+
+        clause_proof& get_clause_proof() { return m_clause_proof; }
+
+        void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) {
+            m_clause_proof.register_on_clause(ctx, on_clause);
+        }
+
         /*
          * user-propagator
          */

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/smt_internalizer.cpp

@@ -353,7 +353,7 @@ namespace smt {
     */
     void context::internalize(expr * n, bool gate_ctx) {
         if (memory::above_high_watermark())
-            throw default_exception("resource limit exceeded during internalization");
+            throw cancel_exception();
         internalize_deep(n);
         internalize_rec(n, gate_ctx);
     }
@@ -1383,6 +1383,8 @@ namespace smt {
             Z3_fallthrough;
         case CLS_AUX: {
             literal_buffer simp_lits;
+            if (m_searching)
+                dump_lemma(num_lits, lits);
             if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
                 if (j && !j->in_region()) {
                     j->del_eh(m);
@@ -1394,6 +1396,7 @@ namespace smt {
             if (!simp_lits.empty()) {
                 j = mk_justification(unit_resolution_justification(*this, j, simp_lits.size(), simp_lits.data()));
             }
+              
             break;
         }
         case CLS_TH_LEMMA:
@@ -1525,7 +1528,6 @@ namespace smt {
     }
 
     void context::dump_lemma(unsigned n, literal const* lits) {
-        
         if (m_fparams.m_lemmas2console) {
             expr_ref fml(m);
             expr_ref_vector fmls(m);
@@ -1591,6 +1593,18 @@ namespace smt {
             TRACE("gate_clause", tout << mk_ll_pp(pr, m););
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
+        else if (clause_proof_active()) {
+            ptr_buffer<expr> new_lits;
+            for (unsigned i = 0; i < num_lits; i++) {
+                literal l      = lits[i];
+                bool_var v     = l.var();
+                expr * atom    = m_bool_var2expr[v]; 
+                new_lits.push_back(l.sign() ? m.mk_not(atom) : atom);
+            }
+            // expr* fact = m.mk_or(new_lits);
+            proof* pr = m.mk_app(symbol("tseitin"), new_lits.size(), new_lits.data(), m.mk_proof_sort());
+            mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
+        }
         else {
             mk_clause(num_lits, lits, nullptr);
         }
@@ -1624,9 +1638,11 @@ namespace smt {
             }
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
-        else {
+        else if (pr && clause_proof_active()) 
+            // support logging of quantifier instantiations and other more detailed information
+            mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
+        else 
             mk_clause(num_lits, lits, nullptr);
-        }
     }
 
     void context::mk_root_clause(literal l1, literal l2, proof * pr) {

src/smt/smt_justification.cpp

@@ -82,7 +82,8 @@ namespace smt {
     }
 
     proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) {
-        SASSERT(m_antecedent);
+        if (!m_antecedent)
+            return nullptr;
         ast_manager& m = cr.get_manager();
         proof_ref_vector prs(m);
         proof * pr = cr.get_proof(m_antecedent);

src/smt/smt_kernel.cpp

@@ -213,6 +213,20 @@ namespace smt {
         return out;
     }
 
+    expr* kernel::congruence_root(expr * e) {
+        smt::enode* n = m_imp->m_kernel.find_enode(e);
+        if (!n)
+            return e;
+        return n->get_root()->get_expr();
+    }
+
+    expr* kernel::congruence_next(expr * e) {
+        smt::enode* n = m_imp->m_kernel.find_enode(e);
+        if (!n)
+            return e;
+        return n->get_next()->get_expr();
+    }
+
     void kernel::collect_statistics(::statistics & st) const {
         m_imp->m_kernel.collect_statistics(st);
     }
@@ -260,6 +274,10 @@ namespace smt {
         m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
     }
 
+    void kernel::register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) {
+        m_imp->m_kernel.register_on_clause(ctx, on_clause);
+    }
+
     void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
         m_imp->m_kernel.user_propagate_register_fixed(fixed_eh);
     }

src/smt/smt_kernel.h

@@ -239,6 +239,13 @@ namespace smt {
         */
         expr_ref_vector cubes(unsigned depth);
 
+        /**
+           \brief access congruence closure
+        */
+        expr* congruence_next(expr* e);
+
+        expr* congruence_root(expr* e);
+
 
         /**
            \brief retrieve depth of variables from decision stack.
@@ -290,6 +297,8 @@ namespace smt {
         */
         static void collect_param_descrs(param_descrs & d);
 
+        void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause);
+
         /**
            \brief initialize a user-propagator "theory"
         */

src/smt/smt_model_checker.cpp

@@ -82,22 +82,18 @@ namespace smt {
         app* fresh_term;
         if (is_app(val) && to_app(val)->get_num_args() > 0) {
             ptr_buffer<expr> args;
-            for (expr* arg : *to_app(val)) {
+            for (expr* arg : *to_app(val)) 
                 args.push_back(get_type_compatible_term(arg));
-            }
             fresh_term = m.mk_app(to_app(val)->get_decl(), args.size(), args.data());
         }
         else {
             expr * sk_term = get_term_from_ctx(val);
-            if (sk_term != nullptr) {
+            if (sk_term != nullptr) 
                 return sk_term;
-            }
 
-            for (expr* f : m_fresh_exprs) {
-                if (f->get_sort() == val->get_sort()) {
+            for (expr* f : m_fresh_exprs) 
+                if (f->get_sort() == val->get_sort()) 
                     return f;
-                }
-            }
             fresh_term = m.mk_fresh_const("sk", val->get_sort());
         }
         m_fresh_exprs.push_back(fresh_term);
@@ -106,13 +102,16 @@ namespace smt {
     }
 
     void model_checker::init_value2expr() {
+        
         if (m_value2expr.empty()) {
             // populate m_value2expr
             for (auto const& kv : *m_root2value) {
                 enode * n   = kv.m_key;
                 expr  * val = kv.m_value;
                 n = n->get_eq_enode_with_min_gen();
-                m_value2expr.insert(val, n->get_expr());
+                expr* e = n->get_expr();
+                if (!m.is_value(e))
+                    m_value2expr.insert(val, e);
             }
         }
     }
@@ -405,13 +404,15 @@ namespace smt {
             m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
             m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3.
             m_fparams->m_axioms2files = false;
-            m_fparams->m_lemmas2console = false;            
+            m_fparams->m_lemmas2console = false;
+            m_fparams->m_proof_log = symbol::null;
         }
         if (!m_aux_context) {
             symbol logic;
             params_ref p;
             p.set_bool("solver.axioms2files", false);
             p.set_bool("solver.lemmas2console", false);
+            p.set_sym("solver.proof.log", symbol::null);
             m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p);
         }
     }

src/smt/smt_model_generator.cpp

@@ -330,27 +330,32 @@ namespace smt {
                 enode * n = curr.get_enode();
                 SASSERT(n->get_root() == n);
                 TRACE("mg_top_sort", tout << curr << "\n";);
-                dependencies.reset();
-                dependency_values.reset();
-                model_value_proc * proc = root2proc[n];
-                SASSERT(proc);
-                proc->get_dependencies(dependencies);
-                for (model_value_dependency const& d : dependencies) {
-                    if (d.is_fresh_value()) {
-                        CTRACE("mg_top_sort", !d.get_value()->get_value(), 
-                               tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
-                        SASSERT(d.get_value()->get_value());
-                        dependency_values.push_back(d.get_value()->get_value());
-                    }
-                    else {
-                        enode * child = d.get_enode();
-                        TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " 
-                              << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
-                        child = child->get_root();
-                        dependency_values.push_back(m_root2value[child]);
+                app* val = nullptr;
+                if (m.is_value(n->get_expr()))
+                    val = to_app(n->get_expr());
+                else {
+                    dependencies.reset();
+                    dependency_values.reset();
+                    model_value_proc * proc = root2proc[n];
+                    SASSERT(proc);
+                    proc->get_dependencies(dependencies);
+                    for (model_value_dependency const& d : dependencies) {
+                        if (d.is_fresh_value()) {
+                            CTRACE("mg_top_sort", !d.get_value()->get_value(), 
+                                   tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
+                            SASSERT(d.get_value()->get_value());
+                            dependency_values.push_back(d.get_value()->get_value());
+                        }
+                        else {
+                            enode * child = d.get_enode();
+                            TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " 
+                                  << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
+                            child = child->get_root();
+                            dependency_values.push_back(m_root2value[child]);
+                        }
                     }
+                    val = proc->mk_value(*this, dependency_values);
                 }
-                app * val = proc->mk_value(*this, dependency_values); 
                 register_value(val);
                 m_asts.push_back(val);
                 m_root2value.insert(n, val);

src/smt/smt_setup.cpp

@@ -212,11 +212,7 @@ namespace smt {
     }
 
     void setup::setup_QF_UF() {
-        m_params.m_relevancy_lvl           = 0;
-        m_params.m_nnf_cnf                 = false;
-        m_params.m_restart_strategy        = RS_LUBY;
-        m_params.m_phase_selection         = PS_CACHING_CONSERVATIVE2;
-        m_params.m_random_initial_activity = IA_RANDOM;
+        m_params.setup_QF_UF();
     }
 
     void setup::setup_QF_DT() {
@@ -240,20 +236,10 @@ namespace smt {
     }
 
     void setup::setup_QF_RDL() {
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false;
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_RDL();
         setup_mi_arith();
     }
 
-    static bool is_dense(static_features const & st) {
-        return 
-            st.m_num_uninterpreted_constants < 1000 &&
-            (st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9;
-    }
-
     static bool is_in_diff_logic(static_features const & st) {
         return 
             st.m_num_arith_eqs == st.m_num_diff_eqs && 
@@ -285,7 +271,7 @@ namespace smt {
         m_params.m_arith_reflect       = false;
         m_params.m_arith_propagate_eqs = false;
         m_params.m_nnf_cnf             = false;
-        if (is_dense(st)) {
+        if (st.is_dense()) {
             m_params.m_restart_strategy = RS_GEOMETRIC;
             m_params.m_restart_adaptive = false;
             m_params.m_phase_selection  = PS_CACHING;
@@ -327,12 +313,7 @@ namespace smt {
 
     void setup::setup_QF_IDL() {
         TRACE("setup", tout << "setup_QF_IDL()\n";);
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false;
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_arith_small_lemma_size = 30;
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_IDL();
         setup_lra_arith();
     }
 
@@ -353,11 +334,11 @@ namespace smt {
         m_params.m_nnf_cnf             = false;
         if (st.m_num_uninterpreted_constants > 5000)
             m_params.m_relevancy_lvl   = 2;
-        else if (st.m_cnf && !is_dense(st))
+        else if (st.m_cnf && !st.is_dense())
             m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
         else
             m_params.m_phase_selection = PS_CACHING;
-        if (is_dense(st) && st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses) {
+        if (st.is_dense() && st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses) {
             m_params.m_restart_adaptive    = false;
             m_params.m_restart_strategy    = RS_GEOMETRIC;
         }
@@ -373,7 +354,7 @@ namespace smt {
         if (m_manager.proofs_enabled()) {
             m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
         }
-        else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
+        else if (!m_params.m_arith_auto_config_simplex && st.is_dense()) {
             TRACE("setup", tout << "using dense diff logic...\n";);
             m_params.m_phase_selection = PS_CACHING_CONSERVATIVE;
             if (st.arith_k_sum_is_small())
@@ -396,15 +377,7 @@ namespace smt {
 
     void setup::setup_QF_UFIDL() {
         TRACE("setup", tout << "setup_QF_UFIDL()\n";);
-        m_params.m_relevancy_lvl    = 0;
-        m_params.m_arith_reflect    = false;
-        m_params.m_nnf_cnf          = false;
-        m_params.m_arith_eq_bounds  = true;
-        m_params.m_arith_eq2ineq    = true;
-        // m_params.m_phase_selection  = PS_THEORY;
-        m_params.m_restart_strategy = RS_GEOMETRIC;
-        m_params.m_restart_factor   = 1.5;
-        m_params.m_restart_adaptive = false;
+        m_params.setup_QF_UFIDL();
         setup_lra_arith();
     }
 
@@ -418,7 +391,7 @@ namespace smt {
         if (st.m_num_uninterpreted_functions == 0) {
             m_params.m_arith_eq2ineq        = true;
             m_params.m_arith_propagate_eqs  = false;
-            if (is_dense(st)) {
+            if (st.is_dense()) {
                 m_params.m_arith_small_lemma_size = 128;
                 m_params.m_lemma_gc_half          = true;
                 m_params.m_restart_strategy       = RS_GEOMETRIC;
@@ -449,35 +422,13 @@ namespace smt {
 
     void setup::setup_QF_LRA() {
         TRACE("setup", tout << "setup_QF_LRA()\n";);
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false;
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_eliminate_term_ite  = true;
-        m_params.m_nnf_cnf             = false;
-        m_params.m_phase_selection       = PS_THEORY;
+        m_params.setup_QF_LRA();
         setup_lra_arith();
     }
 
     void setup::setup_QF_LRA(static_features const & st) {
         check_no_uninterpreted_functions(st, "QF_LRA");
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false;
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_eliminate_term_ite  = true;
-        m_params.m_nnf_cnf             = false;
-        if (numerator(st.m_arith_k_sum) > rational(2000000) && denominator(st.m_arith_k_sum) > rational(500)) {
-            m_params.m_relevancy_lvl       = 2;
-            m_params.m_relevancy_lemma     = false;
-        }
-        m_params.m_phase_selection       = PS_THEORY;
-        if (!st.m_cnf) {
-            m_params.m_restart_strategy      = RS_GEOMETRIC;
-            m_params.m_arith_stronger_lemmas = false;
-            m_params.m_restart_adaptive      = false;
-        }
-        m_params.m_arith_small_lemma_size = 32;
+        m_params.setup_QF_LRA(st);
         setup_lra_arith();
     }
 
@@ -487,56 +438,20 @@ namespace smt {
 
     void setup::setup_QF_LIA() {
         TRACE("setup", tout << "setup_QF_LIA(st)\n";);
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false; 
-        m_params.m_arith_propagate_eqs = false; 
-        m_params.m_nnf_cnf             = false;        
+        m_params.setup_QF_LIA();
         setup_lra_arith();
     }
 
     void setup::setup_QF_LIA(static_features const & st) {
         check_no_uninterpreted_functions(st, "QF_LIA");
         TRACE("setup", tout << "QF_LIA setup\n";);
-
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_eq2ineq       = true;
-        m_params.m_arith_reflect       = false; 
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_nnf_cnf             = false;
-        if (st.m_max_ite_tree_depth > 50) {
-            m_params.m_arith_eq2ineq        = false;
-            m_params.m_pull_cheap_ite       = true;
-            m_params.m_arith_propagate_eqs  = true;
-            m_params.m_relevancy_lvl        = 2; 
-            m_params.m_relevancy_lemma      = false;
-        }
-        else if (st.m_num_clauses == st.m_num_units) {
-            m_params.m_arith_gcd_test         = false;
-            m_params.m_arith_branch_cut_ratio = 4;
-            m_params.m_relevancy_lvl          = 2; 
-            m_params.m_arith_eq2ineq          = true;
-            m_params.m_eliminate_term_ite     = true;
-        } 
-        else {
-            m_params.m_eliminate_term_ite   = true;
-            m_params.m_restart_adaptive     = false;
-            m_params.m_restart_strategy     = RS_GEOMETRIC;
-            m_params.m_restart_factor       = 1.5;
-        }
-        if (st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses && st.m_cnf && st.m_arith_k_sum > rational(100000)) {
-            m_params.m_arith_bound_prop      = bound_prop_mode::BP_NONE;
-            m_params.m_arith_stronger_lemmas = false;
-        }
+        m_params.setup_QF_LIA(st);
         setup_lra_arith();
     }
 
     void setup::setup_QF_UFLIA() {
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_reflect       = false; 
-        m_params.m_nnf_cnf             = false;
-        m_params.m_arith_propagation_threshold = 1000;
         setup_lra_arith();
+        m_params.setup_QF_UFLIA();
     }
 
     void setup::setup_QF_UFLIA(static_features & st) {
@@ -548,103 +463,49 @@ namespace smt {
     }
 
     void setup::setup_QF_UFLRA() {
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_reflect       = false; 
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_UFLRA();
         setup_lra_arith();
     }
 
     void setup::setup_QF_BV() {
         TRACE("setup", tout << "qf-bv\n";);
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_reflect       = false; 
-        m_params.m_bv_cc               = false;
-        m_params.m_bb_ext_gates        = true;
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_BV();
         m_context.register_plugin(alloc(smt::theory_bv, m_context));
     }
 
     void setup::setup_QF_AUFBV() {
-        m_params.m_array_mode          = AR_SIMPLE;
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_bv_cc               = false;
-        m_params.m_bb_ext_gates        = true;
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_AUFBV();
         m_context.register_plugin(alloc(smt::theory_bv, m_context));
         setup_arrays();
     }
 
     void setup::setup_QF_AX() {
         TRACE("setup", tout << "QF_AX\n";);
-        m_params.m_array_mode          = AR_SIMPLE;
-        m_params.m_nnf_cnf             = false;
+        m_params.setup_QF_AX();
         setup_arrays();
     }
 
     void setup::setup_QF_AX(static_features const & st) {
-        m_params.m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
-        m_params.m_nnf_cnf             = false;
-        if (st.m_num_clauses == st.m_num_units) {
-            m_params.m_relevancy_lvl       = 0;
-            m_params.m_phase_selection     = PS_ALWAYS_FALSE;
-        }
-        else {
-            m_params.m_relevancy_lvl       = 2;
-        }
+        m_params.setup_QF_AX(st);
         setup_arrays();
     }
 
     void setup::setup_QF_AUFLIA() {
         TRACE("QF_AUFLIA", tout << "no static features\n";);
-        m_params.m_array_mode          = AR_SIMPLE;
-        m_params.m_nnf_cnf             = false;
-        m_params.m_relevancy_lvl       = 2;
-        m_params.m_restart_strategy    = RS_GEOMETRIC;
-        m_params.m_restart_factor      = 1.5;
-        m_params.m_phase_selection     = PS_CACHING_CONSERVATIVE2;
+        m_params.setup_QF_AUFLIA();
         setup_i_arith();
         setup_arrays();
     }
 
     void setup::setup_QF_AUFLIA(static_features const & st) {
-        m_params.m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
-        if (st.m_has_real)
-            throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
-        m_params.m_nnf_cnf             = false;
-        if (st.m_num_clauses == st.m_num_units) {
-            TRACE("QF_AUFLIA", tout << "using relevancy: 0\n";);
-            m_params.m_relevancy_lvl       = 0;
-            m_params.m_phase_selection     = PS_ALWAYS_FALSE;
-        }
-        else {
-            m_params.m_relevancy_lvl           = 0; // it was 2, for some reason 2 doesn't work anymore TODO: investigate
-            m_params.m_restart_strategy        = RS_GEOMETRIC;
-            m_params.m_restart_factor          = 1.5;
-            m_params.m_phase_selection         = PS_CACHING_CONSERVATIVE2;
-            m_params.m_random_initial_activity = IA_ZERO;
-        }
+        m_params.setup_QF_AUFLIA(st);
         setup_i_arith();
         setup_arrays();
     }
 
     void setup::setup_AUFLIA(bool simple_array) {
         TRACE("setup", tout << "AUFLIA\n";);
-        m_params.m_array_mode              = simple_array ? AR_SIMPLE : AR_FULL;
-        m_params.m_pi_use_database         = true;
-        m_params.m_phase_selection         = PS_ALWAYS_FALSE;
-        m_params.m_restart_strategy        = RS_GEOMETRIC;
-        m_params.m_restart_factor          = 1.5;
-        m_params.m_eliminate_bounds        = true;
-        m_params.m_qi_quick_checker        = MC_UNSAT;
-        m_params.m_qi_lazy_threshold       = 20;
-        m_params.m_mbqi                    = true; // enabling MBQI and MACRO_FINDER by default :-)
-
-        // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general)
-        // It destroys the existing patterns.
-        // m_params.m_macro_finder            = true; 
-        
-        if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
-            m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
+        m_params.setup_AUFLIA(simple_array);
         TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
         m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
         setup_arrays();
@@ -653,29 +514,13 @@ namespace smt {
     void setup::setup_AUFLIA(static_features const & st) {
         if (st.m_has_real)
             throw default_exception("Benchmark has real variables but it is marked as AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
-        m_params.m_qi_eager_threshold      = st.m_num_quantifiers_with_patterns == 0 ? 5 : 7;
+        m_params.setup_AUFLIA(st);
         setup_AUFLIA();
     }
 
     void setup::setup_AUFLIRA(bool simple_array) {
         TRACE("setup", tout << "AUFLIRA\n";);
-        m_params.m_array_mode              = simple_array ? AR_SIMPLE : AR_FULL;
-        m_params.m_phase_selection         = PS_ALWAYS_FALSE;
-        m_params.m_eliminate_bounds        = true;
-        m_params.m_qi_quick_checker        = MC_UNSAT;
-        m_params.m_qi_eager_threshold      = 5;
-        // Added for MBQI release
-        m_params.m_qi_lazy_threshold       = 20;
-        // 
-        m_params.m_macro_finder            = true;
-        if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
-            m_params.m_ng_lift_ite         = lift_ite_kind::LI_CONSERVATIVE;
-        m_params.m_pi_max_multi_patterns   = 10; //<< it was used for SMT-COMP
-        m_params.m_array_lazy_ieq          = true;
-        m_params.m_array_lazy_ieq_delay    = 4;
-        //
-        m_params.m_mbqi                    = true; // enabling MBQI by default :-)
-        // 
+        m_params.setup_AUFLIRA(simple_array);
         setup_mi_arith();
         setup_arrays(); 
     }
@@ -697,10 +542,7 @@ namespace smt {
     }
 
     void setup::setup_LRA() {
-        m_params.m_relevancy_lvl       = 0;
-        m_params.m_arith_reflect       = false;
-        m_params.m_arith_propagate_eqs = false;
-        m_params.m_eliminate_term_ite  = true;
+        m_params.setup_LRA();
         setup_mi_arith();
     }
 
@@ -774,8 +616,6 @@ namespace smt {
         }
     }
 
-
-
     void setup::setup_arith() {
         static_features    st(m_manager);
         IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
@@ -849,9 +689,12 @@ namespace smt {
     }
 
     void setup::setup_bv() {
+        family_id bv_fid = m_manager.mk_family_id("bv");
+        if (m_context.get_theory(bv_fid))
+            return;
         switch(m_params.m_bv_mode) {
         case BS_NO_BV:
-            m_context.register_plugin(alloc(smt::theory_dummy, m_context, m_manager.mk_family_id("bv"), "no bit-vector"));
+            m_context.register_plugin(alloc(smt::theory_dummy, m_context, bv_fid, "no bit-vector"));
             break;
         case BS_BLASTER:
             m_context.register_plugin(alloc(smt::theory_bv, m_context));

src/smt/smt_solver.cpp

@@ -212,6 +212,10 @@ namespace {
             return m_context.get_trail(max_level);
         }
 
+        void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
+            m_context.register_on_clause(ctx, on_clause);
+        }
+
         void user_propagate_init(
             void*                ctx, 
             user_propagator::push_eh_t&   push_eh,
@@ -289,7 +293,7 @@ namespace {
             m_context.get_model(m);
         }
 
-        proof * get_proof() override {
+        proof * get_proof_core() override {
             return m_context.get_proof();
         }
 
@@ -326,6 +330,10 @@ namespace {
             m_context.get_units(units);
         }
 
+        expr* congruence_next(expr* e) override { return m_context.congruence_next(e); }
+        expr* congruence_root(expr* e) override { return m_context.congruence_root(e); }
+
+
         expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override {
             ast_manager& m = get_manager();
             if (!m_cuber) {

src/smt/tactic/ctx_solver_simplify_tactic.h

@@ -13,7 +13,17 @@ Author:
 
     Nikolaj (nbjorner) 2012-3-6
 
-Notes:
+Tactic Documentation:
+
+## Tactic ctx-solver-simplify
+
+### Short Description
+
+A heavy handed version of `ctx-simplify`. It applies SMT checks on sub-formulas to check
+if they can be simplified to `true` or `false` within their context.
+Note that a sub-formula may occur within multiple contexts due to shared sub-terms.
+In this case the tactic is partial and simplifies a limited number of context occurrences.
+
 
 --*/
 #pragma once

src/smt/tactic/smt_tactic_core.cpp

@@ -26,11 +26,11 @@ 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"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "solver/parallel_params.hpp"
 
 typedef obj_map<expr, expr *> expr2expr_map;
@@ -323,7 +323,13 @@ public:
     user_propagator::eq_eh_t    m_diseq_eh;
     user_propagator::created_eh_t m_created_eh;
     user_propagator::decide_eh_t m_decide_eh;
-   
+    void* m_on_clause_ctx = nullptr;
+    user_propagator::on_clause_eh_t m_on_clause_eh;
+
+    void on_clause_delay_init() {
+        if (m_on_clause_eh)
+            m_ctx->register_on_clause(m_on_clause_ctx, m_on_clause_eh);
+    }
 
     void user_propagate_delay_init() {
         if (!m_user_ctx)
@@ -349,6 +355,13 @@ public:
         m_diseq_eh = nullptr;
         m_created_eh = nullptr;
         m_decide_eh = nullptr;
+        m_on_clause_eh = nullptr;
+        m_on_clause_ctx = nullptr;
+    }
+
+    void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
+        m_on_clause_ctx = ctx;
+        m_on_clause_eh = on_clause;
     }
 
     void user_propagate_init(

src/smt/tactic/smt_tactic_core.h

@@ -24,7 +24,6 @@ Notes:
 #include "tactic/goal.h"
 
 class tactic;
-class filter_model_converter;
 
 tactic * mk_smt_tactic_core(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
 // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)

src/smt/tactic/unit_subsumption_tactic.h

@@ -13,12 +13,20 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2012-9-6
 
-Notes:
+Tactic Documentation:
 
-    Background: PDR generates several clauses that subsume each-other.
-    Simplify a goal assuming it is a conjunction of clauses.
-    Subsumed clauses are simplified by using unit-propagation 
-    It uses the smt_context for the solver.
+## Tactic unit-subsume-simplify
+
+### Short Description
+
+implify goal using subsumption based on unit propagation
+
+### Long Description
+
+Background: PDR generates several clauses that subsume each-other.
+Simplify a goal assuming it is a conjunction of clauses.
+Subsumed clauses are simplified by using unit-propagation 
+It uses the default SMT solver.
 
 --*/
 #pragma once

src/smt/theory_arith.h

@@ -436,9 +436,8 @@ namespace smt {
         theory_arith_params &   m_params;
         arith_util              m_util;
         arith_eq_solver         m_arith_eq_solver;
-        bool                    m_found_unsupported_op;
-        bool                    m_found_underspecified_op;
         ptr_vector<app>         m_underspecified_ops;
+        ptr_vector<app>         m_unsupported_ops;
         arith_eq_adapter        m_arith_eq_adapter;
         vector<row>             m_rows;
         svector<unsigned>       m_dead_rows;

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 {
 
@@ -2169,9 +2169,8 @@ namespace smt {
     */
     template<typename Ext>
     bool theory_arith<Ext>::is_shared(theory_var v) const {
-        if (!m_found_underspecified_op) {
+        if (m_underspecified_ops.empty())
             return false;
-        }
         enode * n      = get_enode(v);
         enode * r      = n->get_root();
         enode_vector::const_iterator it  = r->begin_parents();
@@ -2223,12 +2222,12 @@ namespace smt {
                 continue;
             }
             TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
-            m_assume_eq_candidates.push_back(std::make_pair(other, v));
+            m_assume_eq_candidates.push_back({ other , v }); 
             result = true;
         }
 
         if (result)
-            ctx.push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
+            ctx.push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         return delayed_assume_eqs();
     }
 

src/smt/theory_arith_core.h

@@ -29,22 +29,16 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::found_unsupported_op(app * n) {
-        if (!m_found_unsupported_op) {
-            TRACE("arith", tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";);
-            ctx.push_trail(value_trail<bool>(m_found_unsupported_op));
-            m_found_unsupported_op = true;
-        }
+        CTRACE("arith", m_unsupported_ops.empty(), tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";);
+        m_unsupported_ops.push_back(n);
+        ctx.push_trail(push_back_vector<ptr_vector<app>>(m_unsupported_ops));
     }
 
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
+        CTRACE("arith", m_underspecified_ops.empty(), tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";);
         m_underspecified_ops.push_back(n);
         ctx.push_trail(push_back_vector<ptr_vector<app>>(m_underspecified_ops));
-        if (!m_found_underspecified_op) {
-            TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";);
-            ctx.push_trail(value_trail<bool>(m_found_underspecified_op));
-            m_found_underspecified_op = true;
-        }
 
         expr* e = nullptr;
         if (m_util.is_div(n)) {                
@@ -1532,9 +1526,13 @@ namespace smt {
             }
         }
         while (m_final_check_idx != old_idx);
-        if (result == FC_DONE && m_found_unsupported_op) {
-            TRACE("arith", tout << "Found unsupported operation\n";);
-            result = FC_GIVEUP;
+        if (result == FC_DONE) {
+            for (app* n : m_unsupported_ops) {
+                if (!ctx.is_relevant(n))
+                    continue;
+                TRACE("arith", tout << "Found unsupported operation " << mk_pp(n, m) << "\n");
+                result = FC_GIVEUP;
+            }
         }
         return result;
     }
@@ -1733,8 +1731,6 @@ namespace smt {
         m_params(ctx.get_fparams()),
         m_util(m),
         m_arith_eq_solver(m),
-        m_found_unsupported_op(false),
-        m_found_underspecified_op(false),
         m_arith_eq_adapter(*this, m_util),
         m_asserted_qhead(0),
         m_row_vars_top(0),

src/smt/theory_arith_pp.h

@@ -516,13 +516,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::display_bounds_in_smtlib() const {
-        char buffer[128];
         static int id = 0;
-#ifdef _WINDOWS
-        sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "arith_%d.smt", id);
-#else
-        sprintf(buffer, "arith_%d.smt", id);
-#endif
+        std::string buffer = "arith_" + std::to_string(id) + ".smt2";
         std::ofstream out(buffer);
         display_bounds_in_smtlib(out);
         out.close();

src/smt/theory_array.cpp

@@ -380,9 +380,8 @@ namespace smt {
         }
         else {
             if (m_final_check_idx % 2 == 1) {
-                if (assert_delayed_axioms() == FC_CONTINUE)
-                    r = FC_CONTINUE;
-                else 
+                r = assert_delayed_axioms();
+                if (r == FC_DONE) 
                     r = mk_interface_eqs_at_final_check();
             }
             else {

src/smt/theory_array_base.cpp

@@ -529,7 +529,7 @@ namespace smt {
             // issue #3532, #3529
             // 
             if (ctx.is_shared(r) || is_select_arg(r)) {
-                TRACE("array", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+                TRACE("array", tout << "new shared var: #" << r->get_owner_id() << " " << is_select_arg(r) << "\n";);
                 theory_var r_th_var = r->get_th_var(get_id());
                 SASSERT(r_th_var != null_theory_var);
                 result.push_back(r_th_var);

src/smt/theory_bv.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "util/stats.h"
 
+#define ENABLE_QUOT_REM_ENCODING 0
 
 namespace smt {
 
@@ -885,6 +886,7 @@ namespace smt {
         find_wpos(v);
     }
 
+
     bool theory_bv::internalize_term_core(app * term) {
         SASSERT(term->get_family_id() == get_family_id());
         TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, m) << "\n";);
@@ -897,7 +899,11 @@ namespace smt {
         case OP_BSUB:           internalize_sub(term); return true;
         case OP_BMUL:           internalize_mul(term); return true;
         case OP_BSDIV_I:        internalize_sdiv(term); return true;
+#if ENABLE_QUOT_REM_ENCODING
+        case OP_BUDIV_I:        internalize_udiv_quot_rem(term); return true;
+#else
         case OP_BUDIV_I:        internalize_udiv(term); return true;
+#endif
         case OP_BSREM_I:        internalize_srem(term); return true;
         case OP_BUREM_I:        internalize_urem(term); return true;
         case OP_BSMOD_I:        internalize_smod(term); return true;
@@ -1312,7 +1318,7 @@ namespace smt {
         SASSERT(consequent.var() != antecedent.var());
         TRACE("bv_bit_prop", tout << "assigning: " << consequent << " @ " << ctx.get_scope_level();
               tout << " using "; ctx.display_literal(tout, antecedent); 
-              tout << " #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << " idx: " << idx << "\n";
+              tout << " " << enode_pp(get_enode(v1), ctx) << " " << enode_pp(get_enode(v2), ctx) << " idx: " << idx << "\n";
               tout << "propagate_eqc: " << propagate_eqc << "\n";);
         if (consequent == false_literal) {
             m_stats.m_num_conflicts++;
@@ -1352,6 +1358,9 @@ namespace smt {
             // So, we need to propagate the assignment to other bits.
             bool_var bv = consequent.var();
             atom * a    = get_bv2a(bv);
+            CTRACE("bv", !a, tout << ctx.literal2expr(literal(bv, false)) << "\n");
+            if (!a)
+                return;
             SASSERT(a->is_bit());
             bit_atom * b = static_cast<bit_atom*>(a);
             var_pos_occ * curr = b->m_occs;
@@ -1370,7 +1379,7 @@ namespace smt {
     }
 
     void theory_bv::relevant_eh(app * n) {
-        TRACE("arith", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
+        TRACE("arith", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";);
         TRACE("bv", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
         if (m.is_bool(n)) {
             bool_var v = ctx.get_bool_var(n);
@@ -1392,6 +1401,13 @@ namespace smt {
             ctx.mark_as_relevant(n->get_arg(0));
             assert_int2bv_axiom(n);
         }
+#if ENABLE_QUOT_REM_ENCODING
+        else if (m_util.is_bv_udivi(n)) {
+            ctx.mark_as_relevant(n->get_arg(0));
+            ctx.mark_as_relevant(n->get_arg(1));
+            assert_udiv_quot_rem_axiom(n);
+        }
+#endif
         else if (ctx.e_internalized(n)) {
             enode * e    = ctx.get_enode(n);
             theory_var v = e->get_th_var(get_id());
@@ -1476,6 +1492,7 @@ namespace smt {
         m_approximates_large_bvs(false) {
         memset(m_eq_activity, 0, sizeof(m_eq_activity));
         memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
+        m_bb.set_flat_and_or(false);
     }
 
     theory_bv::~theory_bv() {
@@ -1985,5 +2002,43 @@ namespace smt {
         return true;
     }
 
+#if ENABLE_QUOT_REM_ENCODING
+    void theory_bv::internalize_udiv_quot_rem(app* n) {
+        process_args(n);
+        mk_enode(n);
+        theory_var v = ctx.get_enode(n)->get_th_var(get_id()); 
+        mk_bits(v);
+        if (!ctx.relevancy()) 
+            assert_udiv_quot_rem_axiom(n);
+    }
+
+
+    void theory_bv::assert_udiv_quot_rem_axiom(app * q) {
+        // Axioms for quotient/remainder:
+        //      a = b*q + r
+        //      no-mul-overflow(b,q)
+        //      no-add-overflow(bq, r)
+        //      b != 0 => r < b
+        //      b = 0 => q = -1
+        expr* a, *b;
+        VERIFY(m_util.is_bv_udivi(q, a, b));
+        sort* srt = q->get_sort();
+        func_decl_ref rf(m.mk_func_decl(symbol("rem"), srt, srt, srt), m);
+        expr_ref r(m.mk_app(rf, a, b), m);
+        expr_ref bq(m_util.mk_bv_mul(b, q), m);
+        expr_ref bqr(m_util.mk_bv_add(bq, r), m);
+        literal eq = mk_literal(m.mk_eq(a, bqr));
+        literal obq = mk_literal(m_util.mk_bvumul_no_ovfl(b, q));
+        literal obqr = mk_literal(m_util.mk_ule(r, bqr));
+        literal b0 = mk_literal(m.mk_eq(b, m_util.mk_numeral(rational::zero(), srt)));
+        
+        ctx.mk_th_axiom(get_id(), 1, &eq);
+        ctx.mk_th_axiom(get_id(), 1, &obq);
+        ctx.mk_th_axiom(get_id(), 1, &obqr);
+        ctx.mk_th_axiom(get_id(), b0, ~mk_literal(m_util.mk_ule(b, r)));
+        ctx.mk_th_axiom(get_id(), ~b0, mk_literal(m.mk_eq(q, m_util.mk_numeral(rational(-1), srt))));
+    }
+#endif
+
 
 };

src/smt/theory_bv.h

@@ -188,6 +188,7 @@ namespace smt {
         void internalize_urem(app * n);
         void internalize_srem(app * n);
         void internalize_smod(app * n);
+        void internalize_udiv_quot_rem(app* n);
         void internalize_shl(app * n);
         void internalize_lshr(app * n);
         void internalize_ashr(app * n);
@@ -227,6 +228,8 @@ namespace smt {
         void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
         void assert_int2bv_axiom(app* n);
         void assert_bv2int_axiom(app* n);
+        void assert_udiv_quot_rem_axiom(app * n);
+
 
     protected:
         theory_var mk_var(enode * n) override;

src/smt/theory_fpa.cpp

@@ -650,8 +650,7 @@ namespace smt {
             theory_var v = n->get_th_var(get_family_id());
             if (v != -1) {
                 if (first) out << "fpa theory variables:" << std::endl;
-                out << v << " -> " <<
-                    mk_ismt2_pp(n->get_expr(), m) << std::endl;
+                out << v << " -> " << enode_pp(n, ctx) << "\n";
                 first = false;
             }
         }
@@ -661,22 +660,20 @@ namespace smt {
         out << "bv theory variables:" << std::endl;
         for (enode * n : ctx.enodes()) {
             theory_var v = n->get_th_var(m_bv_util.get_family_id());
-            if (v != -1) out << v << " -> " <<
-                mk_ismt2_pp(n->get_expr(), m) << std::endl;
+            if (v != -1) out << v << " -> " << enode_pp(n, ctx) << "\n";
         }
 
         out << "arith theory variables:" << std::endl;
         for (enode* n : ctx.enodes()) {
             theory_var v = n->get_th_var(m_arith_util.get_family_id());
-            if (v != -1) out << v << " -> " <<
-                mk_ismt2_pp(n->get_expr(), m) << std::endl;
+            if (v != -1) out << v << " -> " << enode_pp(n, ctx) << "\n";
         }
 
         out << "equivalence classes:\n";
         for (enode * n : ctx.enodes()) {
             expr * e = n->get_expr();
             expr * r = n->get_root()->get_expr();
-            out << r->get_id() << " --> " << mk_ismt2_pp(e, m) << std::endl;
+            out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n";
         }
     }
 };

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"
@@ -62,7 +62,6 @@ class theory_lra::imp {
 
     struct scope {
         unsigned m_bounds_lim;
-        unsigned m_idiv_lim;
         unsigned m_asserted_qhead;            
         unsigned m_asserted_atoms_lim;
     };
@@ -161,7 +160,6 @@ class theory_lra::imp {
     svector<delayed_atom>  m_asserted_atoms;        
     ptr_vector<expr>       m_not_handled;
     ptr_vector<app>        m_underspecified;
-    ptr_vector<expr>       m_idiv_terms;
     vector<ptr_vector<api_bound> > m_use_list;        // bounds where variables are used.
 
     // attributes for incremental version:
@@ -275,6 +273,11 @@ class theory_lra::imp {
                 (void)_s;
                 m_nla->push();
             }
+            std::function<bool(lpvar)> is_relevant = [&](lpvar v) {
+                theory_var u = lp().local_to_external(v);
+                return ctx().is_relevant(th.get_enode(u));
+            };
+            m_nla->set_relevant(is_relevant);
             smt_params_helper prms(ctx().get_params());
             m_nla->settings().run_order =                   prms.arith_nl_order();
             m_nla->settings().run_tangents =                prms.arith_nl_tangents();
@@ -431,10 +434,23 @@ class theory_lra::imp {
                 }
                 else if (a.is_idiv(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
-                    m_idiv_terms.push_back(n);
                     app_ref mod(a.mk_mod(n1, n2), m);
                     ctx().internalize(mod, false);
                     if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
+                    if (m_nla && !a.is_numeral(n2)) {
+                        // shortcut to create non-linear division axioms.
+                        theory_var q = mk_var(n);
+                        theory_var x = mk_var(n1);
+                        theory_var y = mk_var(n2);
+                        m_nla->add_idivision(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y));
+                    }
+                    if (a.is_numeral(n2) && a.is_bounded(n1)) {
+                        ensure_nla();
+                        theory_var q = mk_var(n);
+                        theory_var x = mk_var(n1);
+                        theory_var y = mk_var(n2);
+                        m_nla->add_bounded_division(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y));
+                    }
                 }
                 else if (a.is_mod(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
@@ -454,6 +470,12 @@ class theory_lra::imp {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);       
                 }
+                else if (a.is_power(n, n1, n2)) {                    
+                    found_unsupported(n);
+                    if (!ctx().relevancy()) mk_power_axiom(n, n1, n2);
+                    st.to_ensure_var().push_back(n1);
+                    st.to_ensure_var().push_back(n2);
+                }
                 else if (!a.is_div0(n)) {
                     found_unsupported(n);
                 }
@@ -543,7 +565,7 @@ class theory_lra::imp {
     }
 
     enode * mk_enode(app * n) {
-        TRACE("arith", tout << expr_ref(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";);
+        TRACE("arith", tout << mk_bounded_pp(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";);
         if (reflect(n))
             for (expr* arg : *n)
                 if (!ctx().e_internalized(arg))
@@ -791,8 +813,17 @@ class theory_lra::imp {
         return internalize_linearized_def(term, st);
     }
 
+    lpvar get_lpvar(expr* e) {
+        return get_lpvar(get_enode(e));
+    }
+
+    lpvar get_lpvar(enode* n)  {
+        ensure_column(n);
+        return n ? get_lpvar(n->get_th_var(get_id())) : lp::null_lpvar;
+    }
+
     lpvar get_lpvar(theory_var v) const {
-        return lp().external_to_local(v);
+        return v == null_theory_var ? lp::null_lpvar : lp().external_to_local(v);
     }
 
     lp::tv get_tv(theory_var v) const {
@@ -989,7 +1020,7 @@ public:
     }
 
     void assign_eh(bool_var v, bool is_true) {
-        TRACE("arith", tout << mk_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";);
+        TRACE("arith", tout << mk_bounded_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";);
         m_asserted_atoms.push_back(delayed_atom(v, is_true));
     }
 
@@ -1034,7 +1065,7 @@ public:
     }
 
     void apply_sort_cnstr(enode* n, sort*) {
-        TRACE("arith", tout << "sort constraint: " << pp(n, m) << "\n";);
+        TRACE("arith", tout << "sort constraint: " << enode_pp(n, ctx()) << "\n";);
 #if 0
         if (!th.is_attached_to_var(n)) {
             mk_var(n->get_owner());
@@ -1048,7 +1079,6 @@ public:
         scope& sc = m_scopes.back();
         sc.m_bounds_lim = m_bounds_trail.size();
         sc.m_asserted_qhead = m_asserted_qhead;
-        sc.m_idiv_lim = m_idiv_terms.size();
         sc.m_asserted_atoms_lim = m_asserted_atoms.size();
         lp().push();
         if (m_nla)
@@ -1063,7 +1093,6 @@ public:
         }
         unsigned old_size = m_scopes.size() - num_scopes;
         del_bounds(m_scopes[old_size].m_bounds_lim);
-        m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim);
         m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim);
         m_asserted_qhead = m_scopes[old_size].m_asserted_qhead;
         m_scopes.resize(old_size);            
@@ -1094,6 +1123,17 @@ public:
             mk_is_int_axiom(n);            
         else if (m.is_ite(n))
             mk_ite_axiom(n);
+        else if (a.is_power(n, n1, n2))
+            mk_power_axiom(n, n1, n2);
+    }
+
+    void mk_power_axiom(expr* p, expr* x, expr* y) {
+        rational r;
+        // r > 0 => r^y > 0
+        if (a.is_extended_numeral(x, r) && r > 0) {
+            expr_ref zero(a.mk_real(0), m);
+            mk_axiom(~mk_literal(a.mk_le(p, zero)));
+        }
     }
 
     //  n < 0 || rem(a, n) =  mod(a, n)
@@ -1408,10 +1448,13 @@ public:
         return v != null_theory_var && lp().external_is_used(v);
     }
 
+    void ensure_column(enode* n) {
+        ensure_column(n->get_th_var(get_id()));
+    }
+
     void ensure_column(theory_var v) {
-        if (!lp().external_is_used(v)) {
+        if (!lp().external_is_used(v) && v != null_theory_var) 
             register_theory_var_in_lar_solver(v);
-        }
     }
 
     mutable vector<std::pair<lp::tv, rational>> m_todo_terms;
@@ -1437,7 +1480,7 @@ public:
     }
     
     void random_update() {
-        if (m_nla)
+        if (m_nla && m_nla->need_check())
             return;
         m_tmp_var_set.clear();
         m_tmp_var_set.resize(th.get_num_vars());
@@ -1515,7 +1558,7 @@ public:
         }
             
         if (num_candidates > 0) {
-            ctx().push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
+            ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         }
 
         return delayed_assume_eqs();
@@ -1551,6 +1594,31 @@ public:
         return !m_asserted_atoms.empty();
     }
 
+    final_check_status eval_power(expr* e) {
+        expr* x, * y;
+        VERIFY(a.is_power(e, x, y));
+
+        switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y), m_nla_lemma_vector)) {
+        case l_true:
+            return FC_DONE;
+        case l_false:
+            for (const nla::lemma & l : m_nla_lemma_vector) 
+                false_case_of_check_nla(l);
+            return FC_CONTINUE;
+        case l_undef:
+            return FC_GIVEUP;
+        default:
+            break;
+        }
+        return FC_GIVEUP;
+    }
+
+    final_check_status eval_unsupported(expr* e) {
+        if (a.is_power(e)) 
+            return eval_power(e);        
+        return FC_GIVEUP;
+    }
+
     final_check_status final_check_eh() {
         if (propagate_core())
             return FC_CONTINUE;
@@ -1600,10 +1668,23 @@ public:
                 return FC_CONTINUE;
             }
             for (expr* e : m_not_handled) {
-                (void) e; // just in case TRACE() is a no-op
-                TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";);        
-                st = FC_GIVEUP;
-            }                
+                if (!ctx().is_relevant(e))
+                    continue;
+                st = FC_DONE;
+                switch (eval_unsupported(e)) {
+                case FC_CONTINUE:
+                    st = FC_CONTINUE;
+                    break;
+                case FC_GIVEUP:
+                    if (st != FC_CONTINUE) 
+                        st = FC_GIVEUP;
+                    break;
+                default:
+                    break;
+                }
+                if (st == FC_CONTINUE)
+                    break;
+            }
             return st;
         case l_false:
             get_infeasibility_explanation_and_set_conflict();
@@ -1718,95 +1799,13 @@ public:
      */
 
     bool check_idiv_bounds() {
-        if (m_idiv_terms.empty()) {
+        if (!m_nla)
             return true;
-        }
-        bool all_divs_valid = true;
-        unsigned count = 0;
-        unsigned offset = ctx().get_random_value(); 
-        for (unsigned j = 0; j < m_idiv_terms.size(); ++j) {
-            unsigned i =  (offset + j) % m_idiv_terms.size();
-            expr* n = m_idiv_terms[i];
-            expr* p = nullptr, *q = nullptr;
-            VERIFY(a.is_idiv(n, p, q));
-            theory_var v = internalize_def(to_app(n));
-            theory_var v1 = internalize_def(to_app(p));
-
-            if (!is_registered_var(v1))
-                continue;
-            lp::impq r1 = get_ivalue(v1);
-            rational r2;
-
-            if (!r1.x.is_int() || r1.x.is_neg() || !r1.y.is_zero()) {
-                // TBD
-                // r1 = 223/4, r2 = 2, r = 219/8 
-                // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
-                // then 
-                //      p/q <= ceil(r1)/floor(r2) => n <= div(ceil(r1), floor(r2))
-                //      p/q >= floor(r1)/ceil(r2) => n >= div(floor(r1), ceil(r2))
-                continue;
-            }
-
-
-            if (a.is_numeral(q, r2) && r2.is_pos()) {
-                if (!a.is_bounded(n)) {
-                    TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
-                    continue;
-                }
-                if (!is_registered_var(v))
-                    continue;
-                lp::impq val_v = get_ivalue(v);
-                if (val_v.y.is_zero() && val_v.x == div(r1.x, r2))
-                    continue;
-            
-                TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
-                rational div_r = div(r1.x, r2);
-                // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2)
-                // p >= q * div(r1, q) => div(r1, q) <= div(p, q)
-                rational mul(1);
-                rational hi = r2 * div_r + r2 - 1;
-                rational lo = r2 * div_r;
-
-                // used to normalize inequalities so they 
-                // don't appear as 8*x >= 15, but x >= 2
-                expr *n1 = nullptr, *n2 = nullptr;
-                if (a.is_mul(p, n1, n2) && a.is_extended_numeral(n1, mul) && mul.is_pos()) {
-                    p = n2;
-                    hi = floor(hi/mul);
-                    lo = ceil(lo/mul);
-                }
-                std::cout << mk_pp(p, m) << " " << mk_pp(n, m) << " " << hi << " " << lo << " " << div_r << "\n";
-                literal p_le_r1  = mk_literal(a.mk_le(p, a.mk_numeral(hi, true)));
-                literal p_ge_r1  = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
-                literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
-                literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
-                {
-                    scoped_trace_stream _sts(th, ~p_le_r1, n_le_div);
-                    mk_axiom(~p_le_r1, n_le_div);
-                }
-                {
-                    scoped_trace_stream _sts(th, ~p_ge_r1, n_ge_div);
-                    mk_axiom(~p_ge_r1, n_ge_div);
-                }
-
-                all_divs_valid = false;
-                ++count;
-
-
-                TRACE("arith",
-                      tout << r1 << " div " << r2 << "\n";
-                      literal_vector lits;
-                      lits.push_back(~p_le_r1);
-                      lits.push_back(n_le_div);
-                      ctx().display_literals_verbose(tout, lits) << "\n\n";
-                      lits[0] = ~p_ge_r1;
-                      lits[1] = n_ge_div;
-                      ctx().display_literals_verbose(tout, lits) << "\n";);                      
-                continue;
-            }
-        }
-        
-        return all_divs_valid;
+        m_nla_lemma_vector.reset();
+        m_nla->check_bounded_divisions(m_nla_lemma_vector);
+        for (auto & lemma : m_nla_lemma_vector)
+            false_case_of_check_nla(lemma);
+        return m_nla_lemma_vector.empty();         
     }
 
     expr_ref var2expr(lpvar v) {
@@ -2023,9 +2022,8 @@ public:
         lbool r = m_nla->check(m_nla_lemma_vector);
         switch (r) {
         case l_false: {
-            for (const nla::lemma & l : m_nla_lemma_vector) {
-                false_case_of_check_nla(l);
-            }
+            for (const nla::lemma & l : m_nla_lemma_vector) 
+                false_case_of_check_nla(l);            
             break;
         }
         case l_true:
@@ -2044,11 +2042,11 @@ public:
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        if (!m_nla) {
-            TRACE("arith", tout << "no nla\n";);
+        CTRACE("arith",!m_nla, tout << "no nla\n";);
+        if (!m_nla)            
+            return l_true;        
+        if (!m_nla->need_check()) 
             return l_true;
-        }
-        if (!m_nla->need_check()) return l_true;
         return check_nla_continue();
     }
 

src/smt/theory_recfun.cpp

@@ -102,9 +102,8 @@ namespace smt {
     void theory_recfun::relevant_eh(app * n) {
         SASSERT(ctx.relevancy());
         // TRACEFN("relevant_eh: (defined) " <<  u().is_defined(n) << " " << mk_pp(n, m));        
-        if (u().is_defined(n) && u().has_defs()) {
+        if (u().is_defined(n) && u().has_defs()) 
             push_case_expand(n);
-        }
     }
 
     void theory_recfun::push_scope_eh() {
@@ -250,7 +249,7 @@ namespace smt {
             expr_ref eq1(m.mk_eq(l, r), m);
             expr_ref fn(m.mk_fresh_const("rec-eq", m.mk_bool_sort()), m);
             expr_ref eq(m.mk_eq(fn, eq1), m);
-            ctx.assert_expr(eq);
+            ctx.add_asserted(eq);
             ctx.internalize_assertions();
             lit = mk_literal(fn);
         }
@@ -418,7 +417,7 @@ namespace smt {
     }
 
     void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
-        if (u().has_defs() || !m_disabled_guards.empty()) {
+        if (u().has_rec_defs() || !m_disabled_guards.empty()) {
             app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
             TRACEFN("add_theory_assumption " << dlimit);
             assumptions.push_back(dlimit);

src/smt/theory_str.cpp

@@ -2470,10 +2470,8 @@ namespace smt {
                 TRACE("str", tout << "SKIP: both concats are already in the same equivalence class" << std::endl;);
             } else {
                 expr_ref_vector items(m);
-                int pos = 0;
                 for (auto itor : resolvedMap) {
                     items.push_back(ctx.mk_eq_atom(itor.first, itor.second));
-                    pos += 1;
                 }
                 expr_ref premise(mk_and(items), m);
                 expr_ref conclusion(ctx.mk_eq_atom(node, resultAst), m);
@@ -4539,6 +4537,7 @@ namespace smt {
             and_item.push_back(ctx.mk_eq_atom(mk_strlen(m),
                                               m_autil.mk_add(mk_strlen(str1Ast), mk_strlen(commonVar)) ));
             pos += 1;
+            (void)pos;
 
             //    addItems[0] = mk_length(t, commonVar);
             //    addItems[1] = mk_length(t, str2Ast);
@@ -6439,6 +6438,7 @@ namespace smt {
                             expr_ref arg2_eq (ctx.mk_eq_atom(arg2, suffixAst), m);
                             and_items.push_back(arg2_eq);
                             and_count += 1;
+                            (void) and_count;
 
                             arrangement_disjunction.push_back(mk_and(and_items));
                         }

src/smt/theory_user_propagator.cpp

@@ -249,7 +249,11 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
 
     // get unassigned variable from enode
     var = enode_to_bool(new_enode, new_bit);
-
+    
+    if (var == null_bool_var)
+        // selected variable is already assigned
+        throw default_exception("expression in \"decide\" is already assigned");
+    
     // in case the callback did not decide on a truth value -> let Z3 decide
     is_pos = ctx.guess(var, phase);
 }
@@ -319,10 +323,12 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
         ctx.set_conflict(js);
     }
     else {
+#if 1
         for (auto& lit : m_lits)
             lit.neg();
         for (auto const& [a,b] : m_eqs)
             m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
+#endif
         
         literal lit; 
         if (has_quantifiers(prop.m_conseq)) {
@@ -335,8 +341,20 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
         else 
             lit = mk_literal(prop.m_conseq);            
         ctx.mark_as_relevant(lit);
+
+#if 0
+        justification* js =
+            ctx.mk_justification(
+                ext_theory_propagation_justification(
+                    get_id(), ctx, m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit));
+
+        ctx.assign(lit, js);
+#endif
+        
+#if 1           
         m_lits.push_back(lit);
         ctx.mk_th_lemma(get_id(), m_lits);
+#endif
         TRACE("user_propagate", ctx.display(tout););
     }
 }

src/smt/theory_wmaxsat.h

@@ -21,7 +21,7 @@ Notes:
 
 #include "smt/smt_theory.h"
 #include "smt/smt_clause.h"
-#include "tactic/generic_model_converter.h"
+#include "ast/converters/generic_model_converter.h"
 
 namespace smt {
     class theory_wmaxsat : public theory {