mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 23:43:59 +00:00
Code Activity

Merge branch 'master' into polysat

Browse source
This commit is contained in:
Jakob Rath 2022-07-21 12:56:50 +02:00
commit e168d8a2eb
109 changed files with 4372 additions and 2743 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params_helper.pyg
View file

@ -72,7 +72,7 @@ def_module_params(module_name='smt',
('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),

5
src/smt/smt_internalizer.cpp
View file

@ -1429,7 +1429,10 @@ namespace smt {
inc_ref(l2);
m_watches[(~l1).index()].insert_literal(l2);
m_watches[(~l2).index()].insert_literal(l1);
if (get_assignment(l2) == l_false) {
if (get_assignment(l1) == l_false) {
assign(l2, b_justification(~l1));
}
else if (get_assignment(l2) == l_false) {
assign(l1, b_justification(~l2));
}
m_clause_proof.add(l1, l2, k, j);

4
src/smt/smt_model_checker.cpp
View file

@ -258,7 +258,7 @@ namespace smt {
bindings.set(num_decls - i - 1, sk_value);
}
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n" << defs << "\n";);
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\ndefs:\n" << defs << "\n";);
if (!defs.empty()) def = mk_and(defs);
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation, def.get());
@ -453,7 +453,7 @@ namespace smt {
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && (!m_context->validate_model())) {
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
// this time force expanding recursive function definitions
// that are not forced true in the current model.

5
src/smt/tactic/smt_tactic_core.cpp
View file

@ -348,6 +348,7 @@ public:
m_eq_eh = nullptr;
m_diseq_eh = nullptr;
m_created_eh = nullptr;
m_decide_eh = nullptr;
}
void user_propagate_init(
@ -385,6 +386,10 @@ public:
void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override {
m_created_eh = created_eh;
}
void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override {
m_decide_eh = decide_eh;
}
};
static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {

10
src/smt/theory_arith_core.h
View file

@ -492,6 +492,7 @@ namespace smt {
void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq, bool simplify_conseq) {
th_rewriter & s = ctx.get_rewriter();
expr_ref s_ante(m), s_conseq(m);
expr_ref p_ante(ante, m), p_conseq(conseq, m); // pinned versions
expr* s_conseq_n, * s_ante_n;
bool negated;
@ -562,7 +563,7 @@ namespace smt {
if (!m_util.is_zero(divisor)) {
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
expr_ref eqz(m), eq(m), lower(m), upper(m), qr(m);
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_int(0);
@ -570,7 +571,8 @@ namespace smt {
abs_divisor = m_util.mk_sub(m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor), one);
s(abs_divisor);
eqz = m.mk_eq(divisor, zero);
eq = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
qr = m_util.mk_add(m_util.mk_mul(divisor, div), mod);
eq = m.mk_eq(qr, dividend);
lower = m_util.mk_ge(mod, zero);
upper = m_util.mk_le(mod, abs_divisor);
TRACE("div_axiom_bug",
@ -584,6 +586,8 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(mod));
if (m_util.is_zero(dividend)) {
mk_axiom(eqz, m.mk_eq(div, zero));
mk_axiom(eqz, m.mk_eq(mod, zero));
@ -591,7 +595,7 @@ namespace smt {
// (or (= y 0) (<= (* y (div x y)) x))
else if (!m_util.is_numeral(divisor)) {
expr_ref div_ge(m), div_le(m), ge(m), le(m);
expr_ref div_ge(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
mk_axiom(eqz, div_ge, false);

63
src/smt/theory_arith_nl.h
View file

@ -80,14 +80,12 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
if (is_fixed(v))
return;
column & c = m_columns[v];
typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries();
for (; it != end; ++it) {
if (it->is_dead() || already_visited_rows.contains(it->m_row_id))
for (auto& ce : c) {
if (ce.is_dead() || already_visited_rows.contains(ce.m_row_id))
continue;
TRACE("non_linear_bug", tout << "visiting row: " << it->m_row_id << "\n";);
already_visited_rows.insert(it->m_row_id);
row & r = m_rows[it->m_row_id];
TRACE("non_linear_bug", tout << "visiting row: " << ce.m_row_id << "\n";);
already_visited_rows.insert(ce.m_row_id);
row & r = m_rows[ce.m_row_id];
theory_var s = r.get_base_var();
// ignore quasi base vars... actually they should not be used if the problem is non linear...
if (is_quasi_base(s))
@ -97,14 +95,10 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
// was eliminated by substitution.
if (s != null_theory_var && is_free(s) && s != v)
continue;
typename vector<row_entry>::const_iterator it2 = r.begin_entries();
typename vector<row_entry>::const_iterator end2 = r.end_entries();
for (; it2 != end2; ++it2) {
if (!it2->is_dead() && !is_fixed(it2->m_var))
mark_var(it2->m_var, vars, already_found);
if (!it2->is_dead() && is_fixed(it2->m_var)) {
TRACE("non_linear", tout << "skipped fixed\n";);
}
for (auto& re : r) {
if (!re.is_dead() && !is_fixed(re.m_var))
mark_var(re.m_var, vars, already_found);
CTRACE("non_linear", !re.is_dead() && is_fixed(re.m_var), tout << "skipped fixed\n");
}
}
}
@ -119,6 +113,7 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
return;
var_set already_found;
row_set already_visited_rows;
for (theory_var v : m_nl_monomials) {
expr * n = var2expr(v);
if (ctx.is_relevant(n))
@ -130,9 +125,9 @@ void theory_arith<Ext>::get_non_linear_cluster(svector<theory_var> & vars) {
TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";);
mark_dependents(v, vars, already_found, already_visited_rows);
}
TRACE("non_linear", tout << "variables in non linear cluster:\n";
for (theory_var v : vars) tout << "v" << v << " ";
tout << "\n";);
TRACE("non_linear", tout << "variables in non linear cluster: ";
for (theory_var v : vars) tout << "v" << v << " "; tout << "\n";
for (theory_var v : m_nl_monomials) tout << "non-linear v" << v << " " << mk_pp(var2expr(v), m) << "\n";);
}
@ -1740,22 +1735,21 @@ grobner::monomial * theory_arith<Ext>::mk_gb_monomial(rational const & _coeff, e
*/
template<typename Ext>
void theory_arith<Ext>::add_row_to_gb(row const & r, grobner & gb) {
TRACE("non_linear", tout << "adding row to gb\n"; display_row(tout, r););
TRACE("grobner", tout << "adding row to gb\n"; display_row(tout, r););
ptr_buffer<grobner::monomial> monomials;
v_dependency * dep = nullptr;
m_tmp_var_set.reset();
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead()) {
rational coeff = it->m_coeff.to_rational();
expr * m = var2expr(it->m_var);
TRACE("non_linear", tout << "monomial: " << mk_pp(m, get_manager()) << "\n";);
grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set);
TRACE("non_linear", tout << "new monomial:\n"; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
if (new_m)
monomials.push_back(new_m);
}
for (auto& re : r) {
if (re.is_dead())
continue;
rational coeff = re.m_coeff.to_rational();
expr * m = var2expr(re.m_var);
grobner::monomial * new_m = mk_gb_monomial(coeff, m, gb, dep, m_tmp_var_set);
if (new_m)
monomials.push_back(new_m);
TRACE("grobner",
tout << "monomial: " << mk_pp(m, get_manager()) << "\n";
tout << "new monomial: "; if (new_m) gb.display_monomial(tout, *new_m); else tout << "null"; tout << "\n";);
}
gb.assert_eq_0(monomials.size(), monomials.data(), dep);
}
@ -2158,8 +2152,9 @@ bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equ
eqs.reset();
gb.get_equations(eqs);
TRACE("grobner", tout << "after gb\n";
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); };
for (grobner::equation* eq : eqs)
gb.display_equation(tout, *eq);
gb.display_equation(tout, *eq, _fn);
);
for (grobner::equation* eq : eqs) {
if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) {
@ -2259,7 +2254,9 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
ptr_vector<grobner::equation> eqs;
do {
TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
TRACE("grobner", tout << "before grobner:\n";
std::function<void(std::ostream& out, expr* v)> _fn = [&](std::ostream& out, expr* v) { out << "v" << expr2var(v); };
gb.display(tout, _fn));
compute_basis(gb, warn);
update_statistics(gb);
TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););

2
src/smt/theory_array_base.cpp
View file

@ -101,7 +101,7 @@ namespace smt {
SASSERT(num_args >= 3);
sel_args.push_back(n);
for (unsigned i = 1; i < num_args - 1; ++i) {
sel_args.push_back(to_app(n->get_arg(i)));
sel_args.push_back(n->get_arg(i));
}
expr_ref sel(m);
sel = mk_select(sel_args.size(), sel_args.data());

9
src/smt/theory_array_full.cpp
View file

@ -594,10 +594,13 @@ namespace smt {
if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr))
return false;
m_stats.m_num_default_lambda_axiom++;
expr* def = mk_default(arr->get_expr());
expr* e = arr->get_expr();
expr* def = mk_default(e);
quantifier* lam = m.is_lambda_def(arr->get_decl());
expr_ref_vector args(m);
args.push_back(lam);
TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n");
expr_ref_vector args(m);
var_subst subst(m, false);
args.push_back(subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args()));
for (unsigned i = 0; i < lam->get_num_decls(); ++i)
args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
expr_ref val(mk_select(args), m);

34
src/smt/theory_bv.cpp
View file

@ -52,9 +52,8 @@ namespace smt {
bits.reset();
m_bits_expr.reset();
for (unsigned i = 0; i < bv_size; i++) {
for (unsigned i = 0; i < bv_size; i++)
m_bits_expr.push_back(mk_bit2bool(owner, i));
}
ctx.internalize(m_bits_expr.data(), bv_size, true);
for (unsigned i = 0; i < bv_size; i++) {
@ -601,9 +600,8 @@ namespace smt {
TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
process_args(n);
mk_enode(n);
if (!ctx.relevancy()) {
if (!ctx.relevancy())
assert_bv2int_axiom(n);
}
}
@ -669,10 +667,12 @@ namespace smt {
mk_enode(n);
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
mk_bits(v);
if (!ctx.relevancy()) {
enode* k = ctx.get_enode(n->get_arg(0));
if (!is_attached_to_var(k))
mk_var(k);
if (!ctx.relevancy())
assert_int2bv_axiom(n);
}
}
void theory_bv::assert_int2bv_axiom(app* n) {
@ -1497,6 +1497,26 @@ namespace smt {
unsigned sz = m_bits[v1].size();
bool changed = true;
TRACE("bv", tout << "bits size: " << sz << "\n";);
if (sz == 0) {
// int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
enode* n1 = get_enode(r1);
for (enode* bv2int : *n1) {
if (!m_util.is_bv2int(bv2int->get_expr()))
continue;
enode* bv2int_arg = bv2int->get_arg(0);
for (enode* p : enode::parents(n1->get_root())) {
if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) {
enode_pair_vector eqs;
eqs.push_back({n1, p->get_arg(0) });
eqs.push_back({n1, bv2int});
justification * js = ctx.mk_justification(
ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
ctx.assign_eq(p, bv2int_arg, eq_justification(js));
break;
}
}
}
}
do {
// This outerloop is necessary to avoid missing propagation steps.
// For example, let's assume that bits1 and bits2 contains the following

66
src/smt/theory_datatype.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "smt/theory_datatype.h"
#include "smt/theory_array.h"
#include "smt/smt_model_generator.h"
#include <iostream>
namespace smt {
@ -519,9 +520,8 @@ namespace smt {
void theory_datatype::explain_is_child(enode* parent, enode* child) {
enode * parentc = oc_get_cstor(parent);
if (parent != parentc) {
if (parent != parentc)
m_used_eqs.push_back(enode_pair(parent, parentc));
}
// collect equalities on all children that may have been used.
bool found = false;
@ -546,14 +546,17 @@ namespace smt {
}
sort* se = nullptr;
if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
for (enode* aarg : get_seq_args(arg)) {
enode* sibling;
for (enode* aarg : get_seq_args(arg, sibling)) {
if (aarg->get_root() == child->get_root()) {
if (aarg != child) {
if (aarg != child)
m_used_eqs.push_back(enode_pair(aarg, child));
}
found = true;
}
}
if (sibling && sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
}
}
VERIFY(found);
@ -582,9 +585,11 @@ namespace smt {
TRACE("datatype",
tout << "occurs_check\n";
for (enode_pair const& p : m_used_eqs) {
for (enode_pair const& p : m_used_eqs)
tout << enode_eq_pp(p, ctx);
});
for (auto const& [a,b] : m_used_eqs)
tout << mk_pp(a->get_expr(), m) << " = " << mk_pp(b->get_expr(), m) << "\n";
);
}
// start exploring subgraph below `app`
@ -596,9 +601,9 @@ namespace smt {
}
v = m_find.find(v);
var_data * d = m_var_data[v];
if (!d->m_constructor) {
if (!d->m_constructor)
return false;
}
enode * parent = d->m_constructor;
oc_mark_on_stack(parent);
auto process_arg = [&](enode* aarg) {
@ -616,9 +621,8 @@ namespace smt {
};
for (enode * arg : enode::args(parent)) {
if (oc_cycle_free(arg)) {
if (oc_cycle_free(arg))
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(parent, arg);
@ -632,9 +636,11 @@ namespace smt {
oc_push_stack(arg);
}
else if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
for (enode* sarg : get_seq_args(arg))
if (process_arg(sarg))
enode* sibling;
for (enode* sarg : get_seq_args(arg, sibling)) {
if (process_arg(sarg))
return true;
}
}
else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
for (enode* aarg : get_array_args(arg))
@ -645,7 +651,7 @@ namespace smt {
return false;
}
ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n) {
ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n, enode*& sibling) {
m_args.reset();
m_todo.reset();
auto add_todo = [&](enode* n) {
@ -654,9 +660,14 @@ namespace smt {
m_todo.push_back(n);
}
};
for (enode* sib : *n)
add_todo(sib);
for (enode* sib : *n) {
if (m_sutil.str.is_concat_of_units(sib->get_expr())) {
add_todo(sib);
sibling = sib;
break;
}
}
for (unsigned i = 0; i < m_todo.size(); ++i) {
enode* n = m_todo[i];
@ -691,7 +702,7 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
TRACE("datatype_verbose", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
m_stats.m_occurs_check++;
bool res = false;
@ -706,7 +717,7 @@ namespace smt {
if (oc_cycle_free(app))
continue;
TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);
TRACE("datatype_verbose", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) {
case ENTER:
@ -830,15 +841,14 @@ namespace smt {
SASSERT(d->m_constructor);
func_decl * c_decl = d->m_constructor->get_decl();
datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
for (enode* arg : enode::args(d->m_constructor)) {
for (enode* arg : enode::args(d->m_constructor))
result->add_dependency(arg);
}
TRACE("datatype",
tout << pp(n, m) << "\n";
tout << "depends on\n";
for (enode* arg : enode::args(d->m_constructor)) {
for (enode* arg : enode::args(d->m_constructor))
tout << " " << pp(arg, m) << "\n";
});
);
return result;
}
@ -965,12 +975,11 @@ namespace smt {
SASSERT(!lits.empty());
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_expr(), m) << "\n";
for (literal l : lits) {
for (literal l : lits)
ctx.display_detailed_literal(tout, l) << "\n";
}
for (auto const& p : eqs) {
for (auto const& p : eqs)
tout << enode_eq_pp(p, ctx);
});
);
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.data(), eqs.size(), eqs.data())));
}
else if (num_unassigned == 1) {
@ -1052,9 +1061,8 @@ namespace smt {
ctx.mark_as_relevant(curr);
return;
}
else if (ctx.get_assignment(curr) != l_false) {
else if (ctx.get_assignment(curr) != l_false)
return;
}
}
if (r == nullptr)
return; // all recognizers are asserted to false... conflict will be detected...

2
src/smt/theory_datatype.h
View file

@ -94,7 +94,7 @@ namespace smt {
void oc_push_stack(enode * n);
ptr_vector<enode> m_args, m_todo;
ptr_vector<enode> const& get_array_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n);
ptr_vector<enode> const& get_seq_args(enode* n, enode*& sibling);
// class for managing state of final_check
class final_check_st {

83
src/smt/theory_lra.cpp
View file

@ -276,23 +276,23 @@ class theory_lra::imp {
m_nla->push();
}
smt_params_helper prms(ctx().get_params());
m_nla->settings().run_order() = prms.arith_nl_order();
m_nla->settings().run_tangents() = prms.arith_nl_tangents();
m_nla->settings().run_horner() = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed() = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner() = prms.arith_nl_grobner();
m_nla->settings().run_nra() = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified() = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching() = false;
m_nla->settings().run_order = prms.arith_nl_order();
m_nla->settings().run_tangents = prms.arith_nl_tangents();
m_nla->settings().run_horner = prms.arith_nl_horner();
m_nla->settings().horner_subs_fixed = prms.arith_nl_horner_subs_fixed();
m_nla->settings().horner_frequency = prms.arith_nl_horner_frequency();
m_nla->settings().horner_row_length_limit = prms.arith_nl_horner_row_length_limit();
m_nla->settings().run_grobner = prms.arith_nl_grobner();
m_nla->settings().run_nra = prms.arith_nl_nra();
m_nla->settings().grobner_subs_fixed = prms.arith_nl_grobner_subs_fixed();
m_nla->settings().grobner_eqs_growth = prms.arith_nl_grobner_eqs_growth();
m_nla->settings().grobner_expr_size_growth = prms.arith_nl_grobner_expr_size_growth();
m_nla->settings().grobner_expr_degree_growth = prms.arith_nl_grobner_expr_degree_growth();
m_nla->settings().grobner_max_simplified = prms.arith_nl_grobner_max_simplified();
m_nla->settings().grobner_number_of_conflicts_to_report = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching = false;
}
}
@ -1224,9 +1224,9 @@ public:
return;
}
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
ctx().get_rewriter()(mod_r);
expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
ctx().internalize(eq_r, false);
ctx().internalize(eq_r, false);
literal eq = ctx().get_literal(eq_r);
rational k(0);
@ -1256,6 +1256,39 @@ public:
}
else {
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
expr_ref mone(a.mk_int(-1), m);
expr_ref modmq(a.mk_sub(mod, abs_q), m);
ctx().get_rewriter()(modmq);
literal eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal mod_lt_q = mk_literal(a.mk_le(modmq, mone));
// q = 0 or p = (p mod q) + q * (p div q)
// q = 0 or (p mod q) >= 0
// q = 0 or (p mod q) < abs(q)
mk_axiom(eqz, eq);
mk_axiom(eqz, mod_ge_0);
mk_axiom(eqz, mod_lt_q);
m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
if (a.is_zero(p)) {
mk_axiom(eqz, mk_literal(m.mk_eq(div, zero)));
mk_axiom(eqz, mk_literal(m.mk_eq(mod, zero)));
}
// (or (= y 0) (<= (* y (div x y)) x))
else if (!a.is_numeral(q)) {
expr_ref div_ge(m);
div_ge = a.mk_ge(a.mk_sub(p, a.mk_mul(q, div)), zero);
ctx().get_rewriter()(div_ge);
mk_axiom(eqz, mk_literal(div_ge));
TRACE("arith", tout << eqz << " " << div_ge << "\n");
}
#if 0
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));
/*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero));
@ -1266,7 +1299,7 @@ public:
// q >= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) >= 0
// q <= 0 or (p mod q) < q
// q >= 0 or (p mod q) < -q
// q >= 0 or (p mod q) < -q
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
@ -1277,11 +1310,11 @@ public:
mk_axiom(q_le_0, mod_ge_0);
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
#endif
#if 0
// seem expensive
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
mk_axiom(q_le_0, ~p_le_0, div_le_0);
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
@ -1293,19 +1326,21 @@ public:
mk_axiom(q_ge_0, p_le_0, ~div_ge_0);
#endif
#if 0
std::function<void(void)> log = [&,this]() {
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
};
if_trace_stream _ts(m, log);
#endif
#if 0
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
#endif
};
if_trace_stream _ts(m, log);
}
if (params().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();

22
src/smt/theory_recfun.cpp
View file

@ -43,32 +43,32 @@ namespace smt {
char const * theory_recfun::get_name() const { return "recfun"; }
theory* theory_recfun::mk_fresh(context* new_ctx) {
theory* theory_recfun::mk_fresh(context* new_ctx) {
return alloc(theory_recfun, *new_ctx);
}
bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
TRACE("recfun", tout << mk_pp(atom, m) << " " << u().has_defs() << "\n");
if (!u().has_defs()) {
// if (u().is_defined(atom))
// throw default_exception("recursive atom definition is out of scope");
return false;
}
for (expr * arg : *atom) {
for (expr * arg : *atom)
ctx.internalize(arg, false);
}
if (!ctx.e_internalized(atom)) {
if (!ctx.e_internalized(atom))
ctx.mk_enode(atom, false, true, true);
}
if (!ctx.b_internalized(atom)) {
bool_var v = ctx.mk_bool_var(atom);
ctx.set_var_theory(v, get_id());
}
if (!ctx.relevancy() && u().is_defined(atom)) {
if (!ctx.b_internalized(atom))
ctx.set_var_theory(ctx.mk_bool_var(atom), get_id());
if (!ctx.relevancy() && u().is_defined(atom))
push_case_expand(atom);
}
return true;
}
bool theory_recfun::internalize_term(app * term) {
if (!u().has_defs()) {
// if (u().is_defined(term))
// throw default_exception("recursive term definition is out of scope");
return false;
}
for (expr* e : *term) {

40
src/smt/theory_seq.cpp
View file

@ -2783,26 +2783,25 @@ bool theory_seq::get_length(expr* e, rational& val) {
todo.push_back(e1);
todo.push_back(e2);
}
else if (m_util.str.is_unit(c)) {
else if (m_util.str.is_unit(c))
val += rational(1);
}
else if (m_util.str.is_empty(c)) {
else if (m_util.str.is_empty(c))
continue;
}
else if (m_util.str.is_string(c, s)) {
else if (m_util.str.is_map(c, e1, e2))
todo.push_back(e2);
else if (m_util.str.is_mapi(c, e1, e2, c))
todo.push_back(c);
else if (m_util.str.is_string(c, s))
val += rational(s.length());
}
else if (!has_length(c)) {
len = mk_len(c);
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";);
return false;
}
else {
len = mk_len(c);
if (m_arith_value.get_value(len, val1) && !val1.is_neg()) {
val += val1;
if (!has_length(c)) {
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";);
return false;
}
else if (m_arith_value.get_value(len, val1) && !val1.is_neg())
val += val1;
else {
TRACE("seq", tout << "length has not been internalized " << mk_pp(c, m) << "\n";);
return false;
@ -3071,9 +3070,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
}
else if (m_util.str.is_is_digit(e)) {
}
else if (m_util.str.is_foldl(e) || m_util.str.is_foldli(e)) {
}
else {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << mk_pp(e, m) << "\n");
UNREACHABLE();
}
}
@ -3216,18 +3219,15 @@ void theory_seq::relevant_eh(app* n) {
add_ubv_string(n);
expr* arg = nullptr;
if (m_sk.is_tail(n, arg)) {
if (m_sk.is_tail(n, arg))
add_length_limit(arg, m_max_unfolding_depth, true);
}
if (m_util.str.is_length(n, arg) && !has_length(arg) && ctx.e_internalized(arg)) {
if (m_util.str.is_length(n, arg) && !has_length(arg) && ctx.e_internalized(arg))
add_length_to_eqc(arg);
}
if (m_util.str.is_replace_all(n) ||
m_util.str.is_replace_re(n) ||
m_util.str.is_replace_re_all(n)
) {
m_util.str.is_replace_re_all(n)) {
add_unhandled_expr(n);
}
}