mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3715

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 12:05:16 -07:00
parent 8e033c1e71
commit cd2f6705aa
2 changed files with 27 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/arith/bound_manager.cpp
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include "tactic/arith/bound_manager.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "tactic/goal.h"
bound_manager::bound_manager(ast_manager & m):

44
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -76,7 +76,7 @@ class eq2bv_tactic : public tactic {
class bvmc : public model_converter {
obj_map<func_decl, func_decl*> m_map;
func_decl_ref_vector m_vars;
unsigned_vector m_values;
vector<rational> m_values;
public:
bvmc(ast_manager& m): m_vars(m) {}
@ -84,7 +84,7 @@ class eq2bv_tactic : public tactic {
m_map.insert(c_new, c_old);
}
void insert(func_decl* var, unsigned val) {
void insert(func_decl* var, rational const& val) {
m_vars.push_back(var);
m_values.push_back(val);
}
@ -111,7 +111,7 @@ class eq2bv_tactic : public tactic {
}
for (unsigned i = 0; i < m_vars.size(); ++i) {
func_decl* f = m_vars.get(i);
new_m->register_decl(f, a.mk_numeral(rational(m_values[i]), f->get_range()));
new_m->register_decl(f, a.mk_numeral(m_values[i], f->get_range()));
}
mdl = new_m;
}
@ -203,16 +203,23 @@ public:
for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {
expr_ref new_curr(m);
proof_ref new_pr(m);
func_decl_ref var(m);
unsigned val;
if (is_bound(g->form(i), var, val) && !m_has_eq.is_marked(var)) {
expr_ref var(m);
if (is_bound(g->form(i), var) && !m_has_eq.is_marked(var)) {
if (m.proofs_enabled()) {
new_pr = m.mk_rewrite(g->form(i), m.mk_true());
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
g->update(i, m.mk_true(), new_pr, nullptr);
mc1->insert(var, val);
continue;
bool strict = true;
rational v;
bool has_val =
(m_bounds.has_upper(var, v, strict) && !strict) && v.is_unsigned() ||
(m_bounds.has_lower(var, v, strict) && !strict && v.is_unsigned());
if (has_val) {
mc1->insert(to_app(var)->get_decl(), v);
g->update(i, m.mk_true(), new_pr, nullptr);
continue;
}
}
m_rw(g->form(i), new_curr, new_pr);
if (g->form(i) == new_curr)
@ -305,29 +312,31 @@ public:
}
}
bool is_upper(expr* f, func_decl_ref& var, unsigned& k) {
bool is_upper(expr* f, expr_ref& var) {
expr* e1, *e2;
unsigned k;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) {
SASSERT(m_bounds.has_upper(e1));
var = to_app(e1)->get_decl();
var = e1;
return true;
}
return false;
}
bool is_lower(expr* f, func_decl_ref& var, unsigned& k) {
bool is_lower(expr* f, expr_ref& var) {
expr* e1, *e2;
unsigned k;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) {
SASSERT(m_bounds.has_lower(e2));
var = to_app(e2)->get_decl();
var = e2;
return true;
}
return false;
}
bool is_bound(expr* f, func_decl_ref& var, unsigned& val) {
return is_lower(f, var, val) || is_upper(f, var, val);
bool is_bound(expr* f, expr_ref& var) {
return is_lower(f, var) || is_upper(f, var);
}
void mark_has_eq(expr* e) {
@ -338,9 +347,8 @@ public:
void collect_fd(expr* f) {
m_trail.push_back(f);
func_decl_ref var(m);
unsigned val;
if (is_bound(f, var, val)) return;
expr_ref var(m);
if (is_bound(f, var)) return;
m_todo.push_back(f);
while (!m_todo.empty()) {
f = m_todo.back();