build

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

src/ast/euf/euf_enode.h

@@ -150,6 +150,8 @@ namespace euf {
         theory_var get_th_var(theory_id id) const { return m_th_vars.find(id); }
         bool is_attached_to(theory_id id) const { return get_th_var(id) != null_theory_var; }
         bool has_th_vars() const { return !m_th_vars.empty(); }
+        bool has_one_th_var() const { return !m_th_vars.empty() && !m_th_vars.get_next();}
+        theory_var get_first_th_id() const { SASSERT(has_th_vars()); return m_th_vars.get_id(); }
 
         void inc_class_size(unsigned n) { m_class_size += n; }
         void dec_class_size(unsigned n) { m_class_size -= n; }

src/sat/smt/euf_internalize.cpp

@@ -23,7 +23,7 @@ namespace euf {
     void solver::internalize(expr* e, bool redundant) {
         if (si.is_bool_op(e))
             attach_lit(si.internalize(e, redundant), e);
-        else if (auto* ext = get_solver(e))
+        else if (auto* ext = expr2solver(e))
             ext->internalize(e, redundant);
         else
             visit_rec(m, e, false, false, redundant);
@@ -33,7 +33,7 @@ namespace euf {
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
         if (si.is_bool_op(e))
             return attach_lit(si.internalize(e, redundant), e);
-        if (auto* ext = get_solver(e))
+        if (auto* ext = expr2solver(e))
             return ext->internalize(e, sign, root, redundant);
         if (!visit_rec(m, e, sign, root, redundant))
             return sat::null_literal;
@@ -67,7 +67,7 @@ namespace euf {
             m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
         if (root && internalize_root(to_app(e), sign, m_args))
             return false;
-        if (auto* s = get_solver(e)) {
+        if (auto* s = expr2solver(e)) {
             s->internalize(e, m_is_redundant);
             return true;
         }
@@ -88,8 +88,8 @@ namespace euf {
             attach_lit(literal(si.add_bool_var(e), false), e);
 
         if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
-            auto* e_ext = get_solver(e);
+            auto* e_ext = expr2solver(e);
-            auto* s_ext = get_solver(m.get_sort(e));
+            auto* s_ext = sort2solver(m.get_sort(e));
             if (s_ext && s_ext != e_ext)
                 s_ext->apply_sort_cnstr(n, m.get_sort(e));
         }

src/sat/smt/euf_model.cpp

@@ -38,7 +38,7 @@ namespace euf {
             return true;
         if (f->get_family_id() == m.get_basic_family_id())
             return false;
-        euf::th_model_builder* mb = get_solver(f);
+        euf::th_model_builder* mb = func_decl2solver(f);
         return mb && mb->include_func_interp(f);
     }
 
@@ -48,7 +48,7 @@ namespace euf {
                 deps.insert(n, nullptr);
                 continue;
             }
-            auto* mb = get_solver(n->get_expr());
+            auto* mb = expr2solver(n->get_expr());
             if (mb)
                 mb->add_dep(n, deps);
             else
@@ -94,14 +94,14 @@ namespace euf {
                 }
                 continue;
             }
-            auto* mb = get_solver(e);
+            auto* mb = expr2solver(e);
             if (mb) 
                 mb->add_value(n, *mdl, values);
             else if (m.is_uninterp(m.get_sort(e))) {
                 expr* v = user_sort.get_fresh_value(m.get_sort(e));
                 values.set(id, v);
             }
-            else if ((mb = get_solver(m.get_sort(e))))
+            else if ((mb = sort2solver(m.get_sort(e))))
                 mb->add_value(n, *mdl, values);
             else {
                 IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");

src/sat/smt/euf_solver.cpp

@@ -53,18 +53,18 @@ namespace euf {
     /**
     * retrieve extension that is associated with Boolean variable.
     */
-    th_solver* solver::get_solver(sat::bool_var v) {
+    th_solver* solver::bool_var2solver(sat::bool_var v) {
         if (v >= m_var2expr.size())
             return nullptr;
         expr* e = m_var2expr[v];
         if (!e)
             return nullptr;
-        return get_solver(e);
+        return expr2solver(e);
     }
 
-    th_solver* solver::get_solver(expr* e) {
+    th_solver* solver::expr2solver(expr* e) {
         if (is_app(e)) 
-            return get_solver(to_app(e)->get_decl());        
+            return func_decl2solver(to_app(e)->get_decl());        
         return nullptr;
     }
 
@@ -112,7 +112,7 @@ namespace euf {
     }
 
     void solver::init_search() {
-        TRACE("euf", display(tout););
+        TRACE("before_search", s().display(tout););
     }
 
     bool solver::is_external(bool_var v) {
@@ -220,14 +220,30 @@ namespace euf {
         size_t* c = to_ptr(l);
         SASSERT(is_literal(c));
         SASSERT(l == get_literal(c));
-        if (m.is_eq(e) && !sign && n->num_args() == 2) {
+        if (m.is_eq(e) && n->num_args() == 2) {
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
-            m_egraph.merge(na, nb, c);
+            if (!sign) {
+                m_egraph.merge(na, nb, c);
+                return;
+            }
+            else 
+                new_diseq(na, nb, l);
         }
-        else {            
+        euf::enode* nb = sign ? mk_false() : mk_true();
-            euf::enode* nb = sign ? mk_false() : mk_true();
+        m_egraph.merge(n, nb, c);        
-            m_egraph.merge(n, nb, c);
+    }
+
+    void solver::new_diseq(enode* n1, enode* n2, literal lit) {
+        enode * r1 = n1->get_root();
+        enode * r2 = n2->get_root();
+        if (r1 == r2) 
+            return;
+        if (r1->has_one_th_var() && r2->has_one_th_var() && r1->get_first_th_id() == r2->get_first_th_id()) {
+            theory_id id = r1->get_first_th_id();
+            theory_var v1 = r1->get_th_var(id);
+            theory_var v2 = r2->get_th_var(id);
+            fid2solver(id)->new_diseq_eh(r1, r2);
         }
     }
 
@@ -412,7 +428,7 @@ namespace euf {
     }
 
     lbool solver::get_phase(bool_var v) { 
-        auto* ext = get_solver(v);
+        auto* ext = bool_var2solver(v);
         if (ext)
             return ext->get_phase(v);
         return l_undef; 

src/sat/smt/euf_solver.h

@@ -125,10 +125,11 @@ namespace euf {
 
         // extensions
         th_solver* get_solver(family_id fid, func_decl* f);
-        th_solver* get_solver(sort* s) { return get_solver(s->get_family_id(), nullptr); }
+        th_solver* sort2solver(sort* s) { return get_solver(s->get_family_id(), nullptr); }
-        th_solver* get_solver(func_decl* f) { return get_solver(f->get_family_id(), f); }
+        th_solver* func_decl2solver(func_decl* f) { return get_solver(f->get_family_id(), f); }
-        th_solver* get_solver(expr* e);
+        th_solver* expr2solver(expr* e);
-        th_solver* get_solver(sat::bool_var v);
+        th_solver* bool_var2solver(sat::bool_var v);
+        th_solver* fid2solver(family_id fid) { return m_id2solver.get(fid, nullptr); }
         void add_solver(family_id fid, th_solver* th);
         void init_ackerman();
 
@@ -143,6 +144,7 @@ namespace euf {
         void propagate_literals();
         void propagate_th_eqs();
         void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
+        void new_diseq(enode* a, enode* b, literal lit);
 
         // proofs
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);

src/sat/smt/sat_th.h

@@ -93,6 +93,10 @@ namespace euf {
 
         virtual void new_eq_eh(euf::th_eq const& eq) {}
 
+        virtual bool use_diseqs() const { return false; }
+
+        virtual void new_diseq_eh(euf::enode* a, euf::enode* b) {}
+
         /**
            \brief Parametric theories (e.g. Arrays) should implement this method.
         */

src/shell/drat_frontend.cpp

@@ -173,6 +173,7 @@ public:
         for (expr* arg : args) 
             sorts.push_back(m.get_sort(arg));
         sort_ref rng(m);
+        func_decl* f = nullptr;
         switch (sexpr->get_kind()) {
         case sexpr::kind_t::COMPOSITE: {
             unsigned sz = sexpr->get_num_children();
@@ -214,7 +215,7 @@ public:
         default:
             goto bail;
         }
-        func_decl* f = ctx.find_func_decl(name, params.size(), params.c_ptr(), args.size(), sorts.c_ptr(), rng.get());
+        f = ctx.find_func_decl(name, params.size(), params.c_ptr(), args.size(), sorts.c_ptr(), rng.get());
         if (!f) 
             goto bail;
         result = ctx.m().mk_app(f, args);

src/smt/smt_context_pp.cpp

@@ -178,14 +178,15 @@ namespace smt {
 
     std::ostream& context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
         for (clause* cp : v) {
-            display_clause_smt2(out, *cp);
+            out << "(";
-            out << "\n";
+            for (auto lit : *cp)
+                out << lit << " ";
+            out << ")\n";
         }
         return out;
     }
 
     std::ostream& context::display_binary_clauses(std::ostream & out) const {
-        bool first = true;
         unsigned l_idx = 0;
         for (watch_list const& wl : m_watches) {
             literal l1 = to_literal(l_idx++);
@@ -195,21 +196,13 @@ namespace smt {
             for (; it2 != end2; ++it2) {
                 literal l2 = *it2;
                 if (l1.index() < l2.index()) {
-                    if (first) {
+                    out << "(" << neg_l1 << " " << l2 << ")\n";
-                        out << "binary clauses:\n";
+#if 0
-                        first = false;
-                    }
                     expr_ref t1(m), t2(m);
                     literal2expr(neg_l1, t1);
                     literal2expr(l2, t2);
                     expr_ref disj(m.mk_or(t1, t2), m);
                     out << mk_bounded_pp(disj, m, 3) << "\n";
-#if 0
-                    out << "(clause ";
-                    display_literal(out, neg_l1);
-                    out << " ";
-                    display_literal(out, l2);
-                    out << ")\n";
 #endif
                 }
             }
@@ -327,6 +320,7 @@ namespace smt {
         display_bool_var_defs(out);
         display_enode_defs(out);
         display_asserted_formulas(out);
+        display_binary_clauses(out);
         if (!m_aux_clauses.empty()) {
             out << "auxiliary clauses:\n";
             display_clauses(out, m_aux_clauses);
@@ -335,7 +329,6 @@ namespace smt {
             out << "lemmas:\n";
             display_clauses(out, m_lemmas);
         }
-        display_binary_clauses(out);
         display_assignment(out);
         display_eqc(out);
         m_cg_table.display_compact(out);

src/smt/smt_literal.cpp

@@ -65,9 +65,9 @@ namespace smt {
         else if (l == false_literal)
             out << "false";
         else if (l.sign())
-            out << "(not p" << l.var() << ")";
+            out << "-" << l.var();
         else
-            out << "p" << l.var();
+            out << l.var();
         return out;
     }
 

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -30,6 +30,7 @@ Notes:
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "ackermannization/ackermannize_bv_tactic.h"
+#include "tactic/smtlogics/smt_tactic_select.h"
 
 #define MEMLIMIT 300
 
@@ -122,8 +123,8 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
 
 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
     tactic * new_sat = cond(mk_produce_proofs_probe(),
-                            and_then(mk_simplify_tactic(m), mk_smt_tactic(m)),
+                            and_then(mk_simplify_tactic(m), mk_smt_tactic_select(m, p)),
                             mk_psat_tactic(m, p));
-    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));
+    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic_select(m, p));
 
 }