mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5d9ed5b0a9
commit
67c4777514
11 changed files with 251 additions and 126 deletions
|
|
@ -1902,7 +1902,7 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
|
|||
}
|
||||
|
||||
br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
|
||||
TRACE("seq", tout << mk_pp(l, m()) << " = " << mk_pp(r, m()) << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(l, m(), 2) << " = " << mk_bounded_pp(r, m(), 2) << "\n";);
|
||||
expr_ref_vector lhs(m()), rhs(m()), res(m());
|
||||
bool changed = false;
|
||||
if (!reduce_eq(l, r, lhs, rhs, changed)) {
|
||||
|
|
|
|||
|
|
@ -410,8 +410,8 @@ namespace polynomial {
|
|||
proc(out, x);
|
||||
}
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
bool is_unit() const { return m_size == 0; }
|
||||
|
|
@ -1576,12 +1576,20 @@ namespace polynomial {
|
|||
display_num_smt2(out, nm, a_i);
|
||||
}
|
||||
else if (nm.is_one(a_i)) {
|
||||
m_i->display(out, proc);
|
||||
if (m_i->size() == 1) {
|
||||
m_i->display_smt2(out, proc);
|
||||
}
|
||||
else {
|
||||
out << "(* ";
|
||||
m_i->display_smt2(out, proc);
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
else {
|
||||
out << "(* ";
|
||||
display_num_smt2(out, nm, a_i);
|
||||
m_i->display(out, proc);
|
||||
out << " ";
|
||||
m_i->display_smt2(out, proc);
|
||||
out << ")";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -45,48 +45,7 @@ struct limit_denominator_rewriter_cfg : public default_rewriter_cfg {
|
|||
}
|
||||
|
||||
bool limit_denominator(rational &num) {
|
||||
rational n, d;
|
||||
n = numerator(num);
|
||||
d = denominator(num);
|
||||
if (d < m_limit) return false;
|
||||
|
||||
/*
|
||||
Iteratively computes approximation using continuous fraction
|
||||
decomposition
|
||||
|
||||
p(-1) = 0, p(0) = 1
|
||||
p(j) = t(j)*p(j-1) + p(j-2)
|
||||
|
||||
q(-1) = 1, q(0) = 0
|
||||
q(j) = t(j)*q(j-1) + q(j-2)
|
||||
|
||||
cf[t1; t2, ..., tr] = p(r) / q(r) for r >= 1
|
||||
reference: https://www.math.u-bordeaux.fr/~pjaming/M1/exposes/MA2.pdf
|
||||
*/
|
||||
|
||||
rational p0(0), p1(1);
|
||||
rational q0(1), q1(0);
|
||||
|
||||
while (d != rational(0)) {
|
||||
rational tj(0), rem(0);
|
||||
rational p2(0), q2(0);
|
||||
tj = div(n, d);
|
||||
|
||||
q2 = tj * q1 + q0;
|
||||
p2 = tj * p1 + p0;
|
||||
if (q2 >= m_limit) {
|
||||
num = p2 / q2;
|
||||
return true;
|
||||
}
|
||||
rem = n - tj * d;
|
||||
p0 = p1;
|
||||
p1 = p2;
|
||||
q0 = q1;
|
||||
q1 = q2;
|
||||
n = d;
|
||||
d = rem;
|
||||
}
|
||||
return false;
|
||||
return rational::limit_denominator(num, m_limit);
|
||||
}
|
||||
|
||||
br_status reduce_app(func_decl *f, unsigned num, expr *const *args,
|
||||
|
|
|
|||
|
|
@ -1162,18 +1162,21 @@ namespace nlsat {
|
|||
new_lit = m_solver.mk_ineq_literal(new_k, new_factors.size(), new_factors.c_ptr(), new_factors_even.c_ptr());
|
||||
if (l.sign())
|
||||
new_lit.neg();
|
||||
TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit); tout << "\n";);
|
||||
TRACE("nlsat_simplify_core", tout << "simplified literal:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";);
|
||||
|
||||
if (max_var(new_lit) < max) {
|
||||
// The conflicting core may have redundant literals.
|
||||
// We should check whether new_lit is true in the current model, and discard it if that is the case
|
||||
VERIFY(m_solver.value(new_lit) != l_undef);
|
||||
if (m_solver.value(new_lit) == l_false)
|
||||
if (m_solver.value(new_lit) == l_true) {
|
||||
new_lit = l;
|
||||
}
|
||||
else {
|
||||
add_literal(new_lit);
|
||||
new_lit = true_literal;
|
||||
return;
|
||||
new_lit = true_literal;
|
||||
}
|
||||
}
|
||||
else {
|
||||
new_lit = normalize(new_lit, max);
|
||||
TRACE("nlsat_simplify_core", tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";);
|
||||
}
|
||||
new_lit = normalize(new_lit, max);
|
||||
TRACE("nlsat_simplify_core", tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << "\n";);
|
||||
}
|
||||
else {
|
||||
new_lit = l;
|
||||
|
|
@ -1333,6 +1336,7 @@ namespace nlsat {
|
|||
poly * eq_p = eq->p(0);
|
||||
VERIFY(simplify(C, eq_p, max));
|
||||
// add equation as an assumption
|
||||
TRACE("nlsat_simpilfy_core", display(tout << "adding equality as assumption ", literal(eq->bvar(), true)); tout << "\n";);
|
||||
add_literal(literal(eq->bvar(), true));
|
||||
}
|
||||
}
|
||||
|
|
@ -1511,7 +1515,7 @@ namespace nlsat {
|
|||
result.set(i, ~result[i]);
|
||||
}
|
||||
DEBUG_CODE(
|
||||
TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()); );
|
||||
TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()) << "\n"; );
|
||||
for (literal l : result) {
|
||||
CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
|
||||
SASSERT(l_true == m_solver.value(l));
|
||||
|
|
@ -1619,12 +1623,12 @@ namespace nlsat {
|
|||
unsigned glb_index = 0, lub_index = 0;
|
||||
scoped_anum lub(m_am), glb(m_am), x_val(m_am);
|
||||
x_val = m_assignment.value(x);
|
||||
bool glb_valid = false, lub_valid = false;
|
||||
for (unsigned i = 0; i < ps.size(); ++i) {
|
||||
p = ps.get(i);
|
||||
scoped_anum_vector & roots = m_roots_tmp;
|
||||
roots.reset();
|
||||
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
|
||||
bool glb_valid = false, lub_valid = false;
|
||||
for (auto const& r : roots) {
|
||||
int s = m_am.compare(x_val, r);
|
||||
SASSERT(s != 0);
|
||||
|
|
@ -1632,23 +1636,19 @@ namespace nlsat {
|
|||
if (s < 0 && (!lub_valid || m_am.lt(r, lub))) {
|
||||
lub_index = i;
|
||||
m_am.set(lub, r);
|
||||
lub_valid = true;
|
||||
}
|
||||
|
||||
if (s > 0 && (!glb_valid || m_am.lt(glb, r))) {
|
||||
glb_index = i;
|
||||
m_am.set(glb, r);
|
||||
m_am.set(glb, r);
|
||||
glb_valid = true;
|
||||
}
|
||||
lub_valid |= s < 0;
|
||||
glb_valid |= s > 0;
|
||||
}
|
||||
if (glb_valid) {
|
||||
++num_glb;
|
||||
}
|
||||
if (lub_valid) {
|
||||
++num_lub;
|
||||
if (s < 0) ++num_lub;
|
||||
if (s > 0) ++num_glb;
|
||||
}
|
||||
}
|
||||
TRACE("nlsat_explain", tout << ps << "\n";);
|
||||
TRACE("nlsat_explain", tout << "glb: " << num_glb << " lub: " << num_lub << "\n" << lub_index << "\n" << glb_index << "\n" << ps << "\n";);
|
||||
|
||||
if (num_lub == 0) {
|
||||
project_plus_infinity(x, ps);
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ def_module_params('nlsat',
|
|||
params=(max_memory_param(),
|
||||
('lazy', UINT, 0, "how lazy the solver is."),
|
||||
('reorder', BOOL, True, "reorder variables."),
|
||||
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
|
||||
('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
|
||||
('minimize_conflicts', BOOL, False, "minimize conflicts"),
|
||||
('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
|
||||
|
|
|
|||
|
|
@ -156,6 +156,8 @@ namespace nlsat {
|
|||
|
||||
unsigned m_scope_lvl;
|
||||
|
||||
struct bvar_assignment {};
|
||||
struct stage {};
|
||||
struct trail {
|
||||
enum kind { BVAR_ASSIGNMENT, INFEASIBLE_UPDT, NEW_LEVEL, NEW_STAGE, UPDT_EQ };
|
||||
kind m_kind;
|
||||
|
|
@ -164,9 +166,9 @@ namespace nlsat {
|
|||
interval_set * m_old_set;
|
||||
atom * m_old_eq;
|
||||
};
|
||||
trail(bool_var b):m_kind(BVAR_ASSIGNMENT), m_b(b) {}
|
||||
trail(bool_var b, bvar_assignment):m_kind(BVAR_ASSIGNMENT), m_b(b) {}
|
||||
trail(interval_set * old_set):m_kind(INFEASIBLE_UPDT), m_old_set(old_set) {}
|
||||
trail(bool stage):m_kind(stage ? NEW_STAGE : NEW_LEVEL) {}
|
||||
trail(bool s, stage):m_kind(s ? NEW_STAGE : NEW_LEVEL) {}
|
||||
trail(atom * a):m_kind(UPDT_EQ), m_old_eq(a) {}
|
||||
};
|
||||
svector<trail> m_trail;
|
||||
|
|
@ -182,6 +184,7 @@ namespace nlsat {
|
|||
bool m_random_order;
|
||||
unsigned m_random_seed;
|
||||
bool m_inline_vars;
|
||||
bool m_log_lemmas;
|
||||
unsigned m_max_conflicts;
|
||||
|
||||
// statistics
|
||||
|
|
@ -240,6 +243,7 @@ namespace nlsat {
|
|||
m_random_order = p.shuffle_vars();
|
||||
m_random_seed = p.seed();
|
||||
m_inline_vars = p.inline_vars();
|
||||
m_log_lemmas = p.log_lemmas();
|
||||
m_ism.set_seed(m_random_seed);
|
||||
m_explain.set_simplify_cores(m_simplify_cores);
|
||||
m_explain.set_minimize_cores(min_cores);
|
||||
|
|
@ -730,6 +734,14 @@ namespace nlsat {
|
|||
}
|
||||
};
|
||||
|
||||
void log_lemma(std::ostream& out, clause const& cls) {
|
||||
display_smt2(out);
|
||||
out << "(assert (not ";
|
||||
display_smt2(out, cls) << "))\n";
|
||||
display(out << "(echo \"", cls) << "\")\n";
|
||||
out << "(check-sat)\n(reset)\n";
|
||||
}
|
||||
|
||||
clause * mk_clause(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
|
||||
SASSERT(num_lits > 0);
|
||||
unsigned cid = m_cid_gen.mk();
|
||||
|
|
@ -741,6 +753,9 @@ namespace nlsat {
|
|||
TRACE("nlsat_sort", tout << "mk_clause:\n"; display(tout, *cls); tout << "\n";);
|
||||
std::sort(cls->begin(), cls->end(), lit_lt(*this));
|
||||
TRACE("nlsat_sort", tout << "after sort:\n"; display(tout, *cls); tout << "\n";);
|
||||
if (learned && m_log_lemmas) {
|
||||
log_lemma(std::cout, *cls);
|
||||
}
|
||||
if (learned)
|
||||
m_learned.push_back(cls);
|
||||
else
|
||||
|
|
@ -764,7 +779,7 @@ namespace nlsat {
|
|||
// -----------------------
|
||||
|
||||
void save_assign_trail(bool_var b) {
|
||||
m_trail.push_back(trail(b));
|
||||
m_trail.push_back(trail(b, bvar_assignment()));
|
||||
}
|
||||
|
||||
void save_set_updt_trail(interval_set * old_set) {
|
||||
|
|
@ -776,11 +791,11 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void save_new_stage_trail() {
|
||||
m_trail.push_back(trail(true));
|
||||
m_trail.push_back(trail(true, stage()));
|
||||
}
|
||||
|
||||
void save_new_level_trail() {
|
||||
m_trail.push_back(trail(false));
|
||||
m_trail.push_back(trail(false, stage()));
|
||||
}
|
||||
|
||||
void undo_bvar_assignment(bool_var b) {
|
||||
|
|
@ -934,8 +949,10 @@ namespace nlsat {
|
|||
\brief Assign literal using the given justification
|
||||
*/
|
||||
void assign(literal l, justification j) {
|
||||
TRACE("nlsat", tout << "assigning literal: "; display(tout, l);
|
||||
tout << "\njustification kind: " << j.get_kind() << "\n";);
|
||||
TRACE("nlsat",
|
||||
display(tout << "assigning literal: ", l);
|
||||
display(tout << " <- ", j););
|
||||
|
||||
SASSERT(assigned_value(l) == l_undef);
|
||||
SASSERT(j != null_justification);
|
||||
SASSERT(!j.is_null());
|
||||
|
|
@ -1086,9 +1103,10 @@ namespace nlsat {
|
|||
switch (j.get_kind()) {
|
||||
case justification::CLAUSE:
|
||||
if (j.get_clause()->assumptions() != nullptr) return;
|
||||
break;
|
||||
break;
|
||||
case justification::LAZY:
|
||||
if (j.get_lazy()->num_clauses() > 0) return;
|
||||
if (j.get_lazy()->num_lits() > 0) return;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
|
@ -1098,8 +1116,10 @@ namespace nlsat {
|
|||
SASSERT(x != null_var);
|
||||
if (m_var2eq[x] != 0 && degree(m_var2eq[x]) <= degree(a))
|
||||
return; // we only update m_var2eq if the new equality has smaller degree
|
||||
TRACE("simplify_core", tout << "Saving equality for "; m_display_var(tout, x) << " (x" << x << ") ";
|
||||
tout << "scope-lvl: " << scope_lvl() << "\n"; display(tout, literal(b, false)) << "\n";);
|
||||
TRACE("nlsat_simplify_core", tout << "Saving equality for "; m_display_var(tout, x) << " (x" << x << ") ";
|
||||
tout << "scope-lvl: " << scope_lvl() << "\n"; display(tout, literal(b, false)) << "\n";
|
||||
display(tout, j);
|
||||
);
|
||||
save_updt_eq_trail(m_var2eq[x]);
|
||||
m_var2eq[x] = a;
|
||||
}
|
||||
|
|
@ -1125,7 +1145,7 @@ namespace nlsat {
|
|||
checkpoint();
|
||||
if (value(l) == l_false)
|
||||
continue;
|
||||
TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
|
||||
CTRACE("nlsat", max_var(l) != m_xk, display(tout); tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
|
||||
SASSERT(value(l) == l_undef);
|
||||
SASSERT(max_var(l) == m_xk);
|
||||
bool_var b = l.var();
|
||||
|
|
@ -1195,7 +1215,6 @@ namespace nlsat {
|
|||
bool process_clause(clause const & cls, bool satisfy_learned) {
|
||||
if (is_satisfied(cls))
|
||||
return true;
|
||||
TRACE("nlsat", display(tout << "processing clause: ", cls) << "\n";);
|
||||
if (m_xk == null_var)
|
||||
return process_boolean_clause(cls);
|
||||
else
|
||||
|
|
@ -1255,7 +1274,22 @@ namespace nlsat {
|
|||
m_irrational_assignments++;
|
||||
m_assignment.set_core(m_xk, w);
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool is_satisfied() {
|
||||
if (m_bk == null_bool_var && m_xk >= num_vars()) {
|
||||
TRACE("nlsat", tout << "found model\n"; display_assignment(tout););
|
||||
fix_patch();
|
||||
SASSERT(check_satisfied(m_clauses));
|
||||
return true; // all variables were assigned, and all clauses were satisfied.
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief main procedure
|
||||
*/
|
||||
|
|
@ -1264,8 +1298,11 @@ namespace nlsat {
|
|||
TRACE("nlsat_proof", tout << "ASSERTED\n"; display(tout););
|
||||
TRACE("nlsat_proof_sk", tout << "ASSERTED\n"; display_abst(tout););
|
||||
TRACE("nlsat_mathematica", display_mathematica(tout););
|
||||
TRACE("nlsat", display_smt2(tout););
|
||||
m_bk = 0;
|
||||
m_xk = null_var;
|
||||
m_conflicts = 0;
|
||||
|
||||
while (true) {
|
||||
CASSERT("nlsat", check_satisfied());
|
||||
if (m_xk == null_var) {
|
||||
|
|
@ -1277,22 +1314,18 @@ namespace nlsat {
|
|||
new_stage(); // peek next arith var
|
||||
}
|
||||
TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";);
|
||||
if (m_bk == null_bool_var && m_xk >= num_vars()) {
|
||||
TRACE("nlsat", tout << "found model\n"; display_assignment(tout););
|
||||
fix_patch();
|
||||
SASSERT(check_satisfied(m_clauses));
|
||||
return l_true; // all variables were assigned, and all clauses were satisfied.
|
||||
if (is_satisfied()) {
|
||||
return l_true;
|
||||
}
|
||||
while (true) {
|
||||
TRACE("nlsat", tout << "processing variable ";
|
||||
TRACE("nlsat_verbose", tout << "processing variable ";
|
||||
if (m_xk != null_var) {
|
||||
m_display_var(tout, m_xk); tout << " " << m_watches[m_xk].size();
|
||||
}
|
||||
else {
|
||||
tout << m_bwatches[m_bk].size() << " boolean b" << m_bk;
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
tout << "\n";);
|
||||
checkpoint();
|
||||
clause * conflict_clause;
|
||||
if (m_xk == null_var)
|
||||
|
|
@ -1301,12 +1334,12 @@ namespace nlsat {
|
|||
conflict_clause = process_clauses(m_watches[m_xk]);
|
||||
if (conflict_clause == nullptr)
|
||||
break;
|
||||
if (!resolve(*conflict_clause))
|
||||
return l_false;
|
||||
if (!resolve(*conflict_clause))
|
||||
return l_false;
|
||||
if (m_conflicts >= m_max_conflicts)
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
|
||||
if (m_xk == null_var) {
|
||||
if (m_bvalues[m_bk] == l_undef) {
|
||||
decide(literal(m_bk, true));
|
||||
|
|
@ -1319,6 +1352,7 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
lbool search_check() {
|
||||
lbool r = l_undef;
|
||||
while (true) {
|
||||
|
|
@ -1521,6 +1555,7 @@ namespace nlsat {
|
|||
// antecedent must be false in the current arith interpretation
|
||||
SASSERT(value(antecedent) == l_false);
|
||||
if (!is_marked(b)) {
|
||||
TRACE("nlsat_resolve", tout << max_var(b) << " " << m_xk << "\n";);
|
||||
SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage
|
||||
TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";);
|
||||
mark(b);
|
||||
|
|
@ -2692,6 +2727,26 @@ namespace nlsat {
|
|||
display_num_assignment(out);
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, justification j) const {
|
||||
switch (j.get_kind()) {
|
||||
case justification::CLAUSE:
|
||||
display(out, *j.get_clause()) << "\n";
|
||||
break;
|
||||
case justification::LAZY: {
|
||||
lazy_justification const& lz = *j.get_lazy();
|
||||
display(out, lz.num_lits(), lz.lits()) << "\n";
|
||||
for (unsigned i = 0; i < lz.num_clauses(); ++i) {
|
||||
display(out, lz.clause(i)) << "\n";
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
out << j.get_kind() << "\n";
|
||||
break;
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const {
|
||||
unsigned sz = a.size();
|
||||
|
|
@ -2769,6 +2824,10 @@ namespace nlsat {
|
|||
out << " 0)";
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const {
|
||||
return display(out, a, proc);
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream & out, root_atom const & a, display_var_proc const & proc) const {
|
||||
proc(out, a.x());
|
||||
|
|
@ -2898,6 +2957,10 @@ namespace nlsat {
|
|||
return display(out, l, m_display_var);
|
||||
}
|
||||
|
||||
std::ostream& display_smt2(std::ostream & out, literal l) const {
|
||||
return display_smt2(out, l, m_display_var);
|
||||
}
|
||||
|
||||
std::ostream& display_mathematica(std::ostream & out, literal l) const {
|
||||
if (l.sign()) {
|
||||
bool_var b = l.var();
|
||||
|
|
@ -2947,7 +3010,7 @@ namespace nlsat {
|
|||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream & out, unsigned num, literal const * ls) {
|
||||
std::ostream& display(std::ostream & out, unsigned num, literal const * ls) const {
|
||||
return display(out, num, ls, m_display_var);
|
||||
}
|
||||
|
||||
|
|
@ -3147,7 +3210,7 @@ namespace nlsat {
|
|||
for (clause* c : m_clauses) {
|
||||
display_smt2(out, *c) << "\n";
|
||||
}
|
||||
out << "))\n(check-sat)" << std::endl;
|
||||
out << "))\n" << std::endl;
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
|
@ -3346,6 +3409,22 @@ namespace nlsat {
|
|||
return display(out, ls.size(), ls.c_ptr());
|
||||
}
|
||||
|
||||
std::ostream& solver::display_smt2(std::ostream & out, literal l) const {
|
||||
return m_imp->display_smt2(out, l);
|
||||
}
|
||||
|
||||
std::ostream& solver::display_smt2(std::ostream & out, unsigned n, literal const* ls) const {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
display_smt2(out, ls[i]);
|
||||
out << " ";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const {
|
||||
return display_smt2(out, ls.size(), ls.c_ptr());
|
||||
}
|
||||
|
||||
std::ostream& solver::display(std::ostream & out, var x) const {
|
||||
return m_imp->m_display_var(out, x);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -245,6 +245,13 @@ namespace nlsat {
|
|||
|
||||
std::ostream& display(std::ostream & out, atom const& a) const;
|
||||
|
||||
std::ostream& display_smt2(std::ostream & out, literal l) const;
|
||||
|
||||
std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const;
|
||||
|
||||
std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const;
|
||||
|
||||
|
||||
/**
|
||||
\brief Display variable
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -350,6 +350,16 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
|
||||
void display_project(std::ostream& out, nlsat::var v, nlsat::scoped_literal_vector const& r1, nlsat::scoped_literal_vector const& r2) {
|
||||
for (auto const& kv : s.m_x2t) {
|
||||
out << "(declare-const x" << kv.m_key << " Real)\n";
|
||||
}
|
||||
s.m_solver.display(out << "(assert (not (exists ((", v) << " Real)) \n";
|
||||
s.m_solver.display_smt2(out << "(and ", r1.size(), r1.c_ptr()) << "))))\n";
|
||||
s.m_solver.display_smt2(out << "(assert (and ", r2.size(), r2.c_ptr()); out << "))\n";
|
||||
out << "(check-sat)\n(reset)\n";
|
||||
}
|
||||
|
||||
void mbp(nlsat::var_vector const& vars, uint_set const& fvars, clause& result) {
|
||||
//
|
||||
// Also project auxiliary variables from clausification.
|
||||
|
|
@ -370,11 +380,10 @@ namespace qe {
|
|||
// renaming variables.
|
||||
for (unsigned i = vars.size(); i-- > 0;) {
|
||||
new_result.reset();
|
||||
TRACE("qe", s.m_solver.display(tout << "project: ", vars[i]) << "\n";);
|
||||
ex.project(vars[i], result.size(), result.c_ptr(), new_result);
|
||||
TRACE("qe", display_project(tout, vars[i], result, new_result););
|
||||
TRACE("qe", display_project(std::cout, vars[i], result, new_result););
|
||||
result.swap(new_result);
|
||||
TRACE("qe", s.m_solver.display(tout, vars[i]) << ": ";
|
||||
s.m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
|
||||
}
|
||||
negate_clause(result);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -140,7 +140,6 @@ void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
|
|||
value.first = r;
|
||||
value.second = d;
|
||||
m_map.insert(e, value);
|
||||
// std::cout << mk_pp(e, m) << " -> " << mk_pp(r, m) << "\n";
|
||||
add_trail(INS, e, r, d);
|
||||
}
|
||||
|
||||
|
|
@ -225,7 +224,7 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
|
|||
|
||||
void theory_seq::solution_map::display(std::ostream& out) const {
|
||||
for (auto const& kv : m_map) {
|
||||
out << mk_bounded_pp(kv.m_key, m) << " |-> " << mk_bounded_pp(kv.m_value.first, m) << "\n";
|
||||
out << mk_bounded_pp(kv.m_key, m, 2) << " |-> " << mk_bounded_pp(kv.m_value.first, m, 2) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -260,7 +259,7 @@ void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) {
|
|||
|
||||
void theory_seq::exclusion_table::display(std::ostream& out) const {
|
||||
for (auto const& kv : m_table) {
|
||||
out << mk_pp(kv.first, m) << " != " << mk_pp(kv.second, m) << "\n";
|
||||
out << mk_bounded_pp(kv.first, m, 2) << " != " << mk_bounded_pp(kv.second, m, 2) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -555,20 +554,20 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
|
|||
context& ctx = get_context();
|
||||
rational lenX;
|
||||
if (!get_length(X, lenX)) {
|
||||
TRACE("seq", tout << "enforce length on " << mk_pp(X, m) << "\n";);
|
||||
TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";);
|
||||
enforce_length(X);
|
||||
return;
|
||||
}
|
||||
if (lenX > rational(units.size())) {
|
||||
expr_ref le(m_autil.mk_le(mk_len(X), m_autil.mk_int(units.size())), m);
|
||||
TRACE("seq", tout << "propagate length on " << mk_pp(X, m) << "\n";);
|
||||
TRACE("seq", tout << "propagate length on " << mk_bounded_pp(X, m, 2) << "\n";);
|
||||
propagate_lit(dep, 0, nullptr, mk_literal(le));
|
||||
return;
|
||||
}
|
||||
SASSERT(lenX.is_unsigned());
|
||||
unsigned lX = lenX.get_unsigned();
|
||||
if (lX == 0) {
|
||||
TRACE("seq", tout << "set empty length " << mk_pp(X, m) << "\n";);
|
||||
TRACE("seq", tout << "set empty length " << mk_bounded_pp(X, m, 2) << "\n";);
|
||||
set_empty(X);
|
||||
}
|
||||
else {
|
||||
|
|
@ -2223,17 +2222,29 @@ bool theory_seq::is_solved() {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
if (false && !m_nqs.empty()) {
|
||||
TRACE("seq", display_disequation(tout << "(seq.giveup ", m_nqs[0]); tout << " is unsolved)\n";);
|
||||
IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
|
||||
return false;
|
||||
}
|
||||
if (!m_ncs.empty()) {
|
||||
TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
|
||||
IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
context& ctx = get_context();
|
||||
for (enode* n : ctx.enodes()) {
|
||||
expr* e = nullptr;
|
||||
rational len1, len2;
|
||||
if (m_util.str.is_length(n->get_owner(), e)) {
|
||||
VERIFY(get_length(e, len1));
|
||||
dependency* dep = nullptr;
|
||||
expr_ref r = canonize(e, dep);
|
||||
if (get_length(r, len2)) {
|
||||
SASSERT(len1 == len2);
|
||||
}
|
||||
else {
|
||||
std::cout << r << "does not have a length\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -2615,7 +2626,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
|
|||
m_rep.update(l, r, deps);
|
||||
enode* n1 = ensure_enode(l);
|
||||
enode* n2 = ensure_enode(r);
|
||||
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_bounded_pp(r, m) << "\n"; display_deps(tout, deps);
|
||||
TRACE("seq", tout << mk_bounded_pp(l, m, 2) << " ==> " << mk_bounded_pp(r, m, 2) << "\n"; display_deps(tout, deps);
|
||||
tout << (n1->get_root() == n2->get_root()) << "\n";);
|
||||
propagate_eq(deps, n1, n2);
|
||||
return true;
|
||||
|
|
@ -3609,7 +3620,7 @@ bool theory_seq::internalize_term(app* term) {
|
|||
}
|
||||
|
||||
void theory_seq::add_length(expr* e, expr* l) {
|
||||
TRACE("seq", tout << get_context().get_scope_level() << " " << mk_pp(e, m) << "\n";);
|
||||
TRACE("seq", tout << get_context().get_scope_level() << " " << mk_bounded_pp(e, m, 2) << "\n";);
|
||||
SASSERT(!m_length.contains(l));
|
||||
m_length.push_back(l);
|
||||
m_has_length.insert(e);
|
||||
|
|
@ -3878,7 +3889,7 @@ void theory_seq::display(std::ostream & out) const {
|
|||
}
|
||||
|
||||
std::ostream& theory_seq::display_nc(std::ostream& out, nc const& nc) const {
|
||||
out << "not " << mk_pp(nc.contains(), m) << "\n";
|
||||
out << "not " << mk_bounded_pp(nc.contains(), m, 2) << "\n";
|
||||
display_deps(out << " <- ", nc.deps()) << "\n";
|
||||
return out;
|
||||
}
|
||||
|
|
@ -3891,7 +3902,11 @@ std::ostream& theory_seq::display_equations(std::ostream& out) const {
|
|||
}
|
||||
|
||||
std::ostream& theory_seq::display_equation(std::ostream& out, eq const& e) const {
|
||||
out << e.ls() << " = " << e.rs() << " <- \n";
|
||||
bool first = true;
|
||||
for (expr* a : e.ls()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
|
||||
out << " = ";
|
||||
for (expr* a : e.rs()) { if (first) first = false; else out << "\n"; out << mk_bounded_pp(a, m, 2); }
|
||||
out << " <- \n";
|
||||
return display_deps(out, e.dep());
|
||||
}
|
||||
|
||||
|
|
@ -3914,11 +3929,11 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co
|
|||
}
|
||||
for (unsigned j = 0; j < e.ls().size(); ++j) {
|
||||
for (expr* t : e.ls(j)) {
|
||||
out << mk_bounded_pp(t, m) << " ";
|
||||
out << mk_bounded_pp(t, m, 2) << " ";
|
||||
}
|
||||
out << " != ";
|
||||
for (expr* t : e.rs(j)) {
|
||||
out << mk_bounded_pp(t, m) << " ";
|
||||
out << mk_bounded_pp(t, m, 2) << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
|
@ -3933,8 +3948,8 @@ std::ostream& theory_seq::display_deps(std::ostream& out, literal_vector const&
|
|||
smt2_pp_environment_dbg env(m);
|
||||
params_ref p;
|
||||
for (auto const& eq : eqs) {
|
||||
out << " (= " << mk_bounded_pp(eq.first->get_owner(), m)
|
||||
<< "\n " << mk_bounded_pp(eq.second->get_owner(), m)
|
||||
out << " (= " << mk_bounded_pp(eq.first->get_owner(), m, 2)
|
||||
<< "\n " << mk_bounded_pp(eq.second->get_owner(), m, 2)
|
||||
<< ")\n";
|
||||
}
|
||||
for (literal l : lits) {
|
||||
|
|
@ -4283,9 +4298,9 @@ bool theory_seq::can_propagate() {
|
|||
|
||||
expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
|
||||
expr_ref result = expand(e, eqs);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " expands to\n" << result << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " expands to\n" << mk_bounded_pp(result, m, 2) << "\n";);
|
||||
m_rewrite(result);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " rewrites to\n" << result << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " rewrites to\n" << mk_bounded_pp(result, m, 2) << "\n";);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
@ -4436,7 +4451,7 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
|
|||
case l_undef:
|
||||
result = e;
|
||||
m_reset_cache = true;
|
||||
TRACE("seq", tout << "undef: " << result << "\n";
|
||||
TRACE("seq", tout << "undef: " << mk_bounded_pp(result, m, 2) << "\n";
|
||||
tout << lit << "@ level: " << ctx.get_scope_level() << "\n";);
|
||||
break;
|
||||
}
|
||||
|
|
@ -4444,9 +4459,9 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
|
|||
}
|
||||
else if (m_util.str.is_itos(e, e1)) {
|
||||
rational val;
|
||||
TRACE("seq", tout << mk_pp(e, m) << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
|
||||
if (get_num_value(e1, val)) {
|
||||
TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " -> " << val << "\n";);
|
||||
expr_ref num(m), res(m);
|
||||
num = m_autil.mk_numeral(val, true);
|
||||
if (!ctx.e_internalized(num)) {
|
||||
|
|
@ -4536,7 +4551,7 @@ void theory_seq::enque_axiom(expr* e) {
|
|||
}
|
||||
|
||||
void theory_seq::deque_axiom(expr* n) {
|
||||
TRACE("seq", tout << "deque: " << mk_pp(n, m) << "\n";);
|
||||
TRACE("seq", tout << "deque: " << mk_bounded_pp(n, m, 2) << "\n";);
|
||||
if (m_util.str.is_length(n)) {
|
||||
add_length_axiom(n);
|
||||
}
|
||||
|
|
@ -5141,7 +5156,7 @@ this translates to:
|
|||
|
||||
|
||||
void theory_seq::add_extract_axiom(expr* e) {
|
||||
TRACE("seq", tout << mk_pp(e, m) << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
|
||||
expr* s = nullptr, *i = nullptr, *l = nullptr;
|
||||
VERIFY(m_util.str.is_extract(e, s, i, l));
|
||||
if (is_tail(s, i, l)) {
|
||||
|
|
@ -5247,7 +5262,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
|
|||
l < 0 => e = empty
|
||||
*/
|
||||
void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
|
||||
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";);
|
||||
expr_ref le = mk_len(e);
|
||||
expr_ref ls = mk_len(s);
|
||||
expr_ref ls_minus_l(mk_sub(ls, l), m);
|
||||
|
|
@ -5362,7 +5377,7 @@ void theory_seq::add_nth_axiom(expr* e) {
|
|||
lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
|
||||
*/
|
||||
void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
|
||||
TRACE("seq", tout << "ensure-nth: " << lit << " " << mk_pp(s, m) << " " << mk_pp(idx, m) << "\n";);
|
||||
TRACE("seq", tout << "ensure-nth: " << lit << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(idx, m, 2) << "\n";);
|
||||
rational r;
|
||||
SASSERT(get_context().get_assignment(lit) == l_true);
|
||||
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
|
||||
|
|
@ -5587,7 +5602,7 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
|
|||
if (!lits.empty()) { ctx.display_literals_verbose(tout, lits) << "\n"; });
|
||||
|
||||
TRACE("seq",
|
||||
tout << "assert: " << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << " <- \n";
|
||||
tout << "assert: " << mk_bounded_pp(e1, m, 2) << " = " << mk_bounded_pp(e2, m, 2) << " <- \n";
|
||||
tout << lits << "\n";);
|
||||
|
||||
justification* js =
|
||||
|
|
@ -5806,7 +5821,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
|
|||
}
|
||||
m_exclude.update(e1, e2);
|
||||
expr_ref eq(m.mk_eq(e1, e2), m);
|
||||
TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);
|
||||
TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << mk_bounded_pp(eq, m, 2) << "\n";);
|
||||
m_rewrite(eq);
|
||||
if (!m.is_false(eq)) {
|
||||
literal lit = mk_eq(e1, e2, false);
|
||||
|
|
@ -6207,7 +6222,7 @@ bool theory_seq::canonizes(bool sign, expr* e) {
|
|||
context& ctx = get_context();
|
||||
dependency* deps = nullptr;
|
||||
expr_ref cont = canonize(e, deps);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";
|
||||
TRACE("seq", tout << mk_bounded_pp(e, m, 2) << " -> " << mk_bounded_pp(cont, m, 2) << "\n";
|
||||
if (deps) display_deps(tout, deps););
|
||||
if ((m.is_true(cont) && !sign) ||
|
||||
(m.is_false(cont) && sign)) {
|
||||
|
|
|
|||
|
|
@ -85,3 +85,48 @@ void rational::finalize() {
|
|||
DEALLOC_MUTEX(g_powers_of_two);
|
||||
}
|
||||
|
||||
bool rational::limit_denominator(rational &num, rational const& limit) {
|
||||
rational n, d;
|
||||
n = numerator(num);
|
||||
d = denominator(num);
|
||||
if (d < limit) return false;
|
||||
|
||||
/*
|
||||
Iteratively computes approximation using continuous fraction
|
||||
decomposition
|
||||
|
||||
p(-1) = 0, p(0) = 1
|
||||
p(j) = t(j)*p(j-1) + p(j-2)
|
||||
|
||||
q(-1) = 1, q(0) = 0
|
||||
q(j) = t(j)*q(j-1) + q(j-2)
|
||||
|
||||
cf[t1; t2, ..., tr] = p(r) / q(r) for r >= 1
|
||||
reference: https://www.math.u-bordeaux.fr/~pjaming/M1/exposes/MA2.pdf
|
||||
*/
|
||||
|
||||
rational p0(0), p1(1);
|
||||
rational q0(1), q1(0);
|
||||
|
||||
while (!d.is_zero()) {
|
||||
rational tj(0), rem(0);
|
||||
rational p2(0), q2(0);
|
||||
tj = div(n, d);
|
||||
|
||||
q2 = tj * q1 + q0;
|
||||
p2 = tj * p1 + p0;
|
||||
if (q2 >= limit) {
|
||||
num = p2/q2;
|
||||
return true;
|
||||
}
|
||||
rem = n - tj * d;
|
||||
p0 = p1;
|
||||
p1 = p2;
|
||||
q0 = q1;
|
||||
q1 = q2;
|
||||
n = d;
|
||||
d = rem;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -421,6 +421,8 @@ public:
|
|||
}
|
||||
return num_bits;
|
||||
}
|
||||
|
||||
static bool limit_denominator(rational &num, rational const& limit);
|
||||
};
|
||||
|
||||
inline bool operator!=(rational const & r1, rational const & r2) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue