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
Nikolaj Bjorner
dcaacf5e9b
add rewrite glue for instantiating equalities, #7154
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-07 15:21:26 -08:00
Nikolaj Bjorner
d6f522e205
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
531bda39ac
fix alias bug
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
657aaf9a0f
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
22616da63b
updates
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
5be8872d6a
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
dfd5c27fec
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
803f0f0c65
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
5455603910
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
9888d87294
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
f46c3782d6
bugfixes
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
d774f07eb3
add eval field to sls-valuation to track temporary values.
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
8f139e862c
updates to multiplication
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
2590d672f4
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
58474df438
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
0e5b504c30
remove bw setting
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
a328366c7d
move to single path mode for search
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
c451e4e50b
na
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
63804c5296
na
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
74e73f2b84
reorg to use datatypes
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
48026edd7f
move to hide bits
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
acc9c21653
move to hide bits
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
cfa6bd4534
update python build dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
b14499f230
prepare for sls experiment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
cf72a916f8
bugfixes, adding plugin solver
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
659e384ee7
bugfixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
cd6382f1c8
fix alias bug
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-05 12:28:30 -08:00
