Nikolaj Bjorner
|
012fc1b72b
|
more detailed tracing of where unmaterialized exceptions happen
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-19 18:15:50 -08:00 |
|
Nikolaj Bjorner
|
e855a50d9b
|
add exception handling to easier diagnose #7418
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-19 11:46:54 -08:00 |
|
Nuno Lopes
|
3586b613f7
|
remove default destructors
|
2024-10-02 22:20:12 +01:00 |
|
THE Spellchecker
|
dc0887db5a
|
Typo Fixes (#6803)
|
2023-07-09 11:56:10 -07:00 |
|
Nikolaj Bjorner
|
1b0c76e3f0
|
fixes to mbqi in the new core based on #6575
|
2023-02-10 16:56:06 -08: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
|
0ca5e7207e
|
#5746
|
2022-01-02 11:35:55 -08:00 |
|
Nikolaj Bjorner
|
e84ddb0d9a
|
more #5746
|
2022-01-02 11:33:21 -08:00 |
|
Nikolaj Bjorner
|
4a6083836a
|
call it data instead of c_ptr for approaching C++11 std::vector convention.
|
2021-04-13 18:17:35 -07:00 |
|
Nikolaj Bjorner
|
42ac3a5363
|
merge with csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-12 19:48:45 -07:00 |
|
Nikolaj Bjorner
|
9ec59fdb93
|
fix #1934
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-17 15:04:25 -08:00 |
|
Nikolaj Bjorner
|
74621e0b7d
|
first eufi example running
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-14 16:08:52 -07:00 |
|
Nikolaj Bjorner
|
c513f3ca09
|
merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 14:57:01 -07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Nikolaj Bjorner
|
3de8c193ea
|
implementing model updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-10-30 16:11:51 -05:00 |
|
Nikolaj Bjorner
|
7a977f0106
|
ensure that timeouts are distinguished from other cancel events #848
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-18 14:54:54 -07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Leonardo de Moura
|
4c98b567e1
|
old_params ==> front_end_params. Isolated abstract solver interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 11:28:14 -07:00 |
|