mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity
18370 commits 49 branches 53 tags 181 MiB
Commit graph

3039 commits

Author SHA1 Message Date
Nikolaj Bjorner
3a37cfca30 switch to solve_eqs2 tactic 2022-11-08 12:23:36 -08:00
Nikolaj Bjorner
f769e2f1f6 have bool rewriter use flat_and_or, and integrate hoist rewriter 2022-11-08 12:21:50 -08:00
Nikolaj Bjorner
238ea0a264 add shorthands for concatentation 2022-11-08 12:21:25 -08:00
Nikolaj Bjorner
3a4b8e2334 add rewrite rules to bv-rewriter 2022-11-08 12:20:51 -08:00
Nikolaj Bjorner
a34701471f clean up hoist rewriter 2022-11-08 12:20:25 -08:00
Nikolaj Bjorner
cbc5b1f4f6 have theory_recfun use recursive function discriminator to control when it is enabled 2022-11-06 12:09:45 -08:00
Nikolaj Bjorner
8ff1e44a95 add discriminator to whether context contains recursive functions to avoid enabling recursive function solver when there are just macros 2022-11-06 11:58:21 -08:00
Nikolaj Bjorner
a4c2a2b22c use ast_util::mk_not to avoid redundant double negations during nff 2022-11-06 11:57:46 -08:00
Nikolaj Bjorner
78f9e6b31a extend error type message with more information - display the arguments that are passed 2022-11-06 11:57:21 -08:00
Nikolaj Bjorner
d8133a47c2 Update solve_eqs.cpp 2022-11-05 22:47:46 -07:00
Nikolaj Bjorner
6c12aaad74 wip - testing solve-eqs2, added as tactic 2022-11-05 22:42:59 -07:00
Nikolaj Bjorner
4d8860c0bc wip - adding context equation solver 
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
 2022-11-05 10:34:57 -07:00
Nikolaj Bjorner
154b09309b fixing build, wip on model reconstruction integration into dependent-expr-state 2022-11-04 14:04:44 -07:00
Nikolaj Bjorner
7bb962d934 add ad-hoc any-of for cross compatibility and simplifying interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 12:49:55 -07:00
Nikolaj Bjorner
49d1490454 add ad-hoc any-of for cross compatibility and simplifying interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 12:48:30 -07:00
Nikolaj Bjorner
de9368bab0 Update expr_replacer.h 2022-11-04 11:25:39 -07:00
Nikolaj Bjorner
28668c6efc set up model reconstruction trail 2022-11-04 11:25:39 -07:00
Nikolaj Bjorner
84af521514 fixes #6439 #6436 2022-11-04 09:36:06 -07:00
Nikolaj Bjorner
626380b3c7 fixing build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-03 22:08:21 -07:00
Nikolaj Bjorner
e8112a6564 add initial stubs for model reconstruction trail 2022-11-03 21:35:07 -07:00
Nikolaj Bjorner
9007bdf780 move horn_subsume_model_converter to ast/converters 2022-11-03 20:26:02 -07:00
Nikolaj Bjorner
25bb935793 move more converters 2022-11-03 20:18:21 -07:00
Nikolaj Bjorner
06eb460c75 move tactic_params to params 2022-11-03 05:50:46 -07:00
Nikolaj Bjorner
1dca6402fb move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
Nikolaj Bjorner
7b12a5c5a8 build fix 2022-11-03 04:49:20 -07:00
Nikolaj Bjorner
070c5c624a wip - converting the equation solver as a simplifier 2022-11-03 03:35:30 -07:00
Nikolaj Bjorner
c0f483528d working on solve_eqs 2022-11-03 03:35:29 -07:00
Nikolaj Bjorner
e141759768 init solve_eqs 2022-11-03 03:35:29 -07:00
Nikolaj Bjorner
df71e83428 remove incorrect assertion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-02 17:32:09 -07:00
Nikolaj Bjorner
0d97d2214c adding virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-02 09:37:55 -07:00
Nikolaj Bjorner
e57674490f adding simplifiers layer 
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
 2022-11-02 08:51:30 -07:00
Nikolaj Bjorner
1646a41b2f minor fixes 
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
 2022-11-02 08:44:55 -07:00
Nikolaj Bjorner
a409a4a677 enforce flat within QF_BV tactic, cap in-processing var-elim loops 2022-10-27 20:10:55 -07:00
Nikolaj Bjorner
1fae3aa152 rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
Nikolaj Bjorner
fe1b4bf5ce disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary 2022-10-26 23:44:38 -07:00
Nikolaj Bjorner
5352a0106d fix #6426 2022-10-26 12:20:55 -07:00
Nikolaj Bjorner
c62c5e9d23 add opportunistic, missing, bv rewrites 
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
 2022-10-25 10:29:48 -07:00
Nikolaj Bjorner
e1a00f4917 remove unused experimental feature - diff 2022-10-24 16:13:24 -07:00
Nikolaj Bjorner
07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -07:00
Nikolaj Bjorner
7b3a634b8d wip - features and bug-fixes to proof logging 2022-10-18 07:54:49 -07:00
Nikolaj Bjorner
ac1552d194 wip - updates to proof logging and self-checking 
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line.

when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation.

new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation.

z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
 2022-10-16 23:33:30 +02:00
Nikolaj Bjorner
8a30128933 formatting updates 2022-10-13 15:20:24 +02:00
Nikolaj Bjorner
4623117af8 wip - proof hints 2022-10-08 20:12:57 +02: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
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
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
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
eba5a5d141 Merge branch 'master' of https://github.com/z3prover/z3 2022-09-20 20:32:07 -07:00