Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update z3 #100

Merged
merged 609 commits into from
Sep 27, 2023
Merged

Update z3 #100

merged 609 commits into from
Sep 27, 2023

Conversation

jurajsic
Copy link
Member

Uptade base z3 to v4.12.2

NikolajBjorner and others added 30 commits January 31, 2023 12:32
@NikolajBjorner
remove empty file
e6f8fe3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix release message
6d8d8f1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
add shortcut filter to avoid traversing model reconstruction trail if…
8495be1 
… there are no intersections with model
@NikolajBjorner
check if trail is empty to avoid collecting variables
88bf3c6
@NikolajBjorner
fix build
ebc2cd5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
add API for creating and attaching simplifiers
550619b 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
add ocaml signature for simplifier
4c6d44f 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
disambiguate overloaded with for Julia bindings
162fa3d 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
update ml api
17bae9b 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
update ml api
9a94a9a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
update ml api
1289937 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
update ml api
d51d518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
update ml api
63c0f35 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@dependabot
Bump docker/build-push-action from 3.3.0 to 4.0.0 (Z3Prover#6562)
151a623
@NikolajBjorner
protecting add_simplifier API against mis-use
19fed09 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
use setter method to easier track updates to settings.
0f86a00
@NikolajBjorner
initialize field
682e868 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix warning
38d526e 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix warnings
30fa37e 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix test
7767144 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix incremental pre-processing to work with assumptions/cores and con…
6c7dd4a 
…sequences

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix incremental pre-processing to work with consequences/cubes
72e7a8a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
add simplifiers to .net API
2e068e3
@NikolajBjorner
add simplifier to java API
4143c54
@NikolajBjorner
compiler warning
ed4a84e 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
compiler warning
efbecb1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
compiler warning fix
741634b 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
remove unused field
0d05104 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
compiler warnings/bugs
39d2818 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
don't apply tactics in parse mode
839f87a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner and others added 21 commits April 26, 2023 10:04
@NikolajBjorner
add gcd-conflicts stats, formatting updates
ace6e8e
@NikolajBjorner
count gcd conflicts
59bc070
@NikolajBjorner
count gcd conflicts, log row id in rows
50c855e
@NikolajBjorner
remove references to validating
3029fb2
@NikolajBjorner
add instrumentation to theory_lra for shuffling final check
d2e3e48
@NikolajBjorner
ensure assume-eqs is invoked after check-lia statically
ef94334 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
adding stubs to find fixed variables
c48dc69 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix regressions Z3Prover#6703
d5231f8 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix processing of else expression for model table
392266c
@NikolajBjorner
formatting updates
c64d61b
@NikolajBjorner
make default argument to ensure_def and mk_def explicit
f176917 
- insert also macro definitions into models
@NikolajBjorner
remove debug output
6c24a70 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@gbagan
JS/TS: add Optimize class (Z3Prover#6712)
0c9a5f6 
* implement  Optimize class for the high level Typescript API

* javascript and wasm: add _malloc to exported functions

fix the bug Z3Prover#6709

* javascript: add tests for the Optimize class

* javascript: no reason that minimize and optimize must be constants
@NikolajBjorner
fix Z3Prover#6713 fix Z3Prover#6714
2e441e3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Merge branch 'master' of https://github.com/z3prover/z3
62e1ec0
@aehyvari
Implement proposed smtlib2 bitvector overflow predicates (Z3Prover#6715)
12e45c9 
* Logical names for function declarations in c++

Currently, for example, the function declaration symbol member for
checking whether multiplication *does not* overflow is called
`m_bv_smul_ovfl`.  Since we are introducing the upcoming smtlib2 symbols
that check that multpliciation *does* overflow, the not overflow check
symbols are renamed to `m_bv_smul_no_ovfl` etc.

* Implement smtlib overflow preds for multiplication

Smtlib2 is being extended to include overflow predicates for bit
vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI).
This commit introduces the predicates `bvumulo` and `bvsmulo` that
return `true` if the unsigned multiplication overflows or the signed
multiplication underflows or overflows, respectively.

* Move mul overflow predicates to BV logic

* Add a todo on illogical argument order

* Implement mk_unary_pred for bv

* Implement bvnego

* Implement bvuaddo

* Implement bvsaddo

* Implement bvusubo

* Implement bvssubo

* Implement bvsdivo
@NikolajBjorner
reformat code to remove brackets
f6ab5a6
@NikolajBjorner
remove output
046b80f 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
disable publish
ba91100 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
updated release notes for 12.2
e417f7d 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@jurajsic
Merge branch 'master' into update_z3
1ba1904
@jurajsic
Copy link
Member Author

Results:

# of formulae: 100031
###################################################################################
####                                   Table 1                                 ####
###################################################################################
| method                     |   max |    mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|-------|---------|----------|------------|-------------|------------|
| z3-noodler-1ba1904-40ca1cd |   132 | 7.04448 |     0.03 |    28.477  |        4307 |       8287 |
| cvc5-1.0.8                 |   132 | 2.81598 |     0.02 |    17.993  |        1772 |          2 |
| z3-4.12.2                  |   132 | 5.2186  |     0.04 |    23.1857 |        2857 |        213 |
| z3str4                     |   132 | 2.3607  |     0.02 |    15.8903 |        1380 |       1385 |
| z3-noodler-0ae38ae-40ca1cd |   132 | 7.04192 |     0.03 |    28.5098 |        4317 |       8291 |

image
image
image

@vhavlena
Copy link
Collaborator

Great! Is it with the newest mata?

@jurajsic
Copy link
Member Author

Not yet, I want to run it after merging this.

@jurajsic
Copy link
Member Author

The table is wrong, the times are broken, this is the correct version:

# of formulae: 100031
###################################################################################
####                                   Table 1                                 ####
###################################################################################
| method                     |    max |     mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|----------|----------|------------|-------------|------------|
| z3-noodler-1ba1904-40ca1cd | 119.58 | 0.889365 |     0.03 |    6.62393 |        4307 |       8287 |
| cvc5-1.0.8                 | 119.36 | 0.485156 |     0.02 |    4.81569 |        1772 |          2 |
| z3-4.12.2                  | 119.29 | 1.48289  |     0.04 |    8.11434 |        2857 |        213 |
| z3str4                     | 118.44 | 0.519939 |     0.02 |    3.77544 |        1380 |       1385 |
| z3-noodler-0ae38ae-40ca1cd | 119.83 | 0.871344 |     0.03 |    6.61873 |        4317 |       8291 |

@jurajsic jurajsic merged commit f211b89 into devel Sep 27, 2023
0 of 9 checks passed
@jurajsic jurajsic deleted the update_z3 branch September 27, 2023 19:27
Adda0
Adda0 reviewed Oct 2, 2023
View reviewed changes
Copy link
Collaborator

@Adda0 Adda0 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Adda0 Adda0 Adda0 left review comments

@vhavlena vhavlena Awaiting requested review from vhavlena

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.