mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
wip - add xor and non-bool ite tseitin rules
This commit is contained in:
parent
cd8b8b603a
commit
62438da0f5
|
@ -13,7 +13,17 @@ Author:
|
|||
|
||||
Nikolaj Bjorner (nbjorner) 2022-10-07
|
||||
|
||||
TODOs:
|
||||
|
||||
- handle distinct
|
||||
- handle other internalization from euf_internalize
|
||||
- equiv should be modulo commutativity (the E-graph indexes expressions modulo commutativity of top-level operator)
|
||||
|
||||
- should we log rules for root clauses too? Root clauses should follow from input.
|
||||
They may be simplified using Tseitin transformation. For example, (and a b) is clausified into
|
||||
two clauses a, b.
|
||||
|
||||
- Tesitin checking could also be performed by depth-bounded SAT (e.g., using BDDs)
|
||||
--*/
|
||||
|
||||
#include "ast/ast_pp.h"
|
||||
|
@ -44,7 +54,7 @@ namespace tseitin {
|
|||
if (!main_expr)
|
||||
return false;
|
||||
|
||||
expr* a, * x, * y, *z;
|
||||
expr* a, * x, * y, *z, *u, *v;
|
||||
|
||||
// (or (and a b) (not a) (not b))
|
||||
// (or (and (not a) b) a (not b))
|
||||
|
@ -53,10 +63,10 @@ namespace tseitin {
|
|||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
|
||||
for (expr* arg : *to_app(main_expr)) {
|
||||
for (expr* arg : *to_app(main_expr))
|
||||
if (!is_complement(arg))
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -83,6 +93,16 @@ namespace tseitin {
|
|||
return true;
|
||||
}
|
||||
|
||||
if (m.is_eq(main_expr, x, y) && m.is_ite(x, z, u, v)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
if (is_marked(z) && equiv(y, v))
|
||||
return true;
|
||||
if (is_complement(z) && equiv(y, u))
|
||||
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))
|
||||
|
@ -112,6 +132,21 @@ namespace tseitin {
|
|||
return true;
|
||||
}
|
||||
|
||||
// (or (xor a b c d) a b (not c) (not d))
|
||||
if (m.is_xor(main_expr)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
int parity = 0;
|
||||
for (expr* arg : *to_app(main_expr))
|
||||
if (is_marked(arg))
|
||||
parity++;
|
||||
else if (is_complement(arg))
|
||||
parity--;
|
||||
if ((parity % 2) == 0)
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m.is_not(main_expr, a)) {
|
||||
|
||||
// (or (not a) a')
|
||||
|
@ -174,17 +209,24 @@ namespace tseitin {
|
|||
return true;
|
||||
}
|
||||
|
||||
// (or (not (xor a b c d)) a b c (not d))
|
||||
if (m.is_xor(a)) {
|
||||
scoped_mark sm(*this);
|
||||
for (expr* arg : *jst)
|
||||
complement_mark(arg);
|
||||
int parity = 1;
|
||||
for (expr* arg : *to_app(main_expr))
|
||||
if (is_marked(arg))
|
||||
parity++;
|
||||
else if (is_complement(arg))
|
||||
parity--;
|
||||
if ((parity % 2) == 0)
|
||||
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_ite(a))
|
||||
return false;
|
||||
if (m.is_distinct(a))
|
||||
return false;
|
||||
#endif
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
|
|
@ -142,23 +142,19 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
|
||||
bool top_level_relevant() {
|
||||
return m_top_level && relevancy_enabled();
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l) {
|
||||
mk_clause(1, &l);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph = nullptr) {
|
||||
void mk_clause(sat::literal l1, sat::literal l2, euf::th_proof_hint* ph) {
|
||||
sat::literal lits[2] = { l1, l2 };
|
||||
mk_clause(2, lits, ph);
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph = nullptr) {
|
||||
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, euf::th_proof_hint* ph) {
|
||||
sat::literal lits[3] = { l1, l2, l3 };
|
||||
mk_clause(3, lits, ph);
|
||||
}
|
||||
|
||||
void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph = nullptr) {
|
||||
void mk_clause(unsigned n, sat::literal * lits, euf::th_proof_hint* ph) {
|
||||
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
|
||||
if (relevancy_enabled())
|
||||
ensure_euf()->add_aux(n, lits);
|
||||
|
|
Loading…
Reference in a new issue