mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-11 17:54:43 +00:00
Code Activity
17752 commits 25 branches 49 tags 159 MiB
Commit graph

530 commits

Author SHA1 Message Date
Nikolaj Bjorner
eba0732629 fix #6675 
disable remove_unused_defs from pb-solver until it is integrated with model reconstruction.
 2023-04-12 19:50:13 -07:00
Nikolaj Bjorner
bb44b91e45 fix #6677 2023-04-10 15:11:10 -07:00
Nikolaj Bjorner
d1c7ff1a36 add unconstrained elimination for sequences 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
9ce5fe707d track assumptions when parsing into a solver. This enables solver.from_file/solver.from_string to support assumptions/cores #6587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-14 11:09:11 -08:00
Nikolaj Bjorner
839f87a10c don't apply tactics in parse mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 20:50:53 -08:00
Nikolaj Bjorner
550619bfcf add API for creating and attaching simplifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 17:06:03 -08:00
Nikolaj Bjorner
8495be11f9 add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model 2023-01-31 13:34:52 -08:00
Nikolaj Bjorner
971b9d4081 fix #6564 
fixes to simplifier command front-end
 2023-01-31 09:32:34 -08:00
Nikolaj Bjorner
238d604a10 android 16 byte alignment for stack allocated memory? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 23:00:44 -08:00
Nikolaj Bjorner
6022c17131 Add simplification customization for SMTLIB2 
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
 2023-01-30 22:38:51 -08:00
Nikolaj Bjorner
25b0b1430c move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532 2023-01-12 12:42:28 -08:00
Nikolaj Bjorner
fcea32344e add missing tactic descriptions, add rewrite for tamagochi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 13:32:26 -08:00
Nikolaj Bjorner
21362c0b98 make case-def and recfun-num-rounds re-parsable for logging 2023-01-04 15:00:25 -08:00
Nikolaj Bjorner
1dca6402fb move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
Nikolaj Bjorner
fc30461828 unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-20 09:09:06 -07:00
Nikolaj Bjorner
f6595c161f add examples with proof replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-19 17:43:56 -07:00
Nikolaj Bjorner
d4885abdc0 fix #6400 
bi-implication was treated as an atomic formula leading to incorrect projection.
 2022-10-17 11:00:21 -07:00
Nikolaj Bjorner
d88384fd51 fix compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-16 15:03:46 -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
993ff40826 fixes to proof logging and checking 2022-10-15 12:42:50 +02:00
Nikolaj Bjorner
a2e0646eed wip - proof checker 2022-10-12 09:34:49 +02:00
Nikolaj Bjorner
de69874076 wip - adding proof checkers, fixes to quantifier proof certificates 2022-10-10 09:46:22 +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
Nikolaj Bjorner
5c9f69829b fixes to trim 2022-10-07 09:58:12 +02: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
c1c659dc93 trying trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-04 16:25:40 +02: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
cffe5fe1a5 remove debug print 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-10-01 17:05:36 -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
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
6a61efbf99 add missing override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-05 13:35:53 -07:00
Nikolaj Bjorner
3011b34b3b log E-matching based quantifier instantiations as hints 2022-08-31 18:59:02 -07:00
Nikolaj Bjorner
4abff18e8d fill in missing pieces of proof hint checker for Farkas and RUP 
The proof validator based on SMT format proof logs uses RUP to check propositional inferences and has plugins for theory axioms/lemmas.
 2022-08-31 05:29:15 -07:00
Nikolaj Bjorner
0f475f45b5 Add RUP checking mode to proof checker. 2022-08-30 09:45:19 -07:00
Nikolaj Bjorner
8b8caf9ded re-add smt-solver for proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-28 18:19:30 -07:00
Nikolaj Bjorner
37fab88de0 respect dependencies, move proof_cmds to extra_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-28 18:16:43 -07:00
Nikolaj Bjorner
f65a244385 move proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-28 18:11:26 -07:00
Nikolaj Bjorner
e2f4fc2307 overhaul of proof format for new solver 
This commit overhauls the proof format (in development) for the new core.

NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.

It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):

- assume  - for input clauses
- learn   - when a clause is learned (or redundant clause is added)
- del     - when a clause is deleted.

The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.

Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.

Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```

Run z3 on a file with above content.
Then run z3 on f.proof

```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```
 2022-08-28 17:44:33 -07:00
Nikolaj Bjorner
2f8b13368d add redirect for warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-23 15:55:55 -07:00
Nikolaj Bjorner
b169292743 add parameter descriptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-16 08:26:53 -07:00
Bruce Mitchener
5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Bruce Mitchener
3e38bbb009
Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
Nikolaj Bjorner
32614722ef fix #6176 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-20 21:19:20 -07:00
Andrea Lattuada
af80bd18ce
Flush the trace stream before displaying sat results (#6162) 2022-07-14 13:43:57 -07:00
Nikolaj Bjorner
894fb836e2 fix build break (debug assertion) and isolate gomory functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-13 17:26:56 -07:00