fix #2774

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

src/ast/rewriter/array_rewriter.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "ast/ast_lt.h"
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/rewriter/var_subst.h"
 
 void array_rewriter::updt_params(params_ref const & _p) {
@@ -74,9 +75,9 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     CTRACE("array_rewriter", st != BR_FAILED, 
            tout << mk_pp(f, m()) << "\n";
            for (unsigned i = 0; i < num_args; ++i) {
-               tout << mk_pp(args[i], m()) << "\n";
+               tout << mk_bounded_pp(args[i], m(), 2) << "\n";
            }
-           tout << "\n --> " << result << "\n";);
+           tout << "\n --> " << mk_bounded_pp(result, m(), 2) << "\n";);
     return st;
 }
 
@@ -178,7 +179,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
             return BR_REWRITE1;
         }
         default:
-            if (m_expand_select_store) {
+            if (m_expand_select_store && to_app(args[0])->get_arg(0)->get_ref_count() == 1) {
                 // select(store(a, I, v), J) --> ite(I=J, v, select(a, J))
                 ptr_buffer<expr> new_args;
                 new_args.push_back(to_app(args[0])->get_arg(0));
@@ -632,7 +633,7 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
 }
 
 bool array_rewriter::is_expandable_store(expr* s) {
-    unsigned count = s->get_ref_count();
+    unsigned count = 0;
     unsigned depth = 0;
     while (m_util.is_store(s)) {
         s = to_app(s)->get_arg(0);
@@ -675,7 +676,7 @@ expr_ref array_rewriter::expand_store(expr* s) {
 }
 
 br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
-    TRACE("array_rewriter", tout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";);
+    TRACE("array_rewriter", tout << mk_bounded_pp(lhs, m(), 2) << " " << mk_bounded_pp(rhs, m(), 2) << "\n";);
     expr* v = nullptr;
     if (m_util.is_const(rhs) && is_lambda(lhs)) {
         std::swap(lhs, rhs);

src/smt/smt_context.cpp

@@ -4312,9 +4312,12 @@ namespace smt {
             theory_id th_id     = l->get_th_id();
 
             for (enode * parent : enode::parents(n)) {
-                family_id fid = parent->get_owner()->get_family_id();
+                app* p = parent->get_owner();
+                family_id fid = p->get_family_id();
                 if (fid != th_id && fid != m.get_basic_family_id()) {
-                    TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";);
+                    TRACE("is_shared", tout << enode_pp(n, *this) 
+                          << "\nis shared because of:\n" 
+                          << enode_pp(parent, *this) << "\n";);
                     return true;
                 }
             }

src/smt/smt_internalizer.cpp

@@ -789,7 +789,7 @@ namespace smt {
                  false /* CC is not enabled */);
         internalize(c, true);
         internalize(t, false);
-        internalize(e, false);
+        internalize(e, false);        
         internalize(eq1, true);
         internalize(eq2, true);
         literal c_lit   = get_literal(c);

src/smt/smt_model_generator.cpp

@@ -430,6 +430,10 @@ namespace smt {
                           tout << "#" << n->get_arg(i)->get_owner_id() << " ";
                       }
                       tout << "\n";
+                      for (expr* arg : args) {
+                          tout << mk_pp(arg, m) << " ";
+                      }
+                      tout << "\n";
                       tout << "value: #" << n->get_owner_id() << "\n" << mk_ismt2_pp(result, m) << "\n";);
                 if (fi->get_entry(args.c_ptr()) == nullptr)
                     fi->insert_new_entry(args.c_ptr(), result);

src/smt/theory_diff_logic.h

@@ -169,7 +169,7 @@ namespace smt {
         arith_eq_adapter               m_arith_eq_adapter;
         theory_diff_logic_statistics   m_stats;
         Graph                          m_graph;
-        theory_var                     m_zero; // cache the variable representing the zero variable.
+        theory_var                     m_izero, m_rzero; // cache the variable representing the zero variable.
         int_vector                     m_scc_id;                  // Cheap equality propagation
         eq_prop_info_set               m_eq_prop_info_set;        // set of existing equality prop infos
         ptr_vector<eq_prop_info>       m_eq_prop_infos;
@@ -226,7 +226,8 @@ namespace smt {
             m_params(params),
             m_util(m),
             m_arith_eq_adapter(*this, params, m_util),
-            m_zero(null_theory_var),
+            m_izero(null_theory_var),
+            m_rzero(null_theory_var),
             m_terms(m),
             m_asserted_qhead(0),
             m_num_core_conflicts(0),
@@ -374,7 +375,7 @@ namespace smt {
 
         void get_implied_bound_antecedents(edge_id bridge_edge, edge_id subsumed_edge, conflict_resolution & cr);
 
-        theory_var get_zero() const { return m_zero; }
+        theory_var get_zero(bool is_int) const { return is_int ? m_izero : m_rzero; }
 
         void inc_conflicts();
 

src/smt/theory_diff_logic_def.h

@@ -71,7 +71,12 @@ void theory_diff_logic<Ext>::init(context * ctx) {
     zero = m_util.mk_numeral(rational(0), true);
     e = ctx->mk_enode(zero, false, false, true);
     SASSERT(!is_attached_to_var(e));
-    m_zero = mk_var(e);
+    m_izero = mk_var(e);
+
+    zero = m_util.mk_numeral(rational(0), false);
+    e = ctx->mk_enode(zero, false, false, true);
+    SASSERT(!is_attached_to_var(e));
+    m_rzero = mk_var(e);
 }
 
 
@@ -207,7 +212,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
     }
     else {
         target = mk_var(lhs);
-        source = get_zero();
+        source = get_zero(m_util.is_int(lhs));
     }
 
     if (is_ge) {
@@ -360,7 +365,8 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
 
     TRACE("arith_final", display(tout); );
     // either will already be zero (as we don't do mixed constraints).
-    m_graph.set_to_zero(m_zero);
+    m_graph.set_to_zero(m_izero);
+    m_graph.set_to_zero(m_rzero);
     SASSERT(is_consistent());
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
@@ -751,22 +757,7 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
         m_graph.enable_edge(m_graph.add_edge(target, source, -k, null_literal));        
         return target;
     }
-    else if (m_util.is_add(n)) {
+    else if (m_util.is_arith_expr(n)) {
-        return null_theory_var;
-    }
-    else if (m_util.is_mul(n)) {
-        return null_theory_var;
-    }
-    else if (m_util.is_div(n)) {
-        return null_theory_var;
-    }
-    else if (m_util.is_idiv(n)) {
-        return null_theory_var;
-    }
-    else if (m_util.is_mod(n)) {
-        return null_theory_var;
-    }
-    else if (m_util.is_rem(n)) {
         return null_theory_var;
     }
     else {
@@ -781,7 +772,7 @@ theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
     enode* e = nullptr;
     context& ctx = get_context();
     if (r.is_zero()) {
-        v = get_zero();
+        v = get_zero(m_util.is_int(n));
     }
     else if (ctx.e_internalized(n)) {
         e = ctx.get_enode(n);
@@ -789,7 +780,7 @@ theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
         SASSERT(v != null_theory_var);
     }
     else {
-        theory_var zero = get_zero();
+        theory_var zero = get_zero(m_util.is_int(n));
         SASSERT(n->get_num_args() == 0);
         e = ctx.mk_enode(n, false, false, true);
         v = mk_var(e);
@@ -847,7 +838,8 @@ void theory_diff_logic<Ext>::reset_eh() {
         dealloc(m_atoms[i]);
     }
     m_graph            .reset();
-    m_zero              = null_theory_var;
+    m_izero              = null_theory_var;
+    m_rzero              = null_theory_var;
     m_atoms            .reset();
     m_asserted_atoms   .reset();
     m_stats            .reset();
@@ -1128,8 +1120,8 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
         S.set_value(node2simplex(i), q);
         inf_mgr.del(q);
     }
-    S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
+    S.set_lower(node2simplex(get_zero(true)), mpq_inf(mpq(0), mpq(0)));
-    S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
+    S.set_upper(node2simplex(get_zero(true)), mpq_inf(mpq(0), mpq(0)));
     svector<unsigned> vars;
     scoped_mpq_vector coeffs(mgr);
     coeffs.push_back(mpq(1));

src/tactic/fd_solver/smtfd_solver.cpp

@@ -138,8 +138,17 @@ Note:
 
 namespace smtfd {
 
+    struct stats {
+        unsigned m_num_lemmas;
+        unsigned m_num_rounds;
+        unsigned m_num_mbqi;
+        unsigned m_num_fresh_bool;
+        stats() { memset(this, 0, sizeof(stats)); }
+    };
+
     class smtfd_abs {
         ast_manager&    m;
+        stats&          m_stats;
         expr_ref_vector m_abs, m_rep, m_atoms, m_atom_defs; // abstraction and representation maps
         array_util      m_autil;
         bv_util         m_butil;
@@ -166,6 +175,7 @@ namespace smtfd {
         expr* fresh_var(expr* t) {
             symbol name = is_app(t) ? to_app(t)->get_name() : (is_quantifier(t) ? symbol("Q") : symbol("X"));
             if (m.is_bool(t)) {
+                ++m_stats.m_num_fresh_bool;
                 return m.mk_fresh_const(name, m.mk_bool_sort());
             }        
             else if (m_butil.is_bv(t)) {
@@ -207,8 +217,9 @@ namespace smtfd {
         }
         
     public:
-        smtfd_abs(ast_manager& m):
+        smtfd_abs(ast_manager& m, stats& s):
             m(m),
+            m_stats(s),
             m_abs(m),
             m_rep(m),
             m_atoms(m),
@@ -335,7 +346,8 @@ namespace smtfd {
                 }
                 if (is_atom(r) && !is_uninterp_const(r)) {
                     expr* rr = fresh_var(r);
-                    m_atom_defs.push_back(m.mk_iff(rr, r));
+                    m_atom_defs.push_back(m.mk_implies(rr, r));
+                    m_atom_defs.push_back(m.mk_implies(r, rr));
                     r = rr;
                 }
                 push_trail(m_abs, m_abs_trail, t, r);
@@ -919,6 +931,7 @@ namespace smtfd {
         void check_select(app* t) {
             expr* a = t->get_arg(0);
             expr_ref vA = eval_abs(a);
+            TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
             enforce_congruence(vA, t, m.get_sort(a));                                 
         }
 
@@ -958,13 +971,18 @@ namespace smtfd {
             for (unsigned i = 1; i < t->get_num_args(); ++i) {
                 expr* arg1 = t->get_arg(i);
                 expr* arg2 = store->get_arg(i);
-                if (arg1 == arg2) continue;
-                expr_ref v1 = eval_abs(arg1);
-                expr_ref v2 = eval_abs(arg2);
                 m_args.push_back(arg1);
-                eqs.push_back(m.mk_eq(arg1, arg2));
+                if (arg1 == arg2) {
+                    // skip
+                }
+                else if (m.are_distinct(arg1, arg2)) {
+                    eqs.push_back(m.mk_false());
+                }
+                else {
+                    eqs.push_back(m.mk_eq(arg1, arg2));
+                }
             }
-            if (eqs.empty()) return;
+            //if (eqs.empty()) return;
             expr_ref eq = mk_and(eqs);
             expr_ref eqV = eval_abs(eq);
             expr_ref val1 = eval_abs(t);
@@ -1024,9 +1042,10 @@ namespace smtfd {
         // 
         void reconcile_stores(app* t, expr* vT, table& tT, expr* vA, table& tA) {
             unsigned r = 0;
-            if (get_lambda(vA) <= 1) {
+            //if (get_lambda(vA) <= 1) {
-                return;
+            //    return;
-            }
+            //}
+            //std::cout << get_lambda(vA) << " " << get_lambda(vT) << "\n";
             inc_lambda(vT);
             for (auto& fA : tA) {
                 f_app fT;
@@ -1581,17 +1600,10 @@ namespace smtfd {
         }
     };
 
-
-    struct stats {
-        unsigned m_num_lemmas;
-        unsigned m_num_rounds;
-        unsigned m_num_mbqi;
-        stats() { memset(this, 0, sizeof(stats)); }
-    };
-
     class solver : public solver_na2as {
+        stats           m_stats;
         ast_manager&    m;
-        mutable smtfd_abs       m_abs;
+        mutable smtfd_abs m_abs;
         unsigned        m_indent;
         plugin_context  m_context;
         uf_plugin       m_uf;
@@ -1612,7 +1624,6 @@ namespace smtfd {
         unsigned_vector m_toggles_lim;
         model_ref       m_model;
         std::string     m_reason_unknown;
-        stats           m_stats;
         unsigned        m_max_conflicts;
 
         void set_delay_simplify() {
@@ -1775,16 +1786,20 @@ namespace smtfd {
                   tout << *m_model.get() << "\n";
                   );
 
+            bool found_bad = false;
             for (expr* a : subterms(core)) {
                 expr_ref val0 = (*m_model)(a);
                 expr_ref val1 = (*m_model)(abs(a));
                 if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
                     std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
-                    std::cout << "core: " << core << "\n";
+                    found_bad = true;
-                    std::cout << *m_model.get() << "\n";
-                    exit(0);
                 }
             }
+            if (found_bad) {
+                std::cout << "core: " << core << "\n";
+                std::cout << *m_model.get() << "\n";
+                exit(0);
+            }
 
             if (!has_q) {
                 return is_decided;
@@ -1874,7 +1889,7 @@ namespace smtfd {
         solver(unsigned indent, ast_manager& m, params_ref const& p):
             solver_na2as(m),
             m(m),
-            m_abs(m),
+            m_abs(m, m_stats),
             m_indent(indent),
             m_context(m_abs, m),
             m_uf(m_context),
@@ -1952,6 +1967,7 @@ namespace smtfd {
                    tout << "axioms:\n" << m_axioms << "\n";
                    tout << "assertions:\n" << m_assertions << "\n";);
 
+            // if (m_axioms.contains(fml)) return;
             SASSERT(!m_axioms.contains(fml));
             m_axioms.push_back(fml);
             _fml = abs(fml);
@@ -2099,6 +2115,7 @@ namespace smtfd {
             st.update("smtfd-num-lemmas", m_stats.m_num_lemmas);
             st.update("smtfd-num-rounds", m_stats.m_num_rounds);
             st.update("smtfd-num-mbqi",   m_stats.m_num_mbqi);
+            st.update("smtfd-num-fresh-bool", m_stats.m_num_fresh_bool);
         }
         void get_unsat_core(expr_ref_vector & r) override { 
             m_fd_sat_solver->get_unsat_core(r);