mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
tseitin rule checking - wip
Unit test ``` (set-option :sat.euf true) (set-option :sat.smt.proof tseitinproof.smt2) (declare-const a1 Bool) (declare-const a2 Bool) (declare-const a3 Bool) (declare-const a4 Bool) (declare-const a5 Bool) (declare-const a6 Bool) (declare-const a7 Bool) (declare-const a8 Bool) (declare-const a9 Bool) (declare-const a10 Bool) (declare-const a11 Bool) (declare-const a12 Bool) (declare-const a13 Bool) (declare-const a14 Bool) (declare-const a15 Bool) (declare-const a16 Bool) (declare-const a17 Bool) (declare-const a18 Bool) (declare-const a19 Bool) (declare-const x1 Bool) (declare-const x2 Bool) (declare-const x3 Bool) (declare-const x4 Bool) (declare-const x5 Bool) (declare-const x6 Bool) (declare-const x7 Bool) (declare-const x8 Bool) (declare-const x9 Bool) (assert (= x1 (and a1 a2))) (assert (= x2 (or a3 a4))) (assert (= x3 (=> a5 a6))) (assert (= x4 (= a7 a8))) (assert (= x5 (if a9 a10 a11))) (assert (= x6 (=> a12 a13))) (check-sat) ``` Output proof ``` (declare-fun a1 () Bool) (declare-fun a2 () Bool) (define-const $26 Bool (and a1 a2)) (declare-fun tseitin (Bool Bool) Proof) (define-const $60 Bool (not $26)) (define-const $61 Proof (tseitin $60 a1)) (infer a1 (not $26) $61) (define-const $62 Proof (tseitin $60 a2)) (infer a2 (not $26) $62) (declare-fun tseitin (Bool Bool Bool) Proof) (define-const $64 Bool (not a2)) (define-const $63 Bool (not a1)) (define-const $65 Proof (tseitin $63 $64 $26)) (infer (not a1) (not a2) $26 $65) (declare-fun x1 () Bool) (assume (not x1) $26) (assume x1 (not $26)) (declare-fun a3 () Bool) (declare-fun a4 () Bool) (define-const $31 Bool (or a3 a4)) (define-const $66 Bool (not a3)) (define-const $67 Proof (tseitin $66 $31)) (infer (not a3) $31 $67) (define-const $68 Bool (not a4)) (define-const $69 Proof (tseitin $68 $31)) (infer (not a4) $31 $69) (define-const $70 Bool (not $31)) (define-const $71 Proof (tseitin a3 a4 $70)) (infer a3 a4 (not $31) $71) (declare-fun x2 () Bool) (assume (not x2) $31) (assume x2 (not $31)) (declare-fun a6 () Bool) (declare-fun a5 () Bool) (define-const $38 Bool (not a5)) (define-const $39 Bool (or a6 $38)) (define-const $72 Bool (not a6)) (define-const $73 Proof (tseitin $72 $39)) (infer (not a6) $39 $73) (define-const $74 Proof (tseitin a5 $39)) (infer a5 $39 $74) (define-const $75 Bool (not $39)) (define-const $76 Proof (tseitin a6 $38 $75)) (infer a6 (not a5) (not $39) $76) (declare-fun x3 () Bool) (assume (not x3) $39) (assume x3 (not $39)) (declare-fun a7 () Bool) (declare-fun a8 () Bool) (define-const $44 Bool (= a7 a8)) (define-const $78 Bool (not a7)) (define-const $77 Bool (not $44)) (define-const $79 Proof (tseitin $77 a8 $78)) (infer (not a7) a8 (not $44) $79) (define-const $80 Bool (not a8)) (define-const $81 Proof (tseitin $77 $80 a7)) (infer a7 (not a8) (not $44) $81) (define-const $82 Proof (tseitin $44 a8 a7)) (infer a7 a8 $44 $82) (define-const $83 Proof (tseitin $44 $80 $78)) (infer (not a7) (not a8) $44 $83) (declare-fun x4 () Bool) (assume (not x4) $44) (assume x4 (not $44)) (declare-fun a9 () Bool) (declare-fun a10 () Bool) (declare-fun a11 () Bool) (define-const $50 Bool (ite a9 a10 a11)) (define-const $85 Bool (not a9)) (define-const $84 Bool (not $50)) (define-const $86 Proof (tseitin $84 $85 a10)) (infer (not a9) a10 (not $50) $86) (define-const $87 Proof (tseitin $84 a9 a11)) (infer a9 a11 (not $50) $87) (define-const $88 Bool (not a10)) (define-const $89 Proof (tseitin $50 $85 $88)) (infer (not a9) (not a10) $50 $89) (define-const $90 Bool (not a11)) (define-const $91 Proof (tseitin $50 a9 $90)) (infer a9 (not a11) $50 $91) (define-const $92 Proof (tseitin $88 $90 $50)) (infer (not a10) (not a11) $50 $92) (define-const $93 Proof (tseitin a10 a11 $84)) (infer a10 a11 (not $50) $93) (declare-fun x5 () Bool) (assume (not x5) $50) (assume x5 (not $50)) (declare-fun a13 () Bool) (declare-fun a12 () Bool) (define-const $57 Bool (not a12)) (define-const $58 Bool (or a13 $57)) (define-const $94 Bool (not a13)) (define-const $95 Proof (tseitin $94 $58)) (infer (not a13) $58 $95) (define-const $96 Proof (tseitin a12 $58)) (infer a12 $58 $96) (define-const $97 Bool (not $58)) (define-const $98 Proof (tseitin a13 $57 $97)) (infer a13 (not a12) (not $58) $98) (declare-fun x6 () Bool) (assume (not x6) $58) (assume x6 (not $58)) ```
This commit is contained in:
Nikolaj Bjorner
parent
fceedf60dc
commit
cd8b8b603a
3 changed files with 131 additions and 28 deletions
|
|
@ -16,6 +16,7 @@ Author:
|
|||
|
||||
--*/
|
||||
|
||||
#include "ast/ast_pp.h"
|
||||
#include "sat/smt/tseitin_proof_checker.h"
|
||||
|
||||
namespace tseitin {
|
||||
|
|
@ -43,16 +44,17 @@ namespace tseitin {
|
|||
if (!main_expr)
|
||||
return false;
|
||||
|
||||
expr* a;
|
||||
expr* a, * x, * y, *z;
|
||||
|
||||
// (or (and a b) (not a) (not b))
|
||||
// (or (and (not a) b) a (not b))
|
||||
if (m.is_and(main_expr)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
if (m.is_not(arg, arg))
|
||||
mark(arg);
|
||||
complement_mark(arg);
|
||||
|
||||
for (expr* arg : *to_app(main_expr)) {
|
||||
if (!is_marked(arg))
|
||||
if (!is_complement(arg))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
|
@ -62,15 +64,54 @@ namespace tseitin {
|
|||
if (m.is_or(main_expr)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
if (m.is_not(arg, arg))
|
||||
mark(arg);
|
||||
for (expr* arg : *to_app(main_expr)) {
|
||||
if (is_marked(arg))
|
||||
return true;
|
||||
}
|
||||
complement_mark(arg);
|
||||
for (expr* arg : *to_app(main_expr))
|
||||
if (is_complement(arg))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
// (or (= a b) a b)
|
||||
// (or (= a b) (not a) (not b))
|
||||
// (or (= (not a) b) a (not b))
|
||||
if (m.is_eq(main_expr, x, y) && m.is_bool(x)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_marked(x) && is_marked(y))
|
||||
return true;
|
||||
if (is_complement(x) && is_complement(y))
|
||||
return true;
|
||||
}
|
||||
|
||||
// (or (if a b c) (not b) (not c))
|
||||
// (or (if a b c) a (not c))
|
||||
// (or (if a b c) (not a) (not b))
|
||||
if (m.is_ite(main_expr, x, y, z) && m.is_bool(z)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_marked(x) && is_complement(z))
|
||||
return true;
|
||||
if (is_complement(x) && is_complement(y))
|
||||
return true;
|
||||
if (is_complement(y) && is_complement(z))
|
||||
return true;
|
||||
IF_VERBOSE(0, verbose_stream() << mk_pp(main_expr, m) << "\n");
|
||||
}
|
||||
|
||||
|
||||
// (or (=> a b) a)
|
||||
// (or (=> a b) (not b))
|
||||
if (m.is_implies(main_expr, x, y)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_marked(x))
|
||||
return true;
|
||||
if (is_complement(y))
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m.is_not(main_expr, a)) {
|
||||
|
||||
// (or (not a) a')
|
||||
|
|
@ -99,11 +140,46 @@ namespace tseitin {
|
|||
return true;
|
||||
}
|
||||
|
||||
// (or (not (= a b) (not a) b)
|
||||
if (m.is_eq(a, x, y) && m.is_bool(x)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_marked(x) && is_complement(y))
|
||||
return true;
|
||||
if (is_marked(y) & is_complement(x))
|
||||
return true;
|
||||
}
|
||||
|
||||
// (or (not (if a b c)) (not a) b)
|
||||
// (or (not (if a b c)) a c)
|
||||
if (m.is_ite(a, x, y, z) && m.is_bool(z)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_complement(x) && is_marked(y))
|
||||
return true;
|
||||
if (is_marked(x) && is_marked(z))
|
||||
return true;
|
||||
if (is_marked(y) && is_marked(z))
|
||||
return true;
|
||||
}
|
||||
|
||||
// (or (not (=> a b)) b (not a))
|
||||
if (m.is_implies(a, x, y)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_complement(x) && is_marked(y))
|
||||
return true;
|
||||
}
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "miss " << mk_pp(main_expr, m) << "\n");
|
||||
|
||||
#if 0
|
||||
if (m.is_implies(a))
|
||||
return false;
|
||||
if (m.is_eq(a))
|
||||
return false;
|
||||
|
||||
if (m.is_ite(a))
|
||||
return false;
|
||||
if (m.is_distinct(a))
|
||||
|
|
|
|||
|
|
@ -29,14 +29,33 @@ namespace tseitin {
|
|||
ast_manager& m;
|
||||
|
||||
expr_fast_mark1 m_mark;
|
||||
expr_fast_mark2 m_nmark;
|
||||
bool equiv(expr* a, expr* b);
|
||||
|
||||
void mark(expr* a) { m_mark.mark(a); }
|
||||
bool is_marked(expr* a) { return m_mark.is_marked(a); }
|
||||
|
||||
void nmark(expr* a) { m_nmark.mark(a); }
|
||||
bool is_nmarked(expr* a) { return m_nmark.is_marked(a); }
|
||||
|
||||
void complement_mark(expr* a) {
|
||||
if (m.is_not(a, a))
|
||||
m_nmark.mark(a);
|
||||
else
|
||||
m_mark.mark(a);
|
||||
}
|
||||
|
||||
bool is_complement(expr* a) {
|
||||
if (m.is_not(a, a))
|
||||
return is_marked(a);
|
||||
else
|
||||
return is_nmarked(a);
|
||||
}
|
||||
|
||||
struct scoped_mark {
|
||||
proof_checker& pc;
|
||||
scoped_mark(proof_checker& pc): pc(pc) {}
|
||||
~scoped_mark() { pc.m_mark.reset(); }
|
||||
~scoped_mark() { pc.m_mark.reset(); pc.m_nmark.reset(); }
|
||||
};
|
||||
public:
|
||||
proof_checker(ast_manager& m):
|
||||
|
|
|
|||
|
|
@ -124,6 +124,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
euf::th_proof_hint* mk_tseitin(sat::literal a, sat::literal b, sat::literal c) {
|
||||
if (m_euf && ensure_euf()->use_drat()) {
|
||||
sat::literal lits[3] = { a, b, c };
|
||||
return ensure_euf()->mk_smt_hint(m_tseitin, 3, lits);
|
||||
}
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
sat::status mk_status(euf::th_proof_hint* ph = nullptr) const {
|
||||
return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
|
||||
}
|
||||
|
|
@ -522,13 +530,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
sat::bool_var k = add_var(false, n);
|
||||
sat::literal l(k, false);
|
||||
cache(n, l);
|
||||
mk_clause(~l, ~c, t);
|
||||
mk_clause(~l, c, e);
|
||||
mk_clause(l, ~c, ~t);
|
||||
mk_clause(l, c, ~e);
|
||||
mk_clause(~l, ~c, t, mk_tseitin(~l, ~c, t));
|
||||
mk_clause(~l, c, e, mk_tseitin(~l, c, e));
|
||||
mk_clause(l, ~c, ~t, mk_tseitin(l, ~c, ~t));
|
||||
mk_clause(l, c, ~e, mk_tseitin(l, c, ~e));
|
||||
if (m_ite_extra) {
|
||||
mk_clause(~t, ~e, l);
|
||||
mk_clause(t, e, ~l);
|
||||
mk_clause(~t, ~e, l, mk_tseitin(~t, ~e, l));
|
||||
mk_clause(t, e, ~l, mk_tseitin(t, e, ~l));
|
||||
}
|
||||
if (aig()) aig()->add_ite(l, c, t, e);
|
||||
if (sign)
|
||||
|
|
@ -555,8 +563,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
sat::literal l(k, false);
|
||||
cache(t, l);
|
||||
// l <=> ~lit
|
||||
mk_clause(lit, l);
|
||||
mk_clause(~lit, ~l);
|
||||
mk_clause(lit, l, mk_tseitin(lit, l));
|
||||
mk_clause(~lit, ~l, mk_tseitin(~lit, ~l));
|
||||
if (sign)
|
||||
l.neg();
|
||||
m_result_stack.push_back(l);
|
||||
|
|
@ -587,9 +595,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
sat::literal l(k, false);
|
||||
cache(t, l);
|
||||
// l <=> (l1 => l2)
|
||||
mk_clause(~l, ~l1, l2);
|
||||
mk_clause(l1, l);
|
||||
mk_clause(~l2, l);
|
||||
mk_clause(~l, ~l1, l2, mk_tseitin(~l, ~l1, l2));
|
||||
mk_clause(l1, l, mk_tseitin(l1, l));
|
||||
mk_clause(~l2, l, mk_tseitin(~l2, l));
|
||||
if (sign)
|
||||
l.neg();
|
||||
m_result_stack.push_back(l);
|
||||
|
|
@ -625,10 +633,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
sat::literal l(k, false);
|
||||
if (m.is_xor(t))
|
||||
l1.neg();
|
||||
mk_clause(~l, l1, ~l2);
|
||||
mk_clause(~l, ~l1, l2);
|
||||
mk_clause(l, l1, l2);
|
||||
mk_clause(l, ~l1, ~l2);
|
||||
mk_clause(~l, l1, ~l2, mk_tseitin(~l, l1, ~l2));
|
||||
mk_clause(~l, ~l1, l2, mk_tseitin(~l, ~l1, l2));
|
||||
mk_clause(l, l1, l2, mk_tseitin(l, l1, l2));
|
||||
mk_clause(l, ~l1, ~l2, mk_tseitin(l, ~l1, ~l2));
|
||||
if (aig()) aig()->add_iff(l, l1, l2);
|
||||
|
||||
cache(t, l);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue