mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'working' of https://z3-1/gw/git/z3 into working

Browse source
This commit is contained in:
unknown 2012-10-10 20:42:36 -07:00
commit 703c0d4f78
56 changed files with 1369 additions and 439 deletions
Download patch file Download diff file Expand all files Collapse all files

2
lib/api_ast.cpp
View file

@ -964,7 +964,7 @@ extern "C" {
case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;

84
lib/ast.cpp
View file

@ -646,7 +646,8 @@ basic_decl_plugin::basic_decl_plugin():
m_def_intro_decl(0),
m_iff_oeq_decl(0),
m_skolemize_decl(0),
m_mp_oeq_decl(0) {
m_mp_oeq_decl(0),
m_hyper_res_decl0(0) {
}
bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const {
@ -751,6 +752,9 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_param
SASSERT(num_parents == 0);
return mk_proof_decl("quant-inst", k, num_parameters, params, num_parents);
}
case PR_HYPER_RESOLVE: {
return mk_proof_decl("hyper-res", k, num_parameters, params, num_parents);
}
default:
UNREACHABLE();
return 0;
@ -813,6 +817,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl);
case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
case PR_HYPER_RESOLVE: return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0);
default:
UNREACHABLE();
return 0;
@ -934,6 +939,7 @@ void basic_decl_plugin::finalize() {
DEC_ARRAY_REF(m_cnf_star_decls);
DEC_ARRAY_REF(m_th_lemma_decls);
DEC_REF(m_hyper_res_decl0);
}
@ -2830,6 +2836,82 @@ proof * ast_manager::mk_th_lemma(
return mk_app(m_basic_family_id, PR_TH_LEMMA, num_params+1, parameters.c_ptr(), args.size(), args.c_ptr());
}
proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
svector<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_vector> const& substs) {
ptr_vector<expr> fmls;
SASSERT(positions.size() + 1 == substs.size());
for (unsigned i = 0; i < num_premises; ++i) {
TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";);
fmls.push_back(get_fact(premises[i]));
}
SASSERT(is_bool(concl));
vector<parameter> params;
for (unsigned i = 0; i < substs.size(); ++i) {
expr_ref_vector const& vec = substs[i];
for (unsigned j = 0; j < vec.size(); ++j) {
params.push_back(parameter(vec[j]));
}
if (i + 1 < substs.size()) {
params.push_back(parameter(positions[i].first));
params.push_back(parameter(positions[i].second));
}
}
ptr_vector<sort> sorts;
ptr_vector<expr> args;
for (unsigned i = 0; i < num_premises; ++i) {
sorts.push_back(mk_proof_sort());
args.push_back(premises[i]);
}
sorts.push_back(mk_bool_sort());
args.push_back(concl);
app* result = mk_app(m_basic_family_id, PR_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr());
SASSERT(result->get_family_id() == m_basic_family_id);
SASSERT(result->get_decl_kind() == PR_HYPER_RESOLVE);
return result;
}
bool ast_manager::is_hyper_resolve(
proof* p,
proof_ref_vector& premises,
expr_ref& conclusion,
svector<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_vector> & substs) {
if (!is_hyper_resolve(p)) {
return false;
}
unsigned sz = p->get_num_args();
SASSERT(sz > 0);
for (unsigned i = 0; i + 1 < sz; ++i) {
premises.push_back(to_app(p->get_arg(i)));
}
conclusion = p->get_arg(sz-1);
func_decl* d = p->get_decl();
unsigned num_p = d->get_num_parameters();
parameter const* params = d->get_parameters();
substs.push_back(expr_ref_vector(*this));
for (unsigned i = 0; i < num_p; ++i) {
if (params[i].is_int()) {
SASSERT(i + 1 < num_p);
SASSERT(params[i+1].is_int());
unsigned x = static_cast<unsigned>(params[i].get_int());
unsigned y = static_cast<unsigned>(params[i+1].get_int());
positions.push_back(std::make_pair(x, y));
substs.push_back(expr_ref_vector(*this));
++i;
}
else {
SASSERT(params[i].is_ast());
ast* a = params[i].get_ast();
SASSERT(is_expr(a));
substs.back().push_back(to_expr(a));
}
}
return true;
}
// -----------------------------------
//

14
lib/ast.h
View file

@ -972,7 +972,7 @@ enum basic_op_kind {
PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, LAST_BASIC_PR
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
};
class basic_decl_plugin : public decl_plugin {
@ -1034,6 +1034,7 @@ protected:
ptr_vector<func_decl> m_cnf_star_decls;
ptr_vector<func_decl> m_th_lemma_decls;
func_decl * m_hyper_res_decl0;
static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; }
bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const;
@ -1928,6 +1929,11 @@ public:
bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; }
proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
svector<std::pair<unsigned, unsigned> > const& positions,
vector<ref_vector<expr, ast_manager> > const& substs);
bool is_undef_proof(expr const * e) const { return e == m_undef_proof; }
bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); }
bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); }
@ -1947,6 +1953,12 @@ public:
bool is_lemma(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_LEMMA); }
bool is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<expr>& binding) const;
bool is_rewrite(expr const* e, expr*& r1, expr*& r2) const;
bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_basic_family_id, PR_HYPER_RESOLVE); }
bool is_hyper_resolve(proof* p,
ref_vector<proof, ast_manager>& premises,
obj_ref<expr, ast_manager>& conclusion,
svector<std::pair<unsigned, unsigned> > & positions,
vector<ref_vector<expr, ast_manager> >& substs);
bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); }

47
lib/dl_bmc_engine.cpp
View file

