mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

debugging dl_bmc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-10 18:37:10 -07:00
parent c9c8fb3834
commit 2b0e1f7c2b
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
lib/dl_bmc_engine.cpp
View file

@ -512,7 +512,6 @@ namespace datalog {
conjs.push_back(tmp);
}
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
expr* rule_pred = m.mk_app(rule_pred_i, trace_arg.get(), path_var.get());
ptr_vector<sort> q_sorts;
vector<symbol> names;
for (unsigned i = 0; i < vars.size(); ++i) {
@ -526,17 +525,18 @@ namespace datalog {
SASSERT(vars.size() == names.size());
symbol qid = r.name(), skid;
patterns.reset();
patterns.push_back(m.mk_pattern(to_app(rule_pred)));
//patterns.reset();
//patterns.push_back(m.mk_pattern(to_app(rule_pred)));
//
//fml = m.mk_implies(rule_pred, rule_body);
//fml = m.mk_forall(vars.size(), q_sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr());
//assert_expr(fml);
expr_ref fml(m);
fml = m.mk_implies(rule_pred, rule_body);
fml = m.mk_forall(vars.size(), q_sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr());
assert_expr(fml);
tmp = m.mk_app(mk_predicate(p), trace_arg.get(), path_var.get());
patterns.reset();
patterns.push_back(m.mk_pattern(to_app(tmp)));
fml = m.mk_implies(tmp, rule_pred);
fml = m.mk_implies(tmp, rule_body);
fml = m.mk_forall(vars.size(), sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr());
assert_expr(fml);