add a way to use new smt core for selected logics

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

src/sat/sat_solver.cpp

@@ -995,6 +995,7 @@ namespace sat {
         literal l, not_l, l1, l2;
         lbool val1, val2;
         bool keep;
+    prop_again:
         while (m_qhead < m_trail.size()) {
             checkpoint();
             m_cleaner.dec();
@@ -1163,11 +1164,13 @@ namespace sat {
                 }
             }
             wlist.set_end(it2);
-            if (m_ext) {
+        }
-                m_ext->unit_propagate();
+        if (m_ext) {
-                if (inconsistent())
+            m_ext->unit_propagate();
-                    return false;
+            if (inconsistent())
-            }
+                return false;
+            if (m_qhead < m_trail.size())
+                goto prop_again;
         }
         SASSERT(m_qhead == m_trail.size());
         SASSERT(!m_inconsistent);
@@ -2665,7 +2668,7 @@ namespace sat {
         // at the backtracking level. This is the case where the external theories miss propagations
         // that only get triggered after decisions.
         
-        if (unique_max && !m_force_conflict_analysis) {
+        if (allow_backtracking() && unique_max && !m_force_conflict_analysis) {
             TRACE("sat", tout << "unique max " << js << " " << m_not_l << "\n";);
             pop_reinit(m_scope_lvl - m_conflict_lvl + 1);
             m_force_conflict_analysis = true;
@@ -2748,6 +2751,14 @@ namespace sat {
                 fill_ext_antecedents(consequent, js, false);
                 for (literal l : m_ext_antecedents) 
                     process_antecedent(l, num_marks);
+#if 0
+                if (m_ext_antecedents.size() <= 1) {
+                    for (literal& l : m_ext_antecedents) 
+                        l.neg();
+                    m_ext_antecedents.push_back(consequent);
+                    mk_clause(m_ext_antecedents.size(), m_ext_antecedents.c_ptr(), sat::status::redundant());
+                }
+#endif
                 break;
             }
             default:
@@ -2852,11 +2863,14 @@ namespace sat {
         updt_phase_counters();
     }
 
-    bool solver::use_backjumping(unsigned num_scopes) {
+    bool solver::use_backjumping(unsigned num_scopes) const {
         return 
             num_scopes > 0 && 
-            (num_scopes <= m_config.m_backtrack_scopes || 
+            (num_scopes <= m_config.m_backtrack_scopes || !allow_backtracking());
-             m_conflicts_since_init <= m_config.m_backtrack_init_conflicts);
+    }
+
+    bool solver::allow_backtracking() const {
+        return m_conflicts_since_init > m_config.m_backtrack_init_conflicts;
     }
 
     void solver::process_antecedent_for_unsat_core(literal antecedent) {

src/sat/sat_solver.h

@@ -574,7 +574,8 @@ namespace sat {
         unsigned       m_conflict_lvl;
         literal_vector m_lemma;
         literal_vector m_ext_antecedents;
-        bool use_backjumping(unsigned num_scopes);
+        bool use_backjumping(unsigned num_scopes) const;
+        bool allow_backtracking() const;
         bool resolve_conflict();
         lbool resolve_conflict_core();
         void learn_lemma_and_backjump();

src/tactic/smtlogics/CMakeLists.txt

@@ -13,6 +13,7 @@ z3_add_component(smtlogic_tactics
     qfufbv_tactic.cpp
     qfuf_tactic.cpp
     quant_tactics.cpp
+    smt_tactic_select.cpp
   COMPONENT_DEPENDENCIES
     ackermannization
     aig_tactic

src/tactic/smtlogics/qfaufbv_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
+#include "tactic/smtlogics/smt_tactic_select.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
 #include "smt/tactic/smt_tactic.h"
 
@@ -59,7 +60,7 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * st = using_params(
         and_then(preamble_st, 
-                 cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m))), main_p);
+                 cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic_select(m, p))), main_p);
     
     st->updt_params(p);
     return st;

src/tactic/smtlogics/qfuf_tactic.cpp

@@ -23,6 +23,7 @@ Notes:
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "smt/tactic/smt_tactic.h"
+#include "tactic/smtlogics/smt_tactic_select.h"
 
 tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
     params_ref s2_p;
@@ -34,7 +35,7 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
                     mk_solve_eqs_tactic(m, p),
                     using_params(mk_simplify_tactic(m, p), s2_p),
                     if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))),
-                    mk_smt_tactic(m, p));
+                    mk_smt_tactic_select(m, p));
 }
 
                     

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -37,6 +37,7 @@ Notes:
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "tactic/smtlogics/qfaufbv_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
+#include "tactic/smtlogics/smt_tactic_select.h"
 #include "solver/tactic2solver.h"
 #include "tactic/bv/bv_bound_chk_tactic.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
@@ -181,8 +182,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * const preamble_st = mk_qfufbv_preamble(m, p);
 
-    tactic * st = using_params(and_then(preamble_st,
+    tactic * st = using_params(
-        cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m))),
+        and_then(preamble_st,
+                 cond(mk_is_qfbv_probe(), 
+                      mk_qfbv_tactic(m), 
+                      mk_smt_tactic_select(m, p))),
         main_p);
 
     st->updt_params(p);
@@ -194,5 +198,5 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
     return and_then(preamble_t,
-        cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m)));
+                    cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic_select(m, p)));
 }

src/tactic/smtlogics/smt_tactic_select.cpp

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_tactic_select.cpp
+
+Abstract:
+
+    Tactic that selects SMT backend.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-14
+
+
+--*/
+#include "smt/tactic/smt_tactic.h"
+#include "sat/tactic/sat_tactic.h"
+#include "sat/sat_params.hpp"
+
+tactic * mk_smt_tactic_select(ast_manager & m, params_ref const & p) {
+    sat_params sp(p);
+    return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic(m, p);
+}
+

src/tactic/smtlogics/smt_tactic_select.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_tactic_select.h
+
+Abstract:
+
+    Tactic that selects SMT backend.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-14
+
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_smt_tactic_select(ast_manager & m, params_ref const & p);
+