mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

wip - tseitin check

Browse source 
```
(set-option :sat.euf true)
(set-option :sat.smt.proof tseitinproof.smt2)
(set-option :tactic.default_tactic smt)

(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)

(declare-const b1 Int)
(declare-const b2 Int)
(declare-const b3 Int)
(declare-const b4 Int)

(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)))
(assert (= x7 (xor a1 a2 a3)))
(assert (= x7 (xor a1 a2 a3 a4 a5 (not a6))))
(assert (= x8 (= (ite a1 b1 b2) b3)))
(check-sat)
(exit)

```
This commit is contained in:
Nikolaj Bjorner 2022-10-11 09:21:36 +02:00
parent 62438da0f5
commit ffeb8f4572
2 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/tseitin_proof_checker.cpp
View file

@ -239,6 +239,4 @@ namespace tseitin {
return x == u && y == z;
return false;
}
}

3
src/sat/smt/tseitin_proof_checker.h
View file

@ -39,10 +39,9 @@ namespace tseitin {
bool is_nmarked(expr* a) { return m_nmark.is_marked(a); }
void complement_mark(expr* a) {
m_mark.mark(a);
if (m.is_not(a, a))
m_nmark.mark(a);
else
m_mark.mark(a);
}
bool is_complement(expr* a) {