mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-05-30 18:14:46 +01:00
commit 7288353575
4 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/dl_decl_plugin.cpp
View file

@ -601,6 +601,22 @@ namespace datalog {
result = mk_compare(OP_DL_LT, m_lt_sym, domain); result = mk_compare(OP_DL_LT, m_lt_sym, domain);
break; break;
case OP_DL_REP: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
break;
}
case OP_DL_ABS: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
break;
}
default: default:
m_manager->raise_exception("operator not recognized"); m_manager->raise_exception("operator not recognized");
return 0; return 0;

2
src/ast/dl_decl_plugin.h
View file

@ -48,6 +48,8 @@ namespace datalog {
OP_RA_CLONE, OP_RA_CLONE,
OP_DL_CONSTANT, OP_DL_CONSTANT,
OP_DL_LT, OP_DL_LT,
OP_DL_REP,
OP_DL_ABS,
LAST_RA_OP LAST_RA_OP
}; };

2
src/smt/smt_model_generator.cpp
View file

@ -102,6 +102,7 @@ namespace smt {
if (th && th->build_models()) { if (th && th->build_models()) {
if (r->get_th_var(th->get_id()) != null_theory_var) { if (r->get_th_var(th->get_id()) != null_theory_var) {
proc = th->mk_value(r, *this); proc = th->mk_value(r, *this);
SASSERT(proc);
} }
else { else {
TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
@ -110,6 +111,7 @@ namespace smt {
} }
else { else {
proc = mk_model_value(r); proc = mk_model_value(r);
SASSERT(proc);
} }
} }
SASSERT(proc); SASSERT(proc);

7
src/smt/theory_dl.cpp
View file

@ -162,7 +162,7 @@ namespace smt {
m.register_factory(alloc(dl_factory, m_util, m.get_model())); m.register_factory(alloc(dl_factory, m_util, m.get_model()));
} }
virtual smt::model_value_proc * mk_value(smt::enode * n) { virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
return alloc(dl_value_proc, *this, n); return alloc(dl_value_proc, *this, n);
} }
@ -201,9 +201,8 @@ namespace smt {
if(!m_reps.find(s, r) || !m_vals.find(s,v)) { if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
SASSERT(!m_reps.contains(s)); SASSERT(!m_reps.contains(s));
sort* bv = b().mk_sort(64); sort* bv = b().mk_sort(64);
// TBD: filter these from model. r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
r = m().mk_fresh_func_decl("rep",1, &s,bv); v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
v = m().mk_fresh_func_decl("val",1, &bv,s);
m_reps.insert(s, r); m_reps.insert(s, r);
m_vals.insert(s, v); m_vals.insert(s, v);
add_trail(r); add_trail(r);