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

fix #5452

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-03 17:23:41 -07:00
parent 7ae4e93e86
commit 40f5270ae2
2 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/tactic/arith/fm_tactic.cpp
View file

@ -93,7 +93,8 @@ class fm_tactic : public tactic {
expr * lhs = to_app(l)->get_arg(0); expr * lhs = to_app(l)->get_arg(0);
expr * rhs = to_app(l)->get_arg(1); expr * rhs = to_app(l)->get_arg(1);
rational c; rational c;
u.is_numeral(rhs, c); if (!u.is_numeral(rhs, c))
return NONE;
if (neg) if (neg)
c.neg(); c.neg();
unsigned num_mons; unsigned num_mons;
@ -112,7 +113,8 @@ class fm_tactic : public tactic {
expr * xi; expr * xi;
rational ai_val; rational ai_val;
if (u.is_mul(monomial, ai, xi)) { if (u.is_mul(monomial, ai, xi)) {
u.is_numeral(ai, ai_val); if (!u.is_numeral(ai, ai_val))
return NONE;
} }
else { else {
xi = monomial; xi = monomial;
@ -120,7 +122,8 @@ class fm_tactic : public tactic {
} }
if (u.is_to_real(xi)) if (u.is_to_real(xi))
xi = to_app(xi)->get_arg(0); xi = to_app(xi)->get_arg(0);
SASSERT(is_uninterp_const(xi)); if (!is_uninterp_const(xi))
return NONE;
if (x == to_app(xi)->get_decl()) { if (x == to_app(xi)->get_decl()) {
a_val = ai_val; a_val = ai_val;
if (neg) if (neg)
@ -129,7 +132,8 @@ class fm_tactic : public tactic {
else { else {
expr_ref val(m); expr_ref val(m);
val = ev(monomial); val = ev(monomial);
SASSERT(u.is_numeral(val)); if (!u.is_numeral(val))
return NONE;
rational tmp; rational tmp;
u.is_numeral(val, tmp); u.is_numeral(val, tmp);
if (neg) if (neg)

5
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -44,6 +44,7 @@ class pb_preprocess_tactic : public tactic {
struct rec { unsigned_vector pos, neg; rec() { } }; struct rec { unsigned_vector pos, neg; rec() { } };
typedef obj_map<app, rec> var_map; typedef obj_map<app, rec> var_map;
ast_manager& m; ast_manager& m;
expr_ref_vector m_trail;
pb_util pb; pb_util pb;
var_map m_vars; var_map m_vars;
unsigned_vector m_ge; unsigned_vector m_ge;
@ -99,7 +100,7 @@ class pb_preprocess_tactic : public tactic {
public: public:
pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()):
m(m), pb(m), m_r(m) {} m(m), m_trail(m), pb(m), m_r(m) {}
~pb_preprocess_tactic() override {} ~pb_preprocess_tactic() override {}
@ -121,6 +122,7 @@ public:
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());
while (simplify(g, *pp)); while (simplify(g, *pp));
m_trail.reset();
// decompose(g); // decompose(g);
} }
@ -406,6 +408,7 @@ private:
void insert(unsigned i, app* e, bool pos) { void insert(unsigned i, app* e, bool pos) {
SASSERT(is_uninterp_const(e)); SASSERT(is_uninterp_const(e));
if (!m_vars.contains(e)) { if (!m_vars.contains(e)) {
m_trail.push_back(e);
m_vars.insert(e, rec()); m_vars.insert(e, rec());
} }
if (pos) { if (pos) {