diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 420174506..a93935fb6 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -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 { diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 95f6b9b21..1ae9723c9 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -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)); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 9c57fe791..b29a80927 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -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); diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 51cda17cd..7f71114f4 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -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; }