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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-23 21:57:19 -07:00
parent e187023304 3d27232b2a
commit 61c25fdc8e
4 changed files with 51 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/nlsat/nlsat_explain.cpp
View file

@ -216,9 +216,10 @@ namespace nlsat {
max_var(p) must be assigned in the current interpretation.
*/
int sign(polynomial_ref const & p) {
TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << "\n";);
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
return m_am.eval_sign_at(p, m_assignment);
int s = m_am.eval_sign_at(p, m_assignment);
TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
return s;
}
/**
@ -1452,7 +1453,6 @@ namespace nlsat {
SASSERT(check_already_added());
SASSERT(num > 0);
TRACE("nlsat_explain", tout << "[explain] set of literals is infeasible in the current interpretation\n"; display(tout, num, ls););
// exit(0);
m_result = &result;
process(num, ls);
reset_already_added();
@ -1738,11 +1738,13 @@ namespace nlsat {
void solve_eq(var x, unsigned idx, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), A(m_pm), B(m_pm), C(m_pm), D(m_pm), E(m_pm), q(m_pm), r(m_pm);
polynomial_ref_vector qs(m_pm);
polynomial_ref_vector As(m_pm), Bs(m_pm);
p = ps.get(idx);
SASSERT(degree(p, x) == 1);
A = m_pm.coeff(p, x, 1);
B = m_pm.coeff(p, x, 0);
As.push_back(m_pm.mk_const(rational(1)));
Bs.push_back(m_pm.mk_const(rational(1)));
B = neg(B);
TRACE("nlsat_explain", tout << "p: " << p << " A: " << A << " B: " << B << "\n";);
// x = B/A
@ -1753,20 +1755,21 @@ namespace nlsat {
D = m_pm.mk_const(rational(1));
E = D;
r = m_pm.mk_zero();
for (unsigned j = 0; j <= d; ++j) {
qs.push_back(D);
D = D*A;
for (unsigned j = As.size(); j <= d; ++j) {
D = As.back(); As.push_back(A * D);
D = Bs.back(); Bs.push_back(B * D);
}
for (unsigned j = 0; j <= d; ++j) {
// A^d*p0 + A^{d-1}*B*p1 + ... + B^j*A^{d-j}*pj + ... + B^d*p_d
C = m_pm.coeff(q, x, j);
TRACE("nlsat_explain", tout << "coeff: q" << j << ": " << C << "\n";);
if (!is_zero(C)) {
D = qs.get(d-j);
D = As.get(d - j);
E = Bs.get(j);
r = r + D*E*C;
}
E = E*B;
}
TRACE("nlsat_explain", tout << "q: " << q << " r: " << r << "\n";);
TRACE("nlsat_explain", tout << "p: " << p << " q: " << q << " r: " << r << "\n";);
ensure_sign(r);
}
else {

10
src/qe/nlqsat.cpp
View file

@ -646,12 +646,8 @@ namespace qe {
while (!vars.empty());
SASSERT(qvars.size() >= 2);
SASSERT(qvars.back().empty());
ackermanize_div(is_forall, qvars, fml);
init_expr2var(qvars);
goal2nlsat g2s;
expr_ref is_true(m), fml1(m), fml2(m);
@ -672,9 +668,7 @@ namespace qe {
m_bound_rvars.push_back(nlsat::var_vector());
max_level lvl;
if (is_exists(i)) lvl.m_ex = i; else lvl.m_fa = i;
for (unsigned j = 0; j < qvars[i].size(); ++j) {
app* v = qvars[i][j].get();
for (app* v : qvars[i]) {
if (m_a2b.is_var(v)) {
SASSERT(m.is_bool(v));
nlsat::bool_var b = m_a2b.to_var(v);
@ -696,7 +690,7 @@ namespace qe {
m_is_true = nlsat::literal(m_a2b.to_var(is_true), false);
// insert literals from arithmetical sub-formulas
nlsat::atom_vector const& atoms = m_solver.get_atoms();
TRACE("qe", m_solver.display(tout); );
TRACE("qe", m_solver.display(tout););
for (unsigned i = 0; i < atoms.size(); ++i) {
if (atoms[i]) {
get_level(nlsat::literal(i, false));

33
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -466,6 +466,38 @@ class tseitin_cnf_tactic : public tactic {
}
return NO;
}
mres match_iff_or(app * t, bool first, bool root) {
expr * a = nullptr, * _b = nullptr;
if (!root) return NO;
if (!is_iff(m, t, a, _b)) return NO;
bool sign = m.is_not(_b, _b);
if (!m.is_or(_b)) return NO;
app* b = to_app(_b);
unsigned num = b->get_num_args();
if (first) {
bool visited = true;
visit(a, visited);
for (expr* arg : *b) {
visit(arg, visited);
}
if (!visited)
return CONT;
}
expr_ref la(m), nla(m), nlb(m), lb(m);
get_lit(a, sign, la);
inv(la, nla);
expr_ref_buffer lits(m);
lits.push_back(nla);
for (expr* arg : *b) {
get_lit(arg, false, lb);
lits.push_back(lb);
inv(lb, nlb);
mk_clause(la, nlb);
}
mk_clause(lits.size(), lits.c_ptr());
return DONE;
}
mres match_iff(app * t, bool first, bool root) {
expr * a, * b;
@ -784,6 +816,7 @@ class tseitin_cnf_tactic : public tactic {
TRY(match_or_3and);
TRY(match_or);
TRY(match_iff3);
// TRY(match_iff_or);
TRY(match_iff);
TRY(match_ite);
TRY(match_not);

4
src/tactic/portfolio/default_tactic.cpp
View file

@ -31,9 +31,11 @@ Notes:
#include "tactic/fpa/qffplra_tactic.h"
#include "tactic/smtlogics/qfaufbv_tactic.h"
#include "tactic/smtlogics/qfauflia_tactic.h"
#include "tactic/portfolio/fd_solver.h"
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_propositional_probe(), if_no_proofs(mk_fd_tactic(m, p)),
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m),
cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
@ -46,7 +48,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p),
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
mk_smt_tactic())))))))))))),
mk_smt_tactic()))))))))))))),
p);
return st;
}