@ -97,9 +97,9 @@ namespace datalog {
return check_linear();
}
else {
check_nonlinear();
IF_VERBOSE(1, verbose_stream() << "non-linear BMC is not supported\n";);
return l_undef;
return check_nonlinear();
}
}
@ -179,7 +179,7 @@ namespace datalog {
substs.push_back(sub1);
substs.push_back(sub);
pr = util.mk_hyper_resolve(2, premises, concl, positions, substs);
pr = m.mk_hyper_resolve(2, premises, concl, positions, substs);
r0 = r1;
}
else {
@ -191,7 +191,7 @@ namespace datalog {
}
else {
substs.push_back(sub);
pr = util.mk_hyper_resolve(1, &p, concl, positions, substs);
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
}
r0 = r2;
}
@ -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) {
@ -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,23 +525,22 @@ 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());
std::cout << mk_pp(fml, m) << "\n";
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_body);
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);
}
}
@ -640,14 +638,19 @@ namespace datalog {
lbool bmc::check_query() {
sort* trace_sort = m_pred2sort.find(m_query_pred);
func_decl_ref q = mk_predicate(m_query_pred);
assert_expr(m.mk_app(q, m.mk_const(symbol("trace"), trace_sort), m.mk_const(symbol("path"),m_path_sort)));
expr_ref trace(m), path(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, path));
lbool is_sat = m_solver.check();
if (is_sat == l_undef) {
model_ref md;
proof_ref pr(m);
m_solver.get_model(md);
IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
md->eval(trace, trace);
IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";);
IF_VERBOSE(2, m_solver.display(verbose_stream()););
}
return is_sat;
}

56
lib/dl_check_table.cpp
View file

