Nikolaj Bjorner
ace727ee0f
fix #6391
2022-10-12 09:34:49 +02:00
Nuno Lopes
a41520acf1
mpf: fix some string copies
2022-10-11 11:59:29 +01:00
Nikolaj Bjorner
1b3684c9c1
wip - fixes to implied-eq proof hints
2022-10-11 09:54:00 +02:00
Nikolaj Bjorner
ffeb8f4572
wip - tseitin check
...
```
(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)
```
2022-10-11 09:21:36 +02:00
Nikolaj Bjorner
62438da0f5
wip - add xor and non-bool ite tseitin rules
2022-10-11 09:15:18 +02:00
Nikolaj Bjorner
cd8b8b603a
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))
```
2022-10-10 23:44:03 +02:00
Nikolaj Bjorner
fceedf60dc
wip - proofs
2022-10-10 16:41:09 +02:00
Nikolaj Bjorner
de69874076
wip - adding proof checkers, fixes to quantifier proof certificates
2022-10-10 09:46:22 +02:00
Nikolaj Bjorner
4623117af8
wip - proof hints
2022-10-08 20:12:57 +02:00
Nikolaj Bjorner
6796ea7e49
add new files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-07 19:22:36 +02:00
Nikolaj Bjorner
35639c5ac0
adding q proof hints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-07 19:21:21 +02:00
Nuno Lopes
661a1624b4
avoid string copying in mpf_manager::set
2022-10-07 14:03:13 +01:00
Nikolaj Bjorner
5c9f69829b
fixes to trim
2022-10-07 09:58:12 +02:00
Nuno Lopes
a792251a82
remove old compat code
2022-10-06 17:22:17 +01:00
Nikolaj Bjorner
9f78a96c1d
wip - trim
2022-10-06 18:19:03 +02:00
Nikolaj Bjorner
4e780d0cc8
trim
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-05 05:43:48 +02:00
Nikolaj Bjorner
f8ca692dee
fixes to trim
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-05 04:32:00 +02:00
Nikolaj Bjorner
c1c659dc93
trying trim
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-04 16:25:40 +02:00
Nikolaj Bjorner
d22c86f9fe
init spacer_iuc_solver properly
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-03 15:53:58 -04:00
Nikolaj Bjorner
6e05162df0
update solver only if there is a manager
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-03 15:27:26 -04:00
Nikolaj Bjorner
b03d4e4fc2
update solver only if there is a manager
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-03 15:26:10 -04:00
Nikolaj Bjorner
5b71f7cf9e
Merge branch 'master' of https://github.com/z3prover/z3
2022-10-03 15:19:01 -04:00
Nuno Lopes
be3c7d7115
delete dead code
2022-10-02 21:44:08 +01:00
Nuno Lopes
1eed058b98
use std::move
2022-10-02 21:34:17 +01:00
Nikolaj Bjorner
ad49dd739b
initialize variables to avoid warning messages whether real or spurious
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-01 17:08:02 -04:00
Nikolaj Bjorner
cffe5fe1a5
remove debug print
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-10-01 17:05:36 -04:00
Nuno Lopes
24ff0f2d36
attempt to fix cmake build
2022-10-01 21:48:27 +01:00
Naxaes
49ebca6c1c
Fix clang build ( #6378 )
2022-10-01 14:01:36 +01:00
Nuno Lopes
47e44c5538
fix build
2022-10-01 12:17:15 +01:00
Nikolaj Bjorner
903cddcaaa
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-30 17:10:18 -04:00
Nikolaj Bjorner
ab045f0645
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-30 16:52:19 -04:00
Nikolaj Bjorner
876ca2f1a5
fix #6371
2022-09-30 14:51:28 -04:00
Nikolaj Bjorner
b9cba82531
work on proof checking
...
- add outline of trim routine
- streamline how proof terms are checked and how residue units are extracted.
2022-09-30 13:04:19 -04:00
Nikolaj Bjorner
ccda49bad5
fix #6376
...
have solver throw an exception when user supplies a non-propositional assumption
2022-09-30 13:03:34 -04:00
Nikolaj Bjorner
6eb2d2acfa
update dependencies for build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-28 11:25:36 -07:00
Nikolaj Bjorner
107981f099
update proof formats for new core
...
- update proof format for quantifier instantiation to track original literals
- update proof replay tools with ability to extract proof object
The formats and features are subject to heavy revisions.
Example
```
(set-option :sat.euf true)
(set-option :sat.smt.proof eufproof.smt2)
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (or (= (f (f (f x))) x) (= (f (f x)) x)))
(assert (not (= (f (f (f (f (f (f x)))))) x)))
(check-sat)
```
eufproof.smt2 is:
```
(declare-fun x () Int)
(declare-fun f (Int) Int)
(define-const $24 Int (f x))
(define-const $25 Int (f $24))
(define-const $26 Int (f $25))
(define-const $27 Bool (= $26 x))
(define-const $28 Bool (= $25 x))
(assume $27 $28)
(define-const $30 Int (f $26))
(define-const $31 Int (f $30))
(define-const $32 Int (f $31))
(define-const $33 Bool (= $32 x))
(assume (not $33))
(declare-fun rup () Proof)
(infer (not $33) rup)
(declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof)
(declare-fun cc (Bool) Proof)
(define-const $42 Bool (= $32 $30))
(define-const $43 Proof (cc $42))
(define-const $40 Bool (= $31 $24))
(define-const $41 Proof (cc $40))
(define-const $38 Bool (= $30 $25))
(define-const $39 Proof (cc $38))
(define-const $36 Bool (= $24 $26))
(define-const $37 Proof (cc $36))
(define-const $34 Bool (not $33))
(define-const $44 Proof (euf $34 $28 $37 $39 $41 $43))
(infer (not $28) $33 $44)
(infer (not $28) rup)
(infer $27 rup)
(declare-fun euf (Bool Bool Proof Proof Proof) Proof)
(define-const $49 Bool (= $32 $26))
(define-const $50 Proof (cc $49))
(define-const $47 Bool (= $31 $25))
(define-const $48 Proof (cc $47))
(define-const $45 Bool (= $24 $30))
(define-const $46 Proof (cc $45))
(define-const $51 Proof (euf $34 $27 $46 $48 $50))
(infer $33 $51)
(infer rup)
```
Example of inspecting proof from Python:
```
from z3 import *
def parse(file):
s = Solver()
set_option("solver.proof.save", True)
set_option("solver.proof.check", False)
s.from_file(file)
for step in s.proof().children():
print(step)
parse("../eufproof.smt2")
```
Proof checking (self-validation) is on by default.
Proof saving is off by default.
You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core.
The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT.
2022-09-28 10:40:43 -07:00
Nikolaj Bjorner
9782d4a730
#5261
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-26 05:04:02 -07:00
Nikolaj Bjorner
7b982a812e
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-25 18:09:32 -07:00
Nikolaj Bjorner
3df8b9c7e2
Merge branch 'master' of https://github.com/z3prover/z3
2022-09-25 18:03:26 -07:00
Nikolaj Bjorner
d7b9cc70d0
smc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-25 18:03:16 -07:00
Nikolaj Bjorner
9be8fc7857
Add EUF (congruence closure) proof hints and checker to the new core
...
EUF proofs are checked modulo union-find.
Equalities are added to to union-find if they are assumptions or if they can be derived using congruence closure. The congruence closure assumptions are added as proof-hints.
Note that this proof format does not track equality inferences, symmetry and transitivity. Instead they are handled by assuming a union-find based checker.
2022-09-25 14:26:20 -07:00
Nikolaj Bjorner
6f2fde87d1
move has-default up before merge of parents
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-24 14:40:30 -07:00
Nikolaj Bjorner
aadb1a2d44
Update msvc-static-build.yml
...
move "permissions" to same location as wasm actions
2022-09-24 09:56:45 -07:00
Nikolaj Bjorner
b3c2169838
Update msvc-static-build.yml
2022-09-24 09:55:15 -07:00
Clemens Eisenhofer
5ca53f37c0
Throw an exception if the variable in decide-callback is already assigned ( #6362 )
...
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
2022-09-24 09:54:14 -07:00
Nikolaj Bjorner
3dfff3d7a1
tracing for fpa
2022-09-23 22:48:54 -07:00
Nikolaj Bjorner
1f150ecd52
#6319
...
#6319 - fix incompleteness in propagation of default to all array terms in the equivalence class.
Fix bug with q_mbi where domain restrictions are not using values because the current model does not evaluate certain bound variables to values. Set model completion when adding these bound variables to the model to ensure their values are not missed.
Add better propagation of diagnostics when tactics and the new solver return unknown. The reason for unknown can now be traced to what theory was culprit (currently no additional information)
2022-09-23 22:22:34 -05:00
Nikolaj Bjorner
6226875283
fix regression with uninitialized variable
2022-09-23 15:51:26 -05:00
Nikolaj Bjorner
c41b6da6bb
#6319
...
using a queue for disequality propagaiton was a regression: values of numerals can change along the same stack so prior passing the filter does not mean it passes later.
2022-09-23 14:47:48 -05:00
Nikolaj Bjorner
79b4357442
#6363
2022-09-23 14:32:01 -05:00
