mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

use theory_seq's internalize_term

Browse source
This commit is contained in:
Murphy Berzish 2016-05-07 15:40:39 -04:00
parent a2d0299621
commit 1d324877cd
2 changed files with 66 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

67
src/smt/theory_str.cpp
View file

@ -139,6 +139,7 @@ void theory_str::assert_implication(expr * premise, expr * conclusion) {
}
bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
/*
TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
SASSERT(atom->get_family_id() == get_family_id());
@ -152,15 +153,21 @@ bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
ctx.internalize(atom->get_arg(i), false);
literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id());
return true;
*/
return internalize_term(atom);
}
bool theory_str::internalize_term(app * term) {
context & ctx = get_context();
ast_manager & m = get_manager();
TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;);
SASSERT(term->get_family_id() == get_family_id());
/* // what I had before
SASSERT(!ctx.e_internalized(term));
unsigned num_args = term->get_num_args();
@ -175,15 +182,67 @@ bool theory_str::internalize_term(app * term) {
attach_new_th_var(e);
/*
if (is_concat(term)) {
instantiate_concat_axiom(e);
}
//if (is_concat(term)) {
// instantiate_concat_axiom(e);
//}
*/
// from theory_seq::internalize_term()
if (ctx.e_internalized(term)) {
enode* e = ctx.get_enode(term);
mk_var(e);
return true;
}
unsigned num_args = term->get_num_args();
expr* arg;
for (unsigned i = 0; i < num_args; i++) {
arg = term->get_arg(i);
mk_var(ensure_enode(arg));
}
if (m.is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id());
ctx.mark_as_relevant(bv);
}
enode* e = 0;
if (ctx.e_internalized(term)) {
e = ctx.get_enode(term);
}
else {
e = ctx.mk_enode(term, false, m.is_bool(term), true);
}
mk_var(e);
return true;
}
enode* theory_str::ensure_enode(expr* e) {
context& ctx = get_context();
if (!ctx.e_internalized(e)) {
ctx.internalize(e, false);
}
enode* n = ctx.get_enode(e);
ctx.mark_as_relevant(n);
return n;
}
theory_var theory_str::mk_var(enode* n) {
if (!m_strutil.is_string(n->get_owner())) {
return null_theory_var;
}
if (is_attached_to_var(n)) {
return n->get_th_var(get_id());
}
else {
theory_var v = theory::mk_var(n);
// m_find.mk_var();
get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n);
return v;
}
}
static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
std::map<expr*, int>::iterator itor = src.begin();
for (; itor != src.end(); itor++) {

4
src/smt/theory_str.h
View file

@ -208,6 +208,8 @@ namespace smt {
protected:
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual enode* ensure_enode(expr* e);
virtual theory_var mk_var(enode * n);
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
@ -224,7 +226,7 @@ namespace smt {
virtual void propagate();
virtual final_check_status final_check_eh();
void attach_new_th_var(enode * n);
virtual void attach_new_th_var(enode * n);
virtual void init_model(model_generator & m);
virtual model_value_proc * mk_value(enode * n, model_generator & mg);