mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in PDR
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
780ad7cc17
commit
83add2bd9b
14 changed files with 176 additions and 34 deletions
|
|
@ -260,6 +260,7 @@ class smt_printer {
|
|||
else {
|
||||
m_out << sym << "[";
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < num_params; ++i) {
|
||||
parameter const& p = params[i];
|
||||
if (p.is_ast()) {
|
||||
|
|
@ -642,11 +643,9 @@ class smt_printer {
|
|||
m_out << m_var_names[m_num_var_names - idx - 1];
|
||||
}
|
||||
else {
|
||||
if (!m_is_smt2) {
|
||||
m_out << "?" << idx;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void pp_marked_expr(expr* n) {
|
||||
if (m_mark.is_marked(n)) {
|
||||
|
|
|
|||
|
|
@ -709,8 +709,7 @@ namespace datalog {
|
|||
|
||||
#define PRT(_x_) ((_x_)?"T":"F")
|
||||
|
||||
bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
|
||||
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
|
||||
bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
|
||||
bool done_something = false;
|
||||
unsigned sz = rules->get_num_rules();
|
||||
|
||||
|
|
@ -731,7 +730,7 @@ namespace datalog {
|
|||
svector<bool>& can_expand = m_head_visitor.can_expand();
|
||||
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
add_rule(source, acc[i].get(), i);
|
||||
add_rule(*rules, acc[i].get(), i);
|
||||
}
|
||||
|
||||
// initialize substitution.
|
||||
|
|
@ -808,7 +807,7 @@ namespace datalog {
|
|||
TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
|
||||
|
||||
del_rule(r, i);
|
||||
add_rule(source, rl_res.get(), i);
|
||||
add_rule(*rules, rl_res.get(), i);
|
||||
|
||||
|
||||
r = rl_res;
|
||||
|
|
@ -828,13 +827,15 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
if (done_something) {
|
||||
rules = alloc(rule_set, m_context);
|
||||
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (valid.get(i)) {
|
||||
rules->add_rule(acc[i].get());
|
||||
res->add_rule(acc[i].get());
|
||||
}
|
||||
}
|
||||
TRACE("dl", rules->display(tout););
|
||||
res->inherit_predicates(*rules);
|
||||
TRACE("dl", res->display(tout););
|
||||
rules = res.detach();
|
||||
}
|
||||
return done_something;
|
||||
}
|
||||
|
|
@ -874,8 +875,14 @@ namespace datalog {
|
|||
}
|
||||
TRACE("dl", res->display(tout << "after eager inlining\n"););
|
||||
}
|
||||
if (something_done) {
|
||||
res->inherit_predicates(source);
|
||||
}
|
||||
else {
|
||||
res = alloc(rule_set, source);
|
||||
}
|
||||
|
||||
if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
|
||||
if (m_context.get_params().inline_linear() && inline_linear(res)) {
|
||||
something_done = true;
|
||||
}
|
||||
|
||||
|
|
@ -883,7 +890,6 @@ namespace datalog {
|
|||
res = 0;
|
||||
}
|
||||
else {
|
||||
res->inherit_predicates(source);
|
||||
m_context.add_model_converter(hsmc.get());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -172,7 +172,7 @@ namespace datalog {
|
|||
/**
|
||||
Inline predicates that are known to not be join-points.
|
||||
*/
|
||||
bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
|
||||
bool inline_linear(scoped_ptr<rule_set>& rules);
|
||||
|
||||
void add_rule(rule_set const& rule_set, rule* r, unsigned i);
|
||||
void del_rule(rule* r, unsigned i);
|
||||
|
|
|
|||
|
|
@ -241,6 +241,7 @@ namespace datalog {
|
|||
tgt.add_rule(new_rule);
|
||||
subs_index.add(new_rule);
|
||||
}
|
||||
tgt.inherit_predicates(orig);
|
||||
TRACE("dl",
|
||||
tout << "original set size: "<<orig.get_num_rules()<<"\n"
|
||||
<< "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
|
||||
|
|
@ -338,7 +339,7 @@ namespace datalog {
|
|||
rule_set * res = alloc(rule_set, m_context);
|
||||
bool modified = transform_rules(source, *res);
|
||||
|
||||
if(!m_have_new_total_rule && !modified) {
|
||||
if (!m_have_new_total_rule && !modified) {
|
||||
dealloc(res);
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -347,7 +348,7 @@ namespace datalog {
|
|||
//During the construction of the new set we may discover new total relations
|
||||
//(by quantifier elimination on the uninterpreted tails).
|
||||
SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
|
||||
while(m_have_new_total_rule) {
|
||||
while (m_have_new_total_rule) {
|
||||
m_have_new_total_rule = false;
|
||||
|
||||
rule_set * old = res;
|
||||
|
|
@ -355,7 +356,6 @@ namespace datalog {
|
|||
transform_rules(*old, *res);
|
||||
dealloc(old);
|
||||
}
|
||||
res->inherit_predicates(source);
|
||||
|
||||
return res;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1004,16 +1004,14 @@ namespace datalog {
|
|||
}
|
||||
svector<symbol> names;
|
||||
used_symbols<> us;
|
||||
|
||||
us(fml);
|
||||
sorts.reverse();
|
||||
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
}
|
||||
|
||||
us(fml);
|
||||
sorts.reverse();
|
||||
for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
|
||||
for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
|
||||
func_decl_ref f(m);
|
||||
|
|
|
|||
|
|
@ -125,12 +125,13 @@ class horn_tactic : public tactic {
|
|||
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
|
||||
|
||||
formula_kind get_formula_kind(expr_ref& f) {
|
||||
normalize(f);
|
||||
expr_ref tmp(f);
|
||||
normalize(tmp);
|
||||
ast_mark mark;
|
||||
expr_ref_vector args(m), body(m);
|
||||
expr_ref head(m);
|
||||
expr* a = 0, *a1 = 0;
|
||||
datalog::flatten_or(f, args);
|
||||
datalog::flatten_or(tmp, args);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
a = args[i].get();
|
||||
check_predicate(mark, a);
|
||||
|
|
@ -147,12 +148,12 @@ class horn_tactic : public tactic {
|
|||
body.push_back(m.mk_not(a));
|
||||
}
|
||||
}
|
||||
f = m.mk_and(body.size(), body.c_ptr());
|
||||
if (head) {
|
||||
f = m.mk_implies(f, head);
|
||||
// f = m.mk_implies(f, head);
|
||||
return IS_RULE;
|
||||
}
|
||||
else {
|
||||
f = m.mk_and(body.size(), body.c_ptr());
|
||||
return IS_QUERY;
|
||||
}
|
||||
}
|
||||
|
|
@ -239,10 +240,13 @@ class horn_tactic : public tactic {
|
|||
switch (is_reachable) {
|
||||
case l_true: {
|
||||
// goal is unsat
|
||||
g->assert_expr(m.mk_false());
|
||||
if (produce_proofs) {
|
||||
proof_ref proof = m_ctx.get_proof();
|
||||
pc = proof2proof_converter(m, proof);
|
||||
g->assert_expr(m.mk_false(), proof, 0);
|
||||
}
|
||||
else {
|
||||
g->assert_expr(m.mk_false());
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -43,6 +43,7 @@ Notes:
|
|||
#include "ast_ll_pp.h"
|
||||
#include "proof_checker.h"
|
||||
#include "smt_value_sort.h"
|
||||
#include "proof_utils.h"
|
||||
|
||||
namespace pdr {
|
||||
|
||||
|
|
@ -1225,6 +1226,7 @@ namespace pdr {
|
|||
m_search(m_params.bfs_model_search()),
|
||||
m_last_result(l_undef),
|
||||
m_inductive_lvl(0),
|
||||
m_expanded_lvl(0),
|
||||
m_cancel(false)
|
||||
{
|
||||
}
|
||||
|
|
@ -1680,6 +1682,9 @@ namespace pdr {
|
|||
proof = m_search.get_proof_trace(*this);
|
||||
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
|
||||
apply(m, m_pc.get(), proof);
|
||||
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
|
||||
// proof_utils::push_instantiations_up(proof);
|
||||
// TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
|
||||
return proof;
|
||||
}
|
||||
|
||||
|
|
@ -1711,6 +1716,7 @@ namespace pdr {
|
|||
bool reachable;
|
||||
while (true) {
|
||||
checkpoint();
|
||||
m_expanded_lvl = lvl;
|
||||
reachable = check_reachability(lvl);
|
||||
if (reachable) {
|
||||
throw model_exception();
|
||||
|
|
@ -1770,6 +1776,10 @@ namespace pdr {
|
|||
SASSERT(n.is_open());
|
||||
expr_ref_vector cube(m);
|
||||
|
||||
if (n.level() < m_expanded_lvl) {
|
||||
m_expanded_lvl = n.level();
|
||||
}
|
||||
|
||||
if (n.pt().is_reachable(n.state())) {
|
||||
TRACE("pdr", tout << "reachable\n";);
|
||||
close_node(n);
|
||||
|
|
@ -1835,7 +1845,7 @@ namespace pdr {
|
|||
if (m_params.simplify_formulas_pre()) {
|
||||
simplify_formulas();
|
||||
}
|
||||
for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
|
||||
for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
|
||||
checkpoint();
|
||||
bool all_propagated = true;
|
||||
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
|
||||
|
|
|
|||
|
|
@ -303,6 +303,7 @@ namespace pdr {
|
|||
mutable model_search m_search;
|
||||
lbool m_last_result;
|
||||
unsigned m_inductive_lvl;
|
||||
unsigned m_expanded_lvl;
|
||||
ptr_vector<core_generalizer> m_core_generalizers;
|
||||
stats m_stats;
|
||||
volatile bool m_cancel;
|
||||
|
|
|
|||
|
|
@ -1081,6 +1081,7 @@ namespace pdr {
|
|||
arith_util a;
|
||||
bv_util bv;
|
||||
bool m_is_dl;
|
||||
bool m_test_for_utvpi;
|
||||
|
||||
bool is_numeric(expr* e) const {
|
||||
if (a.is_numeral(e)) {
|
||||
|
|
@ -1115,6 +1116,16 @@ namespace pdr {
|
|||
}
|
||||
return false;
|
||||
}
|
||||
if (m_test_for_utvpi) {
|
||||
if (a.is_mul(e, e1, e2)) {
|
||||
if (is_minus_one(e1)) {
|
||||
return is_offset(e2);
|
||||
}
|
||||
if (is_minus_one(e2)) {
|
||||
return is_offset(e1);
|
||||
}
|
||||
}
|
||||
}
|
||||
return !is_arith_expr(e);
|
||||
}
|
||||
|
||||
|
|
@ -1140,6 +1151,9 @@ namespace pdr {
|
|||
if (!a.is_add(lhs, arg1, arg2))
|
||||
return false;
|
||||
// x
|
||||
if (m_test_for_utvpi) {
|
||||
return is_offset(arg1) && is_offset(arg2);
|
||||
}
|
||||
if (is_arith_expr(arg1))
|
||||
std::swap(arg1, arg2);
|
||||
if (is_arith_expr(arg1))
|
||||
|
|
@ -1209,7 +1223,9 @@ namespace pdr {
|
|||
}
|
||||
|
||||
public:
|
||||
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
|
||||
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
|
||||
|
||||
void test_for_utvpi() { m_test_for_utvpi = true; }
|
||||
|
||||
void operator()(expr* e) {
|
||||
if (!m_is_dl) {
|
||||
|
|
@ -1248,6 +1264,16 @@ namespace pdr {
|
|||
return test.is_dl();
|
||||
}
|
||||
|
||||
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
|
||||
test_diff_logic test(m);
|
||||
test.test_for_utvpi();
|
||||
expr_fast_mark1 mark;
|
||||
for (unsigned i = 0; i < num_fmls; ++i) {
|
||||
quick_for_each_expr(test, mark, fmls[i]);
|
||||
}
|
||||
return test.is_dl();
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
template class rewriter_tpl<pdr::ite_hoister_cfg>;
|
||||
|
|
|
|||
|
|
@ -151,6 +151,8 @@ namespace pdr {
|
|||
|
||||
bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
|
||||
|
||||
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#include "dl_util.h"
|
||||
#include "proof_utils.h"
|
||||
#include "ast_smt2_pp.h"
|
||||
#include "var_subst.h"
|
||||
|
||||
class reduce_hypotheses {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
|
@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) {
|
|||
obj_map<proof,proof*> cache;
|
||||
::permute_unit_resolution(refs, cache, pr);
|
||||
}
|
||||
|
||||
class push_instantiations_up_cl {
|
||||
ast_manager& m;
|
||||
public:
|
||||
push_instantiations_up_cl(ast_manager& m): m(m) {}
|
||||
|
||||
void operator()(proof_ref& p) {
|
||||
expr_ref_vector s0(m);
|
||||
p = push(p, s0);
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
proof* push(proof* p, expr_ref_vector const& sub) {
|
||||
proof_ref_vector premises(m);
|
||||
expr_ref conclusion(m);
|
||||
svector<std::pair<unsigned, unsigned> > positions;
|
||||
vector<expr_ref_vector> substs;
|
||||
|
||||
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
|
||||
for (unsigned i = 0; i < premises.size(); ++i) {
|
||||
compose(substs[i], sub);
|
||||
premises[i] = push(premises[i].get(), substs[i]);
|
||||
substs[i].reset();
|
||||
}
|
||||
instantiate(sub, conclusion);
|
||||
return
|
||||
m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion,
|
||||
positions,
|
||||
substs);
|
||||
}
|
||||
if (sub.empty()) {
|
||||
return p;
|
||||
}
|
||||
if (m.is_modus_ponens(p)) {
|
||||
SASSERT(m.get_num_parents(p) == 2);
|
||||
proof* p0 = m.get_parent(p, 0);
|
||||
proof* p1 = m.get_parent(p, 1);
|
||||
if (m.get_fact(p0) == m.get_fact(p)) {
|
||||
return push(p0, sub);
|
||||
}
|
||||
expr* e1, *e2;
|
||||
if (m.is_rewrite(p1, e1, e2) &&
|
||||
is_quantifier(e1) && is_quantifier(e2) &&
|
||||
to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
|
||||
expr_ref r1(e1,m), r2(e2,m);
|
||||
instantiate(sub, r1);
|
||||
instantiate(sub, r2);
|
||||
p1 = m.mk_rewrite(r1, r2);
|
||||
return m.mk_modus_ponens(push(p0, sub), p1);
|
||||
}
|
||||
}
|
||||
premises.push_back(p);
|
||||
substs.push_back(sub);
|
||||
conclusion = m.get_fact(p);
|
||||
instantiate(sub, conclusion);
|
||||
return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
|
||||
}
|
||||
|
||||
void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
|
||||
for (unsigned i = 0; i < sub.size(); ++i) {
|
||||
expr_ref e(m);
|
||||
var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
|
||||
sub[i] = e;
|
||||
}
|
||||
}
|
||||
|
||||
void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
|
||||
if (sub.empty()) {
|
||||
return;
|
||||
}
|
||||
if (!is_forall(fml)) {
|
||||
return;
|
||||
}
|
||||
quantifier* q = to_quantifier(fml);
|
||||
if (q->get_num_decls() != sub.size()) {
|
||||
TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
|
||||
tout << mk_pp(q, m) << "\n";
|
||||
tout << sub.size() << "\n";);
|
||||
return;
|
||||
}
|
||||
var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
void proof_utils::push_instantiations_up(proof_ref& pr) {
|
||||
push_instantiations_up_cl push(pr.get_manager());
|
||||
push(pr);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -36,6 +36,12 @@ public:
|
|||
*/
|
||||
static void permute_unit_resolution(proof_ref& pr);
|
||||
|
||||
/**
|
||||
\brief Push instantiations created in hyper-resolutions up to leaves.
|
||||
This produces a "ground" proof where leaves are annotated by instantiations.
|
||||
*/
|
||||
static void push_instantiations_up(proof_ref& pr);
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1159,7 +1159,7 @@ namespace smt2 {
|
|||
m_num_expr_frames++;
|
||||
unsigned num_vars = parse_sorted_vars();
|
||||
if (num_vars == 0)
|
||||
throw parser_exception("invalied quantifier, list of sorted variables is empty");
|
||||
throw parser_exception("invalid quantifier, list of sorted variables is empty");
|
||||
}
|
||||
|
||||
symbol parse_indexed_identifier_core() {
|
||||
|
|
|
|||
|
|
@ -94,7 +94,6 @@ public:
|
|||
smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {}
|
||||
|
||||
virtual ~smt_strategic_solver_factory() {}
|
||||
|
||||
virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) {
|
||||
symbol l;
|
||||
if (m_logic != symbol::null)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue