add simplification with qe-lite as an option #5767

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

src/qe/lite/qe_lite.h

@@ -60,6 +60,8 @@ public:
         \brief full rewriting based light-weight quantifier elimination round.
     */
     void operator()(expr_ref& fml, proof_ref& pr);
+
+    void operator()(expr* fml, expr_ref& result, proof_ref& pr) { result = fml; (*this)(result, pr); }
 };
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());

src/sat/smt/pb_solver.cpp

@@ -1403,8 +1403,10 @@ namespace pb {
             if (m_solver) m_solver->set_external(lit.var());
             c->watch_literal(*this, lit);
             c->watch_literal(*this, ~lit);
-        }        
+        }     
-        SASSERT(c->well_formed());
+        if (!c->well_formed()) 
+            std::cout << *c << "\n";
+        VERIFY(c->well_formed());
         if (m_solver && m_solver->get_config().m_drat) {
             std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
                 out << "c ba constraint " << *c << " 0\n";

src/smt/params/qi_params.cpp

@@ -28,6 +28,7 @@ void qi_params::updt_params(params_ref const & _p) {
     m_mbqi_trace = p.mbqi_trace();
     m_mbqi_force_template = p.mbqi_force_template();
     m_mbqi_id = p.mbqi_id();
+    m_qe_lite = p.q_lite();
     m_qi_profile = p.qi_profile();
     m_qi_profile_freq = p.qi_profile_freq();
     m_qi_max_instances = p.qi_max_instances();

src/smt/params/qi_params.h

@@ -30,26 +30,27 @@ enum quick_checker_mode {
 struct qi_params {
     std::string        m_qi_cost;
     std::string        m_qi_new_gen;
-    double             m_qi_eager_threshold;
+    double             m_qi_eager_threshold = 10.0;
-    double             m_qi_lazy_threshold;
+    double             m_qi_lazy_threshold = 20.0;
-    unsigned           m_qi_max_eager_multipatterns;
+    unsigned           m_qi_max_eager_multipatterns = 0;
-    unsigned           m_qi_max_lazy_multipattern_matching;
+    unsigned           m_qi_max_lazy_multipattern_matching = 2;
-    bool               m_qi_profile;
+    bool               m_qi_profile = false;
-    unsigned           m_qi_profile_freq;
+    unsigned           m_qi_profile_freq = UINT_MAX;
-    quick_checker_mode m_qi_quick_checker;
+    quick_checker_mode m_qi_quick_checker = MC_NO;
-    bool               m_qi_lazy_quick_checker;
+    bool               m_qi_lazy_quick_checker = true;
-    bool               m_qi_promote_unsat;
+    bool               m_qi_promote_unsat = true;
-    unsigned           m_qi_max_instances;
+    unsigned           m_qi_max_instances = UINT_MAX;
-    bool               m_qi_lazy_instantiation;
+    bool               m_qi_lazy_instantiation = false;
-    bool               m_qi_conservative_final_check;
+    bool               m_qi_conservative_final_check = false;
+    bool               m_qe_lite = false;
 
-    bool               m_mbqi;
+    bool               m_mbqi = true;
-    unsigned           m_mbqi_max_cexs;
+    unsigned           m_mbqi_max_cexs = 1;
-    unsigned           m_mbqi_max_cexs_incr;
+    unsigned           m_mbqi_max_cexs_incr = 1;
-    unsigned           m_mbqi_max_iterations;
+    unsigned           m_mbqi_max_iterations = 1000;
-    bool               m_mbqi_trace;
+    bool               m_mbqi_trace = false;
-    unsigned           m_mbqi_force_template;
+    unsigned           m_mbqi_force_template = 10;
-    const char *       m_mbqi_id;
+    const char *       m_mbqi_id = nullptr;
 
     qi_params(params_ref const & p = params_ref()):
         /*
@@ -78,26 +79,7 @@ struct qi_params {
           matching loop detection.
         */
         m_qi_cost("(+ weight generation)"),
-        m_qi_new_gen("cost"), 
+        m_qi_new_gen("cost") 
-        m_qi_eager_threshold(10.0),
-        m_qi_lazy_threshold(20.0), // reduced to give a chance to MBQI
-        m_qi_max_eager_multipatterns(0),
-        m_qi_max_lazy_multipattern_matching(2),
-        m_qi_profile(false),
-        m_qi_profile_freq(UINT_MAX),
-        m_qi_quick_checker(MC_NO),
-        m_qi_lazy_quick_checker(true),
-        m_qi_promote_unsat(true),
-        m_qi_max_instances(UINT_MAX),
-        m_qi_lazy_instantiation(false),
-        m_qi_conservative_final_check(false),
-        m_mbqi(true), // enabled by default
-        m_mbqi_max_cexs(1),
-        m_mbqi_max_cexs_incr(1),
-        m_mbqi_max_iterations(1000),
-        m_mbqi_trace(false),
-        m_mbqi_force_template(10),
-        m_mbqi_id(nullptr)
     {
         updt_params(p);
     }

src/smt/params/smt_params_helper.pyg

@@ -35,6 +35,7 @@ def_module_params(module_name='smt',
                           ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
                           ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'),
                           ('q.lift_ite', UINT, 0, '0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers'),
+                          ('q.lite', BOOL, False, 'Use cheap quantifier elimination during pre-processing'),
                           ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
                           ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
                           ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),

src/solver/assertions/CMakeLists.txt

@@ -4,4 +4,5 @@ z3_add_component(solver_assertions
   COMPONENT_DEPENDENCIES
     smt2parser
     smt_params
+    qe_lite
 )

src/solver/assertions/asserted_formulas.cpp

@@ -49,6 +49,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re
     m_refine_inj_axiom(*this),
     m_max_bv_sharing_fn(*this),
     m_elim_term_ite(*this),
+    m_qe_lite(*this),
     m_pull_nested_quantifiers(*this),
     m_elim_bvs_from_quantifiers(*this),
     m_cheap_quant_fourier_motzkin(*this),
@@ -285,6 +286,7 @@ void asserted_formulas::reduce() {
     m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
     if (!invoke(m_ng_lift_ite)) return;
     if (!invoke(m_elim_term_ite)) return;
+    if (!invoke(m_qe_lite)) return;
     if (!invoke(m_refine_inj_axiom)) return;
     if (!invoke(m_distribute_forall)) return;
     if (!invoke(m_find_macros)) return;

src/solver/assertions/asserted_formulas.h

@@ -37,6 +37,7 @@ Revision History:
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/pattern/pattern_inference.h"
 #include "smt/params/smt_params.h"
+#include "qe/lite/qe_lite.h"
 
 
 class asserted_formulas {
@@ -190,6 +191,8 @@ class asserted_formulas {
     MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true);
     MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true);
 
+    MK_SIMPLIFIERA(qe_lite_fn, qe_lite, "qe-lite", af.m_smt_params.m_qe_lite && af.has_quantifiers(), (af.m, af.m_params), true);
+
 
     reduce_asserted_formulas_fn m_reduce_asserted_formulas;
     distribute_forall_fn        m_distribute_forall;
@@ -197,6 +200,7 @@ class asserted_formulas {
     refine_inj_axiom_fn         m_refine_inj_axiom;
     max_bv_sharing_fn           m_max_bv_sharing_fn;
     elim_term_ite_fn            m_elim_term_ite;
+    qe_lite_fn                  m_qe_lite;
     pull_nested_quantifiers     m_pull_nested_quantifiers;
     elim_bvs_from_quantifiers   m_elim_bvs_from_quantifiers;
     cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;