Nikolaj Bjorner
b60e1a2ed2
fixup variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 20:06:45 -07:00
Nikolaj Bjorner
969511ac00
fixup std-order / inv-order
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 19:35:16 -07:00
Nikolaj Bjorner
a98c925069
optimize var_subst
2024-10-03 18:14:47 -07:00
Nuno Lopes
3586b613f7
remove default destructors
2024-10-02 22:20:12 +01:00
Nikolaj Bjorner
328616b8b2
fix build warnings
2024-09-30 17:25:19 -07:00
Nikolaj Bjorner
7da58b9e84
fix build warnings
2024-09-30 10:34:26 -07:00
Nikolaj Bjorner
5413018d86
Update euf_ac_plugin.cpp
2024-09-30 08:43:17 -07:00
Nikolaj Bjorner
826835fd7c
fixes to build warnings
2024-09-30 08:23:31 -07:00
Nikolaj Bjorner
d047b86439
pypi publish
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-26 21:35:28 +01:00
Nikolaj Bjorner
f4452a0348
pypi publish
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-26 21:34:55 +01:00
Nikolaj Bjorner
eb8c63080a
Refactor and fix uninitialized variables and improve function consistency across multiple modules
2024-09-23 13:34:33 +01:00
Nuno Lopes
499ed5d844
remove unneeded iterator functions
2024-09-23 12:59:04 +01:00
Nuno Lopes
737c2208fa
delete more default constructors
...
reduces code size by 0.1%
2024-09-23 12:59:04 +01:00
Nuno Lopes
a62fede64b
remove a few default constructors
2024-09-23 08:17:58 +01:00
Nuno Lopes
22d9bfad35
fix warning with iterators due to non-const comparator
2024-09-23 08:10:56 +01:00
Nikolaj Bjorner
1e580a7f12
update to c++20, remove debug output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-22 21:30:44 +01:00
Nikolaj Bjorner
96c1375786
#7391
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-22 19:35:03 +01:00
Nikolaj Bjorner
a9f8ec1bcb
updated handling of value initialization for bit-vectors
2024-09-22 21:30:11 +03:00
Nikolaj Bjorner
ba5cec7704
additional rewrites for bv2int
2024-09-22 21:29:12 +03:00
Nikolaj Bjorner
fa7fc8ef5e
Refactor bv_rewriter functions using unified variable assignment and early break logic
2024-09-22 13:04:49 +03:00
Nikolaj Bjorner
d66609ea14
fix #7389
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-22 02:41:11 +03:00
Nikolaj Bjorner
0c48a50d59
Add support for initializing variable values in solver and optimize contexts in Z3
2024-09-20 18:28:26 +03:00
Nikolaj Bjorner
8349ee0069
Add support for const array in all logics as per issue #7383
2024-09-19 11:44:18 +03:00
Nuno Lopes
8061765574
remove default destructors & some default constructors
...
Another ~700 KB reduction in binary size
2024-09-04 22:30:23 +01:00
Nuno Lopes
ef58376c14
replace a few old-school constructors for a 0.5% reduction in code size
...
don't waste those 128 KB!
2024-09-02 16:13:46 +01:00
Nikolaj Bjorner
49ba3bc12f
address compiler warnings gcc-13
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-08-26 11:33:54 -07:00
Nikolaj Bjorner
3e518b9e8b
fix #7331
2024-08-06 03:54:25 -07:00
Nikolaj Bjorner
25e683e4e1
fix finalize method
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-07-28 19:10:30 -07:00
Nikolaj Bjorner
ac7014a68b
expose public
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-07-29 03:18:20 +02:00
Nikolaj Bjorner
f94500c3ca
fix #7309
2024-07-28 13:18:08 +02:00
Nikolaj Bjorner
ef86f5fcc2
add partial evaluation cases for algebraic data-types for recursive functions.
2024-06-16 16:07:16 -07:00
Nikolaj Bjorner
81ebd52f61
#7207
...
the utility that computes case analysis is brittle when the body of a function contains ite expressions that are not relevant to recursive unfolding.
The fold-rec occurrences that get inserted to harness large case splits work against throttling case generation: they get treated as recursive functions that have to be guarded.
2024-06-16 15:04:42 -07:00
Nikolaj Bjorner
972d35204c
reshuffle priorities on multiplication allow non-determinism.
2024-06-15 10:47:10 -07:00
Nikolaj Bjorner
a6b502779b
fix #7252
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-06-13 17:52:17 -07:00
Nikolaj Bjorner
b831a589e5
fixes to #7250
2024-06-12 08:50:24 -07:00
Nikolaj Bjorner
2ad9f220f2
add logging
2024-04-30 16:57:59 -07:00
Nikolaj Bjorner
bebcd94703
enable logging nla lemmas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-25 10:29:34 -04:00
Nikolaj Bjorner
2a4f0e785b
tidy
2024-04-20 18:04:10 -04:00
Nikolaj Bjorner
2682c2ef2b
sls updates
...
- add SINGLE_THREAD mode
- add interface to retrieve "best" model so far
2024-04-13 16:42:26 +02:00
Nikolaj Bjorner
c0bdc7cdd6
enable concurrent sls with new solver core
...
allow using sls engine (for bit-vectors) with the new core.
Examples
z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=0 /st C:\QF_BV_SAT\bench_10.smt2
z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st C:\QF_BV_SAT\bench_10.smt2
z3 C:\QF_BV_SAT\bench_11100.smt2 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st
2024-04-11 10:49:30 +02:00
Nikolaj Bjorner
510534dbd4
cleanup
2024-04-10 19:09:30 -07:00
Nikolaj Bjorner
974ea7b68d
maintain ownership of dependency
2024-04-10 17:57:14 -07:00
Nikolaj Bjorner
9a681b1a37
reorg sls
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-09 10:44:53 -07:00
Nikolaj Bjorner
bab7ca2b70
fixes to bv-sls
2024-04-07 14:24:13 -07:00
Nikolaj Bjorner
d7c0e17f96
fixes to tighten-range
2024-04-02 21:12:09 -07:00
Nikolaj Bjorner
2ce202db75
add special handling of lshr, ashr
2024-04-02 21:09:18 -07:00
Nikolaj Bjorner
84092cbd96
add engine-init to control model transfer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-30 15:12:32 -07:00
Nikolaj Bjorner
51f1e2655c
updates to sls
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-30 12:59:05 -07:00
Nikolaj Bjorner
6455de9dd3
fix #7179
...
Ensure that flat associative rewriting is disabled if rewriter.flat is set to false.
2024-03-21 09:39:13 -07:00
someplaceguy
7bbe3fb2b6
fix (get-proof) command to respect option pp.simplify_implies ( #7157 )
2024-03-09 15:13:42 -08:00
