mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
parent
95eb0a0521
commit
3d1c40ce23
|
@ -1814,7 +1814,6 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
SASSERT(m_ast_table.contains(n));
|
||||
}
|
||||
|
||||
|
||||
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
|
||||
|
||||
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
|
||||
|
|
|
@ -478,7 +478,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
SASSERT(num_args == 2);
|
||||
st = mk_seq_at(args[0], args[1], result);
|
||||
break;
|
||||
#if 0
|
||||
#if 1
|
||||
case OP_SEQ_NTH:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_nth(args[0], args[1], result);
|
||||
|
@ -1805,6 +1805,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
|
|||
bool changed = false;
|
||||
if (!reduce_eq(l, r, lhs, rhs, changed)) {
|
||||
result = m().mk_false();
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (!changed) {
|
||||
|
@ -1814,6 +1815,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
|
|||
res.push_back(m().mk_eq(lhs.get(i), rhs.get(i)));
|
||||
}
|
||||
result = mk_and(res);
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
|
|
|
@ -291,7 +291,7 @@ namespace smt {
|
|||
ptr_vector<model_value_proc> procs;
|
||||
svector<source> sources;
|
||||
buffer<model_value_dependency> dependencies;
|
||||
ptr_vector<expr> dependency_values;
|
||||
expr_ref_vector dependency_values(m_manager);
|
||||
mk_value_procs(root2proc, roots, procs);
|
||||
top_sort_sources(roots, root2proc, sources);
|
||||
TRACE("sorted_sources",
|
||||
|
@ -307,6 +307,9 @@ namespace smt {
|
|||
tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
|
||||
}
|
||||
});
|
||||
|
||||
scoped_reset _scoped_reset(*this, procs);
|
||||
|
||||
for (source const& curr : sources) {
|
||||
if (curr.is_fresh_value()) {
|
||||
sort * s = curr.get_value()->get_sort();
|
||||
|
@ -336,10 +339,7 @@ namespace smt {
|
|||
enode * child = d.get_enode();
|
||||
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
|
||||
child = child->get_root();
|
||||
app * val = nullptr;
|
||||
m_root2value.find(child, val);
|
||||
SASSERT(val);
|
||||
dependency_values.push_back(val);
|
||||
dependency_values.push_back(m_root2value[child]);
|
||||
}
|
||||
}
|
||||
app * val = proc->mk_value(*this, dependency_values);
|
||||
|
@ -347,11 +347,7 @@ namespace smt {
|
|||
m_asts.push_back(val);
|
||||
m_root2value.insert(n, val);
|
||||
}
|
||||
}
|
||||
std::for_each(procs.begin(), procs.end(), delete_proc<model_value_proc>());
|
||||
std::for_each(m_extra_fresh_values.begin(), m_extra_fresh_values.end(), delete_proc<extra_fresh_value>());
|
||||
m_extra_fresh_values.reset();
|
||||
|
||||
}
|
||||
// send model
|
||||
for (enode * n : m_context->enodes()) {
|
||||
if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
|
||||
|
@ -364,11 +360,17 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
model_generator::scoped_reset::scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs):
|
||||
mg(mg), procs(procs) {}
|
||||
|
||||
model_generator::scoped_reset::~scoped_reset() {
|
||||
std::for_each(procs.begin(), procs.end(), delete_proc<model_value_proc>());
|
||||
std::for_each(mg.m_extra_fresh_values.begin(), mg.m_extra_fresh_values.end(), delete_proc<extra_fresh_value>());
|
||||
mg.m_extra_fresh_values.reset();
|
||||
}
|
||||
|
||||
app * model_generator::get_value(enode * n) const {
|
||||
app * val = nullptr;
|
||||
m_root2value.find(n->get_root(), val);
|
||||
SASSERT(val);
|
||||
return val;
|
||||
return m_root2value[n->get_root()];
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -490,7 +492,7 @@ namespace smt {
|
|||
finalize_theory_models();
|
||||
register_macros();
|
||||
TRACE("model", model_v2_pp(tout, *m_model, true););
|
||||
return m_model;
|
||||
return m_model.get();
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -32,6 +32,7 @@ Revision History:
|
|||
#include "smt/smt_types.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
#include "util/map.h"
|
||||
#include "util/ref.h"
|
||||
|
||||
class value_factory;
|
||||
class proto_model;
|
||||
|
@ -146,7 +147,7 @@ namespace smt {
|
|||
\brief The array values has size equal to the size of the argument \c result in get_dependencies.
|
||||
It contain the values built for the dependencies.
|
||||
*/
|
||||
virtual app * mk_value(model_generator & m, ptr_vector<expr> & values) = 0;
|
||||
virtual app * mk_value(model_generator & m, expr_ref_vector const & values) = 0;
|
||||
/**
|
||||
\brief Return true if it is associated with a fresh value.
|
||||
*/
|
||||
|
@ -161,7 +162,7 @@ namespace smt {
|
|||
app * m_value;
|
||||
public:
|
||||
expr_wrapper_proc(app * v):m_value(v) {}
|
||||
app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return m_value; }
|
||||
app * mk_value(model_generator & m, expr_ref_vector const & values) override { return m_value; }
|
||||
};
|
||||
|
||||
class fresh_value_proc : public model_value_proc {
|
||||
|
@ -169,7 +170,7 @@ namespace smt {
|
|||
public:
|
||||
fresh_value_proc(extra_fresh_value * v):m_value(v) {}
|
||||
void get_dependencies(buffer<model_value_dependency> & result) override;
|
||||
app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
|
||||
app * mk_value(model_generator & m, expr_ref_vector const & values) override { return to_app(values[0]); }
|
||||
bool is_fresh() const override { return true; }
|
||||
};
|
||||
|
||||
|
@ -183,7 +184,7 @@ namespace smt {
|
|||
unsigned m_fresh_idx;
|
||||
obj_map<enode, app *> m_root2value;
|
||||
ast_ref_vector m_asts;
|
||||
proto_model * m_model;
|
||||
ref<proto_model> m_model;
|
||||
obj_hashtable<func_decl> m_hidden_ufs;
|
||||
|
||||
void init_model();
|
||||
|
@ -205,6 +206,13 @@ namespace smt {
|
|||
|
||||
void top_sort_sources(ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc, svector<source> & sorted_sources);
|
||||
|
||||
struct scoped_reset {
|
||||
model_generator& mg;
|
||||
ptr_vector<model_value_proc>& procs;
|
||||
scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs);
|
||||
~scoped_reset();
|
||||
};
|
||||
|
||||
public:
|
||||
model_generator(ast_manager & m);
|
||||
~model_generator();
|
||||
|
@ -219,7 +227,7 @@ namespace smt {
|
|||
proto_model & get_model() { SASSERT(m_model); return *m_model; }
|
||||
void register_value(expr * val);
|
||||
ast_manager & get_manager() { return m_manager; }
|
||||
proto_model * mk_model();
|
||||
proto_model* mk_model();
|
||||
|
||||
obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
|
||||
app * get_value(enode * n) const;
|
||||
|
|
|
@ -910,7 +910,7 @@ namespace smt {
|
|||
result.append(m_dependencies.size(), m_dependencies.c_ptr());
|
||||
}
|
||||
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
|
||||
// values must have size = m_num_entries * (m_dim + 1) + ((m_else || m_unspecified_else) ? 0 : 1)
|
||||
// an array value is a lookup table + else_value
|
||||
// each entry has m_dim indexes that map to a value.
|
||||
|
|
|
@ -691,7 +691,7 @@ namespace smt {
|
|||
void get_dependencies(buffer<model_value_dependency> & result) override {
|
||||
result.append(m_dependencies.size(), m_dependencies.c_ptr());
|
||||
}
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
|
||||
SASSERT(values.size() == m_dependencies.size());
|
||||
return mg.get_manager().mk_app(m_constructor, values.size(), values.c_ptr());
|
||||
}
|
||||
|
|
|
@ -76,7 +76,7 @@ namespace smt {
|
|||
|
||||
void get_dependencies(buffer<smt::model_value_dependency> & result) override {}
|
||||
|
||||
app * mk_value(smt::model_generator & mg, ptr_vector<expr> & ) override {
|
||||
app * mk_value(smt::model_generator & mg, expr_ref_vector const & ) override {
|
||||
smt::context& ctx = m_th.get_context();
|
||||
app* result = nullptr;
|
||||
expr* n = m_node->get_owner();
|
||||
|
|
|
@ -125,7 +125,7 @@ namespace smt {
|
|||
m_is_initialized = true;
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) {
|
||||
TRACE("t_fpa_detail",
|
||||
ast_manager & m = m_th.get_manager();
|
||||
for (unsigned i = 0; i < values.size(); i++)
|
||||
|
@ -200,7 +200,7 @@ namespace smt {
|
|||
return result;
|
||||
}
|
||||
|
||||
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
|
||||
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) {
|
||||
SASSERT(values.size() == 1);
|
||||
|
||||
TRACE("t_fpa_detail",
|
||||
|
|
|
@ -120,7 +120,7 @@ namespace smt {
|
|||
result.append(m_deps);
|
||||
}
|
||||
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override;
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
|
||||
};
|
||||
|
||||
class fpa_rm_value_proc : public model_value_proc {
|
||||
|
@ -141,7 +141,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
~fpa_rm_value_proc() override {}
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override;
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
|
||||
};
|
||||
|
||||
protected:
|
||||
|
|
|
@ -2326,7 +2326,7 @@ namespace smt {
|
|||
result.append(m_dependencies.size(), m_dependencies.c_ptr());
|
||||
}
|
||||
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const& values) override {
|
||||
ast_manager& m = mg.get_manager();
|
||||
SASSERT(values.size() == m_dependencies.size());
|
||||
SASSERT(values.size() == m_app->get_num_args());
|
||||
|
|
|
@ -2113,12 +2113,14 @@ bool theory_seq::check_extensionality() {
|
|||
m_lhs.reset(); m_rhs.reset();
|
||||
bool change = false;
|
||||
if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
|
||||
TRACE("seq", tout << "exclude " << mk_pp(o1, m) << " " << mk_pp(o2, m) << "\n";);
|
||||
m_exclude.update(o1, o2);
|
||||
continue;
|
||||
}
|
||||
bool excluded = false;
|
||||
for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
|
||||
if (m_exclude.contains(m_lhs[j].get(), m_rhs[j].get())) {
|
||||
if (m_exclude.contains(m_lhs.get(j), m_rhs.get(j))) {
|
||||
TRACE("seq", tout << "excluded " << j << " " << m_lhs << " " << m_rhs << "\n";);
|
||||
excluded = true;
|
||||
}
|
||||
}
|
||||
|
@ -2517,6 +2519,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
|
|||
b = m_todo.back();
|
||||
if (a == b || m.is_ite(b)) {
|
||||
m_todo.reset();
|
||||
std::cout << " yes\n";
|
||||
return true;
|
||||
}
|
||||
m_todo.pop_back();
|
||||
|
@ -2524,8 +2527,14 @@ bool theory_seq::occurs(expr* a, expr* b) {
|
|||
m_todo.push_back(e1);
|
||||
m_todo.push_back(e2);
|
||||
}
|
||||
else if (m_util.str.is_unit(b, e1)) {
|
||||
m_todo.push_back(e1);
|
||||
}
|
||||
else if (m_util.str.is_nth(b, e1, e2)) {
|
||||
m_todo.push_back(e1);
|
||||
}
|
||||
}
|
||||
return false;
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
@ -2536,7 +2545,7 @@ bool theory_seq::is_var(expr* a) const {
|
|||
!m_util.str.is_empty(a) &&
|
||||
!m_util.str.is_string(a) &&
|
||||
!m_util.str.is_unit(a) &&
|
||||
!m_util.str.is_itos(a) &&
|
||||
!m_util.str.is_itos(a) &&
|
||||
// !m_util.str.is_extract(a) &&
|
||||
!m.is_ite(a);
|
||||
}
|
||||
|
@ -3981,7 +3990,7 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
|
||||
app * mk_value(model_generator & mg, expr_ref_vector const & values) override {
|
||||
SASSERT(values.size() == m_dependencies.size());
|
||||
expr_ref_vector args(th.m);
|
||||
unsigned j = 0, k = 0;
|
||||
|
@ -5182,8 +5191,8 @@ void theory_seq::add_at_axiom(expr* e) {
|
|||
}
|
||||
else {
|
||||
expr_ref len_e = mk_len(e);
|
||||
expr_ref x = mk_skolem(m_pre, s, i);
|
||||
expr_ref y = mk_skolem(m_tail, s, i);
|
||||
expr_ref x = mk_skolem(m_pre, s, i);
|
||||
expr_ref y = mk_skolem(m_tail, s, i);
|
||||
expr_ref xey = mk_concat(x, e, y);
|
||||
expr_ref len_x = mk_len(x);
|
||||
add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
|
||||
|
@ -5208,7 +5217,10 @@ void theory_seq::add_nth_axiom(expr* e) {
|
|||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
|
||||
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
|
||||
// at(s,i) = [nth(s,i)]
|
||||
expr_ref rhs(s, m);
|
||||
if (!m_util.str.is_at(s)) rhs = m_util.str.mk_at(s, i);
|
||||
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), rhs, false));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -399,7 +399,7 @@ namespace smt {
|
|||
void add_theory_assumptions(expr_ref_vector & assumptions) override;
|
||||
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
|
||||
char const * get_name() const override { return "seq"; }
|
||||
bool include_func_interp(func_decl* f) override { return m_util.str.is_nth(f); }
|
||||
bool include_func_interp(func_decl* f) override { return false; } // m_util.str.is_nth(f); }
|
||||
theory_var mk_var(enode* n) override;
|
||||
void apply_sort_cnstr(enode* n, sort* s) override;
|
||||
void display(std::ostream & out) const override;
|
||||
|
|
Loading…
Reference in a new issue