mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity
19407 commits 30 branches 51 tags 167 MiB
Commit graph

19407 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Jakob Rath
05442e8788 lemma_invariant 2022-09-30 13:12:47 +02:00
Jakob Rath
5e54cd3e44 Add basic support for not, or, xor, nand, nor via rewriting 2022-09-30 13:02:32 +02:00
Jakob Rath
9b907d709f minor 2022-09-29 18:25:28 +02:00
Jakob Rath
8242069ba6 One more case for ule_constraint::is_always_false 2022-09-29 18:22:31 +02:00
Jakob Rath
6218931dde We only need one of is_true/is_false 2022-09-29 17:19:47 +02:00
Jakob Rath
79c82a3d97 update ule_constraint::is_currently_true 2022-09-29 17:02:30 +02: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
Jakob Rath
8d803a1266 Move unfinished make_asserting code 2022-09-28 19:19:33 +02:00
Jakob Rath
0dae3bad6a Fix subsumption terminology 2022-09-28 15:35:05 +02:00
Jakob Rath
7be82a36f2 Recognize x != k among new literals in lemma 2022-09-28 15:16:05 +02:00
Jakob Rath
6715058876 Simplify equations into canonical form 
Also simplify constraints that are always false due to parity
 2022-09-28 13:22:17 +02:00
Jakob Rath
480ba01cb0 Log ule rewrites 2022-09-28 11:01:23 +02:00
Jakob Rath
e08e124790 Expand always-false check 2022-09-28 10:57:40 +02:00
Jakob Rath
27b31c88d2 re-enable ule rewrite 2022-09-28 10:53:55 +02:00
Jakob Rath
d09e3eaa37 Update notes 2022-09-27 18:00:30 +02:00
Jakob Rath
0f993e3977 New constraints need to be eval'd 2022-09-27 17:56:26 +02:00
Jakob Rath
602a9e3914 test_l4b for another always-false constraint 2022-09-27 17:55:29 +02:00
Jakob Rath
74d8497ed9 Fix subsumption for unilinear case 2022-09-27 17:53:45 +02: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
Nikolaj Bjorner
3d9512b93c fix #6363 2022-09-23 14:32:01 -05:00
Nikolaj Bjorner
de74e342c6
#5261 2022-09-23 13:19:55 -05:00
Jakob Rath
1df749ad33 Merge branch 'master' into polysat 2022-09-23 17:14:26 +02:00
Jakob Rath
67c778a6da unit test notes 2022-09-23 16:53:07 +02:00
Jakob Rath
49590e0e01 Conflict from viable_fallback also depends on the current assignment 2022-09-23 16:45:56 +02:00
Jakob Rath
4e4b4fdd06 subsumption notes 2022-09-23 16:45:23 +02:00
Jakob Rath
3c60c418e7 fix assertion 2022-09-23 16:15:38 +02:00
Jakob Rath
0a0953ae78 Reduce log output 2022-09-23 16:12:39 +02:00
Jakob Rath
8ed6938cbe remove/update comment 2022-09-23 16:06:14 +02:00
Jakob Rath
4312611bd6 nicer lit_pp 2022-09-23 16:06:14 +02:00
Jakob Rath
a4f0e3a228 Add level to conflict 
- reset conflict at correct level when popping user scopes
- functions as flag when handling inconsistent input (e.g., opposite literals)
- now all constraints in the conflict core should have bvalue == l_true
 2022-09-23 16:06:14 +02:00
Jakob Rath
86d00b536a move todo notes to cpp file 2022-09-23 15:45:53 +02:00
Nikolaj Bjorner
4c6d7158cb extended debugging for sat.euf 2022-09-22 17:05:32 -05:00