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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-03 19:47:38 -07:00
parent 40f5270ae2
commit 2891ac7dec
1 changed files with 10 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -132,10 +132,9 @@ class fm_tactic : public tactic {
else { else {
expr_ref val(m); expr_ref val(m);
val = ev(monomial); val = ev(monomial);
if (!u.is_numeral(val))
return NONE;
rational tmp; rational tmp;
u.is_numeral(val, tmp); if (!u.is_numeral(val, tmp))
return NONE;
if (neg) if (neg)
tmp.neg(); tmp.neg();
c -= tmp; c -= tmp;
@ -166,11 +165,9 @@ class fm_tactic : public tactic {
fm_model_converter(ast_manager & _m):m(_m) {} fm_model_converter(ast_manager & _m):m(_m) {}
~fm_model_converter() override { ~fm_model_converter() override {
m.dec_array_ref(m_xs.size(), m_xs.data()); m.dec_array_ref(m_xs.size(), m_xs.data());
vector<clauses>::iterator it = m_clauses.begin(); for (auto& c : m_clauses)
vector<clauses>::iterator end = m_clauses.end(); m.dec_array_ref(c.size(), c.data());
for (; it != end; ++it)
m.dec_array_ref(it->size(), it->data());
} }
void insert(func_decl * x, clauses & c) { void insert(func_decl * x, clauses & c) {
@ -181,6 +178,7 @@ class fm_tactic : public tactic {
m_clauses.back().swap(c); m_clauses.back().swap(c);
} }
void get_units(obj_map<expr, bool>& units) override { units.reset(); } void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void operator()(model_ref & md) override { void operator()(model_ref & md) override {
@ -256,11 +254,8 @@ class fm_tactic : public tactic {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
out << "\n(" << m_xs[i]->get_name(); out << "\n(" << m_xs[i]->get_name();
clauses const & cs = m_clauses[i]; clauses const & cs = m_clauses[i];
clauses::const_iterator it = cs.begin(); for (auto& c : cs)
clauses::const_iterator end = cs.end(); out << "\n " << mk_ismt2_pp(c, m, 2);
for (; it != end; ++it) {
out << "\n " << mk_ismt2_pp(*it, m, 2);
}
out << ")"; out << ")";
} }
out << ")\n"; out << ")\n";
@ -278,10 +273,8 @@ class fm_tactic : public tactic {
clauses const & cs = m_clauses[i]; clauses const & cs = m_clauses[i];
res->m_clauses.push_back(clauses()); res->m_clauses.push_back(clauses());
clauses & new_cs = res->m_clauses.back(); clauses & new_cs = res->m_clauses.back();
clauses::const_iterator it = cs.begin(); for (auto& c : cs) {
clauses::const_iterator end = cs.end(); app * new_c = translator(c);
for (; it != end; ++it) {
app * new_c = translator(*it);
to_m.inc_ref(new_c); to_m.inc_ref(new_c);
new_cs.push_back(new_c); new_cs.push_back(new_c);
} }