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

add clause proof module, small improvements to bapa

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-30 15:57:19 -07:00
parent 48fc3d752e
commit f128398bf9
7 changed files with 101 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_ast.cpp
View file

@ -996,6 +996,10 @@ extern "C" {
case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM;
case PR_ASSUMPTION_ADD: return Z3_OP_PR_ASSUMPTION_ADD;
case PR_LEMMA_ADD: return Z3_OP_PR_LEMMA_ADD;
case PR_REDUNDANT_DEL: return Z3_OP_PR_REDUNDANT_DEL;
case PR_CLAUSE_TRAIL: return Z3_OP_PR_CLAUSE_TRAIL;
case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;

16
src/api/z3_api.h
View file

@ -644,6 +644,18 @@ typedef enum
unfolding the Boolean connectives in the axioms a small
bounded number of steps (=3).
- Z3_OP_PR_ASSUMPTION_ADD
Clausal proof adding axiom
- Z3_OP_PR_LEMMA_ADD
Clausal proof lemma addition
- Z3_OP_PR_REDUNDANT_DEL
Clausal proof lemma deletion
- Z3_OP_PR_CLAUSE_TRAIL,
Clausal proof trail of additions and deletions
- Z3_OP_PR_DEF_INTRO: Introduces a name for a formula/term.
Suppose e is an expression with free variables x, and def-intro
introduces the name n(x). The possible cases are:
@ -1143,6 +1155,10 @@ typedef enum {
Z3_OP_PR_IFF_FALSE,
Z3_OP_PR_COMMUTATIVITY,
Z3_OP_PR_DEF_AXIOM,
Z3_OP_PR_ASSUMPTION_ADD,
Z3_OP_PR_LEMMA_ADD,
Z3_OP_PR_REDUNDANT_DEL,
Z3_OP_PR_CLAUSE_TRAIL,
Z3_OP_PR_DEF_INTRO,
Z3_OP_PR_APPLY_DEF,
Z3_OP_PR_IFF_OEQ,

51
src/ast/rewriter/array_rewriter.cpp
View file

@ -352,6 +352,11 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
return BR_REWRITE3;
}
if (m().is_not(f) && m_util.is_map(args[0]) && m().is_not(m_util.get_map_func_decl(args[0]))) {
result = to_app(args[0])->get_arg(0);
return BR_DONE;
}
if (m().is_and(f)) {
ast_mark mark;
ptr_buffer<expr> es;
@ -373,16 +378,48 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
}
}
es.shrink(j);
j = 0;
for (expr* e : es) {
if (m().is_not(e, e) && mark.is_marked(e)) {
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, m().mk_false());
return BR_DONE;
if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e))) {
expr * arg = to_app(e)->get_arg(0);
if (mark.is_marked(arg)) {
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, m().mk_false());
return BR_DONE;
}
// a & (!a & b & c) -> a & !(b & c)
if (m_util.is_map(arg) && m().is_and(m_util.get_map_func_decl(arg))) {
unsigned k = 0;
ptr_buffer<expr> gs;
bool and_change = false;
gs.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
for (unsigned i = 0; i < gs.size(); ++i) {
expr* g = gs[i];
if (mark.is_marked(g)) {
change = true;
and_change = true;
}
else if (m_util.is_map(g) && m().is_and(m_util.get_map_func_decl(g))) {
gs.append(to_app(g)->get_num_args(), to_app(g)->get_args());
}
else {
gs[k++] = gs[i];
}
}
gs.shrink(k);
if (and_change) {
std::sort(gs.begin(), gs.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
expr* arg = m_util.mk_map_assoc(f, gs.size(), gs.c_ptr());
es[j] = m_util.mk_map(m().mk_not_decl(), 1, &arg);
}
}
}
++j;
}
if (change) {
std::sort(es.begin(), es.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
return BR_DONE;
return BR_REWRITE2;
}
}
@ -408,7 +445,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
}
es.shrink(j);
for (expr* e : es) {
if (m().is_not(e, e) && mark.is_marked(e)) {
if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e)) && mark.is_marked(to_app(e)->get_arg(0))) {
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, m().mk_true());
return BR_DONE;
@ -416,7 +453,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
}
if (change) {
result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
return BR_DONE;
return BR_REWRITE1;
}
}

18
src/cmd_context/basic_cmds.cpp
View file

@ -174,14 +174,16 @@ public:
};
ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (!ctx.produce_proofs())
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
if (!ctx.has_manager() ||
ctx.cs_state() != cmd_context::css_unsat)
if (!ctx.has_manager())
throw cmd_exception("proof is not available");
if (ctx.ignore_check())
return;
expr_ref pr(ctx.m());
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
if (!pr && !ctx.produce_proofs())
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
if (!pr)
throw cmd_exception("proof is not available");
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
throw cmd_exception("proof is not well sorted");
@ -209,6 +211,8 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it
ctx.cs_state() != cmd_context::css_unsat)
throw cmd_exception("proof is not available");
proof_ref pr(ctx.m());
if (ctx.ignore_check())
return;
pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0)
throw cmd_exception("proof is not available");
@ -238,6 +242,8 @@ static void print_core(cmd_context& ctx) {
}
ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
if (ctx.ignore_check())
return;
if (!ctx.produce_unsat_cores())
throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)");
if (!ctx.has_manager() ||
@ -247,6 +253,8 @@ ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
});
ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", {
if (ctx.ignore_check())
return;
if (!ctx.produce_unsat_assumptions())
throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)");
if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) {

31
src/tactic/goal.cpp
View file

@ -128,16 +128,14 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
m().del(m_dependencies);
m_inconsistent = true;
m().push_back(m_forms, m().mk_false());
if (proofs_enabled())
m().push_back(m_proofs, saved_pr);
m().push_back(m_proofs, saved_pr);
if (unsat_core_enabled())
m().push_back(m_dependencies, saved_d);
}
else {
SASSERT(!m_inconsistent);
m().push_back(m_forms, f);
if (proofs_enabled())
m().push_back(m_proofs, pr);
m().push_back(m_proofs, pr);
if (unsat_core_enabled())
m().push_back(m_dependencies, d);
}
@ -248,11 +246,12 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
expr_ref _f(f, m());
proof_ref _pr(pr, m());
expr_dependency_ref _d(d, m());
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
if (m_inconsistent) {
return;
if (proofs_enabled())
}
if (pr) {
slow_process(f, pr, d);
}
else {
expr_ref fr(f, m());
quick_process(false, fr, d);
@ -278,11 +277,9 @@ void goal::get_formulas(expr_ref_vector & result) const {
}
void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
// KLM: don't know why this assertion is no longer true
// SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
if (proofs_enabled()) {
if (pr) {
expr_ref out_f(m());
proof_ref out_pr(m());
slow_process(true, f, pr, d, out_f, out_pr);
@ -455,9 +452,8 @@ void goal::shrink(unsigned j) {
unsigned sz = size();
for (unsigned i = j; i < sz; i++)
m().pop_back(m_forms);
if (proofs_enabled())
for (unsigned i = j; i < sz; i++)
m().pop_back(m_proofs);
for (unsigned i = j; i < sz; i++)
m().pop_back(m_proofs);
if (unsat_core_enabled())
for (unsigned i = j; i < sz; i++)
m().pop_back(m_dependencies);
@ -478,8 +474,7 @@ void goal::elim_true() {
continue;
}
m().set(m_forms, j, f);
if (proofs_enabled())
m().set(m_proofs, j, m().get(m_proofs, i));
m().set(m_proofs, j, m().get(m_proofs, i));
if (unsat_core_enabled())
m().set(m_dependencies, j, m().get(m_dependencies, i));
j++;
@ -565,8 +560,7 @@ void goal::elim_redundancies() {
continue;
}
m().set(m_forms, j, f);
if (proofs_enabled())
m().set(m_proofs, j, pr(i));
m().set(m_proofs, j, pr(i));
if (unsat_core_enabled())
m().set(m_dependencies, j, dep(i));
j++;
@ -596,8 +590,7 @@ goal * goal::translate(ast_translation & translator) const {
unsigned sz = m().size(m_forms);
for (unsigned i = 0; i < sz; i++) {
res->m().push_back(res->m_forms, translator(m().get(m_forms, i)));
if (res->proofs_enabled())
res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
if (res->unsat_core_enabled())
res->m().push_back(res->m_dependencies, dep_translator(m().get(m_dependencies, i)));
}

2
src/tactic/goal.h
View file

@ -121,7 +121,7 @@ public:
unsigned num_exprs() const;
expr * form(unsigned i) const { return m().get(m_forms, i); }
proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m().get(m_proofs, i)) : nullptr; }
proof * pr(unsigned i) const { return m().size(m_proofs) > i ? static_cast<proof*>(m().get(m_proofs, i)) : nullptr; }
expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : nullptr; }
void update(unsigned i, expr * f, proof * pr = nullptr, expr_dependency * dep = nullptr);

12
src/util/uint_set.h
View file

@ -364,6 +364,11 @@ public:
SASSERT(!contains(x));
}
unsigned elem_at(unsigned index) {
SASSERT(index < m_size);
return m_elems[index];
}
bool contains(unsigned x) const { return x < m_index.size() && m_index[x] < m_size && m_elems[m_index[x]] == x; }
void reset() { m_size = 0; }
bool empty() const { return m_size == 0; }
@ -372,8 +377,13 @@ public:
typedef unsigned_vector::const_iterator iterator;
iterator begin() const { return m_elems.begin(); }
iterator end() const { return m_elems.begin() + m_size; }
};
inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) {
for (unsigned i : s) out << i << " ";
return out;
}
#endif /* UINT_SET_H_ */