mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
18861 commits 23 branches 48 tags 157 MiB
Commit graph

32 commits

Author SHA1 Message Date
Nikolaj Bjorner 51f1e2655c updates to sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-30 12:59:05 -07:00
Nikolaj Bjorner 738c5b6d0d add warning messages for #7100 2024-01-30 21:30:37 -08:00
Nikolaj Bjorner e321643bf5 move sls core functionality to be independent of tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-22 12:00:52 -08:00
Nikolaj Bjorner 4d9af7848d add parameter to disable pattern inference #6884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:27:37 -07:00
Guido Martínez 3517361a73
Adding some options in support of F* (#6774) 
* patterns: add option for pattern decomposition (pi.decompose_patterns)

True by default, retaining current behavior.

* rewriter: add option for sorting of disjunctions (rewriter.sort_disjunctions)

True by default, retaining current behavior.
 2023-06-20 16:10:37 -07:00
Nikolaj Bjorner 68f43ac7a4 make der selective to configuration. For F*, quantifiers are hand or machine generated in specific formats and the tool depends on e-matching to use precisely the format of the quantifiers that have been entered. For other cases of quantifiers, destructive equality resolution (der) can be expected to offer simplifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-06 16:15:04 -07:00
Nikolaj Bjorner fd97be0e3e move sat.smt.proof.check_rup into solver.proof.check_rup #6616 2023-03-01 21:03:27 -08:00
Nuno Lopes d30cb55bae don't flush stream when printing param vals 2023-01-03 09:35:17 +00:00
Nikolaj Bjorner d47dd159d7 set encoding into gparams because this is the only entry point in zstring #6490 2022-12-14 09:43:29 -08:00
Nikolaj Bjorner c7781f346d move parameter sat.smt.proof to solver.proof.log 
this update breaks use cases that set sat.smt.proof to True.
As it is such a new feature and the change affects possibly at most the tutorial it is made without compatibility layers.
 2022-11-23 11:37:23 +07:00
Nikolaj Bjorner 8afec86fe8 add option for flat_and_or 2022-11-08 12:19:27 -08:00
Nikolaj Bjorner 06eb460c75 move tactic_params to params 2022-11-03 05:50:46 -07: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 a628e4c4e5 updates to printer to get instantiations, take 1 2022-08-25 11:22:35 -07:00
Nikolaj Bjorner 78eaefe5a8 move solver-params to params 2022-08-08 11:34:41 +03:00
Nikolaj Bjorner ea2a843325 flat only 
remove option for uzers (users who are in reality fuzzers) to toggle flat option. The legacy arithmetic solver bakes in assumptions about flat format so it isn't helpful to expose this to fuzzers, I mean uzers.
 2022-06-30 19:59:46 -07:00
Nikolaj Bjorner 431c3af409 fix #5929 - add parameter bv_le2extract to allow disabling the disassembly to extract 2022-03-27 18:23:41 -10:00
Nikolaj Bjorner fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
CEisenhofer 47fdd6c060
Added 16 bit string-encoding (#5540) 2021-09-09 11:35:16 +02:00
Nikolaj Bjorner cf9e55fa96 #5516 
expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes.
 2021-09-01 17:44:17 -07:00
Nuno Lopes 524dcd35f9 reorder fields of context_params to save memory 
plus improve error checking in context_params::set_uint
 2021-04-13 18:35:58 +01:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner 3f93cc3f0b use unicode by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 16:39:31 -08:00
Nikolaj Bjorner dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner 299e1788b8 fix #4808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:03:17 -08:00
Nikolaj Bjorner f354671465 add parameter for scenario from #4743 2020-10-30 01:14:34 -07:00
Nikolaj Bjorner 35e3d8425c move fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 11:16:21 -07:00
Nikolaj Bjorner 11c90cc142 move parameters from ast/rewriter to params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 11:11:16 -07:00
Nikolaj Bjorner 455d53ef27 missing cmakelists 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 10:46:17 -07:00
Nikolaj Bjorner b9cbb08858 shuffle dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:51:39 -07:00