#4532 - arithmetic using SAT for interpreted atoms such as (< 0 0)

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 8, 2020 · ec3066c · ec3066c
1 parent e1a0a2e
commit ec3066c
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 6 deletions.
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
@@ -152,7 +152,7 @@ struct goal2sat::imp {
                 sat::bool_var v = m_solver.add_var(ext);
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
-                TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << "\n";);
+                TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
                 if (!is_uninterp_const(t)) {
                     m_interpreted_atoms.push_back(t);
                 }
@@ -953,6 +953,11 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
     }
 }
 
+bool goal2sat::has_interpreted_atoms() const {
+    return m_interpreted_atoms && !m_interpreted_atoms->empty();
+}
+
+
 
 sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
 
@@ -982,7 +987,10 @@ void sat2goal::mc::flush_gmc() {
                 lit0.neg();
                 def = m.mk_not(def);
             }
-            m_gmc->add(lit2expr(lit0), def);
+            expr_ref e = lit2expr(lit0);
+            expr* r = nullptr;
+            if (is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)))
+                m_gmc->add(e, def);
             clause.reset();
             tail.reset();
         }
@@ -1199,7 +1207,7 @@ struct sat2goal::imp {
         // collect units
         unsigned trail_sz = s.init_trail_size();
         for (unsigned i = 0; i < trail_sz; ++i) {
-            checkpoint();
+            checkpoint();            
             r.assert_expr(lit2expr(mc, s.trail_literal(i)));
         }
 

diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
@@ -65,6 +65,8 @@ class goal2sat {
 
     void get_interpreted_atoms(expr_ref_vector& atoms);
 
+    bool has_interpreted_atoms() const;
+
 };
 
 

diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
@@ -50,7 +50,7 @@ class sat_tactic : public tactic {
             obj_map<expr, sat::literal> dep2asm;
             sat::literal_vector assumptions;
             m_goal2sat(*g, m_params, *m_solver, map, dep2asm);
-            TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
+            TRACE("sat", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
                   for (auto const& kv : map) {
                       if (!is_uninterp_const(kv.m_key))
                           tout << mk_ismt2_pp(kv.m_key, m) << "\n";
@@ -112,8 +112,8 @@ class sat_tactic : public tactic {
                 ref<sat2goal::mc> mc;
                 m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
                 g->add(mc.get());
-                if (produce_core) {
-                    // sat2goal does not preseve assumptions
+                if (produce_core || m_goal2sat.has_interpreted_atoms()) {
+                    // sat2goal does not preseve assumptions or assignments to interpreted atoms
                     g->updt_prec(goal::OVER);
                 }
             }