mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
added QBMC backend based on quantified bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
294da9acff
commit
67b57c8c28
|
|
@ -28,6 +28,7 @@ Revision History:
|
|||
#include "bool_rewriter.h"
|
||||
#include "model_smt2_pp.h"
|
||||
#include "ast_smt_pp.h"
|
||||
#include "well_sorted.h"
|
||||
|
||||
namespace datalog {
|
||||
bmc::bmc(context& ctx):
|
||||
|
|
@ -39,11 +40,8 @@ namespace datalog {
|
|||
m_rules(ctx),
|
||||
m_query_pred(m),
|
||||
m_answer(m),
|
||||
m_path_sort(m) {
|
||||
m_fparams.m_model = true;
|
||||
m_fparams.m_model_compact = true;
|
||||
m_fparams.m_mbqi = false;
|
||||
// m_fparams.m_auto_config = false;
|
||||
m_path_sort(m),
|
||||
m_bv(m) {
|
||||
}
|
||||
|
||||
bmc::~bmc() {}
|
||||
|
|
@ -95,6 +93,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
if (is_linear()) {
|
||||
if (m_ctx.get_engine() == QBMC_ENGINE) {
|
||||
return check_qlinear();
|
||||
}
|
||||
return check_linear();
|
||||
}
|
||||
else {
|
||||
|
|
@ -113,6 +114,9 @@ namespace datalog {
|
|||
return true;
|
||||
}
|
||||
|
||||
// --------------------------------------------------------------------------
|
||||
// Basic linear BMC based on incrementally unfolding the transition relation.
|
||||
|
||||
void bmc::get_model_linear(unsigned level) {
|
||||
rule_manager& rm = m_ctx.get_rule_manager();
|
||||
expr_ref level_query = mk_level_predicate(m_query_pred, level);
|
||||
|
|
@ -124,18 +128,18 @@ namespace datalog {
|
|||
SASSERT(m.is_true(md->get_const_interp(to_app(level_query)->get_decl())));
|
||||
dl_decl_util util(m);
|
||||
|
||||
TRACE("dl", model_smt2_pp(tout, m, *md, 0););
|
||||
TRACE("bmc", model_smt2_pp(tout, m, *md, 0););
|
||||
|
||||
rule_ref r0(rm), r1(rm), r2(rm);
|
||||
while (true) {
|
||||
TRACE("dl", tout << "Predicate: " << pred->get_name() << "\n";);
|
||||
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
|
||||
expr_ref_vector sub(m);
|
||||
rule_vector const& rls = m_rules.get_predicate_rules(pred);
|
||||
rule* r = 0;
|
||||
unsigned i = 0;
|
||||
for (; i < rls.size(); ++i) {
|
||||
expr_ref rule_i = mk_level_rule(pred, i, level);
|
||||
TRACE("dl", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
|
||||
TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
|
||||
if (m.is_true(md->get_const_interp(to_app(rule_i)->get_decl()))) {
|
||||
r = rls[i];
|
||||
break;
|
||||
|
|
@ -210,8 +214,16 @@ namespace datalog {
|
|||
}
|
||||
|
||||
|
||||
lbool bmc::check_linear() {
|
||||
void bmc::setup_linear() {
|
||||
m_fparams.m_relevancy_lvl = 0;
|
||||
m_fparams.m_model = true;
|
||||
m_fparams.m_model_compact = true;
|
||||
m_fparams.m_mbqi = false;
|
||||
// m_fparams.m_auto_config = false;
|
||||
}
|
||||
|
||||
lbool bmc::check_linear() {
|
||||
setup_linear();
|
||||
for (unsigned i = 0; ; ++i) {
|
||||
IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";);
|
||||
checkpoint();
|
||||
|
|
@ -233,8 +245,8 @@ namespace datalog {
|
|||
return m_solver.check(1, &q);
|
||||
}
|
||||
|
||||
void bmc::assert_expr(expr* e) {
|
||||
TRACE("dl", tout << mk_pp(e, m) << "\n";);
|
||||
void bmc::assert_expr(expr* e) {
|
||||
TRACE("bmc", tout << mk_pp(e, m) << "\n";);
|
||||
m_solver.assert_expr(e);
|
||||
}
|
||||
|
||||
|
|
@ -258,7 +270,6 @@ namespace datalog {
|
|||
}
|
||||
|
||||
expr_ref bmc::mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) {
|
||||
SASSERT(idx < pred->get_arity());
|
||||
std::stringstream _name;
|
||||
_name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx;
|
||||
symbol nm(_name.str().c_str());
|
||||
|
|
@ -328,7 +339,8 @@ namespace datalog {
|
|||
expr_ref rule_i = mk_level_rule(p, i, level);
|
||||
rules.push_back(rule_i);
|
||||
if (level == 0 && r.get_uninterpreted_tail_size() > 0) {
|
||||
assert_expr(m.mk_not(rule_i));
|
||||
tmp = m.mk_not(rule_i);
|
||||
assert_expr(tmp);
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
@ -354,22 +366,333 @@ namespace datalog {
|
|||
conjs.push_back(tmp);
|
||||
}
|
||||
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
|
||||
|
||||
assert_expr(m.mk_implies(rule_i, rule_body));
|
||||
rule_body = m.mk_implies(rule_i, rule_body);
|
||||
assert_expr(rule_body);
|
||||
}
|
||||
bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp);
|
||||
assert_expr(m.mk_implies(level_pred, tmp));
|
||||
tmp = m.mk_implies(level_pred, tmp);
|
||||
assert_expr(tmp);
|
||||
}
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Basic linear BMC based on indexed variables using quantified bit-vector domains.
|
||||
|
||||
lbool bmc::check_qlinear() {
|
||||
setup_qlinear();
|
||||
m_bit_width = 4;
|
||||
lbool res = l_false;
|
||||
while (res == l_false) {
|
||||
m_solver.push();
|
||||
IF_VERBOSE(1, verbose_stream() << "bit_width: " << m_bit_width << "\n";);
|
||||
compile_qlinear();
|
||||
checkpoint();
|
||||
func_decl_ref q = mk_q_func_decl(m_query_pred);
|
||||
expr* T = m.mk_const(symbol("T"), mk_index_sort());
|
||||
expr_ref fml(m.mk_app(q, T), m);
|
||||
assert_expr(fml);
|
||||
res = m_solver.check();
|
||||
|
||||
if (res == l_true) {
|
||||
res = get_model_qlinear();
|
||||
}
|
||||
m_solver.pop(1);
|
||||
++m_bit_width;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
sort_ref bmc::mk_index_sort() {
|
||||
return sort_ref(m_bv.mk_sort(m_bit_width), m);
|
||||
}
|
||||
|
||||
var_ref bmc::mk_index_var() {
|
||||
return var_ref(m.mk_var(0, mk_index_sort()), m);
|
||||
}
|
||||
|
||||
void bmc::compile_qlinear() {
|
||||
sort_ref index_sort = mk_index_sort();
|
||||
var_ref var = mk_index_var();
|
||||
sort* index_sorts[1] = { index_sort };
|
||||
symbol tick("T");
|
||||
rule_set::decl2rules::iterator it = m_rules.begin_grouped_rules();
|
||||
rule_set::decl2rules::iterator end = m_rules.end_grouped_rules();
|
||||
for (; it != end; ++it) {
|
||||
func_decl* p = it->m_key;
|
||||
rule_vector const& rls = *it->m_value;
|
||||
// Assert: forall level . p(T) => body of rule i + equalities for head of rule i
|
||||
func_decl_ref pr = mk_q_func_decl(p);
|
||||
expr_ref pred = expr_ref(m.mk_app(pr, var.get()), m);
|
||||
expr_ref_vector rules(m), sub(m), conjs(m);
|
||||
expr_ref trm(m), rule_body(m), rule_i(m);
|
||||
for (unsigned i = 0; i < rls.size(); ++i) {
|
||||
sub.reset();
|
||||
conjs.reset();
|
||||
rule& r = *rls[i];
|
||||
rule_i = m.mk_app(mk_q_rule(p, i), var.get());
|
||||
rules.push_back(rule_i);
|
||||
|
||||
mk_qrule_vars(r, i, sub);
|
||||
|
||||
// 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);
|
||||
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);
|
||||
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);
|
||||
conjs.push_back(trm);
|
||||
}
|
||||
if (r.get_uninterpreted_tail_size() > 0) {
|
||||
conjs.push_back(m_bv.mk_ule(mk_q_one(), var));
|
||||
}
|
||||
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
|
||||
trm = m.mk_implies(rule_i, rule_body);
|
||||
trm = m.mk_forall(1, index_sorts, &tick, trm, 1);
|
||||
assert_expr(trm);
|
||||
}
|
||||
bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), trm);
|
||||
trm = m.mk_implies(pred, trm);
|
||||
trm = m.mk_forall(1, index_sorts, &tick, trm, 1);
|
||||
SASSERT(is_well_sorted(m, trm));
|
||||
assert_expr(trm);
|
||||
}
|
||||
}
|
||||
|
||||
void bmc::setup_qlinear() {
|
||||
m_fparams.m_relevancy_lvl = 2;
|
||||
m_fparams.m_model = true;
|
||||
m_fparams.m_model_compact = true;
|
||||
m_fparams.m_mbqi = true;
|
||||
}
|
||||
|
||||
void bmc::mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
|
||||
sort_ref_vector sorts(m);
|
||||
r.get_vars(sorts);
|
||||
// populate substitution of bound variables.
|
||||
sub.reset();
|
||||
sub.resize(sorts.size());
|
||||
|
||||
for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
|
||||
expr* arg = r.get_head()->get_arg(k);
|
||||
if (is_var(arg)) {
|
||||
unsigned idx = to_var(arg)->get_idx();
|
||||
if (!sub[idx].get()) {
|
||||
sub[idx] = mk_q_arg(r.get_decl(), 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) {
|
||||
expr* arg = r.get_tail(j)->get_arg(k);
|
||||
if (is_var(arg)) {
|
||||
unsigned idx = to_var(arg)->get_idx();
|
||||
if (!sub[idx].get()) {
|
||||
sub[idx] = mk_q_arg(q, k, false);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) {
|
||||
if (sorts[j].get() && !sub[j].get()) {
|
||||
sub[j] = mk_q_var(r.get_decl(), sorts[j].get(), rule_id, idx++);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref bmc::mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) {
|
||||
std::stringstream _name;
|
||||
_name << pred->get_name() << "#" << rule_id << "_" << idx;
|
||||
symbol nm(_name.str().c_str());
|
||||
var_ref var = mk_index_var();
|
||||
return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m);
|
||||
}
|
||||
|
||||
expr_ref bmc::mk_q_arg(func_decl* pred, unsigned idx, bool is_current) {
|
||||
SASSERT(idx < pred->get_arity());
|
||||
std::stringstream _name;
|
||||
_name << pred->get_name() << "#" << idx;
|
||||
symbol nm(_name.str().c_str());
|
||||
expr_ref var(mk_index_var(), m);
|
||||
if (!is_current) {
|
||||
var = m_bv.mk_bv_sub(var, mk_q_one());
|
||||
}
|
||||
return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), pred->get_domain(idx)), var), m);
|
||||
}
|
||||
|
||||
expr_ref bmc::mk_q_one() {
|
||||
return mk_q_num(1);
|
||||
}
|
||||
|
||||
expr_ref bmc::mk_q_num(unsigned i) {
|
||||
return expr_ref(m_bv.mk_numeral(i, m_bit_width), m);
|
||||
}
|
||||
|
||||
func_decl_ref bmc::mk_q_func_decl(func_decl* f) {
|
||||
std::stringstream _name;
|
||||
_name << f->get_name() << "#";
|
||||
symbol nm(_name.str().c_str());
|
||||
return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m);
|
||||
}
|
||||
|
||||
func_decl_ref bmc::mk_q_rule(func_decl* f, unsigned rule_id) {
|
||||
std::stringstream _name;
|
||||
_name << f->get_name() << "#" << rule_id;
|
||||
symbol nm(_name.str().c_str());
|
||||
return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m);
|
||||
}
|
||||
|
||||
|
||||
expr_ref bmc::eval_q(model_ref& model, func_decl* f, unsigned i) {
|
||||
func_decl_ref fn = mk_q_func_decl(f);
|
||||
expr_ref t(m), result(m);
|
||||
t = m.mk_app(mk_q_func_decl(f), mk_q_num(i));
|
||||
model->eval(t, result);
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref bmc::eval_q(model_ref& model, expr* t, unsigned i) {
|
||||
expr_ref tmp(m), result(m), num(m);
|
||||
var_subst vs(m, false);
|
||||
num = mk_q_num(i);
|
||||
expr* nums[1] = { num };
|
||||
vs(t, 1, nums, tmp);
|
||||
model->eval(tmp, result);
|
||||
return result;
|
||||
}
|
||||
|
||||
lbool bmc::get_model_qlinear() {
|
||||
rule_manager& rm = m_ctx.get_rule_manager();
|
||||
func_decl_ref q = mk_q_func_decl(m_query_pred);
|
||||
expr_ref T(m), rule_i(m), vl(m);
|
||||
model_ref md;
|
||||
proof_ref pr(m);
|
||||
rule_unifier unifier(m_ctx);
|
||||
rational num;
|
||||
unsigned level, bv_size;
|
||||
|
||||
m_solver.get_model(md);
|
||||
func_decl* pred = m_query_pred;
|
||||
dl_decl_util util(m);
|
||||
T = m.mk_const(symbol("T"), mk_index_sort());
|
||||
md->eval(T, vl);
|
||||
VERIFY (m_bv.is_numeral(vl, num, bv_size));
|
||||
SASSERT(num.is_unsigned());
|
||||
level = num.get_unsigned();
|
||||
SASSERT(m.is_true(eval_q(md, m_query_pred, level)));
|
||||
TRACE("bmc", model_smt2_pp(tout, m, *md, 0););
|
||||
|
||||
rule_ref r0(rm), r1(rm), r2(rm);
|
||||
while (true) {
|
||||
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
|
||||
expr_ref_vector sub(m);
|
||||
rule_vector const& rls = m_rules.get_predicate_rules(pred);
|
||||
rule* r = 0;
|
||||
unsigned i = 0;
|
||||
for (; i < rls.size(); ++i) {
|
||||
rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level));
|
||||
TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
|
||||
if (m.is_true(eval_q(md, rule_i, level))) {
|
||||
r = rls[i];
|
||||
break;
|
||||
}
|
||||
}
|
||||
SASSERT(r);
|
||||
mk_qrule_vars(*r, i, sub);
|
||||
// we have rule, we have variable names of rule.
|
||||
|
||||
// extract values for the variables in the rule.
|
||||
for (unsigned j = 0; j < sub.size(); ++j) {
|
||||
expr_ref vl = eval_q(md, sub[j].get(), i);
|
||||
if (vl) {
|
||||
// vl can be 0 if the interpretation does not assign a value to it.
|
||||
sub[j] = vl;
|
||||
}
|
||||
else {
|
||||
sub[j] = m.mk_var(j, m.get_sort(sub[j].get()));
|
||||
}
|
||||
}
|
||||
svector<std::pair<unsigned, unsigned> > positions;
|
||||
vector<expr_ref_vector> substs;
|
||||
expr_ref fml(m), concl(m);
|
||||
|
||||
r->to_formula(fml);
|
||||
r2 = r;
|
||||
rm.substitute(r2, sub.size(), sub.c_ptr());
|
||||
if (r0) {
|
||||
VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
|
||||
expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
|
||||
expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false);
|
||||
apply_subst(sub, sub2);
|
||||
unifier.apply(*r0.get(), 0, *r2.get(), r1);
|
||||
r1->to_formula(concl);
|
||||
scoped_coarse_proof _sp(m);
|
||||
|
||||
proof* p = m.mk_asserted(fml);
|
||||
proof* premises[2] = { pr, p };
|
||||
|
||||
positions.push_back(std::make_pair(0, 1));
|
||||
|
||||
substs.push_back(sub1);
|
||||
substs.push_back(sub);
|
||||
pr = m.mk_hyper_resolve(2, premises, concl, positions, substs);
|
||||
r0 = r1;
|
||||
}
|
||||
else {
|
||||
r2->to_formula(concl);
|
||||
scoped_coarse_proof _sp(m);
|
||||
proof* p = m.mk_asserted(fml);
|
||||
if (sub.empty()) {
|
||||
pr = p;
|
||||
}
|
||||
else {
|
||||
substs.push_back(sub);
|
||||
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
|
||||
}
|
||||
r0 = r2;
|
||||
}
|
||||
|
||||
if (level == 0) {
|
||||
SASSERT(r->get_uninterpreted_tail_size() == 0);
|
||||
break;
|
||||
}
|
||||
--level;
|
||||
SASSERT(r->get_uninterpreted_tail_size() == 1);
|
||||
pred = r->get_decl(0);
|
||||
}
|
||||
scoped_coarse_proof _sp(m);
|
||||
apply(m, m_pc.get(), pr);
|
||||
m_answer = pr;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
// --------------------------------------------------------------------------
|
||||
// Basic non-linear BMC based on compiling into data-types (it is inefficient)
|
||||
|
||||
|
||||
lbool bmc::check_nonlinear() {
|
||||
m_fparams.m_relevancy_lvl = 2;
|
||||
setup_nonlinear();
|
||||
declare_datatypes();
|
||||
compile_nonlinear();
|
||||
return check_query();
|
||||
}
|
||||
|
||||
void bmc::setup_nonlinear() {
|
||||
setup_linear();
|
||||
m_fparams.m_relevancy_lvl = 2;
|
||||
}
|
||||
|
||||
func_decl_ref bmc::mk_predicate(func_decl* pred) {
|
||||
std::stringstream _name;
|
||||
_name << pred->get_name() << "#";
|
||||
|
|
@ -597,7 +920,7 @@ namespace datalog {
|
|||
m_pinned.push_back(new_sorts[i].get());
|
||||
}
|
||||
if (new_sorts.size() > 0) {
|
||||
TRACE("dl", dtu.display_datatype(new_sorts[0].get(), tout););
|
||||
TRACE("bmc", dtu.display_datatype(new_sorts[0].get(), tout););
|
||||
}
|
||||
del_datatype_decls(dts.size(), dts.c_ptr());
|
||||
|
||||
|
|
@ -700,10 +1023,11 @@ namespace datalog {
|
|||
lbool bmc::check_query() {
|
||||
sort* trace_sort = m_pred2sort.find(m_query_pred);
|
||||
func_decl_ref q = mk_predicate(m_query_pred);
|
||||
expr_ref trace(m), path(m);
|
||||
expr_ref trace(m), path(m), fml(m);
|
||||
trace = m.mk_const(symbol("trace"), trace_sort);
|
||||
path = m.mk_const(symbol("path"), m_path_sort);
|
||||
assert_expr(m.mk_app(q, trace.get(), path.get()));
|
||||
fml = m.mk_app(q, trace.get(), path.get());
|
||||
assert_expr(fml);
|
||||
while (true) {
|
||||
lbool is_sat = m_solver.check();
|
||||
model_ref md;
|
||||
|
|
@ -729,7 +1053,8 @@ namespace datalog {
|
|||
m_solver.pop(1);
|
||||
if (is_sat == l_false) {
|
||||
IF_VERBOSE(1, verbose_stream() << "infeasible trace " << mk_pp(trace_val, m) << "\n";);
|
||||
m_solver.assert_expr(m.mk_not(eq));
|
||||
eq = m.mk_not(eq);
|
||||
m_solver.assert_expr(eq);
|
||||
}
|
||||
return is_sat != l_false;
|
||||
}
|
||||
|
|
@ -771,6 +1096,9 @@ namespace datalog {
|
|||
m_solver.collect_statistics(st);
|
||||
}
|
||||
|
||||
void bmc::collect_params(param_descrs& p) {
|
||||
}
|
||||
|
||||
expr_ref bmc::get_answer() {
|
||||
return m_answer;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "params.h"
|
||||
#include "statistics.h"
|
||||
#include "smt_solver.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
|
@ -44,6 +45,8 @@ namespace datalog {
|
|||
volatile bool m_cancel;
|
||||
proof_converter_ref m_pc;
|
||||
sort_ref m_path_sort;
|
||||
bv_util m_bv;
|
||||
unsigned m_bit_width;
|
||||
|
||||
lbool check_query();
|
||||
|
||||
|
|
@ -66,9 +69,8 @@ namespace datalog {
|
|||
bool is_linear() const;
|
||||
|
||||
lbool check_nonlinear();
|
||||
|
||||
void setup_nonlinear();
|
||||
bool check_model_nonlinear(model_ref& md, expr* trace);
|
||||
|
||||
void mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path);
|
||||
|
||||
func_decl_ref mk_predicate(func_decl* p);
|
||||
|
|
@ -77,31 +79,39 @@ namespace datalog {
|
|||
|
||||
// linear check
|
||||
lbool check_linear();
|
||||
|
||||
lbool check_linear(unsigned level);
|
||||
|
||||
void compile_linear();
|
||||
|
||||
void compile_linear(unsigned level);
|
||||
|
||||
void compile_linear(rule& r, unsigned level);
|
||||
|
||||
expr_ref mk_level_predicate(symbol const& name, unsigned level);
|
||||
|
||||
expr_ref mk_level_predicate(func_decl* p, unsigned level);
|
||||
|
||||
expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level);
|
||||
|
||||
expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level);
|
||||
|
||||
expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
|
||||
|
||||
expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
|
||||
void get_model_linear(unsigned level);
|
||||
void setup_linear();
|
||||
|
||||
void assert_expr(expr* e);
|
||||
|
||||
void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub);
|
||||
|
||||
// quantified linear check
|
||||
void compile_qlinear();
|
||||
void setup_qlinear();
|
||||
lbool check_qlinear();
|
||||
lbool get_model_qlinear();
|
||||
sort_ref mk_index_sort();
|
||||
var_ref mk_index_var();
|
||||
void mk_qrule_vars(datalog::rule const& r, unsigned i, expr_ref_vector& sub);
|
||||
expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx);
|
||||
expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current);
|
||||
expr_ref mk_q_one();
|
||||
expr_ref mk_q_num(unsigned i);
|
||||
expr_ref eval_q(model_ref& model, expr* t, unsigned i);
|
||||
expr_ref eval_q(model_ref& model, func_decl* f, unsigned i);
|
||||
func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id);
|
||||
func_decl_ref mk_q_func_decl(func_decl* f);
|
||||
|
||||
public:
|
||||
bmc(context& ctx);
|
||||
|
||||
|
|
@ -119,7 +129,7 @@ namespace datalog {
|
|||
|
||||
expr_ref get_answer();
|
||||
|
||||
|
||||
static void collect_params(param_descrs& p);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -589,6 +589,7 @@ namespace datalog {
|
|||
ensure_pdr();
|
||||
return m_pdr->get_num_levels(pred);
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
throw default_exception("get_num_levels is unsupported for bmc");
|
||||
default:
|
||||
throw default_exception("unknown engine");
|
||||
|
|
@ -604,6 +605,7 @@ namespace datalog {
|
|||
ensure_pdr();
|
||||
return m_pdr->get_cover_delta(level, pred);
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
throw default_exception("operation is unsupported for BMC engine");
|
||||
default:
|
||||
throw default_exception("unknown engine");
|
||||
|
|
@ -620,6 +622,7 @@ namespace datalog {
|
|||
m_pdr->add_cover(level, pred, property);
|
||||
break;
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
throw default_exception("operation is unsupported for BMC engine");
|
||||
default:
|
||||
throw default_exception("unknown engine");
|
||||
|
|
@ -751,6 +754,7 @@ namespace datalog {
|
|||
check_positive_predicates(r);
|
||||
break;
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
check_existential_tail(r);
|
||||
check_positive_predicates(r);
|
||||
break;
|
||||
|
|
@ -969,12 +973,14 @@ namespace datalog {
|
|||
PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion"););
|
||||
|
||||
pdr::dl_interface::collect_params(p);
|
||||
bmc::collect_params(p);
|
||||
insert_timeout(p);
|
||||
}
|
||||
|
||||
void context::updt_params(params_ref const& p) {
|
||||
m_params.copy(p);
|
||||
if (m_pdr.get()) m_pdr->updt_params();
|
||||
|
||||
}
|
||||
|
||||
void context::collect_predicates(decl_set & res) {
|
||||
|
|
@ -1109,11 +1115,13 @@ namespace datalog {
|
|||
void context::cancel() {
|
||||
m_cancel = true;
|
||||
if (m_pdr.get()) m_pdr->cancel();
|
||||
if (m_bmc.get()) m_bmc->cancel();
|
||||
}
|
||||
|
||||
void context::cleanup() {
|
||||
m_cancel = false;
|
||||
if (m_pdr.get()) m_pdr->cleanup();
|
||||
if (m_bmc.get()) m_bmc->cleanup();
|
||||
}
|
||||
|
||||
class context::engine_type_proc {
|
||||
|
|
@ -1157,6 +1165,9 @@ namespace datalog {
|
|||
else if (e == symbol("bmc")) {
|
||||
m_engine = BMC_ENGINE;
|
||||
}
|
||||
else if (e == symbol("qbmc")) {
|
||||
m_engine = QBMC_ENGINE;
|
||||
}
|
||||
|
||||
if (m_engine == LAST_ENGINE) {
|
||||
expr_fast_mark1 mark;
|
||||
|
|
@ -1190,6 +1201,7 @@ namespace datalog {
|
|||
case QPDR_ENGINE:
|
||||
return pdr_query(query);
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
return bmc_query(query);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
|
@ -1450,6 +1462,7 @@ namespace datalog {
|
|||
m_last_answer = m_pdr->get_answer();
|
||||
return m_last_answer.get();
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
ensure_bmc();
|
||||
m_last_answer = m_bmc->get_answer();
|
||||
return m_last_answer.get();
|
||||
|
|
@ -1471,6 +1484,7 @@ namespace datalog {
|
|||
m_pdr->display_certificate(out);
|
||||
return true;
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
m_bmc->display_certificate(out);
|
||||
return true;
|
||||
default:
|
||||
|
|
@ -1490,6 +1504,7 @@ namespace datalog {
|
|||
m_pdr->collect_statistics(st);
|
||||
break;
|
||||
case BMC_ENGINE:
|
||||
case QBMC_ENGINE:
|
||||
m_bmc->collect_statistics(st);
|
||||
break;
|
||||
default:
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ namespace datalog {
|
|||
PDR_ENGINE,
|
||||
QPDR_ENGINE,
|
||||
BMC_ENGINE,
|
||||
QBMC_ENGINE,
|
||||
LAST_ENGINE
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -278,7 +278,10 @@ namespace pdr {
|
|||
if (is_infty_level(src_level)) {
|
||||
verbose_stream() << "infty";
|
||||
}
|
||||
else verbose_stream() << src_level;
|
||||
else {
|
||||
verbose_stream() << src_level;
|
||||
}
|
||||
verbose_stream() << "\n";
|
||||
for (unsigned i = 0; i < src.size(); ++i) {
|
||||
verbose_stream() << mk_pp(src[i].get(), m) << "\n";
|
||||
});
|
||||
|
|
@ -831,7 +834,11 @@ namespace pdr {
|
|||
|
||||
void model_search::set_leaf(model_node& n) {
|
||||
erase_children(n);
|
||||
SASSERT(n.is_open());
|
||||
SASSERT(n.is_open());
|
||||
enqueue_leaf(n);
|
||||
}
|
||||
|
||||
void model_search::enqueue_leaf(model_node& n) {
|
||||
if (m_bfs) {
|
||||
m_leaves.push_front(&n);
|
||||
}
|
||||
|
|
@ -1047,7 +1054,7 @@ namespace pdr {
|
|||
if (uses_level && m_root->level() > n.level()) {
|
||||
IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";);
|
||||
n.increase_level();
|
||||
m_leaves.push_back(&n);
|
||||
enqueue_leaf(n);
|
||||
}
|
||||
else {
|
||||
model_node* p = n.parent();
|
||||
|
|
@ -1076,8 +1083,7 @@ namespace pdr {
|
|||
m_search(m_params.get_bool(":bfs-model-search", true)),
|
||||
m_last_result(l_undef),
|
||||
m_inductive_lvl(0),
|
||||
m_cancel(false),
|
||||
m_is_dl(false)
|
||||
m_cancel(false)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -1296,7 +1302,6 @@ namespace pdr {
|
|||
void context::init_core_generalizers(datalog::rule_set& rules) {
|
||||
reset_core_generalizers();
|
||||
classifier_proc classify(m, rules);
|
||||
m_is_dl = false;
|
||||
bool use_mc = m_params.get_bool(":use-multicore-generalizer", false);
|
||||
if (use_mc) {
|
||||
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
|
||||
|
|
@ -1312,7 +1317,6 @@ namespace pdr {
|
|||
if (classify.is_dl()) {
|
||||
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
|
||||
m_fparams.m_arith_expand_eqs = true;
|
||||
m_is_dl = true;
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
@ -1654,7 +1658,6 @@ namespace pdr {
|
|||
void context::create_children(model_node& n) {
|
||||
SASSERT(n.level() > 0);
|
||||
bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
|
||||
// use_model_generalizer = use_model_generalizer || is_dl();
|
||||
|
||||
pred_transformer& pt = n.pt();
|
||||
model_ref M = n.model_ptr();
|
||||
|
|
@ -1693,12 +1696,14 @@ namespace pdr {
|
|||
pt.get_aux_vars(r, aux_vars);
|
||||
vars.append(aux_vars.size(), aux_vars.c_ptr());
|
||||
|
||||
scoped_ptr<expr_replacer> rep;
|
||||
qe_lite qe(m);
|
||||
expr_ref phi1 = m_pm.mk_and(Phi);
|
||||
qe(vars, phi1);
|
||||
if (!use_model_generalizer) {
|
||||
reduce_disequalities(*M, 3, phi1);
|
||||
}
|
||||
get_context().get_rewriter()(phi1);
|
||||
|
||||
IF_VERBOSE(2,
|
||||
verbose_stream() << "Vars:\n";
|
||||
|
|
@ -1720,7 +1725,7 @@ namespace pdr {
|
|||
M->eval(vars[i]->get_decl(), tmp);
|
||||
sub.insert(vars[i].get(), tmp, pr);
|
||||
}
|
||||
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
|
||||
if (!rep) rep = mk_expr_simp_replacer(m);
|
||||
rep->set_substitution(&sub);
|
||||
(*rep)(phi1);
|
||||
IF_VERBOSE(2, verbose_stream() << "Projected:\n" << mk_pp(phi1, m) << "\n";);
|
||||
|
|
@ -1733,7 +1738,7 @@ namespace pdr {
|
|||
for (unsigned i = 0; i < Phi.size(); ++i) {
|
||||
m_pm.collect_indices(Phi[i].get(), indices);
|
||||
if (indices.size() == 0) {
|
||||
IF_VERBOSE(2, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";);
|
||||
}
|
||||
else if (indices.size() == 1) {
|
||||
child_states[indices.back()].push_back(Phi[i].get());
|
||||
|
|
@ -1755,11 +1760,12 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
tmp = Phi[i].get();
|
||||
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
|
||||
if (!rep) rep = mk_expr_simp_replacer(m);
|
||||
rep->set_substitution(&sub);
|
||||
(*rep)(tmp);
|
||||
child_states[indices[0]].push_back(tmp);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
expr_ref n_cube(m);
|
||||
|
|
@ -1774,8 +1780,6 @@ namespace pdr {
|
|||
IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
|
||||
}
|
||||
check_pre_closed(n);
|
||||
|
||||
|
||||
TRACE("pdr", m_search.display(tout););
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -231,31 +231,22 @@ namespace pdr {
|
|||
void erase_children(model_node& n);
|
||||
void erase_leaf(model_node& n);
|
||||
void remove_node(model_node& n);
|
||||
void enqueue_leaf(model_node& n); // add leaf to priority queue.
|
||||
public:
|
||||
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
|
||||
|
||||
~model_search();
|
||||
|
||||
void reset();
|
||||
|
||||
model_node* next();
|
||||
|
||||
bool is_repeated(model_node& n) const;
|
||||
|
||||
void add_leaf(model_node& n); // add fresh node.
|
||||
|
||||
void set_leaf(model_node& n); // Set node as leaf, remove children.
|
||||
|
||||
void set_root(model_node* n);
|
||||
|
||||
model_node& get_root() const { return *m_root; }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
expr_ref get_trace() const;
|
||||
|
||||
proof_ref get_proof_trace(context const& ctx) const;
|
||||
|
||||
void backtrack_level(bool uses_level, model_node& n);
|
||||
};
|
||||
|
||||
|
|
@ -308,7 +299,6 @@ namespace pdr {
|
|||
volatile bool m_cancel;
|
||||
model_converter_ref m_mc;
|
||||
proof_converter_ref m_pc;
|
||||
bool m_is_dl;
|
||||
|
||||
// Functions used by search.
|
||||
void solve_impl();
|
||||
|
|
@ -366,7 +356,7 @@ namespace pdr {
|
|||
datalog::context& get_context() const { SASSERT(m_context); return *m_context; }
|
||||
expr_ref get_answer();
|
||||
|
||||
bool is_dl() const { return m_is_dl; }
|
||||
bool is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; }
|
||||
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
|
|
|||
Loading…
Reference in a new issue