mirror of
https://github.com/Z3Prover/z3
synced 2026-07-04 06:16:09 +00:00
Merge branch 'master' into derive-with-ranges
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
2703351f54
149 changed files with 6936 additions and 2049 deletions
|
|
@ -4672,7 +4672,6 @@ namespace smt {
|
|||
theory_id th_id = l->get_id();
|
||||
|
||||
for (enode * parent : enode::parents(n)) {
|
||||
auto p = parent->get_expr();
|
||||
family_id fid = parent->get_family_id();
|
||||
if (fid != th_id && fid != m.get_basic_family_id()) {
|
||||
if (is_beta_redex(parent, n))
|
||||
|
|
|
|||
|
|
@ -219,7 +219,7 @@ namespace smt {
|
|||
|
||||
if (use_inv) {
|
||||
unsigned sk_term_gen = 0;
|
||||
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
|
||||
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, *cex, sk_term_gen);
|
||||
if (sk_term != nullptr) {
|
||||
TRACE(model_checker, tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
|
||||
SASSERT(!m.is_model_value(sk_term));
|
||||
|
|
@ -233,15 +233,10 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
expr * sk_term = get_term_from_ctx(sk_value);
|
||||
func_decl * f = nullptr;
|
||||
if (sk_term != nullptr) {
|
||||
TRACE(model_checker, tout << "sk term " << mk_pp(sk_term, m) << "\n");
|
||||
sk_value = sk_term;
|
||||
}
|
||||
// last ditch: am I an array?
|
||||
else if (false && autil.is_as_array(sk_value, f) && cex->get_func_interp(f) && cex->get_func_interp(f)->get_array_interp(f)) {
|
||||
sk_value = cex->get_func_interp(f)->get_array_interp(f);
|
||||
}
|
||||
|
||||
}
|
||||
if (contains_model_value(sk_value)) {
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ Revision History:
|
|||
--*/
|
||||
#include "util/backtrackable_set.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/has_free_vars.h"
|
||||
#include "ast/macros/macro_util.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
|
|
@ -31,6 +32,7 @@ Revision History:
|
|||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/well_sorted.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/rewriter/term_enumeration.h"
|
||||
#include "model/model_pp.h"
|
||||
#include "model/model_macro_solver.h"
|
||||
#include "smt/smt_model_finder.h"
|
||||
|
|
@ -107,9 +109,15 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
expr* get_inv(expr* v) const {
|
||||
expr* get_inv(expr* v, model& mdl) const {
|
||||
expr* t = nullptr;
|
||||
m_inv.find(v, t);
|
||||
if (!t) {
|
||||
for (auto [k, term] : m_inv) {
|
||||
if (mdl.are_equal(k, v))
|
||||
return term;
|
||||
}
|
||||
}
|
||||
return t;
|
||||
}
|
||||
|
||||
|
|
@ -120,14 +128,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
void mk_inverse(evaluator& ev) {
|
||||
for (auto const& kv : m_elems) {
|
||||
expr* t = kv.m_key;
|
||||
for (auto const &[t, gen] : m_elems) {
|
||||
SASSERT(!contains_model_value(t));
|
||||
unsigned gen = kv.m_value;
|
||||
expr* t_val = ev.eval(t, true);
|
||||
if (!t_val) break;
|
||||
TRACE(model_finder, tout << mk_pp(t, m) << " " << mk_pp(t_val, m) << "\n";);
|
||||
|
||||
expr* old_t = nullptr;
|
||||
if (m_inv.find(t_val, old_t)) {
|
||||
unsigned old_t_gen = 0;
|
||||
|
|
@ -187,14 +192,14 @@ namespace smt {
|
|||
\brief Base class used to solve model construction constraints.
|
||||
*/
|
||||
class node {
|
||||
unsigned m_id;
|
||||
node* m_find{ nullptr };
|
||||
unsigned m_eqc_size{ 1 };
|
||||
unsigned m_id = 0;
|
||||
node* m_find = nullptr;
|
||||
unsigned m_eqc_size = 1;
|
||||
|
||||
sort* m_sort; // sort of the elements in the instantiation set.
|
||||
sort* m_sort = nullptr; // sort of the elements in the instantiation set.
|
||||
|
||||
bool m_mono_proj{ false }; // relevant for integers & reals & bit-vectors
|
||||
bool m_signed_proj{ false }; // relevant for bit-vectors.
|
||||
bool m_mono_proj = false; // relevant for integers & reals & bit-vectors
|
||||
bool m_signed_proj = false; // relevant for bit-vectors.
|
||||
ptr_vector<node> m_avoid_set;
|
||||
ptr_vector<expr> m_exceptions;
|
||||
|
||||
|
|
@ -291,7 +296,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void insert(expr* n, unsigned generation) {
|
||||
if (is_ground(n))
|
||||
if (is_ground(n) || (has_quantifiers(n) && !has_free_vars(n))) // this is a closed term
|
||||
get_root()->m_set->insert(n, generation);
|
||||
}
|
||||
|
||||
|
|
@ -599,7 +604,10 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
r = tmp;
|
||||
TRACE(model_finder, tout << "eval\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
|
||||
TRACE(model_finder, tout << "eval-failed\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
|
||||
if (is_lambda(tmp)) {
|
||||
r = m.mk_fresh_const("lambda", tmp->get_sort());
|
||||
}
|
||||
}
|
||||
m_eval_cache[model_completion].insert(n, r);
|
||||
m_eval_cache_range.push_back(r);
|
||||
|
|
@ -1235,8 +1243,8 @@ namespace smt {
|
|||
void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector<instantiation_set>& uvar_inst_sets, context* ctx) override {
|
||||
if (m_f != mhead)
|
||||
return;
|
||||
uvar_inst_sets.reserve(m_var_j + 1, 0);
|
||||
if (uvar_inst_sets[m_var_j] == 0)
|
||||
uvar_inst_sets.reserve(m_var_j + 1, nullptr);
|
||||
if (uvar_inst_sets[m_var_j] == nullptr)
|
||||
uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager());
|
||||
instantiation_set* s = uvar_inst_sets[m_var_j];
|
||||
SASSERT(s != nullptr);
|
||||
|
|
@ -1369,6 +1377,79 @@ namespace smt {
|
|||
|
||||
};
|
||||
|
||||
class ho_var : public qinfo {
|
||||
unsigned m_var_i;
|
||||
public:
|
||||
ho_var(ast_manager& m, unsigned i) : qinfo(m), m_var_i(i) {
|
||||
}
|
||||
|
||||
char const *get_kind() const override {
|
||||
return "ho_var";
|
||||
}
|
||||
|
||||
bool is_equal(qinfo const *qi) const override {
|
||||
if (qi->get_kind() != get_kind())
|
||||
return false;
|
||||
ho_var const *other = static_cast<ho_var const *>(qi);
|
||||
return m_var_i == other->m_var_i;
|
||||
}
|
||||
|
||||
void display(std::ostream &out) const override {
|
||||
out << "(" << "ho-var: " << m_var_i << ")";
|
||||
}
|
||||
|
||||
void process_auf(quantifier *q, auf_solver &s, context *ctx) override {
|
||||
/* node * S_i = */ s.get_uvar(q, m_var_i);
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier *q, auf_solver &s, context *ctx) override {
|
||||
node *S = s.get_uvar(q, m_var_i);
|
||||
sort *srt = S->get_sort();
|
||||
|
||||
IF_VERBOSE(3, verbose_stream() << "ho_var::populate_inst_sets: " << q->get_id() << " " << mk_pp(srt, m) << "\n";);
|
||||
term_enumeration tn(m);
|
||||
// Add ground terms of type S.
|
||||
// Add productions for functions in E-graph
|
||||
// add other possible relevant functions such as equality over srt, Boolean operators
|
||||
|
||||
ast_mark visited;
|
||||
tn.add_production(m.mk_true());
|
||||
tn.add_production(m.mk_false());
|
||||
for (enode *n : ctx->enodes()) {
|
||||
if (!ctx->is_relevant(n))
|
||||
continue;
|
||||
auto e = n->get_expr();
|
||||
if (srt == n->get_sort()) {
|
||||
TRACE(model_finder, tout << "inserting " << mk_pp(e, m) << " into inst set\n");
|
||||
S->insert(e, n->get_generation());
|
||||
}
|
||||
else if (is_uninterp_const(e)) {
|
||||
TRACE(model_finder, tout << "add production " << mk_pp(e, m) << "\n");
|
||||
tn.add_production(e);
|
||||
}
|
||||
else if (is_uninterp(e)) {
|
||||
auto f = to_app(e)->get_decl();
|
||||
if (visited.is_marked(f))
|
||||
continue;
|
||||
visited.mark(f, true);
|
||||
TRACE(model_finder, tout << "add function " << mk_pp(f, m) << "\n");
|
||||
tn.add_production(f);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned max_count = 20;
|
||||
for (auto t : tn.enum_terms(srt)) {
|
||||
if (max_count == 0)
|
||||
break;
|
||||
--max_count;
|
||||
unsigned generation = 0; // todo - inherited from sub-term of t?
|
||||
TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m)
|
||||
<< " to instantiation set of S" << std::endl;);
|
||||
S->insert(t, generation);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
/**
|
||||
\brief auf_arr is a term (pattern) of the form:
|
||||
|
|
@ -2105,7 +2186,10 @@ namespace smt {
|
|||
process_app(to_app(curr));
|
||||
}
|
||||
else if (is_var(curr)) {
|
||||
m_info->m_is_auf = false; // unexpected occurrence of variable.
|
||||
if (m_array_util.is_array(curr)) {
|
||||
insert_qinfo(alloc(ho_var, m, to_var(curr)->get_idx()));
|
||||
}
|
||||
m_info->m_is_auf = false;
|
||||
}
|
||||
else {
|
||||
SASSERT(is_lambda(curr));
|
||||
|
|
@ -2163,7 +2247,6 @@ namespace smt {
|
|||
}
|
||||
|
||||
SASSERT(is_quantifier(atom));
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
void process_literal(expr* atom, polarity pol) {
|
||||
|
|
@ -2203,9 +2286,15 @@ namespace smt {
|
|||
if (is_app(curr)) {
|
||||
if (to_app(curr)->get_family_id() == m.get_basic_family_id() && m.is_bool(curr)) {
|
||||
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
|
||||
case OP_IMPLIES:
|
||||
case OP_IMPLIES:
|
||||
process_literal(to_app(curr)->get_arg(0), neg(pol));
|
||||
process_literal(to_app(curr)->get_arg(1), pol);
|
||||
break;
|
||||
case OP_XOR:
|
||||
UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs
|
||||
for (expr *arg : *to_app(curr)) {
|
||||
visit_formula(arg, pol);
|
||||
visit_formula(arg, neg(pol));
|
||||
}
|
||||
break;
|
||||
case OP_OR:
|
||||
case OP_AND:
|
||||
|
|
@ -2515,11 +2604,12 @@ namespace smt {
|
|||
|
||||
Store in generation the generation of the result
|
||||
*/
|
||||
expr* model_finder::get_inv(quantifier* q, unsigned i, expr* val, unsigned& generation) {
|
||||
expr* model_finder::get_inv(quantifier* q, unsigned i, expr* val, model& mdl,unsigned& generation) {
|
||||
instantiation_set const* s = get_uvar_inst_set(q, i);
|
||||
if (s == nullptr)
|
||||
return nullptr;
|
||||
expr* t = s->get_inv(val);
|
||||
|
||||
expr* t = s->get_inv(val, mdl);
|
||||
if (m_auf_solver->is_default_representative(t))
|
||||
return val;
|
||||
if (t != nullptr) {
|
||||
|
|
@ -2555,16 +2645,27 @@ namespace smt {
|
|||
obj_map<expr, expr*> const& inv = s->get_inv_map();
|
||||
if (inv.empty())
|
||||
continue; // nothing to do
|
||||
ptr_buffer<expr> eqs;
|
||||
for (auto const& [val, _] : inv) {
|
||||
if (val->get_sort() == sk->get_sort())
|
||||
eqs.push_back(m.mk_eq(sk, val));
|
||||
expr_ref_vector eqs(m), defs(m);
|
||||
|
||||
for (auto const& [val, term] : inv) {
|
||||
if (val->get_sort() == sk->get_sort()) {
|
||||
if (is_lambda(term)) {
|
||||
eqs.push_back(m.mk_eq(sk, val));
|
||||
defs.push_back(m.mk_eq(val, term));
|
||||
}
|
||||
else
|
||||
eqs.push_back(m.mk_eq(sk, val));
|
||||
}
|
||||
}
|
||||
if (!eqs.empty()) {
|
||||
expr_ref new_cnstr(m);
|
||||
new_cnstr = m.mk_or(eqs);
|
||||
TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
|
||||
aux_ctx->assert_expr(new_cnstr);
|
||||
for (auto def : defs) {
|
||||
TRACE(model_finder, tout << "assert_def:\n" << mk_pp(def, m) << "\n";);
|
||||
aux_ctx->assert_expr(def);
|
||||
}
|
||||
asserted_something = true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ namespace smt {
|
|||
void fix_model(proto_model * m);
|
||||
|
||||
quantifier * get_flat_quantifier(quantifier * q);
|
||||
expr * get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation);
|
||||
expr * get_inv(quantifier * q, unsigned i, expr * val, model& m, unsigned & generation);
|
||||
bool restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks);
|
||||
|
||||
void restart_eh();
|
||||
|
|
|
|||
|
|
@ -396,15 +396,15 @@ namespace smt {
|
|||
}
|
||||
|
||||
final_check_status theory_array::assert_delayed_axioms() {
|
||||
if (!m_params.m_array_delay_exp_axiom)
|
||||
return FC_DONE;
|
||||
final_check_status r = FC_DONE;
|
||||
unsigned num_vars = get_num_vars();
|
||||
for (unsigned v = 0; v < num_vars; ++v) {
|
||||
var_data * d = m_var_data[v];
|
||||
if (d->m_prop_upward && instantiate_axiom2b_for(v))
|
||||
r = FC_CONTINUE;
|
||||
}
|
||||
if (m_params.m_array_delay_exp_axiom) {
|
||||
unsigned num_vars = get_num_vars();
|
||||
for (unsigned v = 0; v < num_vars; ++v) {
|
||||
var_data *d = m_var_data[v];
|
||||
if (d->m_prop_upward && instantiate_axiom2b_for(v))
|
||||
r = FC_CONTINUE;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -67,7 +67,6 @@ namespace smt {
|
|||
return mk_select(num_args, args);
|
||||
}
|
||||
|
||||
|
||||
app * theory_array_base::mk_store(unsigned num_args, expr * const * args) {
|
||||
return m.mk_app(get_family_id(), OP_STORE, 0, nullptr, num_args, args);
|
||||
}
|
||||
|
|
@ -279,7 +278,7 @@ namespace smt {
|
|||
SASSERT(n1->get_num_args() == n2->get_num_args());
|
||||
unsigned n = n1->get_num_args();
|
||||
// skipping first argument of the select.
|
||||
for(unsigned i = 1; i < n; ++i) {
|
||||
for (unsigned i = 1; i < n; ++i) {
|
||||
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -295,9 +294,8 @@ namespace smt {
|
|||
enode * r1 = v1->get_root();
|
||||
enode * r2 = v2->get_root();
|
||||
|
||||
if (r1->get_class_size() > r2->get_class_size()) {
|
||||
std::swap(r1, r2);
|
||||
}
|
||||
if (r1->get_class_size() > r2->get_class_size())
|
||||
std::swap(r1, r2);
|
||||
|
||||
m_array_value.reset();
|
||||
// populate m_array_value if the select(a, i) parent terms of r1
|
||||
|
|
@ -335,7 +333,7 @@ namespace smt {
|
|||
return false; // axiom was already instantiated
|
||||
if (already_diseq(n1, n2))
|
||||
return false;
|
||||
m_extensionality_todo.push_back(std::make_pair(n1, n2));
|
||||
m_extensionality_todo.push_back({n1, n2});
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -348,7 +346,7 @@ namespace smt {
|
|||
enode * nodes[2] = { a1, a2 };
|
||||
if (!ctx.add_fingerprint(this, 1, 2, nodes))
|
||||
return; // axiom was already instantiated
|
||||
m_congruent_todo.push_back(std::make_pair(a1, a2));
|
||||
m_congruent_todo.push_back({a1, a2});
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -581,11 +579,11 @@ namespace smt {
|
|||
enode * n2 = get_enode(v2);
|
||||
sort * s2 = n2->get_sort();
|
||||
if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
|
||||
app * eq = mk_eq_atom(n1->get_expr(), n2->get_expr());
|
||||
if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
|
||||
app_ref eq = app_ref(mk_eq_atom(n1->get_expr(), n2->get_expr()), m);
|
||||
if (!ctx.b_internalized(eq.get()) || !ctx.is_relevant(eq.get())) {
|
||||
result++;
|
||||
ctx.internalize(eq, true);
|
||||
ctx.mark_as_relevant(eq);
|
||||
ctx.mark_as_relevant(eq.get());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -850,7 +848,7 @@ namespace smt {
|
|||
if (i < num_args) {
|
||||
SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
|
||||
parent_sel_set->insert(sel);
|
||||
todo.push_back(std::make_pair(parent_root, sel));
|
||||
todo.push_back({parent_root, sel});
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -437,7 +437,7 @@ namespace smt {
|
|||
return lit == arg;
|
||||
};
|
||||
auto lit1 = clause.get(0);
|
||||
auto lit2 = clause.get(1);
|
||||
[[maybe_unused]] auto lit2 = clause.get(1);
|
||||
auto position = 0;
|
||||
if (is_complement_to(is_true, lit1, e))
|
||||
position = 0;
|
||||
|
|
|
|||
|
|
@ -4029,7 +4029,7 @@ public:
|
|||
if (!lp().is_feasible() || lp().has_changed_columns())
|
||||
make_feasible();
|
||||
vi = get_lpvar(v);
|
||||
auto st = lp().maximize_term(vi, term_max);
|
||||
auto st = lp().maximize_term(vi, term_max, /*fix_int_cols*/ true);
|
||||
if (has_int() && lp().has_inf_int()) {
|
||||
st = lp::lp_status::FEASIBLE;
|
||||
lp().restore_x();
|
||||
|
|
|
|||
|
|
@ -66,7 +66,6 @@ namespace smt {
|
|||
unsigned m_final_check_ls_steps = 30000;
|
||||
unsigned m_final_check_ls_steps_delta = 10000;
|
||||
unsigned m_final_check_ls_steps_min = 10000;
|
||||
unsigned m_final_check_ls_steps_max = 30000;
|
||||
bool m_has_unassigned_clause_after_resolve = false;
|
||||
unsigned m_after_resolve_decide_gap = 4;
|
||||
unsigned m_after_resolve_decide_count = 0;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue