mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-07 23:06:12 -07:00
parent e1a0a2e536
commit ec3066c28a
3 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/sat/tactic/goal2sat.cpp
View file

@ -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)));
}

2
src/sat/tactic/goal2sat.h
View file

@ -65,6 +65,8 @@ public:
void get_interpreted_atoms(expr_ref_vector& atoms);
bool has_interpreted_atoms() const;
};

6
src/sat/tactic/sat_tactic.cpp
View file

@ -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);
}
}