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

fix #3225

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-10 15:10:18 -07:00
parent dd4eb7f97c
commit 99784a92ef
3 changed files with 12 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/nlsat/nlsat_solver.cpp
View file

@ -640,16 +640,6 @@ namespace nlsat {
literal mk_ineq_literal(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even) {
SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ);
if (sz == 0) {
switch (k) {
case atom::LT: return false_literal; // 0 < 0
case atom::EQ: return true_literal; // 0 == 0
case atom::GT: return false_literal; // 0 > 0
default:
UNREACHABLE();
return null_literal;
}
}
bool is_const = true;
polynomial::manager::scoped_numeral cnst(m_pm.m());
m_pm.m().set(cnst, 1);
@ -2657,6 +2647,7 @@ namespace nlsat {
for (clause* c : m_clauses) {
if (solve_var(*c, v, p, q)) {
q = -q;
TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";);
m_patch_var.push_back(v);
m_patch_num.push_back(q);
m_patch_denom.push_back(p);
@ -2698,6 +2689,8 @@ namespace nlsat {
u_map<literal> b2l;
scoped_literal_vector lits(m_solver);
svector<bool> even;
polynomial::manager::scoped_numeral cnst(m_pm.m());
m_pm.m().set(cnst, 1);
unsigned num_atoms = m_atoms.size();
for (unsigned j = 0; j < num_atoms; ++j) {
atom* a = m_atoms[j];
@ -2712,9 +2705,12 @@ namespace nlsat {
poly * po = a1.p(i);
m_pm.substitute(po, x, q, p, pr);
change |= pr != po;
TRACE("nlsat", tout << pr << "\n";);
if (m_pm.is_zero(pr)) {
ps.reset();
even.reset();
even.push_back(false);
ps.push_back(pr);
break;
}
if (m_pm.is_const(pr)) {

8
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -83,7 +83,7 @@ class nlsat_tactic : public tactic {
bool eval_model(model& model, goal& g) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
if (!model.is_true(g.form(i))) {
if (model.is_false(g.form(i))) {
TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(0, verbose_stream() << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(1, verbose_stream() << model << "\n");
@ -152,12 +152,12 @@ class nlsat_tactic : public tactic {
m_display_var.m_var2expr.reset();
t2x.mk_inv(m_display_var.m_var2expr);
m_solver.set_display_var(m_display_var);
TRACE("nlsat", m_solver.display(tout););
IF_VERBOSE(10000, m_solver.display(verbose_stream()));
IF_VERBOSE(10000, g->display(verbose_stream()));
lbool st = m_solver.check();
if (st == l_undef) {
}
else if (st == l_true) {
@ -176,7 +176,7 @@ class nlsat_tactic : public tactic {
}
}
}
else {
else if (st == l_false) {
expr_dependency* lcore = nullptr;
if (g->unsat_core_enabled()) {
vector<nlsat::assumption, false> assumptions;

4
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -867,8 +867,8 @@ class solve_eqs_tactic : public tactic {
expr_dependency_ref new_dep(m());
for (app * v : m_ordered_vars) {
checkpoint();
expr_ref new_def(m());
proof_ref new_pr(m());
expr_ref new_def(m());
proof_ref new_pr(m());
expr * def = nullptr;
proof * pr = nullptr;
expr_dependency * dep = nullptr;