Nikolaj Bjorner
4773bec975
check for null before debug assertions
2024-12-30 09:44:23 -08:00
Nikolaj Bjorner
d8741b4aec
have apply-update check can_set instead of caller
2024-12-30 08:56:09 -08:00
Nikolaj Bjorner
bcf66f214f
code cleanup, add comments
2024-12-30 08:51:49 -08:00
Nuno Lopes
322dcec531
Add 2 new API functions to get depth & groundness of exprs ( #7479 )
...
* Update api_ast.cpp
* Update z3_api.h
2024-12-30 08:49:43 -08:00
Dmitri
f99e1ee581
Support BitVectors in the TypeScript Optimize API ( #7480 )
...
This is just a change in type declarations to allow calling minimize/maximize with BitVectors.
2024-12-30 08:49:30 -08:00
Clemens Eisenhofer
19c95f8561
Add new string repair heuristic ( #7496 )
...
* Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping
* Removed debug code
* One check was missing
* Trying different update generation function
* Renamed function
* Added parameter to select string update function
2024-12-30 08:49:07 -08:00
Clemens Eisenhofer
e002c57aa2
Fixed range regex ( #7497 )
2024-12-30 08:48:09 -08:00
Nikolaj Bjorner
d81de1a67e
align updated version of lookahead with legacy heuristics
2024-12-29 21:22:32 -08:00
Nikolaj Bjorner
6ea68310c9
fix stack overflow regression in bool_rewriter
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-28 18:21:59 -08:00
Nikolaj Bjorner
3526d03cca
remove VERIFY output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-28 18:01:32 -08:00
Nikolaj Bjorner
f41134d1b6
h
...
- avoid more platform specific behavior when using m_mk_extract,
- rename mk_eq in bool_rewriter to mk_eq_plain to distinguish it from mk_eq_rw
- rework bv_lookahead to be more closely based on sls_engine, which has much better heuristic behavior than attempt 1.
2024-12-28 17:40:25 -08:00
Nikolaj Bjorner
a5bc5ed813
try uneven lookahead skew
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-12-28 17:40:25 -08:00
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