@ -48,6 +48,7 @@ namespace datalog {
table_base const* check_table_plugin::tocheck(table_base const* r) { return r?(get(*r).m_tocheck):0; }
table_base * check_table_plugin::mk_empty(const table_signature & s) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
table_base* checker = m_checker.mk_empty(s);
table_base* tocheck = m_tocheck.mk_empty(s);
return alloc(check_table, *this, s, tocheck, checker);
@ -65,9 +66,11 @@ namespace datalog {
}
virtual table_base* operator()(const table_base & t1, const table_base & t2) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2));
table_base* tchecker = (*m_checker)(checker(t1), checker(t2));
return alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
return result;
}
};
@ -89,9 +92,10 @@ namespace datalog {
}
virtual void operator()(table_base& tgt, const table_base& src, table_base* delta) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
(*m_tocheck)(tocheck(tgt), tocheck(src), tocheck(delta));
(*m_checker)(checker(tgt), checker(src), checker(delta));
SASSERT(get(tgt).well_formed());
get(tgt).well_formed();
}
};
@ -113,9 +117,11 @@ namespace datalog {
}
table_base* operator()(table_base const& src) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
table_base* tchecker = (*m_checker)(checker(src));
table_base* ttocheck = (*m_tocheck)(tocheck(src));
return alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker);
return result;
}
};
@ -136,9 +142,11 @@ namespace datalog {
}
table_base* operator()(table_base const& src) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
table_base* tchecker = (*m_checker)(checker(src));
table_base* ttocheck = (*m_tocheck)(tocheck(src));
return alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker);
return result;
}
};
@ -162,7 +170,7 @@ namespace datalog {
void operator()(table_base & t) {
(*m_checker)(checker(t));
(*m_tocheck)(tocheck(t));
SASSERT(get(t).well_formed());
get(t).well_formed();
}
};
@ -187,7 +195,7 @@ namespace datalog {
virtual void operator()(table_base& src) {
(*m_checker)(checker(src));
(*m_tocheck)(tocheck(src));
SASSERT(get(src).well_formed());
get(src).well_formed();
}
};
@ -211,7 +219,7 @@ namespace datalog {
virtual void operator()(table_base& src) {
(*m_checker)(checker(src));
(*m_tocheck)(tocheck(src));
SASSERT(get(src).well_formed());
get(src).well_formed();
}
};
@ -236,9 +244,10 @@ namespace datalog {
}
virtual void operator()(table_base& src, table_base const& negated_obj) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
(*m_checker)(checker(src), checker(negated_obj));
(*m_tocheck)(tocheck(src), tocheck(negated_obj));
SASSERT(get(src).well_formed());
get(src).well_formed();
}
};
@ -258,14 +267,14 @@ namespace datalog {
check_table::check_table(check_table_plugin & p, const table_signature & sig):
table_base(p, sig) {
SASSERT(well_formed());
(well_formed());
}
check_table::check_table(check_table_plugin & p, const table_signature & sig, table_base* tocheck, table_base* checker):
table_base(p, sig),
m_checker(checker),
m_tocheck(tocheck) {
SASSERT(well_formed());
well_formed();
}
check_table::~check_table() {
@ -274,6 +283,10 @@ namespace datalog {
}
bool check_table::well_formed() const {
get_plugin().m_count++;
if (get_plugin().m_count == 497) {
std::cout << "here\n";
}
iterator it = m_tocheck->begin(), end = m_tocheck->end();
for (; it != end; ++it) {
table_fact fact;
@ -281,7 +294,9 @@ namespace datalog {
if (!m_checker->contains_fact(fact)) {
m_tocheck->display(verbose_stream());
m_checker->display(verbose_stream());
verbose_stream() << get_plugin().m_count << "\n";
UNREACHABLE();
fatal_error(0);
return false;
}
}
@ -292,7 +307,9 @@ namespace datalog {
if (!m_tocheck->contains_fact(fact)) {
m_tocheck->display(verbose_stream());
m_checker->display(verbose_stream());
verbose_stream() << get_plugin().m_count << "\n";
UNREACHABLE();
fatal_error(0);
return false;
}
}
@ -300,20 +317,28 @@ namespace datalog {
}
bool check_table::empty() const {
if (m_tocheck->empty() != m_checker->empty()) {
m_tocheck->display(verbose_stream());
m_checker->display(verbose_stream());
verbose_stream() << get_plugin().m_count << "\n";
fatal_error(0);
}
return m_tocheck->empty();
}
void check_table::add_fact(const table_fact & f) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
m_tocheck->add_fact(f);
m_checker->add_fact(f);
SASSERT(well_formed());
well_formed();
}
void check_table::remove_fact(const table_element* f) {
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
m_tocheck->remove_fact(f);
m_checker->remove_fact(f);
SASSERT(well_formed());
well_formed();
}
bool check_table::contains_fact(const table_fact & f) const {
@ -321,11 +346,14 @@ namespace datalog {
}
table_base * check_table::clone() const {
return alloc(check_table, get_plugin(), get_signature(), m_tocheck->clone(), m_checker->clone());
IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";);
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->clone(), m_checker->clone());
return result;
}
table_base * check_table::complement(func_decl* p) const {
return alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
return result;
}
};

3
lib/dl_check_table.h
View file

@ -32,6 +32,7 @@ namespace datalog {
friend class check_table;
table_plugin& m_checker;
table_plugin& m_tocheck;
unsigned m_count;
protected:
class join_fn;
class union_fn;
@ -47,7 +48,7 @@ namespace datalog {
check_table_plugin(relation_manager & manager, symbol const& checker, symbol const& tocheck)
: table_plugin(symbol("check"), manager),
m_checker(*manager.get_table_plugin(checker)),
m_tocheck(*manager.get_table_plugin(tocheck)) {}
m_tocheck(*manager.get_table_plugin(tocheck)), m_count(0) {}
virtual table_base * mk_empty(const table_signature & s);

34
lib/dl_context.cpp
View file

@ -54,6 +54,7 @@ Revision History:
#include"expr_functors.h"
#include"dl_mk_partial_equiv.h"
#include"dl_mk_bit_blast.h"
#include"datatype_decl_plugin.h"
namespace datalog {
@ -1118,10 +1119,11 @@ namespace datalog {
class context::engine_type_proc {
ast_manager& m;
arith_util a;
datatype_util dt;
DL_ENGINE m_engine;
public:
engine_type_proc(ast_manager& m): m(m), a(m), m_engine(DATALOG_ENGINE) {}
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
DL_ENGINE get_engine() const { return m_engine; }
void operator()(expr* e) {
@ -1134,6 +1136,9 @@ namespace datalog {
else if (is_var(e) && m.is_bool(e)) {
m_engine = PDR_ENGINE;
}
else if (dt.is_datatype(m.get_sort(e))) {
m_engine = PDR_ENGINE;
}
}
};
@ -1209,9 +1214,8 @@ namespace datalog {
lbool context::pdr_query(expr* query) {
ensure_pdr();
lbool result = m_pdr->query(query);
m_last_answer = m_pdr->get_answer();
return result;
m_last_answer = 0;
return m_pdr->query(query);
}
void context::ensure_bmc() {
@ -1222,9 +1226,8 @@ namespace datalog {
lbool context::bmc_query(expr* query) {
ensure_bmc();
lbool result = m_bmc->query(query);
m_last_answer = m_bmc->get_answer();
return result;
m_last_answer = 0;
return m_bmc->query(query);
}
#define BEGIN_QUERY() \
@ -1437,6 +1440,23 @@ namespace datalog {
}
expr* context::get_answer_as_formula() {
if (m_last_answer) {
return m_last_answer.get();
}
switch(get_engine()) {
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
m_last_answer = m_pdr->get_answer();
return m_last_answer.get();
case BMC_ENGINE:
ensure_bmc();
m_last_answer = m_bmc->get_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
m_last_answer = m.mk_false();
return m_last_answer.get();
}

86
lib/dl_decl_plugin.cpp
View file

@ -489,12 +489,6 @@ namespace datalog {
return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
}
func_decl * dl_decl_plugin::mk_hyper_res(unsigned num_params, parameter const* params, unsigned arity, sort *const* domain) {
ast_manager& m = *m_manager;
func_decl_info info(m_family_id, OP_DL_HYPER_RESOLVE, num_params, params);
return m_manager->mk_func_decl(m_hyper_resolve_sym, arity, domain, m_manager->mk_proof_sort(), info);
}
func_decl * dl_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
@ -606,10 +600,6 @@ namespace datalog {
result = mk_compare(OP_DL_LT, m_lt_sym, domain);
break;
case OP_DL_HYPER_RESOLVE:
result = mk_hyper_res(num_parameters, parameters, arity, domain);
break;
default:
m_manager->raise_exception("operator not recognized");
return 0;
@ -752,80 +742,4 @@ namespace datalog {
return m.mk_app(f, num_args, args);
}
proof* dl_decl_util::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
svector<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_vector> const& substs) {
ptr_vector<expr> fmls;
SASSERT(positions.size() + 1 == substs.size());
for (unsigned i = 0; i < num_premises; ++i) {
TRACE("dl", tout << mk_pp(premises[i], m) << "\n";);
fmls.push_back(m.get_fact(premises[i]));
}
SASSERT(m.is_bool(concl));
vector<parameter> params;
for (unsigned i = 0; i < substs.size(); ++i) {
expr_ref_vector const& vec = substs[i];
for (unsigned j = 0; j < vec.size(); ++j) {
params.push_back(parameter(vec[j]));
}
if (i + 1 < substs.size()) {
params.push_back(parameter(positions[i].first));
params.push_back(parameter(positions[i].second));
}
}
ptr_vector<sort> sorts;
ptr_vector<expr> args;
for (unsigned i = 0; i < num_premises; ++i) {
sorts.push_back(m.mk_proof_sort());
args.push_back(premises[i]);
}
sorts.push_back(m.mk_bool_sort());
args.push_back(concl);
app* result = m.mk_app(m_fid, OP_DL_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr());
SASSERT(result->get_family_id() == m_fid);
SASSERT(result->get_decl_kind() == OP_DL_HYPER_RESOLVE);
return result;
}
bool dl_decl_util::is_hyper_resolve(
proof* p,
proof_ref_vector& premises,
expr_ref& conclusion,
svector<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_vector> & substs) const {
if (!is_hyper_resolve(p)) {
return false;
}
unsigned sz = p->get_num_args();
SASSERT(sz > 0);
for (unsigned i = 0; i + 1 < sz; ++i) {
premises.push_back(to_app(p->get_arg(i)));
}
conclusion = p->get_arg(sz-1);
func_decl* d = p->get_decl();
unsigned num_p = d->get_num_parameters();
parameter const* params = d->get_parameters();
substs.push_back(expr_ref_vector(m));
for (unsigned i = 0; i < num_p; ++i) {
if (params[i].is_int()) {
SASSERT(i + 1 < num_p);
SASSERT(params[i+1].is_int());
unsigned x = static_cast<unsigned>(params[i].get_int());
unsigned y = static_cast<unsigned>(params[i+1].get_int());
positions.push_back(std::make_pair(x, y));
substs.push_back(expr_ref_vector(m));
++i;
}
else {
SASSERT(params[i].is_ast());
ast* a = params[i].get_ast();
SASSERT(is_expr(a));
substs.back().push_back(to_expr(a));
}
}
return true;
}
};

43
lib/dl_decl_plugin.h
View file

@ -48,7 +48,6 @@ namespace datalog {
OP_RA_CLONE,
OP_DL_CONSTANT,
OP_DL_LT,
OP_DL_HYPER_RESOLVE,
LAST_RA_OP
};
@ -211,48 +210,6 @@ namespace datalog {
family_id get_family_id() const { return m_fid; }
/**
\brief Hyper-resolution rule that works for Horn clauses (implication)
Somewhat related to unit resolution and resolution rule from SPC, but
a general sledgehammer rule.
The clause/implication from the first premise is the main clause.
One of the literals in each of the other premises is resolved with the main clause.
The facts in the premises are closed formulas. Substitutions required for unification
are passed in.
positions is a vector of pairs of positions in the main clause and the side clause.
For clauses that are disjunctions the positions are indexed from 0 starting with the first
literal.
We use the following (Prolog style) convention for Horn implications:
The head of a Horn implication is position 0,
the first conjunct in the body of an implication is position 1
the second conjunct in the body of an implication is position 2
For general implications where the head is a disjunction, the
first n positions correspond to the n disjuncts in the head.
The next m positions correspond to the m conjuncts in the body.
*/
proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
svector<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_vector> const& substs);
bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_fid, OP_DL_HYPER_RESOLVE); }
/**
\brief extract components of a hyper-resolution proof rule.
*/
bool is_hyper_resolve(proof* p,
proof_ref_vector& premises,
expr_ref& conclusion,
svector<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_vector>& substs) const;
};
};

2
lib/dl_mk_rule_inliner.cpp
View file

@ -735,7 +735,7 @@ namespace datalog {
}
m_subst.reset();
m_subst.reserve_vars(max_var+1);
m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), m_head_index.get_approx_num_regs()));
m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), 2+m_head_index.get_approx_num_regs()));
svector<bool> valid;
valid.reset();

