mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 03:11:30 +00:00
Code Activity
21795 commits 42 branches 58 tags 185 MiB
Commit graph

77 commits

Author SHA1 Message Date
Copilot
2436943794
Standardize for-loop increments to prefix form (++i) (#8199) 
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-14 19:55:31 -08:00
Arie Gurfinkel
51d3c279d0
QEL: Fast Approximated Quantifier Elimination (#6820) 
* qe_lite: cleanup and comment

no change to code

* mbp_arrays: refactor out partial equality (peq)

Partial array equality, PEQ, is used as an intermediate
expression during MBP for arrays. We need to factor it out
so that it can be shared between MBP-QEL and existing MBP.

Partial array equality (peq) is used in MBP for arrays.
Factoring this out to be used by multiple MBP implementations.

* rewriter: new rewrite rules

These rules are specializes for terms that are created in QEL.
QEL commit is comming later

* datatype_rw: new rewrite rule for ADTs

The rule handles this special case:

    (cons (head x) (tail x)) --> x

* array_rewriter rules for rewriting PEQs

Special rules to simplify PEQs

* th_rewriter: wire PEQ simplifications

* spacer_iuc: avoid terms with default in IUC

Spacer prfers to not have a term representing default value of an array.
This guides IUC from picking such terms in interpolation

* mbp_term_graph: replace root with repr

* mbp_term_graph: formatting

* mbp_term_graph: class_props, getters, setters

Class properties allow to keep information for an equivalence class.

Getters and setters for terms allow accessing information

* mbp_term_graph: auxiliary methods for qel

QEL commit is comming later in the history

* mbp_term_graph: bug fix

* mbp_term_graph: pick, refine repr, compute cgrnd

* mbp_term_graph: internalize deq

* mbp_term_graph: constructor

* mbp_term_graph: optionally internalize equalities

Reperesent equalities explicitly by nodes in the term_graph

* qel

* formatting

* comments on term_lt

* get terms and other api for mbp_qel

* plugins for mbp_qel

* mbp_qel_util: utilities for mbp_qel

* qe_mbp: QEL-based mbp

* qel: expose QEL API

* spacer: replace qe_lite in qe_project_spacer by qel

This changes the default projection engine that spacer uses.

* cmd_context: debug commands for qel and mbp_qel

New commands are

  mbp-qel -- MBP with term graphs
  qel     -- QEL with term graphs
  qe-lite -- older qelite

* qe_mbp: model-based rewriters for arrays

* qe_mbp: QEL-based projection functions

* qsat: wire in QEL-based mbp

* qsat: debug code

* qsat: maybe a bug fix

Changed the code to follow the paper by adding all predicates above a given
level, not just predicates of immediately preceding level.

* chore: use new api to create solver in qsat

* mbp_term_graph use all_of idiom

* feat: solver for integer multiplication

* array_peq: formatting, no change to code

* mbp_qel_util: block comment + format

* mbt_term_graph: clang-format

* bug fix. Move dt rewrite to qe_mbp

* array_peq: add header

* run clang format on mbp plugins

* clang format on mul solver

* format do-while

* format

* format do-while

* update release notes

---------

Co-authored-by: hgvk94 <hgvk94@gmail.com>
Co-authored-by: Isabel Garcia <igarciac@uwaterloo.ca>
 2023-08-02 09:34:06 -07:00
Nikolaj Bjorner
68a437e615 revert to logging conflict to get EUF trim to work 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-25 09:45:35 -07:00
Nikolaj Bjorner
3d8f75b3d8 enable on-clause with dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-18 16:59:02 -07:00
Nikolaj Bjorner
f0d3cbe39d add dependency tracking to proof from trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-04 16:24:09 +02:00
Nikolaj Bjorner
ae29a54876 categorize theory axioms as inferences in output to capture justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-04 09:12:58 +02:00
Nikolaj Bjorner
d9e7b8c21f fixes to trim 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-03 19:26:19 +02:00
Nikolaj Bjorner
5f22e98396 fix #6766 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-18 10:05:34 -07: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
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
ab045f0645 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-09-30 16:52:19 -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
f65a244385 move proof_cmds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-28 18:11:26 -07: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
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
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
937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner
2f756da294
adding dt-solver (#4739) 
* adding dt-solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move mbp to self-contained module

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Create CMakeLists.txt

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename to bool_var2expr to indicate type class

* mbp

* na
 2020-10-18 15:28:21 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
794aafa6f8 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-23 12:14:34 -06:00
Nikolaj Bjorner
4e81085292 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-21 10:29:42 -06:00
Nikolaj Bjorner
78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner
9566d379d6 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 19:44:56 -07:00
Nikolaj Bjorner
9bd4050e0c use ref-vector for shared occurrences to avoid hash-table overhead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 13:43:39 -08:00
Nikolaj Bjorner
0d400a5ad6 fix bit2bool bug reported by Jianying Li 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-04 07:46:53 -08:00
Nikolaj Bjorner
bd53fa801e handle case input format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 21:42:18 -07:00
Nikolaj Bjorner
20fc573d5b add laxer check for oeq_quant_intro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 11:24:56 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
9ba76a1332 fixing eufi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ec8e3f2aee consolidate use of plugin by moving declarations up front (separate from constructor at this point) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
ba504e4243 debugging mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:52 -07:00