mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity
19081 commits 23 branches 48 tags 156 MiB
Commit graph

19081 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes 3aacc62229 api: hint the compiler that logging enabled is unlikely 2024-12-28 09:52:36 +00:00
Nuno Lopes bd8c870bbe api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
Nikolaj Bjorner 0b9ed925d6 try dual phase lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 13:34:48 -08:00
Nikolaj Bjorner 1f55ec5cef fix random update to a legal one 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 13:01:47 -08:00
Nikolaj Bjorner c82518ca36 include cmath to define std::pow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 12:29:44 -08:00
Nikolaj Bjorner b0eee16109 fix double override bug in bv_lookahead, integrate with bv_eval 2024-12-27 12:26:18 -08:00
Clemens Eisenhofer 8de0005ab3
Bugfix seq-eq sls (#7495) 
* Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping

* Removed debug code

* One check was missing
 2024-12-27 08:40:34 -08:00
Nikolaj Bjorner 5eb71c3be6 integrate lookahead v1 into repair loop 
this ports some functionality from lookahead solver for qfbv-sls into sls-smt.
 2024-12-26 17:49:30 -08:00
Nikolaj Bjorner c58171478f remove dead code 2024-12-26 13:48:55 -08:00
Nikolaj Bjorner d3a6521185 rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead. 2024-12-26 13:06:28 -08:00
Nikolaj Bjorner 13dcfd26dd remove debug out 2024-12-25 15:23:47 -08:00
Nikolaj Bjorner c9cae77304 update regex membership to be slightly better tuned 2024-12-25 10:56:16 -08:00
Nikolaj Bjorner f4ed432244 try a basic heuristic that finds some string that belongs to re. 2024-12-25 10:10:59 -08:00
Nikolaj Bjorner 09825edcd8 remove compute depth in favor of already existing get_depth 2024-12-23 18:49:54 -08:00
Nikolaj Bjorner e332904fb2 cosmetic updates 2024-12-23 18:49:38 -08:00
Nikolaj Bjorner 85d3041a80 avoid platform non-reproducibility due to argument evaluation ordering 2024-12-23 17:13:51 -08:00
Nikolaj Bjorner 23c4728d68 remove some platform specific behavior 2024-12-23 16:28:10 -08:00
Nikolaj Bjorner 554191885e remove platform dependent print 2024-12-23 16:13:36 -08:00
Nikolaj Bjorner 4f4cafbc98 start update with expr-inverter to handle PB 2024-12-22 18:17:42 -08:00
Nikolaj Bjorner b592ce4707 reserve space in heap to avoid debug check in elim_unconstrained 2024-12-22 18:17:40 -08:00
Nuno Lopes 97c70ba501 remove some uneeded constructors 2024-12-22 15:06:58 +00:00
Nikolaj Bjorner fb5bbb8074 read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0 2024-12-22 14:07:29 +01:00
Nikolaj Bjorner a214dc32e8 add some comments, fix nyis 2024-12-22 13:52:19 +01:00
Nikolaj Bjorner 65b678dd42 use bail_out instead of early return to ensure marks are cleared 2024-12-22 06:14:38 +01:00
Nikolaj Bjorner 78ce6c1c6c revert relevancy override 2024-12-21 18:10:10 +01:00
Nikolaj Bjorner 3b2315d771 remove verbose output 2024-12-21 15:52:57 +01:00
Nikolaj Bjorner 578804acf4 fix #7460 2024-12-21 14:42:23 +01:00
Nikolaj Bjorner 2044fb460d fix #7490 2024-12-21 14:32:02 +01:00
Nikolaj Bjorner 8dec84110b add lia2card tactic as default #7483 2024-12-21 13:11:22 +01:00
Nikolaj Bjorner 4f7b6c794e always copy Microsoft.Z3.xml into package directory #7482 2024-12-21 13:10:05 +01:00
Nikolaj Bjorner 07b1ee5dcc mask regression on fpa by not auto-setting relevancy=0 2024-12-21 12:41:04 +01:00
Nikolaj Bjorner da6a5facca revert change to setup_context that delays it until there are assertions 2024-12-21 11:53:46 +01:00
Nikolaj Bjorner db9f45dfec set relevancy = 0 in auto-config mode when there are bit-vectors and no quantifiers, #7484 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-20 18:10:46 +01:00
Nikolaj Bjorner 114cae50a5 update gcm script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-20 17:27:21 +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
Nuno Lopes e4ab2944fe
Optimize expr_safe_replace for quantifiers when all source patterns are vars (#7481) 
* Update expr_safe_replace.cpp

* Update expr_safe_replace.cpp

* Update expr_safe_replace.cpp
 2024-12-19 23:05:13 +01:00
Nuno Lopes c33bc2c8be expr_abstract: save 1 hashtable lookup per app argument 
when we already know that the app is missing one arg to rewrite
 2024-12-18 09:50:50 +00:00
Nuno Lopes 2f5c0a6985 remove 2 unneeded lambda captures 2024-12-17 16:02:24 +00:00
Nuno Lopes 6f24123f0c reduce hash table lookups in expr_abstract in half 2024-12-16 11:00:55 +00:00
Nikolaj Bjorner a6e59ea45e fix build flags for release.yaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-16 04:41:29 +01:00
Nikolaj Bjorner a97ad76bb6 publish pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-15 13:00:50 -08:00
Nikolaj Bjorner 200ef236da Update RELEASE_NOTES.md 2024-12-15 06:01:44 -08:00
Nikolaj Bjorner e40972b7f7 Update release.yml 
disable publish to pypi during release dry-runs
 2024-12-15 05:55:48 -08:00
Nikolaj Bjorner b529a58b91 add unit test for incremental equation edit distance with repair 2024-12-15 05:53:28 -08:00
Nikolaj Bjorner 31ee56c1ca wip - incremental edit distance algorithm 2024-12-13 09:30:49 -08:00
Nikolaj Bjorner 538f74d64c extract stats with finalize for parallel mode 2024-12-13 09:30:49 -08:00
Oskar Haarklou Veileborg b4295620b3
Add __enter__ and __exit__ methods on Optimize class (#7477) 
This enables the use of the with statement for the Optimize class to
concisely call push() and pop(). This works similarly to the Solver
class.
 2024-12-13 09:19:04 -08:00
Nikolaj Bjorner 1e5c59a06f add repair step for str.replace 2024-12-12 09:15:36 -08:00
Nikolaj Bjorner e8c2360043 fix #7461 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-09 16:57:17 -08:00
Nikolaj Bjorner 8f5658b77d add another baseline heuristic for string equalities, add cases for array axioms. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-09 15:55:19 -08:00