4
lib/dl_mk_slice.cpp
View file

@ -181,7 +181,7 @@ namespace datalog {
proof_ref_vector premises0(m);
vector<expr_ref_vector> substs, substs0;
if (!util.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) {
if (!m.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) {
return false;
}
unsigned num_args = p->get_num_args();
@ -240,7 +240,7 @@ namespace datalog {
r1 = r3;
}
r1->to_formula(concl);
proof* new_p = util.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
m_pinned_exprs.push_back(new_p);
m_pinned_rules.push_back(r1.get());
m_sliceform2rule.insert(slice_concl, r1.get());

4
lib/dl_skip_table.cpp
View file

@ -215,7 +215,9 @@ namespace datalog {
col2 = m_cycle[0];
swap2(n, col1, col2);
}
return alloc(skip_table, s.get_plugin(), get_result_signature(), n);
skip_table* res = alloc(skip_table, s.get_plugin(), get_result_signature(), n);
TRACE("skip",res->display(tout););
return res;
}
};

8
lib/dl_util.cpp
View file

@ -605,6 +605,12 @@ namespace datalog {
body.push_back(r.get_tail(i));
}
}
TRACE("dl_dr",
tout << r.get_decl()->get_name() << "\n";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << "\n";
});
mc->insert(r.get_head(), body.size(), body.c_ptr());
}
}
@ -634,7 +640,7 @@ namespace datalog {
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";);
pr = util.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
pc->insert(pr);
}

28
lib/goal.cpp
View file

@ -284,6 +284,30 @@ void goal::display_with_dependencies(cmd_context & ctx, std::ostream & out) cons
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
}
void goal::display_with_dependencies(std::ostream & out) const {
ptr_vector<expr> deps;
out << "(goal";
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
out << "\n |-";
deps.reset();
m().linearize(dep(i), deps);
ptr_vector<expr>::iterator it = deps.begin();
ptr_vector<expr>::iterator end = deps.end();
for (; it != end; ++it) {
expr * d = *it;
if (is_uninterp_const(d)) {
out << " " << mk_ismt2_pp(d, m());
}
else {
out << " #" << d->get_id();
}
}
out << "\n " << mk_ismt2_pp(form(i), m(), 2);
}
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
}
void goal::display(cmd_context & ctx) const {
display(ctx, ctx.regular_stream());
}
@ -473,7 +497,7 @@ void goal::elim_redundancies() {
proof * prs[2] = { pr(get_idx(atom)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
expr_dependency * d = 0;
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_idx(atom)), dep(i));
push_back(m().mk_false(), p, d);
@ -490,7 +514,7 @@ void goal::elim_redundancies() {
proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
expr_dependency * d = 0;
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_not_idx(f)), dep(i));
push_back(m().mk_false(), p, d);

