mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity
19793 commits 44 branches 51 tags 170 MiB
Commit graph

113 commits

Author SHA1 Message Date
Lev Nachmanson
119e54f3a9 remove some debug output 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-30 15:39:00 -07:00
Lev Nachmanson
6712b769a6 t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-30 14:36:14 -07:00
Lev Nachmanson
fd4cc17689 t0 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2025-06-30 13:52:52 -07:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
 2025-05-28 14:31:25 +01:00
Nikolaj Bjorner
87f7a20e14 Add (updated and general) solve_for functionality for arithmetic, add congruence_explain to API to retrieve explanation for why two terms are congruent Tweak handling of smt.qi.max_instantations 
Add API solve_for(vars).
It takes a list of variables and returns a triangular solved form for the variables.
Currently for arithmetic. The solved form is a list with elements of the form (var, term, guard).
Variables solved in the tail of the list do not occur before in the list.
For example it can return a solution [(x, z, True), (y, x + z, True)] because first x was solved to be z,
then y was solved to be x + z which is the same as 2z.

Add congruent_explain that retuns an explanation for congruent terms.
Terms congruent in the final state after calling SimpleSolver().check() can be queried for
an explanation, i.e., a list of literals that collectively entail the equality under congruence closure.
The literals are asserted in the final state of search.

Adjust smt_context cancellation for the smt.qi.max_instantiations parameter.
It gets checked when qi-queue elements are consumed.
Prior it was checked on insertion time, which didn't allow for processing as many
instantations as there were in the queue. Moreover, it would not cancel the solver.
So it would keep adding instantations to the queue when it was full / depleted the
configuration limit.
 2024-12-19 23:27:57 +01:00
Nikolaj Bjorner
05e053247d add facility to solve for a linear term over API 2024-11-30 09:34:27 -08:00
Nikolaj Bjorner
48712b4f60 Add initial value setting for variables in Z3 API, solver, and optimize modules 2024-09-18 16:13:15 +03:00
Nikolaj Bjorner
adad468cd7 allow copy within a user scope #6827 
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
 2023-07-31 19:46:08 -07:00
Nikolaj Bjorner
b451735aa0 fix #6778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-06-25 21:08:13 -07:00
Nikolaj Bjorner
f6d411d54b experimental feature to access congruence closure of SimpleSolver 
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.

```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
 2022-12-30 21:41:27 -08: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
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
Clemens Eisenhofer
e11496bc65
Added decide-callback to user-propagator (#5978) 
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate

* Added decide-callback to user-propagator

* Refactoring

* Fixed index
 2022-04-15 20:07:17 +02:00
Nikolaj Bjorner
3cc9d7f443 improve pre-processing 2022-04-15 12:55:26 +02:00
Nikolaj Bjorner
2e00f2f32d
Propagator (#5845) 
* user propagator without ids

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

* user propagator without ids

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

* fix signature

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

* references #5818

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

* fix c++ build

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

* switch to vs 2022

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

* switch 2022

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

* Update propagator example (I) (#5835)

* fix #5829

* na

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

* switch to vs 2022

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

* Adapted the example to the changes in the propagator

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* context goes out of scope in stack allocation, so can't used scoped context when passing objects around

* parameter check

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

* add rewriter

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

* Fixed bug in user-propagator "created" (#5843)

Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
 2022-02-17 09:21:41 +02:00
Nikolaj Bjorner
3f3d058567 extract also units from search state 2022-02-07 06:16:22 +02: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
f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner
4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner
9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner
5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -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
0ec567fe15 integrate v2 of lns 2021-02-04 15:47:40 -08:00
Nikolaj Bjorner
fb1509d011 expose internal API for set_phase 2021-02-02 14:29:06 -08:00
Nikolaj Bjorner
f519c58ace Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 
Usage:
z3 4924.smt2 smt.candidate_models=true
 2020-12-30 14:38:41 -08:00
Nikolaj Bjorner
367e5fdd52
delay internalize (#4714) 
* adding array solver

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

* use default in model construction

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

* debug delay internalization

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

* bv

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

* arrays

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

* get rid of implied values and bounds

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

* redo egraph

* remove out

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

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
03276b12b1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-22 19:12:02 -07:00
Nikolaj Bjorner
96f10b8c1c user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-22 19:01:04 -07:00
Nikolaj Bjorner
2d5b749745 extend solver callbacks with methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 19:24:59 -07:00
Nikolaj Bjorner
080be7a2af merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 12:14:28 -07:00
Nikolaj Bjorner
77088745d0 missing override specifiers per #4654 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-20 11:25:52 -07:00
Nikolaj Bjorner
4857d60c99 user propagator over the API 2020-08-18 21:53:02 -07:00
Nikolaj Bjorner
0c93c7aa08 adding user propagation to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-18 10:30:10 -07:00
Nikolaj Bjorner
152c95f72a adding user-propagator ability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-17 22:39:55 -07:00
Nikolaj Bjorner
ca3ec22b7a handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-16 23:29:24 -07:00
Nikolaj Bjorner
59d8895d15 add accessors for implied values to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-28 19:46:39 -07:00
Nikolaj Bjorner
e8ef9a85a4 fix #4327 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 13:22:13 -07:00
Nikolaj Bjorner
a6e7ed039c fix #3587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:18:37 -07:00
Nuno Lopes
d79692b185 remove unused file & hide a few symbols 2020-01-31 17:13:28 +00:00
Nikolaj Bjorner
c560ee54e8 fix #2802 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-13 13:02:58 -08:00
Nikolaj Bjorner
e950453685 force propagation for smt cubing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 14:19:16 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
d2dcb39c11 add smt lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-17 20:24:29 +03:00
Nikolaj Bjorner
89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner
8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Nikolaj Bjorner
74621e0b7d first eufi example running 
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
Nikolaj Bjorner
bfeb15b876 move to list of clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:50 -07:00