mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-27 08:51:22 -07:00
commit 06c9a9f3e1
148 changed files with 3478 additions and 2141 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/base/bind_variables.cpp
View file

@ -38,7 +38,7 @@ expr_ref bind_variables::operator()(expr* fml, bool is_forall) {
if (!m_names.empty()) {
m_bound.reverse();
m_names.reverse();
result = m.mk_quantifier(is_forall, m_bound.size(), m_bound.c_ptr(), m_names.c_ptr(), result);
result = m.mk_quantifier(is_forall ? forall_k : exists_k, m_bound.size(), m_bound.c_ptr(), m_names.c_ptr(), result);
}
m_pinned.reset();
m_cache.reset();

9
src/muz/base/dl_context.cpp
View file

@ -1044,7 +1044,7 @@ namespace datalog {
quantifier* q = to_quantifier(body);
expr* e = q->get_expr();
if (m.is_implies(e, body, e2)) {
fml = m.mk_quantifier(false, q->get_num_decls(),
fml = m.mk_quantifier(exists_k, q->get_num_decls(),
q->get_decl_sorts(), q->get_decl_names(),
body);
}
@ -1251,13 +1251,10 @@ namespace datalog {
obj_map<sort, unsigned> max_vars;
for (unsigned i = 0; i < rules.size(); ++i) {
expr* r = rules[i].get();
if (!is_quantifier(r)) {
if (!is_forall(r)) {
continue;
}
quantifier* q = to_quantifier(r);
if (!q->is_forall()) {
continue;
}
if (has_quantifiers(q->get_expr())) {
continue;
}
@ -1292,7 +1289,7 @@ namespace datalog {
subst.push_back(fresh_vars[vars[max_var]].get());
}
vsubst(q->get_expr(), subst.size(), subst.c_ptr(), res);
res = vsubst(q->get_expr(), subst.size(), subst.c_ptr());
rules[i] = res.get();
}
}

20
src/muz/base/dl_rule.cpp
View file

@ -292,7 +292,7 @@ namespace datalog {
args.push_back(m.mk_var(0, m.mk_bool_sort()));
}
}
sub(q, args.size(), args.c_ptr(), q);
q = sub(q, args.size(), args.c_ptr());
vars.reset();
m_free_vars(q);
vars.append(m_free_vars.size(), m_free_vars.c_ptr());
@ -438,11 +438,7 @@ namespace datalog {
e = e2;
}
}
if (is_quantifier(e)) {
q = to_quantifier(e);
return q->is_forall();
}
return false;
return ::is_forall(e);
}
@ -745,7 +741,7 @@ namespace datalog {
expr_ref unbound_tail_pre_quant(m), fixed_tail(m), quant_tail(m);
var_subst vs(m, false);
vs(unbound_tail, subst.size(), subst.c_ptr(), unbound_tail_pre_quant);
unbound_tail_pre_quant = vs(unbound_tail, subst.size(), subst.c_ptr());
quant_tail = m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(), unbound_tail_pre_quant);
@ -816,10 +812,10 @@ namespace datalog {
app_ref_vector new_tail(m);
svector<bool> tail_neg;
var_subst vs(m, false);
vs(r->get_head(), sz, es, tmp);
tmp = vs(r->get_head(), sz, es);
new_head = to_app(tmp);
for (unsigned i = 0; i < r->get_tail_size(); ++i) {
vs(r->get_tail(i), sz, es, tmp);
tmp = vs(r->get_tail(i), sz, es);
new_tail.push_back(to_app(tmp));
tail_neg.push_back(r->is_neg_tail(i));
}
@ -984,8 +980,7 @@ namespace datalog {
var_subst vs(m, false);
expr_ref new_head_e(m);
vs(m_head, subst_vals.size(), subst_vals.c_ptr(), new_head_e);
expr_ref new_head_e = vs(m_head, subst_vals.size(), subst_vals.c_ptr());
m.inc_ref(new_head_e);
m.dec_ref(m_head);
@ -993,8 +988,7 @@ namespace datalog {
for (unsigned i = 0; i < m_tail_size; i++) {
app * old_tail = get_tail(i);
expr_ref new_tail_e(m);
vs(old_tail, subst_vals.size(), subst_vals.c_ptr(), new_tail_e);
expr_ref new_tail_e = vs(old_tail, subst_vals.size(), subst_vals.c_ptr());
bool sign = is_neg_tail(i);
m.inc_ref(new_tail_e);
m.dec_ref(old_tail);

10
src/muz/base/dl_rule.h
View file

@ -82,12 +82,10 @@ namespace datalog {
quantifier_finder_proc() : m_exist(false), m_univ(false) {}
void operator()(var * n) { }
void operator()(quantifier * n) {
if (n->is_forall()) {
m_univ = true;
}
else {
SASSERT(n->is_exists());
m_exist = true;
switch (n->get_kind()) {
case forall_k: m_univ = true; break;
case exists_k: m_exist = true; break;
case lambda_k: UNREACHABLE();
}
}
void operator()(app * n) { }

179
src/muz/base/dl_rule_set.cpp
View file

@ -31,27 +31,20 @@ namespace datalog {
rule_dependencies::rule_dependencies(const rule_dependencies & o, bool reversed):
m_context(o.m_context) {
if (reversed) {
iterator oit = o.begin();
iterator oend = o.end();
for (; oit!=oend; ++oit) {
func_decl * pred = oit->m_key;
item_set & orig_items = *oit->get_value();
for (auto & kv : o) {
func_decl * pred = kv.m_key;
item_set & orig_items = *kv.get_value();
ensure_key(pred);
item_set::iterator dit = orig_items.begin();
item_set::iterator dend = orig_items.end();
for (; dit!=dend; ++dit) {
func_decl * master_pred = *dit;
for (func_decl * master_pred : orig_items) {
insert(master_pred, pred);
}
}
}
else {
iterator oit = o.begin();
iterator oend = o.end();
for (; oit!=oend; ++oit) {
func_decl * pred = oit->m_key;
item_set & orig_items = *oit->get_value();
for (auto & kv : o) {
func_decl * pred = kv.m_key;
item_set & orig_items = *kv.get_value();
m_data.insert(pred, alloc(item_set, orig_items));
}
}
@ -86,14 +79,10 @@ namespace datalog {
void rule_dependencies::populate(const rule_set & rules) {
SASSERT(m_data.empty());
rule_set::decl2rules::iterator it = rules.m_head2rules.begin();
rule_set::decl2rules::iterator end = rules.m_head2rules.end();
for (; it != end; ++it) {
ptr_vector<rule> * rules = it->m_value;
ptr_vector<rule>::iterator it2 = rules->begin();
ptr_vector<rule>::iterator end2 = rules->end();
for (; it2 != end2; ++it2) {
populate(*it2);
for (auto & kv : rules.m_head2rules) {
ptr_vector<rule> * rules = kv.m_value;
for (rule* r : *rules) {
populate(r);
}
}
}
@ -150,54 +139,41 @@ namespace datalog {
void rule_dependencies::restrict(const item_set & allowed) {
ptr_vector<func_decl> to_remove;
iterator pit = begin();
iterator pend = end();
for (; pit!=pend; ++pit) {
func_decl * pred = pit->m_key;
for (auto const& kv : *this) {
func_decl * pred = kv.m_key;
if (!allowed.contains(pred)) {
to_remove.insert(pred);
continue;
}
item_set& itms = *pit->get_value();
item_set& itms = *kv.get_value();
set_intersection(itms, allowed);
}
ptr_vector<func_decl>::iterator rit = to_remove.begin();
ptr_vector<func_decl>::iterator rend = to_remove.end();
for (; rit != rend; ++rit) {
remove_m_data_entry(*rit);
}
for (func_decl* f : to_remove)
remove_m_data_entry(f);
}
void rule_dependencies::remove(func_decl * itm) {
remove_m_data_entry(itm);
iterator pit = begin();
iterator pend = end();
for (; pit != pend; ++pit) {
item_set & itms = *pit->get_value();
for (auto const& kv : *this) {
item_set & itms = *kv.get_value();
itms.remove(itm);
}
}
void rule_dependencies::remove(const item_set & to_remove) {
item_set::iterator rit = to_remove.begin();
item_set::iterator rend = to_remove.end();
for (; rit!=rend; ++rit) {
remove_m_data_entry(*rit);
for (auto * item : to_remove) {
remove_m_data_entry(item);
}
iterator pit = begin();
iterator pend = end();
for (; pit!=pend; ++pit) {
item_set * itms = pit->get_value();
for (auto & kv : *this) {
item_set * itms = kv.get_value();
set_difference(*itms, to_remove);
}
}
unsigned rule_dependencies::out_degree(func_decl * f) const {
unsigned res = 0;
iterator pit = begin();
iterator pend = end();
for (; pit!=pend; ++pit) {
item_set & itms = *pit->get_value();
for (auto & kv : *this) {
item_set & itms = *kv.get_value();
if (itms.contains(f)) {
res++;
}
@ -333,19 +309,11 @@ namespace datalog {
void rule_set::inherit_predicates(rule_set const& other) {
m_refs.append(other.m_refs);
set_union(m_output_preds, other.m_output_preds);
{
obj_map<func_decl, func_decl*>::iterator it = other.m_orig2pred.begin();
obj_map<func_decl, func_decl*>::iterator end = other.m_orig2pred.end();
for (; it != end; ++it) {
m_orig2pred.insert(it->m_key, it->m_value);
}
for (auto & kv : other.m_orig2pred) {
m_orig2pred.insert(kv.m_key, kv.m_value);
}
{
obj_map<func_decl, func_decl*>::iterator it = other.m_pred2orig.begin();
obj_map<func_decl, func_decl*>::iterator end = other.m_pred2orig.end();
for (; it != end; ++it) {
m_pred2orig.insert(it->m_key, it->m_value);
}
for (auto & kv : other.m_pred2orig) {
m_pred2orig.insert(kv.m_key, kv.m_value);
}
}
@ -537,26 +505,19 @@ namespace datalog {
void rule_set::display_deps( std::ostream & out ) const
{
const pred_set_vector & strats = get_strats();
pred_set_vector::const_iterator sit = strats.begin();
pred_set_vector::const_iterator send = strats.end();
for (; sit!=send; ++sit) {
func_decl_set & strat = **sit;
func_decl_set::iterator fit=strat.begin();
func_decl_set::iterator fend=strat.end();
bool non_empty = false;
for (; fit!=fend; ++fit) {
func_decl * first = *fit;
const func_decl_set & deps = m_deps.get_deps(first);
func_decl_set::iterator dit=deps.begin();
func_decl_set::iterator dend=deps.end();
for (; dit!=dend; ++dit) {
non_empty = true;
func_decl * dep = *dit;
out<<first->get_name()<<" -> "<<dep->get_name()<<"\n";
}
}
if (non_empty && sit!=send) {
bool non_empty = false;
for (func_decl_set* strat : strats) {
if (non_empty) {
out << "\n";
non_empty = false;
}
for (func_decl * first : *strat) {
const func_decl_set & deps = m_deps.get_deps(first);
for (func_decl * dep : deps) {
non_empty = true;
out<<first->get_name()<<" -> " <<dep->get_name()<<"\n";
}
}
}
}
@ -568,11 +529,8 @@ namespace datalog {
// -----------------------------------
rule_stratifier::~rule_stratifier() {
comp_vector::iterator it = m_strats.begin();
comp_vector::iterator end = m_strats.end();
for (; it!=end; ++it) {
SASSERT(*it);
dealloc(*it);
for (auto * t : m_strats) {
dealloc(t);
}
}
@ -617,10 +575,8 @@ namespace datalog {
m_stack_P.push_back(el);
const item_set & children = m_deps.get_deps(el);
item_set::iterator cit=children.begin();
item_set::iterator cend=children.end();
for (; cit!=cend; ++cit) {
traverse(*cit);
for (T* ch : children) {
traverse(ch);
}
if (el == m_stack_P.back()) {
@ -646,10 +602,8 @@ namespace datalog {
}
//detect strong components
rule_dependencies::iterator it = m_deps.begin();
rule_dependencies::iterator end = m_deps.end();
for (; it!=end; ++it) {
T * el = it->m_key;
for (auto const& kv : m_deps) {
T * el = kv.m_key;
//we take a note of the preorder number with which this sweep started
m_first_preorder = m_next_preorder;
traverse(el);
@ -662,19 +616,13 @@ namespace datalog {
in_degrees.resize(m_components.size());
//init in_degrees
it = m_deps.begin();
end = m_deps.end();
for (; it != end; ++it) {
T * el = it->m_key;
item_set * out_edges = it->m_value;
for (auto const& kv : m_deps) {
T * el = kv.m_key;
item_set * out_edges = kv.m_value;
unsigned el_comp = 0;
VERIFY( m_component_nums.find(el, el_comp) );
unsigned el_comp = m_component_nums[el];
item_set::iterator eit = out_edges->begin();
item_set::iterator eend = out_edges->end();
for (; eit!=eend; ++eit) {
T * tgt = *eit;
for (T * tgt : *out_edges) {
unsigned tgt_comp = m_component_nums.find(tgt);
@ -701,15 +649,9 @@ namespace datalog {
unsigned strats_index = 0;
while (strats_index < m_strats.size()) { //m_strats.size() changes inside the loop!
item_set * comp = m_strats[strats_index];
item_set::iterator cit=comp->begin();
item_set::iterator cend=comp->end();
for (; cit!=cend; ++cit) {
T * el = *cit;
for (T * el : *comp) {
const item_set & deps = m_deps.get_deps(el);
item_set::iterator eit=deps.begin();
item_set::iterator eend=deps.end();
for (; eit!=eend; ++eit) {
T * tgt = *eit;
for (T * tgt : deps) {
unsigned tgt_comp = 0;
VERIFY( m_component_nums.find(tgt, tgt_comp) );
@ -724,7 +666,7 @@ namespace datalog {
m_components[tgt_comp] = 0;
}
}
traverse(*cit);
traverse(el);
}
}
strats_index++;
@ -738,12 +680,9 @@ namespace datalog {
SASSERT(m_pred_strat_nums.empty());
unsigned strat_cnt = m_strats.size();
for (unsigned strat_index=0; strat_index<strat_cnt; strat_index++) {
for (unsigned strat_index=0; strat_index < strat_cnt; strat_index++) {
item_set * comp = m_strats[strat_index];
item_set::iterator cit=comp->begin();
item_set::iterator cend=comp->end();
for (; cit != cend; ++cit) {
T * el = *cit;
for (T * el : *comp) {
m_pred_strat_nums.insert(el, strat_index);
}
}
@ -761,10 +700,8 @@ namespace datalog {
m_deps.display(out << "dependencies\n");
out << "strata\n";
for (unsigned i = 0; i < m_strats.size(); ++i) {
item_set::iterator it = m_strats[i]->begin();
item_set::iterator end = m_strats[i]->end();
for (; it != end; ++it) {
out << (*it)->get_name() << " ";
for (auto * item : *m_strats[i]) {
out << item->get_name() << " ";
}
out << "\n";
}

3
src/muz/base/dl_util.cpp
View file

@ -115,8 +115,7 @@ namespace datalog {
expr_ref tmp(m);
for (unsigned i = 0; i < tgt.size(); ++i) {
if (tgt[i].get()) {
vs(tgt[i].get(), sub.size(), sub.c_ptr(), tmp);
tgt[i] = tmp;
tgt[i] = vs(tgt[i].get(), sub.size(), sub.c_ptr());
}
else {
tgt[i] = sub[i];

32
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -108,20 +108,20 @@ namespace datalog {
// apply substitution to body.
var_subst vs(m, false);
for (unsigned k = 0; k < p->get_arity(); ++k) {
vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), trm);
trm = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr());
conjs.push_back(m.mk_eq(trm, mk_q_arg(p, k, true)));
}
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
func_decl* q = r.get_decl(j);
for (unsigned k = 0; k < q->get_arity(); ++k) {
vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), trm);
trm = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr());
conjs.push_back(m.mk_eq(trm, mk_q_arg(q, k, false)));
}
func_decl_ref qr = mk_q_func_decl(q);
conjs.push_back(m.mk_app(qr, m_bv.mk_bv_sub(var, mk_q_one())));
}
for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
vs(r.get_tail(j), sub.size(), sub.c_ptr(), trm);
trm = vs(r.get_tail(j), sub.size(), sub.c_ptr());
conjs.push_back(trm);
}
if (r.get_uninterpreted_tail_size() > 0) {
@ -238,7 +238,7 @@ namespace datalog {
var_subst vs(m, false);
num = mk_q_num(i);
expr* nums[1] = { num };
vs(t, 1, nums, tmp);
tmp = vs(t, 1, nums);
return (*model)(tmp);
}
@ -535,7 +535,7 @@ namespace datalog {
for (unsigned j = 0; j < sz; ++j) {
func_decl* head_j = r->get_decl(j);
app* body_j = r->get_tail(j);
vs(body_j, sub.size(), sub.c_ptr(), prop_body);
prop_body = vs(body_j, sub.size(), sub.c_ptr());
prs.push_back(get_proof(md, head_j, to_app(prop_body), level-1));
positions.push_back(std::make_pair(j+1,0));
substs.push_back(expr_ref_vector(m));
@ -609,11 +609,9 @@ namespace datalog {
}
expr_ref skolemize_vars(rule& r, expr_ref_vector const& args, ptr_vector<sort> const& vars, expr* e) {
expr_ref result(m);
expr_ref_vector binding = mk_skolem_binding(r, vars, args);
var_subst vs(m, false);
vs(e, binding.size(), binding.c_ptr(), result);
return result;
return vs(e, binding.size(), binding.c_ptr());
}
func_decl_ref mk_body_func(rule& r, ptr_vector<sort> const& args, unsigned index, sort* s) {
@ -646,8 +644,8 @@ namespace datalog {
return expr_ref(e, m);
}
var_subst vs(m, false);
vs(e, binding.size(), binding.c_ptr(), tmp);
vs(pat, binding.size(), binding.c_ptr(), head);
tmp = vs(e, binding.size(), binding.c_ptr());
head = vs(pat, binding.size(), binding.c_ptr());
patterns.push_back(m.mk_pattern(to_app(head)));
symbol qid, skid;
return expr_ref(m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qid, skid, 1, patterns.c_ptr()), m);
@ -892,7 +890,7 @@ namespace datalog {
// apply substitution to body.
var_subst vs(m, false);
for (unsigned k = 0; k < p->get_arity(); ++k) {
vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr());
expr_ref arg = mk_arg(p, k, path_var, trace_arg);
conjs.push_back(m.mk_eq(tmp, arg));
}
@ -906,7 +904,7 @@ namespace datalog {
}
func_decl* q = r.get_decl(j);
for (unsigned k = 0; k < q->get_arity(); ++k) {
vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr());
expr_ref arg = mk_arg(q, k, path_arg, vars[j].get());
conjs.push_back(m.mk_eq(tmp, arg));
}
@ -914,7 +912,7 @@ namespace datalog {
conjs.push_back(m.mk_app(q_pred, vars[j].get(), path_arg));
}
for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_tail(j), sub.size(), sub.c_ptr());
conjs.push_back(tmp);
}
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
@ -1048,7 +1046,7 @@ namespace datalog {
expr_ref fml(m), head(m), tmp(m);
app_ref path1(m);
var_subst vs(m, false);
// var_subst vs(m, false);
mk_subst(*rules[i], path, trace, sub);
rm.to_formula(*rules[i], fml);
prs.push_back(rules[i]->get_proof());
@ -1399,20 +1397,20 @@ namespace datalog {
// apply substitution to body.
var_subst vs(m, false);
for (unsigned k = 0; k < p->get_arity(); ++k) {
vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr());
conjs.push_back(m.mk_eq(tmp, mk_level_arg(p, k, level)));
}
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
SASSERT(level > 0);
func_decl* q = r.get_decl(j);
for (unsigned k = 0; k < q->get_arity(); ++k) {
vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr());
conjs.push_back(m.mk_eq(tmp, mk_level_arg(q, k, level-1)));
}
conjs.push_back(mk_level_predicate(q, level-1));
}
for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
vs(r.get_tail(j), sub.size(), sub.c_ptr(), tmp);
tmp = vs(r.get_tail(j), sub.size(), sub.c_ptr());
conjs.push_back(tmp);
}
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);

2
src/muz/clp/clp_context.cpp
View file

@ -121,7 +121,7 @@ namespace datalog {
m_ground[i] = m.mk_fresh_const("c", fv[i]);
}
}
m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
e = m_var_subst(e, m_ground.size(), m_ground.c_ptr());
}
static bool rule_sort_fn(const rule *r1, const rule *r2) {

32
src/muz/rel/check_relation.cpp
View file

@ -59,9 +59,7 @@ namespace datalog {
for (unsigned i = 0; i < sig.size(); ++i) {
vars.push_back(m.mk_const(symbol(i), sig[i]));
}
expr_ref result(m);
sub(fml, vars.size(), vars.c_ptr(), result);
return result;
return sub(fml, vars.size(), vars.c_ptr());
}
void check_relation::add_fact(const relation_fact & f) {
@ -292,7 +290,7 @@ namespace datalog {
}
}
var_subst sub(m, false);
sub(fml, vars.size(), vars.c_ptr(), fml1);
fml1 = sub(fml, vars.size(), vars.c_ptr());
bound.reverse();
fml1 = m.mk_exists(bound.size(), bound.c_ptr(), names.c_ptr(), fml1);
return fml1;
@ -333,7 +331,7 @@ namespace datalog {
for (unsigned i = 0; i < sig2.size(); ++i) {
vars.push_back(m.mk_var(i + sig1.size(), sig2[i]));
}
sub(fml2, vars.size(), vars.c_ptr(), fml2);
fml2 = sub(fml2, vars.size(), vars.c_ptr());
fml1 = m.mk_and(fml1, fml2);
for (unsigned i = 0; i < cols1.size(); ++i) {
unsigned v1 = cols1[i];
@ -372,14 +370,14 @@ namespace datalog {
expr_ref fml1(m), fml2(m);
src.to_formula(fml1);
dst.to_formula(fml2);
subst(fml1, sub.size(), sub.c_ptr(), fml1);
fml1 = subst(fml1, sub.size(), sub.c_ptr());
expr_ref_vector vars(m);
for (unsigned i = 0; i < sig2.size(); ++i) {
vars.push_back(m.mk_const(symbol(i), sig2[i]));
}
subst(fml1, vars.size(), vars.c_ptr(), fml1);
subst(fml2, vars.size(), vars.c_ptr(), fml2);
fml1 = subst(fml1, vars.size(), vars.c_ptr());
fml2 = subst(fml2, vars.size(), vars.c_ptr());
check_equiv("permutation", fml1, fml2);
}
@ -405,8 +403,8 @@ namespace datalog {
strm << "x" << i;
vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));
}
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml2, vars.size(), vars.c_ptr(), fml2);
fml1 = sub(fml1, vars.size(), vars.c_ptr());
fml2 = sub(fml2, vars.size(), vars.c_ptr());
check_equiv("filter", fml1, fml2);
}
@ -453,8 +451,8 @@ namespace datalog {
strm << "x" << i;
vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));
}
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml2, vars.size(), vars.c_ptr(), fml2);
fml1 = sub(fml1, vars.size(), vars.c_ptr());
fml2 = sub(fml2, vars.size(), vars.c_ptr());
check_equiv("union", fml1, fml2);
@ -466,13 +464,13 @@ namespace datalog {
// dst \ dst0 == delta & dst & \ dst0
expr_ref fml4(m), fml5(m);
fml4 = m.mk_and(fml2, m.mk_not(dst0));
sub(fml4, vars.size(), vars.c_ptr(), fml4);
sub(d, vars.size(), vars.c_ptr(), d);
fml4 = sub(fml4, vars.size(), vars.c_ptr());
d = sub(d, vars.size(), vars.c_ptr());
check_contains("union_delta low", d, fml4);
//
// delta >= delta0
//
sub(delta0, vars.size(), vars.c_ptr(), d0);
d0 = sub(delta0, vars.size(), vars.c_ptr());
check_contains("union delta0", d, d0);
//
@ -480,8 +478,8 @@ namespace datalog {
//
fml4 = m.mk_or(fml2, delta0);
fml5 = m.mk_or(d, dst0);
sub(fml4, vars.size(), vars.c_ptr(), fml4);
sub(fml5, vars.size(), vars.c_ptr(), fml5);
fml4 = sub(fml4, vars.size(), vars.c_ptr());
fml5 = sub(fml5, vars.size(), vars.c_ptr());
check_equiv("union no overflow", fml4, fml5);
}
}

3
src/muz/rel/dl_compiler.cpp
View file

@ -725,8 +725,7 @@ namespace datalog {
}
}
expr_ref renamed(m);
m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr(), renamed);
expr_ref renamed = m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr());
app_ref app_renamed(to_app(renamed), m);
if (remove_columns.empty()) {
if (!dealloc)

12
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -1311,8 +1311,7 @@ namespace datalog {
if(m_rel_cond_columns.empty()) {
expr_ref_vector renaming(m_manager);
get_renaming_args(r.m_sig2table, r.get_signature(), renaming);
expr_ref table_cond(m_manager);
m_subst(condition, renaming.size(), renaming.c_ptr(), table_cond);
expr_ref table_cond = m_subst(condition, renaming.size(), renaming.c_ptr());
m_table_filter = rmgr.mk_filter_interpreted_fn(r.get_table(), to_app(table_cond));
}
else {
@ -1361,9 +1360,7 @@ namespace datalog {
continue;
}
if(!m_rel_filter) {
expr_ref inner_cond(m_manager);
m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.c_ptr(),
inner_cond);
expr_ref inner_cond = m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.c_ptr());
m_rel_filter = rmgr.mk_filter_interpreted_fn(*inner, to_app(inner_cond));
}
(*m_rel_filter)(*inner);
@ -1411,11 +1408,10 @@ namespace datalog {
//create the condition with table values substituted in and relation values properly renamed
expr_ref inner_cond(m_manager);
m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.c_ptr(),
inner_cond);
inner_cond = m_subst(m_cond, m_renaming_for_inner_rel.size(), m_renaming_for_inner_rel.c_ptr());
relation_base * new_rel = old_rel.clone();
scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond));
(*filter)(*new_rel);

3
src/muz/rel/dl_mk_explanations.cpp
View file

@ -471,8 +471,7 @@ namespace datalog {
SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));
subst_arg[ofs-i] = r.m_data.get(i);
}
expr_ref res(m_manager);
m_subst(m_new_rule, subst_arg.size(), subst_arg.c_ptr(), res);
expr_ref res = m_subst(m_new_rule, subst_arg.size(), subst_arg.c_ptr());
r.m_data[m_col_idx] = to_app(res);
}
};

8
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -237,8 +237,8 @@ namespace datalog {
expr_ref_vector norm_subst = get_normalizer(t1, t2);
expr_ref t1n_ref(m);
expr_ref t2n_ref(m);
m_var_subst(t1, norm_subst.size(), norm_subst.c_ptr(), t1n_ref);
m_var_subst(t2, norm_subst.size(), norm_subst.c_ptr(), t2n_ref);
t1n_ref = m_var_subst(t1, norm_subst.size(), norm_subst.c_ptr());
t2n_ref = m_var_subst(t2, norm_subst.size(), norm_subst.c_ptr());
app * t1n = to_app(t1n_ref);
app * t2n = to_app(t2n_ref);
if (t1n->get_id() > t2n->get_id()) {
@ -531,7 +531,7 @@ namespace datalog {
expr_ref_vector normalizer = get_normalizer(rt1, rt2);
reverse_renaming(m, normalizer, denormalizer);
expr_ref new_transf(m);
m_var_subst(t_new, denormalizer.size(), denormalizer.c_ptr(), new_transf);
new_transf = m_var_subst(t_new, denormalizer.size(), denormalizer.c_ptr());
var_idx_set transf_vars = rm.collect_vars(new_transf);
TRACE("dl", tout << mk_pp(rt1, m) << " " << mk_pp(rt2, m) << " -> " << new_transf << "\n";);
counter.count_vars(rt2, -1);
@ -549,7 +549,7 @@ namespace datalog {
TRACE("dl", tout << normalizer << "\nnorm\n" << normalizer2 << "\n";);
denormalizer.reset();
reverse_renaming(m, normalizer2, denormalizer);
m_var_subst(t_new, denormalizer.size(), denormalizer.c_ptr(), new_transf);
new_transf = m_var_subst(t_new, denormalizer.size(), denormalizer.c_ptr());
SASSERT(non_local_vars.subset_of(rm.collect_vars(new_transf)));
TRACE("dl", tout << mk_pp(rt2, m) << " " << mk_pp(rt1, m) << " -> " << new_transf << "\n";);
}

3
src/muz/rel/dl_relation_manager.cpp
View file

@ -1395,8 +1395,7 @@ namespace datalog {
args.push_back(m_decl_util.mk_numeral(el, m_free_vars[i]));
}
expr_ref ground(m_ast_manager);
m_vs(m_condition.get(), args.size(), args.c_ptr(), ground);
expr_ref ground = m_vs(m_condition.get(), args.size(), args.c_ptr());
m_simp(ground);
return m_ast_manager.is_false(ground);

5
src/muz/rel/dl_sieve_relation.cpp
View file

@ -85,7 +85,7 @@ namespace datalog {
s.push_back(m.mk_var(idx, sig[i]));
}
get_inner().to_formula(tmp);
get_plugin().get_context().get_var_subst()(tmp, sz, s.c_ptr(), fml);
fml = get_plugin().get_context().get_var_subst()(tmp, sz, s.c_ptr());
}
@ -584,8 +584,7 @@ namespace datalog {
}
subst_vect[subst_ofs-i] = m.mk_var(r.m_sig2inner[i], sig[i]);
}
expr_ref inner_cond(m);
get_context().get_var_subst()(condition, subst_vect.size(), subst_vect.c_ptr(), inner_cond);
expr_ref inner_cond = get_context().get_var_subst()(condition, subst_vect.size(), subst_vect.c_ptr());
relation_mutator_fn * inner_fun = get_manager().mk_filter_interpreted_fn(r.get_inner(), to_app(inner_cond));
if(!inner_fun) {

10
src/muz/spacer/spacer_context.cpp
View file

@ -526,7 +526,7 @@ void lemma::mk_expr_core() {
sorts.push_back(get_sort(zks.get(i)));
names.push_back(zks.get(i)->get_decl()->get_name());
}
m_body = m.mk_quantifier(true, zks.size(),
m_body = m.mk_quantifier(forall_k, zks.size(),
sorts.c_ptr(),
names.c_ptr(),
m_body, 15, symbol(m_body->get_id()));
@ -633,7 +633,7 @@ void lemma::instantiate(expr * const * exprs, expr_ref &result, expr *e) {
expr *body = to_quantifier(lem)->get_expr();
unsigned num_decls = to_quantifier(lem)->get_num_decls();
var_subst vs(m, false);
vs(body, num_decls, exprs, result);
result = vs(body, num_decls, exprs);
}
void lemma::set_level (unsigned lvl) {
@ -1347,7 +1347,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
if (is_sat == l_true || is_sat == l_undef) {
if (core) { core->reset(); }
if (model && model->get()) {
if (model) {
r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
TRACE ("spacer", tout << "reachable "
<< "is_concrete " << is_concrete << " rused: ";
@ -1621,9 +1621,7 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule)
ground_free_vars(trans, var_reprs, aux_vars, ut_size == 0);
SASSERT(is_all_non_null(var_reprs));
expr_ref tmp(m);
var_subst(m, false)(trans, var_reprs.size (),
(expr*const*)var_reprs.c_ptr(), tmp);
expr_ref tmp = var_subst(m, false)(trans, var_reprs.size (), (expr*const*)var_reprs.c_ptr());
flatten_and (tmp, side);
trans = mk_and(side);
side.reset ();

2
src/muz/spacer/spacer_iuc_proof.h
View file

@ -33,7 +33,7 @@ public:
bool is_h_marked(proof* p) {return m_h_mark.is_marked(p);}
bool is_b_pure (proof *p) {
return !is_h_marked (p) && is_core_pure(m.get_fact (p));
return !is_h_marked (p) && !this->is_a_marked(p) && is_core_pure(m.get_fact (p));
}
void display_dot(std::ostream &out);

1171
src/muz/spacer/spacer_proof_utils.cpp
View file

File diff suppressed because it is too large Load diff

36
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -36,28 +36,27 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin) {
}
void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
// traverse proof
proof_post_order it(m_pr.get(), m);
while (it.hasNext()) {
proof* currentNode = it.next();
proof* curr = it.next();
if (m.get_num_parents(currentNode) > 0) {
bool need_to_mark_closed = true;
bool done = is_closed(curr);
if (done) continue;
for (proof* premise : m.get_parents(currentNode)) {
need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
}
// save result
m_closed.mark(currentNode, need_to_mark_closed);
if (m.get_num_parents(curr) > 0) {
done = true;
for (proof* p : m.get_parents(curr)) done &= !is_b_open(p);
set_closed(curr, done);
}
// we have now collected all necessary information, so we can visit the node
// if the node mixes A-reasoning and B-reasoning and contains non-closed premises
if (m_pr.is_a_marked(currentNode) &&
m_pr.is_b_marked(currentNode) &&
!m_closed.is_marked(currentNode)) {
compute_partial_core(currentNode); // then we need to compute a partial core
// we have now collected all necessary information,
// so we can visit the node
// if the node mixes A-reasoning and B-reasoning
// and contains non-closed premises
if (!done) {
if (is_a(curr) && is_b(curr)) {
compute_partial_core(curr);
}
}
}
@ -74,7 +73,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
void unsat_core_learner::compute_partial_core(proof* step) {
for (unsat_core_plugin* plugin : m_plugins) {
if (m_closed.is_marked(step)) break;
if (is_closed(step)) break;
plugin->compute_partial_core(step);
}
}
@ -93,9 +92,6 @@ void unsat_core_learner::set_closed(proof* p, bool value) {
m_closed.mark(p, value);
}
bool unsat_core_learner::is_b_open(proof *p) {
return m_pr.is_b_marked(p) && !is_closed (p);
}
void unsat_core_learner::add_lemma_to_core(expr* lemma) {
m_unsat_core.push_back(lemma);

33
src/muz/spacer/spacer_unsat_core_learner.h
View file

@ -22,6 +22,7 @@ Revision History:
#include "ast/ast.h"
#include "muz/spacer/spacer_util.h"
#include "muz/spacer/spacer_proof_utils.h"
#include "muz/spacer/spacer_iuc_proof.h"
namespace spacer {
@ -31,13 +32,32 @@ namespace spacer {
class unsat_core_learner {
typedef obj_hashtable<expr> expr_set;
ast_manager& m;
iuc_proof& m_pr;
ptr_vector<unsat_core_plugin> m_plugins;
ast_mark m_closed;
expr_ref_vector m_unsat_core;
public:
unsat_core_learner(ast_manager& m, iuc_proof& pr) :
m(m), m_pr(pr), m_unsat_core(m) {};
virtual ~unsat_core_learner();
ast_manager& m;
iuc_proof& m_pr;
ast_manager& get_manager() {return m;}
bool is_a(proof *pr) {
// AG: treat hypotheses as A
// AG: assume that all B-hyp have been eliminated
// AG: this is not yet true in case of arithmetic eq_prop
return m_pr.is_a_marked(pr) || is_h(pr);
}
bool is_b(proof *pr) {return m_pr.is_b_marked(pr);}
bool is_h(proof *pr) {return m_pr.is_h_marked(pr);}
bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);}
bool is_b_open(proof *p) {return m_pr.is_b_marked(p) && !is_closed (p);}
/*
* register a plugin for computation of partial unsat cores
@ -59,7 +79,6 @@ namespace spacer {
bool is_closed(proof* p);
void set_closed(proof* p, bool value);
bool is_b_open (proof *p);
/*
* adds a lemma to the unsat core
@ -67,14 +86,6 @@ namespace spacer {
void add_lemma_to_core(expr* lemma);
private:
ptr_vector<unsat_core_plugin> m_plugins;
ast_mark m_closed;
/*
* collects the lemmas of the unsat-core
* will at the end be inserted into unsat_core.
*/
expr_ref_vector m_unsat_core;
/*
* computes partial core for step by delegating computation to plugins

214
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -34,82 +34,81 @@ Revision History:
namespace spacer {
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner):
m(learner.m), m_learner(learner) {};
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx):
m(ctx.get_manager()), m_ctx(ctx) {};
void unsat_core_plugin_lemma::compute_partial_core(proof* step) {
SASSERT(m_learner.m_pr.is_a_marked(step));
SASSERT(m_learner.m_pr.is_b_marked(step));
for (proof* premise : m.get_parents(step)) {
if (m_learner.is_b_open (premise)) {
SASSERT(m_ctx.is_a(step));
SASSERT(m_ctx.is_b(step));
for (auto* p : m.get_parents(step)) {
if (m_ctx.is_b_open (p)) {
// by IH, premises that are AB marked are already closed
SASSERT(!m_learner.m_pr.is_a_marked(premise));
add_lowest_split_to_core(premise);
SASSERT(!m_ctx.is_a(p));
add_lowest_split_to_core(p);
}
}
m_learner.set_closed(step, true);
m_ctx.set_closed(step, true);
}
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const
{
SASSERT(m_learner.is_b_open(step));
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const {
SASSERT(m_ctx.is_b_open(step));
ptr_buffer<proof> todo;
todo.push_back(step);
while (!todo.empty()) {
proof* pf = todo.back();
todo.pop_back();
// if current step hasn't been processed,
if (!m_learner.is_closed(pf)) {
m_learner.set_closed(pf, true);
if (!m_ctx.is_closed(pf)) {
m_ctx.set_closed(pf, true);
// the step is b-marked and not closed.
// by I.H. the step must be already visited
// so if it is also a-marked, it must be closed
SASSERT(m_learner.m_pr.is_b_marked(pf));
SASSERT(!m_learner.m_pr.is_a_marked(pf));
SASSERT(m_ctx.is_b(pf));
SASSERT(!m_ctx.is_a(pf));
// the current step needs to be interpolated:
expr* fact = m.get_fact(pf);
// if we trust the current step and we are able to use it
if (m_learner.m_pr.is_b_pure (pf) &&
(m.is_asserted(pf) || is_literal(m, fact))) {
if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || is_literal(m, fact))) {
// just add it to the core
m_learner.add_lemma_to_core(fact);
m_ctx.add_lemma_to_core(fact);
}
// otherwise recurse on premises
else {
for (proof* premise : m.get_parents(pf))
if (m_learner.is_b_open(premise))
for (proof* premise : m.get_parents(pf))
if (m_ctx.is_b_open(premise))
todo.push_back(premise);
}
}
}
}
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step)
{
SASSERT(m_learner.m_pr.is_a_marked(step));
SASSERT(m_learner.m_pr.is_b_marked(step));
/***
* FARKAS
*/
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) {
SASSERT(m_ctx.is_a(step));
SASSERT(m_ctx.is_b(step));
// XXX this assertion should be true so there is no need to check for it
SASSERT (!m_learner.is_closed (step));
SASSERT (!m_ctx.is_closed (step));
func_decl* d = step->get_decl();
symbol sym;
if (!m_learner.is_closed(step) && // if step is not already interpolated
is_farkas_lemma(m, step)) {
// weaker check: d->get_num_parameters() >= m.get_num_parents(step) + 2
TRACE("spacer.farkas",
tout << "looking at: " << mk_pp(step, m) << "\n";);
if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) {
// weaker check : d->get_num_parameters() >= m.get_num_parents(step) + 2
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
SASSERT(m.has_fact(step));
coeff_lits_t coeff_lits;
expr_ref_vector pinned(m);
/* The farkas lemma represents a subproof starting from premise(-set)s A, BNP and BP(ure) and
* ending in a disjunction D. We need to compute the contribution of BP, i.e. a formula, which
* is entailed by BP and together with A and BNP entails D.
@ -134,34 +133,35 @@ namespace spacer {
* as workaround we take the absolute value of the provided coefficients.
*/
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
STRACE("spacer.farkas",
verbose_stream() << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(step, i);
rational coef = params[i].get_rational();
bool b_pure = m_learner.m_pr.is_b_pure (prem);
verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
}
);
bool can_be_closed = true;
TRACE("spacer.farkas",
tout << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(step, i);
rational coef = params[i].get_rational();
bool b_pure = m_ctx.is_b_pure (prem);
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
}
);
bool done = true;
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * premise = m.get_parent(step, i);
if (m_learner.is_b_open (premise)) {
SASSERT(!m_learner.m_pr.is_a_marked(premise));
if (m_learner.m_pr.is_b_pure (step)) {
if (m_ctx.is_b_open (premise)) {
SASSERT(!m_ctx.is_a(premise));
if (m_ctx.is_b_pure (premise)) {
if (!m_use_constant_from_a) {
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
}
}
else {
can_be_closed = false;
// -- mixed premise, won't be able to close this proof step
done = false;
if (m_use_constant_from_a) {
rational coefficient = params[i].get_rational();
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
@ -175,10 +175,11 @@ namespace spacer {
}
}
}
// TBD: factor into another method
if (m_use_constant_from_a) {
params += m.get_num_parents(step); // point to the first Farkas coefficient, which corresponds to a formula in the conclusion
// the conclusion can either be a single formula or a disjunction of several formulas, we have to deal with both situations
if (m.get_num_parents(step) + 2 < d->get_num_parameters()) {
unsigned num_args = 1;
@ -190,7 +191,7 @@ namespace spacer {
args = _or->get_args();
}
SASSERT(m.get_num_parents(step) + 2 + num_args == d->get_num_parameters());
bool_rewriter brw(m);
for (unsigned i = 0; i < num_args; ++i) {
expr* premise = args[i];
@ -205,13 +206,12 @@ namespace spacer {
}
// only if all b-premises can be used directly, add the farkas core and close the step
if (can_be_closed) {
m_learner.set_closed(step, true);
expr_ref res = compute_linear_combination(coeff_lits);
m_learner.add_lemma_to_core(res);
}
// AG: this decision needs to be re-evaluated. If the proof cannot be closed, literals above
// AG: it will go into the core. However, it does not mean that this literal should/could not be added.
m_ctx.set_closed(step, done);
expr_ref res = compute_linear_combination(coeff_lits);
TRACE("spacer.farkas", tout << "Farkas core: " << res << "\n";);
m_ctx.add_lemma_to_core(res);
}
}
@ -235,12 +235,12 @@ namespace spacer {
void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step)
{
SASSERT(m_learner.m_pr.is_a_marked(step));
SASSERT(m_learner.m_pr.is_b_marked(step));
SASSERT(m_ctx.is_a(step));
SASSERT(m_ctx.is_b(step));
func_decl* d = step->get_decl();
symbol sym;
if (!m_learner.is_closed(step) && // if step is not already interpolated
if (!m_ctx.is_closed(step) && // if step is not already interpolated
is_farkas_lemma(m, step)) {
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
SASSERT(m.has_fact(step));
@ -249,25 +249,25 @@ namespace spacer {
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
STRACE("spacer.farkas",
verbose_stream() << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(step, i);
rational coef = params[i].get_rational();
bool b_pure = m_learner.m_pr.is_b_pure (prem);
verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n";
}
);
TRACE("spacer.farkas",
tout << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(step, i);
rational coef = params[i].get_rational();
bool b_pure = m_ctx.is_b_pure (prem);
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
}
);
bool can_be_closed = true;
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * premise = m.get_parent(step, i);
if (m_learner.m_pr.is_b_marked(premise) && !m_learner.is_closed(premise))
if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise))
{
SASSERT(!m_learner.m_pr.is_a_marked(premise));
SASSERT(!m_ctx.is_a(premise));
if (m_learner.m_pr.is_b_pure(premise))
if (m_ctx.is_b_pure(premise))
{
rational coefficient = params[i].get_rational();
linear_combination.push_back
@ -283,7 +283,7 @@ namespace spacer {
// only if all b-premises can be used directly, close the step and add linear combinations for later processing
if (can_be_closed)
{
m_learner.set_closed(step, true);
m_ctx.set_closed(step, true);
if (!linear_combination.empty())
{
m_linear_combinations.push_back(linear_combination);
@ -340,7 +340,7 @@ namespace spacer {
// 4. extract linear combinations from matrix and add result to core
for (unsigned k = 0; k < i; ++k)// i points to the row after the last row which is non-zero
{
coeff_lits_t coeff_lits;
coeff_lits_t coeff_lits;
for (unsigned l = 0; l < matrix.num_cols(); ++l) {
if (!matrix.get(k,l).is_zero()) {
coeff_lits.push_back(std::make_pair(matrix.get(k, l), ordered_basis[l]));
@ -349,19 +349,19 @@ namespace spacer {
SASSERT(!coeff_lits.empty());
expr_ref linear_combination = compute_linear_combination(coeff_lits);
m_learner.add_lemma_to_core(linear_combination);
m_ctx.add_lemma_to_core(linear_combination);
}
}
expr_ref unsat_core_plugin_farkas_lemma_optimized::compute_linear_combination(const coeff_lits_t& coeff_lits) {
expr_ref unsat_core_plugin_farkas_lemma_optimized::compute_linear_combination(const coeff_lits_t& coeff_lits) {
smt::farkas_util util(m);
for (auto const & p : coeff_lits) {
util.add(p.first, p.second);
}
expr_ref negated_linear_combination = util.get();
SASSERT(m.is_not(negated_linear_combination));
return expr_ref(mk_not(m, negated_linear_combination), m);
return expr_ref(mk_not(m, negated_linear_combination), m);
//TODO: rewrite the get-method to return nonnegated stuff?
}
@ -449,7 +449,7 @@ namespace spacer {
for (unsigned j = 0; j < matrix.num_cols(); ++j) {
SASSERT(matrix.get(i, j).is_int());
app_ref a_ij(util.mk_numeral(matrix.get(i,j), true), m);
app_ref sum(util.mk_int(0), m);
for (unsigned k = 0; k < n; ++k) {
sum = util.mk_add(sum, util.mk_mul(coeffs[i][k].get(), bounded_vectors[j][k].get()));
@ -458,7 +458,7 @@ namespace spacer {
s->assert_expr(eq);
}
}
// check result
lbool res = s->check_sat(0, nullptr);
@ -480,7 +480,7 @@ namespace spacer {
SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already
expr_ref linear_combination = compute_linear_combination(coeff_lits);
m_learner.add_lemma_to_core(linear_combination);
m_ctx.add_lemma_to_core(linear_combination);
}
return;
}
@ -504,10 +504,10 @@ namespace spacer {
{
ptr_vector<proof> todo;
SASSERT(m_learner.m_pr.is_a_marked(step));
SASSERT(m_learner.m_pr.is_b_marked(step));
SASSERT(m_ctx.is_a(step));
SASSERT(m_ctx.is_b(step));
SASSERT(m.get_num_parents(step) > 0);
SASSERT(!m_learner.is_closed(step));
SASSERT(!m_ctx.is_closed(step));
todo.push_back(step);
while (!todo.empty())
@ -516,7 +516,7 @@ namespace spacer {
todo.pop_back();
// if we need to deal with the node and if we haven't added the corresponding edges so far
if (!m_learner.is_closed(current) && !m_visited.is_marked(current))
if (!m_ctx.is_closed(current) && !m_visited.is_marked(current))
{
// compute smallest subproof rooted in current, which has only good edges
// add an edge from current to each leaf of that subproof
@ -527,7 +527,7 @@ namespace spacer {
}
}
m_learner.set_closed(step, true);
m_ctx.set_closed(step, true);
}
@ -538,7 +538,7 @@ namespace spacer {
ptr_buffer<proof> todo_subproof;
for (proof* premise : m.get_parents(step)) {
if (m_learner.m_pr.is_b_marked(premise)) {
if (m_ctx.is_b(premise)) {
todo_subproof.push_back(premise);
}
}
@ -548,21 +548,21 @@ namespace spacer {
todo_subproof.pop_back();
// if we need to deal with the node
if (!m_learner.is_closed(current))
if (!m_ctx.is_closed(current))
{
SASSERT(!m_learner.m_pr.is_a_marked(current)); // by I.H. the step must be already visited
SASSERT(!m_ctx.is_a(current)); // by I.H. the step must be already visited
// and the current step needs to be interpolated:
if (m_learner.m_pr.is_b_marked(current))
if (m_ctx.is_b(current))
{
// if we trust the current step and we are able to use it
if (m_learner.m_pr.is_b_pure (current) &&
if (m_ctx.is_b_pure (current) &&
(m.is_asserted(current) ||
is_literal(m, m.get_fact(current))))
{
// we found a leaf of the subproof, so
// 1) we add corresponding edges
if (m_learner.m_pr.is_a_marked(step))
if (m_ctx.is_a(step))
{
add_edge(nullptr, current); // current is sink
}
@ -682,9 +682,9 @@ namespace spacer {
void unsat_core_plugin_min_cut::finalize() {
unsigned_vector cut_nodes;
m_min_cut.compute_min_cut(cut_nodes);
for (unsigned cut_node : cut_nodes) {
m_learner.add_lemma_to_core(m_node_to_formula[cut_node]);
m_ctx.add_lemma_to_core(m_node_to_formula[cut_node]);
}
}
}

16
src/muz/spacer/spacer_unsat_core_plugin.h
View file

@ -35,14 +35,14 @@ namespace spacer {
virtual ~unsat_core_plugin() {};
virtual void compute_partial_core(proof* step) = 0;
virtual void finalize(){};
unsat_core_learner& m_learner;
unsat_core_learner& m_ctx;
};
class unsat_core_plugin_lemma : public unsat_core_plugin {
class unsat_core_plugin_lemma : public unsat_core_plugin {
public:
unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){};
void compute_partial_core(proof* step) override;
unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){};
void compute_partial_core(proof* step) override;
private:
void add_lowest_split_to_core(proof* step) const;
};
@ -54,7 +54,7 @@ namespace spacer {
bool use_constant_from_a=true) :
unsat_core_plugin(learner),
m_split_literals(split_literals),
m_use_constant_from_a(use_constant_from_a) {};
m_use_constant_from_a(use_constant_from_a) {};
void compute_partial_core(proof* step) override;
private:
bool m_split_literals;
@ -64,8 +64,8 @@ namespace spacer {
*/
expr_ref compute_linear_combination(const coeff_lits_t& coeff_lits);
};
class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin {
class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin {
public:
unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {};
void compute_partial_core(proof* step) override;

4
src/muz/spacer/spacer_util.cpp
View file

@ -785,7 +785,7 @@ namespace {
void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
expr_free_vars fv;
ast_manager &m = out.get_manager();
ast_manager &m = out.m();
fv(e);
if (vars.size() < fv.size()) {
@ -795,7 +795,7 @@ namespace {
sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
vars[i] = mk_zk_const(m, i, s);
var_subst vs(m, false);
vs(e, vars.size(),(expr * *) vars.c_ptr(), out);
out = vs(e, vars.size(),(expr * *) vars.c_ptr());
}
}

18
src/muz/tab/tab_context.cpp
View file

@ -561,13 +561,13 @@ namespace tb {
}
vars.push_back(m.mk_const(symbol(i), sorts[i]));
}
vs(g.get_head(), vars.size(), vars.c_ptr(), fml);
fml = vs(g.get_head(), vars.size(), vars.c_ptr());
m_head = to_app(fml);
for (unsigned i = 0; i < g.get_num_predicates(); ++i) {
vs(g.get_predicate(i), vars.size(), vars.c_ptr(), fml);
fml = vs(g.get_predicate(i), vars.size(), vars.c_ptr());
m_preds.push_back(to_app(fml));
}
vs(g.get_constraint(), vars.size(), vars.c_ptr(), fml);
fml = vs(g.get_constraint(), vars.size(), vars.c_ptr());
fmls.push_back(fml);
m_precond = m.mk_and(fmls.size(), fmls.c_ptr());
IF_VERBOSE(2,
@ -1132,12 +1132,12 @@ namespace tb {
}
}
if (change) {
m_S2(result->get_constraint(), m_rename.size(), m_rename.c_ptr(), constraint);
constraint = m_S2(result->get_constraint(), m_rename.size(), m_rename.c_ptr());
for (unsigned i = 0; i < result->get_num_predicates(); ++i) {
m_S2(result->get_predicate(i), m_rename.size(), m_rename.c_ptr(), tmp);
tmp = m_S2(result->get_predicate(i), m_rename.size(), m_rename.c_ptr());
predicates[i] = to_app(tmp);
}
m_S2(result->get_head(), m_rename.size(), m_rename.c_ptr(), tmp);
tmp = m_S2(result->get_head(), m_rename.size(), m_rename.c_ptr());
head = to_app(tmp);
result->init(head, predicates, constraint);
}
@ -1168,7 +1168,7 @@ namespace tb {
if (vars[i]) {
v = m.mk_var(i, vars[i]);
m_S1.apply(2, delta, expr_offset(v, offset), tmp);
m_S2(tmp, m_rename.size(), m_rename.c_ptr(), tmp);
tmp = m_S2(tmp, m_rename.size(), m_rename.c_ptr());
insert_subst(offset, tmp);
}
else {
@ -1613,8 +1613,8 @@ namespace datalog {
}
expr_ref body = clause.get_body();
var_subst vs(m, false);
vs(body, subst.size(), subst.c_ptr(), body);
out << mk_pp(body, m) << "\n";
body = vs(body, subst.size(), subst.c_ptr());
out << body << "\n";
}
void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2,

2
src/muz/transforms/dl_mk_coalesce.cpp
View file

@ -98,7 +98,7 @@ namespace datalog {
}
var_subst vs(m, false);
for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) {
vs(r->get_tail(i), revsub.size(), revsub.c_ptr(), result);
result = vs(r->get_tail(i), revsub.size(), revsub.c_ptr());
conjs.push_back(result);
}
bwr.mk_and(conjs.size(), conjs.c_ptr(), result);

8
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -156,8 +156,7 @@ namespace datalog {
SASSERT(m_binding[i]);
});
m_binding.reverse();
expr_ref res(m);
instantiate(m, q, m_binding.c_ptr(), res);
expr_ref res = instantiate(m, q, m_binding.c_ptr());
m_binding.reverse();
m_cnst2var(res);
conjs.push_back(res);
@ -222,10 +221,7 @@ namespace datalog {
for (unsigned i = 0; i < qs.size(); ++i) {
instantiate_quantifier(qs[i].get(), conjs);
}
obj_map<func_decl, ptr_vector<expr>*>::iterator it = m_funs.begin(), end = m_funs.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
for (auto & kv : m_funs) dealloc(kv.m_value);
m_funs.reset();
fml = m.mk_and(conjs.size(), conjs.c_ptr());

2
src/muz/transforms/dl_mk_scale.cpp
View file

@ -69,7 +69,7 @@ namespace datalog {
// Hedge that we don't have to handle the general case for models produced
// by Horn clause solvers.
SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0);
vs(new_fi->get_else(), subst.size(), subst.c_ptr(), tmp);
tmp = vs(new_fi->get_else(), subst.size(), subst.c_ptr());
old_fi->set_else(tmp);
old_model->register_decl(old_p, old_fi);
}

6
src/muz/transforms/dl_mk_slice.cpp
View file

@ -352,7 +352,7 @@ namespace datalog {
}
if (!new_fi->is_partial()) {
TRACE("dl", tout << mk_pp(new_fi->get_else(), m) << "\n";);
vs(new_fi->get_else(), subst.size(), subst.c_ptr(), tmp);
tmp = vs(new_fi->get_else(), subst.size(), subst.c_ptr());
old_fi->set_else(tmp);
}
unsigned num_entries = new_fi->num_entries();
@ -362,7 +362,7 @@ namespace datalog {
func_entry const* e = new_fi->get_entry(j);
for (unsigned k = 0, l = 0; k < old_p->get_arity(); ++k) {
if (!is_sliced.get(k)) {
vs(e->get_arg(l++), subst.size(), subst.c_ptr(), tmp);
tmp = vs(e->get_arg(l++), subst.size(), subst.c_ptr());
args.push_back(tmp);
}
else {
@ -370,7 +370,7 @@ namespace datalog {
}
SASSERT(l <= new_p->get_arity());
}
vs(e->get_result(), subst.size(), subst.c_ptr(), res);
res = vs(e->get_result(), subst.size(), subst.c_ptr());
old_fi->insert_entry(args.c_ptr(), res.get());
}
old_model->register_decl(old_p, old_fi);