1
lib/goal.h
View file

@ -180,6 +180,7 @@ public:
void display_dimacs(std::ostream & out) const;
void display_with_dependencies(cmd_context & ctx, std::ostream & out) const;
void display_with_dependencies(cmd_context & ctx) const;
void display_with_dependencies(std::ostream & out) const;
bool sat_preserved() const {
return prec() == PRECISE || prec() == UNDER;

37
lib/horn_subsume_model_converter.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast_pp.h"
#include "model_smt2_pp.h"
#include "bool_rewriter.h"
#include "th_rewriter.h"
void horn_subsume_model_converter::insert(app* head, expr* body) {
func_decl_ref pred(m);
@ -174,19 +175,49 @@ bool horn_subsume_model_converter::mk_horn(
}
}
void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
//
// predicates that have not been assigned values
// in the Horn model are assumed false.
//
if (m.is_bool(n) &&
!m_md->has_interpretation(n->get_decl()) &&
(n->get_family_id() == null_family_id)) {
TRACE("dl_mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
if (n->get_decl()->get_arity() == 0) {
m_md->register_decl(n->get_decl(), m.mk_false());
}
else {
func_interp* fi = alloc(func_interp, m, n->get_decl()->get_arity());
fi->set_else(m.mk_false());
m_md->register_decl(n->get_decl(), fi);
}
}
}
void horn_subsume_model_converter::add_default_false_interpretation(expr* e, model_ref& md) {
add_default_proc proc(m, md);
for_each_expr(proc, e);
}
void horn_subsume_model_converter::operator()(model_ref& mr) {
TRACE("dl_mc", model_smt2_pp(tout, m, *mr, 0););
for (unsigned i = m_funcs.size(); i > 0; ) {
--i;
func_decl* h = m_funcs[i].get();
expr_ref body(m_bodies[i].get(), m);
unsigned arity = h->get_arity();
add_default_false_interpretation(body, mr);
TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
expr_ref tmp(body);
mr->eval(tmp, body);
TRACE("dl", tout << "eval: " << mk_pp(tmp, m) << "\nto:\n" << mk_pp(body, m) << "\n";);
TRACE("dl", model_smt2_pp(tout, m, *mr, 0););
th_rewriter rw(m);
rw(body);
TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
if (arity == 0) {
expr* e = mr->get_const_interp(h);
if (e) {

10
lib/horn_subsume_model_converter.h
View file

@ -42,6 +42,16 @@ class horn_subsume_model_converter : public model_converter {
func_decl_ref_vector m_funcs;
expr_ref_vector m_bodies;
void add_default_false_interpretation(expr* e, model_ref& md);
struct add_default_proc {
ast_manager& m;
model_ref& m_md;
add_default_proc(ast_manager& m, model_ref& md): m(m), m_md(md) {}
void operator()(app* n);
void operator()(expr* n) {}
};
public:
horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m) {}

93
lib/imdd.cpp
View file

@ -255,6 +255,7 @@ void imdd_manager::mark_as_dead(imdd * d) {
void imdd_manager::deallocate_imdd(imdd * d) {
SASSERT(d->is_dead());
memset(d, 0, sizeof(*d));
m_alloc.deallocate(sizeof(imdd), d);
}
@ -724,7 +725,7 @@ imdd * imdd_manager::mk_union_core(imdd * d1, imdd * d2, bool destructive, bool
if (head1 < head2) {
it1.move_to(head2);
head1 = it1 != end1 ? it1->begin_key() : UINT_MAX;
head1 = it1 != end1 ? (it1->begin_key() < head2?head2:it1->begin_key()): UINT_MAX;
}
else if (head1 > head2) {
copy_upto(head2, it2, end2, head1, to_insert);
@ -1635,7 +1636,8 @@ imdd* imdd_manager::filter_identical_loop3(imdd * d, unsigned v1, bool del1, uns
}
void imdd_manager::merge_intervals(svector<interval>& dst, svector<interval> const& src) {
svector<interval> tmp;
svector<interval>& tmp = m_i_nodes_tmp;
tmp.reset();
// invariant: intervals are sorted.
for (unsigned i = 0, j = 0; i < src.size() || j < dst.size();) {
SASSERT(!(i + 1 < src.size()) || src[i].m_hi < src[i+1].m_lo);
@ -1685,8 +1687,8 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
// For each level up to 'v' create a list of nodes visited
// insert to a map the set of intervals that visit the node.
//
filter_id_map nodes;
filter_id_map::obj_map_entry* e;
m_nodes.reset();
filter_id_map& nodes = m_nodes;
imdd* d1, *d2, *d3;
vector<ptr_vector<imdd> > levels;
levels.push_back(ptr_vector<imdd>());
@ -1696,24 +1698,23 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
imdd* curr_child;
for (; it != end; ++it) {
curr_child = it->val();
e = nodes.insert_if_not_there2(curr_child, svector<interval>());
if (e->get_data().m_value.empty()) {
svector<interval>& iv = nodes.init(curr_child);
if (iv.empty()) {
levels.back().push_back(curr_child);
}
e->get_data().m_value.push_back(interval(it->begin_key(), it->end_key()));
iv.push_back(interval(it->begin_key(), it->end_key()));
}
for (unsigned j = 0; j+1 < v; ++j) {
levels.push_back(ptr_vector<imdd>());
for (unsigned i = 0; i < levels[j].size(); ++i) {
d1 = levels[j][i];
svector<interval> i_nodes = nodes.find(d1);
svector<interval>& i_nodes = nodes.init(d1);
it = d1->begin_children();
end = d1->end_children();
for(; it != end; ++it) {
imdd* curr_child = it->val();
e = nodes.insert_if_not_there2(curr_child, svector<interval>());
svector<interval>& i_nodes2 = e->get_data().m_value;
svector<interval>& i_nodes2 = nodes.init(curr_child);
if (i_nodes2.empty()) {
levels[j+1].push_back(curr_child);
i_nodes2.append(i_nodes);
@ -1730,7 +1731,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
tout << "Level: " << i << "\n";
for (unsigned j = 0; j < levels[i].size(); ++j) {
tout << levels[i][j]->get_id() << " ";
svector<interval> const& i_nodes = nodes.find(levels[i][j]);
svector<interval> const& i_nodes = nodes.init(levels[i][j]);
for (unsigned k = 0; k < i_nodes.size(); ++k) {
tout << i_nodes[k].m_lo << ":" << i_nodes[k].m_hi << " ";
}
@ -1749,15 +1750,16 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
// => del1 & !del2: d |-> [I |-> d'[I:ch]] // intersections of intervals.
//
filter_idd_map nodes_dd;
m_nodes_dd.reset();
filter_idd_map& nodes_dd = m_nodes_dd;
SASSERT(levels.size() == v);
for (unsigned i = 0; i < levels[v-1].size(); ++i) {
d1 = levels[v-1][i];
svector<interval> const & i_nodes = nodes.find(d1);
svector<interval> const & i_nodes = nodes.init(d1);
it = d1->begin_children();
end = d1->end_children();
unsigned j = 0;
svector<interval_dd> i_nodes_dd;
svector<interval_dd>& i_nodes_dd = nodes_dd.init(d1);
while (it != end && j < i_nodes.size()) {
unsigned lo1 = it->begin_key();
unsigned hi1 = it->end_key();
@ -1816,7 +1818,6 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
i_nodes_dd[k].m_dd = d2;
}
}
nodes_dd.insert(d1, i_nodes_dd);
}
TRACE("imdd", print_filter_idd(tout, nodes_dd););
@ -1841,15 +1842,21 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
--i;
for (unsigned j = 0; j < levels[i].size(); ++j) {
d1 = levels[i][j];
svector<interval_dd> i_nodes_dd;
svector<interval> i_nodes = nodes.find(d1);
m_i_nodes_dd.reset();
svector<interval> i_nodes = nodes.init(d1);
svector<interval_dd>& i_nodes_dd = nodes_dd.init(d1);
it = d1->begin_children();
end = d1->end_children();
unsigned_vector offsets;
unsigned num_children = 0;
for( ; it != end; ++it, ++num_children);
m_offsets.reset();
unsigned_vector& offsets = m_offsets;
offsets.resize(num_children);
it = d1->begin_children();
for( ; it != end; ++it) {
curr_child = it->val();
refine_intervals(i_nodes, nodes_dd.find(curr_child));
offsets.push_back(0);
refine_intervals(i_nodes, nodes_dd.init(curr_child));
}
for (unsigned k = 0; k < i_nodes.size(); ++k) {
@ -1858,7 +1865,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
it = d1->begin_children();
for(unsigned child_id = 0; it != end; ++it, ++child_id) {
curr_child = it->val();
svector<interval_dd> const& ch_nodes_dd = nodes_dd.find(curr_child);
svector<interval_dd> const& ch_nodes_dd = nodes_dd.init(curr_child);
unsigned offset = offsets[child_id];
TRACE("imdd_verbose", tout << intv.m_lo << ":" << intv.m_hi << "\n";
for (unsigned l = offset; l < ch_nodes_dd.size(); ++l) {
@ -1899,7 +1906,7 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
}
}
TRACE("imdd", tout << d1->get_id() << ": "; print_interval_dd(tout, i_nodes_dd););
nodes_dd.insert(d1, i_nodes_dd);
}
}
@ -1919,11 +1926,14 @@ imdd* imdd_manager::filter_identical_mk_nodes(imdd* d, unsigned v, bool del1, bo
it = d->begin_children();
end = d->end_children();
d1 = _mk_empty(d->get_arity()-del1-del2);
svector<interval_dd> i_nodes_dd, i_nodes_tmp;
m_i_nodes_dd.reset();
m_i_nodes_tmp.reset();
svector<interval_dd>& i_nodes_dd = m_i_nodes_dd;
svector<interval_dd>& i_nodes_tmp = m_i_nodes_dd_tmp;
for (; it != end; ++it) {
curr_child = it->val();
i_nodes_tmp.reset();
svector<interval_dd> const& i_nodes_dd1 = nodes_dd.find(curr_child);
svector<interval_dd> const& i_nodes_dd1 = nodes_dd.init(curr_child);
for (unsigned i = 0, j = 0; i < i_nodes_dd.size() || j < i_nodes_dd1.size(); ) {
if (i < i_nodes_dd.size() && j < i_nodes_dd1.size()) {
interval_dd const& iv1 = i_nodes_dd[i];
@ -1986,9 +1996,9 @@ void imdd_manager::print_interval_dd(std::ostream& out, svector<interval_dd> con
void imdd_manager::print_filter_idd(std::ostream& out, filter_idd_map const& m) {
filter_idd_map::iterator it = m.begin(), end = m.end();
for (; it != end; ++it) {
out << it->m_key->get_id() << ": ";
print_interval_dd(out, it->m_value);
for (unsigned i = 0; it != end; ++it, ++i) {
out << i << ": ";
print_interval_dd(out, *it);
}
}
@ -1999,12 +2009,16 @@ void imdd_manager::print_filter_idd(std::ostream& out, filter_idd_map const& m)
*/
void imdd_manager::refine_intervals(svector<interval>& i_nodes, svector<interval_dd> const& i_nodes_dd) {
svector<interval> result;
for (unsigned i = 0, j = 0; i < i_nodes.size(); ++i) {
result.push_back(i_nodes[i]);
unsigned lo = result.back().m_lo;
unsigned hi = result.back().m_hi;
for (; j < i_nodes_dd.size(); ++j) {
m_i_nodes.reset();
svector<interval>& result = m_i_nodes;
unsigned sz1 = i_nodes.size();
unsigned sz2 = i_nodes_dd.size();
for (unsigned i = 0, j = 0; i < sz1; ++i) {
interval& iv = i_nodes[i];
result.push_back(iv);
unsigned lo = iv.m_lo;
unsigned hi = iv.m_hi;
for (; j < sz2; ++j) {
unsigned lo1 = i_nodes_dd[j].m_lo;
unsigned hi1 = i_nodes_dd[j].m_hi;
SASSERT(lo <= hi);
@ -2402,6 +2416,7 @@ void imdd_manager::mk_swap_acc1_dupdt(imdd_ref & d, unsigned lower, unsigned upp
if (lower <= upper) {
add_child(d, lower, upper, grandchild);
}
TRACE("mk_swap_bug", tout << "after mk_swap_acc1_dupt\n" << mk_ll_pp(d, *this) << "\n";);
}
void imdd_manager::mk_swap_acc1(imdd * d, imdd_ref & r, unsigned lower, unsigned upper, imdd * grandchild, bool memoize_res) {
@ -2437,6 +2452,7 @@ void imdd_manager::mk_swap_acc1(imdd * d, imdd_ref & r, unsigned lower, unsigned
if (lower <= upper) {
add_child(r, lower, upper, grandchild);
}
TRACE("mk_swap_bug", tout << "after mk_swap_acc1\n" << mk_ll_pp(r, *this) << "\n";);
}
/**
@ -2456,6 +2472,7 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
imdd_children::ext_iterator it;
imdd_children::ext_iterator end;
r->m_children.move_geq(it, lower1);
SASSERT(m_swap_new_child == 0);
while(it != end && lower1 <= upper1) {
imdd_children::entry const & curr_entry = *it;
@ -2463,6 +2480,7 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
unsigned curr_entry_end_key = curr_entry.end_key();
imdd * curr_entry_val = curr_entry.val();
bool move_head = true;
TRACE("mk_swap_bug", tout << lower1 << " " << upper1 << " " << curr_entry_begin_key << "\n";);
if (upper1 < curr_entry_begin_key)
break;
if (lower1 < curr_entry_begin_key) {
@ -2509,6 +2527,10 @@ void imdd_manager::mk_swap_acc2(imdd_ref & r, unsigned lower1, unsigned upper1,
imdd * new_child = mk_swap_new_child(lower2, upper2, grandchild);
add_child(r, lower1, upper1, new_child);
}
if (m_swap_new_child != 0) {
dec_ref(m_swap_new_child);
m_swap_new_child = 0;
}
TRACE("mk_swap_bug", tout << "after mk_swap_acc2\n" << mk_ll_pp(r, *this) << "\n";);
}
@ -2562,10 +2584,7 @@ void imdd_manager::mk_swap_top_vars(imdd * d, imdd_ref & r, bool memoize_res) {
imdd * grandchild = it2->val();
mk_swap_acc2(r, it2->begin_key(), it2->end_key(), it->begin_key(), it->end_key(), grandchild, memoize_res);
}
if (m_swap_new_child != 0) {
dec_ref(m_swap_new_child);
m_swap_new_child = 0;
}
SASSERT(m_swap_new_child == 0);
}
if (memoize_res && m_swap_granchildren_memoized) {

83
lib/imdd.h
View file

@ -394,8 +394,87 @@ class imdd_manager {
imdd* m_dd;
interval_dd(unsigned lo, unsigned hi, imdd* d): interval(lo, hi), m_dd(d) {}
};
typedef obj_map<imdd, svector<interval> > filter_id_map;
typedef obj_map<imdd, svector<interval_dd> > filter_idd_map;
template<typename I>
class id_map {
unsigned m_T;
unsigned_vector m_Ts;
svector<svector<I>*> m_vecs;
unsigned_vector m_alloc;
unsigned m_first_free;
void hard_reset() {
std::for_each(m_vecs.begin(), m_vecs.end(), delete_proc<svector<I> >());
m_alloc.reset();
m_first_free = 0;
m_vecs.reset();
m_Ts.reset();
m_T = 0;
}
void allocate_entry(unsigned id) {
if (m_vecs[id]) {
return;
}
while (m_first_free < m_alloc.size()) {
if (m_vecs[m_first_free] && m_Ts[m_first_free] < m_T) {
svector<I>* v = m_vecs[m_first_free];
m_vecs[m_first_free] = 0;
m_vecs[id] = v;
++m_first_free;
return;
}
++m_first_free;
}
m_vecs[id] = alloc(svector<I>);
m_alloc.push_back(id);
}
public:
id_map():m_T(0) {}
~id_map() { hard_reset(); }
void reset() { ++m_T; m_first_free = 0; if (m_T == UINT_MAX) hard_reset(); }
svector<I>& init(imdd* d) {
unsigned id = d->get_id();
if (id >= m_vecs.size()) {
m_vecs.resize(id+1);
m_Ts.resize(id+1);
}
if (m_Ts[id] < m_T) {
allocate_entry(id);
m_vecs[id]->reset();
m_Ts[id] = m_T;
}
return *m_vecs[id];
}
typedef svector<I> data;
struct iterator {
unsigned m_offset;
id_map const& m;
iterator(unsigned o, id_map const& m):m_offset(o),m(m) {}
data const & operator*() const { return *m.m_vecs[m_offset]; }
data const * operator->() const { return &(operator*()); }
data * operator->() { return &(operator*()); }
iterator & operator++() { ++m_offset; return move_to_used(); }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator==(iterator const & it) const { return m_offset == it.m_offset; }
bool operator!=(iterator const & it) const { return m_offset != it.m_offset; }
iterator & move_to_used() {
while (m_offset < m.m_vecs.size() &&
m.m_Ts[m_offset] < m.m_T) {
++m_offset;
}
return *this;
}
};
iterator begin() const { return iterator(0, *this).move_to_used(); }
iterator end() const { return iterator(m_vecs.size(), *this); }
};
typedef id_map<interval > filter_id_map;
typedef id_map<interval_dd > filter_idd_map;
filter_id_map m_nodes;
filter_idd_map m_nodes_dd;
svector<interval_dd> m_i_nodes_dd, m_i_nodes_dd_tmp;
svector<interval> m_i_nodes, m_i_nodes_tmp;
unsigned_vector m_offsets;
void filter_identical_main3(imdd * d, imdd_ref& r, unsigned num_vars, unsigned * vars, bool destructive, bool memoize_res);
void filter_identical_main3(imdd * d, imdd_ref& r, unsigned v1, bool del1, unsigned v2, bool del2, bool memoize_res);
imdd* filter_identical_loop3(imdd * d, unsigned v1, bool del1, unsigned v2, bool del2, bool memoize_res);

2
lib/pdr_context.cpp
View file

@ -1093,7 +1093,7 @@ namespace pdr {
}
expr_ref fml_concl(m);
reduced_rule->to_formula(fml_concl);
p1 = util.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
}
cache.insert(n->state(), p1);
rules.insert(n->state(), reduced_rule);

7
lib/pdr_farkas_learner.cpp
View file

@ -60,6 +60,11 @@ namespace pdr {
return a.mk_add(e1, e2);
}
app* mk_mul(expr* e1, expr* e2) {
mk_coerce(e1, e2);
return a.mk_mul(e1, e2);
}
app* mk_le(expr* e1, expr* e2) {
mk_coerce(e1, e2);
return a.mk_le(e1, e2);
@ -86,7 +91,7 @@ namespace pdr {
tmp = e;
}
else {
tmp = a.mk_mul(a.mk_numeral(c, a.is_int(e)), e);
tmp = mk_mul(a.mk_numeral(c, c.is_int() && a.is_int(e)), e);
}
res = mk_add(res, tmp);
}

4
lib/rewriter_def.h
View file

@ -37,9 +37,9 @@ void rewriter_tpl<Config>::process_var(var * v) {
unsigned idx = v->get_idx();
if (idx < m_bindings.size()) {
expr * r = m_bindings[m_bindings.size() - idx - 1];
TRACE("process_var", tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
TRACE("process_var", if (r) tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
tout << "bindings:\n";
for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
for (unsigned i = 0; i < m_bindings.size(); i++) if (m_bindings[i]) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
if (r != 0) {
if (m_num_qvars == 0 || is_ground(r)) {
result_stack().push_back(r);

1
lib/simplify_tactic.cpp
View file

@ -67,6 +67,7 @@ struct simplify_tactic::imp {
TRACE("after_simplifier_bug", g.display(tout););
g.elim_redundancies();
TRACE("after_simplifier", g.display(tout););
TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
SASSERT(g.is_well_sorted());
}

4
lib/theory_arith_core.h
View file

@ -479,8 +479,8 @@ namespace smt {
return;
}
expr* to_r = m_util.mk_to_real(n);
expr* lo = m_util.mk_le(to_r, x);
expr* hi = m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false)));
expr_ref lo(m_util.mk_le(to_r, x), m);
expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
mk_axiom(m.mk_false(), lo);
mk_axiom(m.mk_false(), hi);
}

44
lib/z3_api.h
View file

@ -761,6 +761,47 @@ typedef enum
- gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
- Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule.
The premises of the rules is a sequence of clauses.
The first clause argument is the main clause of the rule.
One literal from the second, third, .. clause is resolved
with a literal from the first (main) clause.
Premises of the rules are of the form
\nicebox{
(or l0 l1 l2 .. ln)
}
or
\nicebox{
(=> (and ln+1 ln+2 .. ln+m) l0)
}
or in the most general (ground) form:
\nicebox{
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
}
In other words we use the following (Prolog style) convention for Horn
implications:
The head of a Horn implication is position 0,
the first conjunct in the body of an implication is position 1
the second conjunct in the body of an implication is position 2
For general implications where the head is a disjunction, the
first n positions correspond to the n disjuncts in the head.
The next m positions correspond to the m conjuncts in the body.
The premises can be universally quantified so that the most
general non-ground form is:
\nicebox{
(forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)))
}
The hyper-resolution rule takes a sequence of parameters.
The parameters are substitutions of bound variables separated by pairs
of literal positions from the main clause and side clause.
- Z3_OP_RA_STORE: Insert a record into a relation.
The function takes \c n+1 arguments, where the first argument is the relation and the remaining \c n elements
correspond to the \c n columns of the relation.
@ -982,6 +1023,7 @@ typedef enum {
Z3_OP_PR_SKOLEMIZE,
Z3_OP_PR_MODUS_PONENS_OEQ,
Z3_OP_PR_TH_LEMMA,
Z3_OP_PR_HYPER_RESOLVE,
// Sequences
Z3_OP_RA_STORE = 0x600,
@ -5039,7 +5081,7 @@ END_MLAPI_EXCLUDE
/**
\brief Backtrack one backtracking point.
\sa Z3_fixedpoing_push
\sa Z3_fixedpoint_push
\pre The number of calls to pop cannot exceed calls to push.
*/