strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params

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

src/nlsat/tactic/qfnra_nlsat_tactic.cpp

@@ -42,26 +42,28 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
     else
         factor = mk_skip_tactic();
 
-    return and_then(and_then(using_params(mk_simplify_tactic(m, p),
+    return and_then(
-                                          main_p),
+        mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10),
-                             using_params(mk_purify_arith_tactic(m, p),
+        and_then(using_params(mk_simplify_tactic(m, p),
-                                          purify_p),
+                              main_p),
-                             mk_propagate_values_tactic(m, p),
+                 using_params(mk_purify_arith_tactic(m, p),
-                             mk_solve_eqs_tactic(m, p),
+                              purify_p),
-                             using_params(mk_purify_arith_tactic(m, p),
+                 mk_propagate_values_tactic(m, p),
-                                          purify_p),
+                 mk_solve_eqs_tactic(m, p),
-                             mk_elim_uncnstr_tactic(m, p),
+                 using_params(mk_purify_arith_tactic(m, p),
-                             mk_elim_term_ite_tactic(m, p)),
+                              purify_p),
-                    and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
+                 mk_elim_uncnstr_tactic(m, p),
-                             factor,
+                 mk_elim_term_ite_tactic(m, p)),
-                             mk_solve_eqs_tactic(m, p),
+        and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
-                             using_params(mk_purify_arith_tactic(m, p),
+            factor,
-                                          purify_p),
+            mk_solve_eqs_tactic(m, p),
-                             using_params(mk_simplify_tactic(m, p),
+            using_params(mk_purify_arith_tactic(m, p),
-                                          main_p),
+                         purify_p),
-                             mk_tseitin_cnf_core_tactic(m, p),
+            using_params(mk_simplify_tactic(m, p),
-                             using_params(mk_simplify_tactic(m, p),
+                         main_p),
-                                          main_p),
+            mk_tseitin_cnf_core_tactic(m, p),
-                             mk_nlsat_tactic(m, p)));
+            using_params(mk_simplify_tactic(m, p),
+                         main_p),
+            mk_nlsat_tactic(m, p)));
 }
 

src/smt/smt_setup.cpp

@@ -492,7 +492,7 @@ namespace smt {
         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.m_nnf_cnf             = false;        
         setup_lra_arith();
     }
 

src/smt/theory_lra.cpp

@@ -298,13 +298,15 @@ class theory_lra::imp {
 
     void init_solver() {
         if (m_solver) return;
-        lp_params lp(ctx().get_params());
+
-        m_solver = alloc(lp::lar_solver); 
+        reset_variable_values();
         m_theory_var2var_index.reset();
+        m_solver = alloc(lp::lar_solver); 
+        lp_params lp(ctx().get_params());
         m_solver->settings().set_resource_limit(m_resource_limit);
         m_solver->settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lp.simplex_strategy());
-        reset_variable_values();
         m_solver->settings().bound_propagation() = BP_NONE != propagation_mode();
+        m_solver->settings().m_enable_hnf = lp.enable_hnf();
         m_solver->set_track_pivoted_rows(lp.bprop_on_pivoted_rows());
 
         // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
@@ -2712,7 +2714,6 @@ public:
         if (dump_lemmas()) {
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
             (void)id;
-            //SASSERT(id != 55);
         }
     }
 
@@ -2732,7 +2733,6 @@ public:
         if (dump_lemmas()) {                
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
             (void)id;
-            // SASSERT(id != 71);
         }
     }
 

src/tactic/arith/probe_arith.cpp

@@ -127,6 +127,43 @@ public:
     }
 };
 
+struct has_nlmul {
+    struct found {};
+    ast_manager& m;
+    arith_util   a;
+    has_nlmul(ast_manager& m):m(m), a(m) {}
+    
+    void throw_found(expr* e) {
+        TRACE("probe", tout << expr_ref(e, m) << ": " << sort_ref(m.get_sort(e), m) << "\n";);
+        SASSERT(false);
+        throw found();
+    }
+
+    void operator()(var *) { }
+
+    void operator()(quantifier *) { }
+
+    void operator()(app * n) {
+        family_id fid = n->get_family_id();
+        if (fid == a.get_family_id()) {
+            switch (n->get_decl_kind()) {
+            case OP_MUL:
+                if (n->get_num_args() != 2 || !a.is_numeral(n->get_arg(0)))
+                    throw_found(n);
+                break;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (!a.is_numeral(n->get_arg(1)))
+                    throw_found(n);
+				break;
+            case OP_POWER:
+                throw_found(n);
+            default:
+                break;
+            }
+        }
+    }
+};
+
 probe * mk_arith_avg_degree_probe() {
     return alloc(arith_degree_probe, true);
 }
@@ -441,13 +478,13 @@ struct is_non_nira_functor {
                 if (m_linear) {
                     if (n->get_num_args() != 2)
                         throw_found(n);
-                    if (!u.is_numeral(n->get_arg(0)))
+                    if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1))) 
                         throw_found(n);
                 }
                 return;
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
                 if (m_linear && !u.is_numeral(n->get_arg(1)))
