From c9c8fb38344831141e8856a3577f6ea43bc919ee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Oct 2012 18:32:52 -0700 Subject: [PATCH] debugging dl_bmc Signed-off-by: Nikolaj Bjorner --- lib/dl_bmc_engine.cpp | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp index 1ff04196d..5f785c96e 100644 --- a/lib/dl_bmc_engine.cpp +++ b/lib/dl_bmc_engine.cpp @@ -465,7 +465,7 @@ namespace datalog { path_arg = path_var.get(); } else { - path_arg = m.mk_app(succs[j-1], path_var.get()); + path_arg = m.mk_app(succs[j], path_var.get()); } for (unsigned k = 0; k < q->get_arity(); ++k) { expr* arg = r.get_tail(j)->get_arg(k); @@ -496,7 +496,7 @@ namespace datalog { path_arg = path_var.get(); } else { - path_arg = m.mk_app(succs[j-1], path_var.get()); + path_arg = m.mk_app(succs[j], path_var.get()); } func_decl* q = r.get_decl(j); for (unsigned k = 0; k < q->get_arity(); ++k) { @@ -531,18 +531,16 @@ namespace datalog { 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()); - std::cout << mk_pp(fml, m) << "\n"; 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_forall(vars.size(), sorts.c_ptr(), names.c_ptr(), fml, 1, qid, skid, 1, patterns.c_ptr()); + assert_expr(fml); + } - bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp); - symbol names[2] = { symbol("Trace"), symbol("Path") }; - symbol qid = p->get_name(), skid; - patterns.reset(); - patterns.push_back(m.mk_pattern(to_app(pred))); - expr_ref fml(m); - fml = m.mk_implies(pred, tmp); - fml = m.mk_forall(2, sorts, names, fml, 1, qid, skid, 1, patterns.c_ptr()); - assert_expr(fml); } }