-                    throw_found(n);
+                    throw_found(n); 
                 return;
             case OP_IS_INT:
                 if (m_real)
@@ -478,27 +515,27 @@ struct is_non_nira_functor {
 
 static bool is_qfnia(goal const & g) {
     is_non_nira_functor p(g.m(), true, false, false, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_qfnra(goal const & g) {
     is_non_nira_functor p(g.m(), false, true, false, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nia(goal const & g) {
     is_non_nira_functor p(g.m(), true, false, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nra(goal const & g) {
     is_non_nira_functor p(g.m(), false, true, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_nira(goal const & g) {
     is_non_nira_functor p(g.m(), true, true, true, false);
-    return !test(g, p);
+    return !test(g, p) && test<has_nlmul>(g);
 }
 
 static bool is_lra(goal const & g) {
@@ -560,12 +597,16 @@ struct is_non_qfufnra_functor {
                 }
                 return;
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
-                if (!u.is_numeral(n->get_arg(1)))
+                if (!u.is_numeral(n->get_arg(1))) {
+                    TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                     throw_found();
+                }
                 return;
             case OP_POWER: 
-                if (!u.is_numeral(n->get_arg(1)))
+                if (!u.is_numeral(n->get_arg(1))) {
+                    TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                     throw_found();
+                }
                 m_has_nonlinear = true;
                 return;
             case OP_IS_INT:
@@ -574,6 +615,7 @@ struct is_non_qfufnra_functor {
                 throw_found();
                 return;
             default:
+                TRACE("arith", tout << "non-linear " << expr_ref(n, m) << "\n";);
                 throw_found();
             }
         } 

src/tactic/fpa/qffplra_tactic.cpp

@@ -26,6 +26,23 @@ tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) {
     return st;
 }
 
+struct is_fpa_function {
+    struct found {};
+    ast_manager & m;
+    fpa_util      fu;
+    
+    is_fpa_function(ast_manager & _m) : m(_m), fu(m) {}
+
+    void operator()(var *) { }
+
+    void operator()(quantifier *) { }
+
+    void operator()(app * n) {
+        if (n->get_family_id() == fu.get_family_id()) 
+            throw found();
+    }
+};
+
 struct is_non_qffplra_predicate {
     struct found {};
     ast_manager & m;
@@ -61,7 +78,9 @@ struct is_non_qffplra_predicate {
 class is_qffplra_probe : public probe {
 public:
     result operator()(goal const & g) override {
-        return !test<is_non_qffplra_predicate>(g);
+        return 
+            test<is_fpa_function>(g) && 
+            !test<is_non_qffplra_predicate>(g);
     }
 
     ~is_qffplra_probe() override {}

src/tactic/smtlogics/qfnia_tactic.cpp

@@ -110,9 +110,11 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
 
 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
 
-    return and_then(mk_qfnia_premable(m, p),
+    return and_then(
-                    or_else(mk_qfnia_sat_solver(m, p),
+        mk_report_verbose_tactic("(qfnia-tactic)", 10),
-                            try_for(mk_qfnia_smt_solver(m, p), 2000),
+        mk_qfnia_premable(m, p),
-                            mk_qfnia_nlsat_solver(m, p),
+        or_else(mk_qfnia_sat_solver(m, p),
-                            mk_qfnia_smt_solver(m, p)));
+                try_for(mk_qfnia_smt_solver(m, p), 2000),
+                mk_qfnia_nlsat_solver(m, p),
+                mk_qfnia_smt_solver(m, p)));
 }

src/util/lp/int_solver.cpp

@@ -600,6 +600,9 @@ lia_move int_solver::make_hnf_cut() {
 }
 
 lia_move int_solver::hnf_cut() {
+    if (!settings().m_enable_hnf) {
+        return lia_move::undef;
+    }
     if ((m_number_of_calls) % settings().hnf_cut_period() == 0) {
         return make_hnf_cut();
     }

src/util/lp/lp_params.pyg

@@ -5,6 +5,7 @@ def_module_params('lp',
                    ('min', BOOL, False, 'minimize cost'),
                    ('print_stats', BOOL, False, 'print statistic'),
                    ('simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
+                   ('enable_hnf', BOOL, True, 'enable hnf cuts'),
                    ('bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation')
                           ))           
 

src/util/lp/lp_settings.h

@@ -197,6 +197,7 @@ public:
     bool             m_int_patch_only_integer_values;
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
+    bool             m_enable_hnf;
 
 
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }
@@ -263,7 +264,8 @@ public:
                     m_int_pivot_fixed_vars_from_basis(false),
                     m_int_patch_only_integer_values(true),
                     limit_on_rows_for_hnf_cutter(75),
-                    limit_on_columns_for_hnf_cutter(150)
+                    limit_on_columns_for_hnf_cutter(150),
+                    m_enable_hnf(true)
     {}
 
     void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }