Weng Shiwei
b70ba6ed73
Update doc for mk_context.
2024-06-16 20:07:49 -04: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
01e47bfe26
fix #7245
2024-06-15 02:29:32 -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
35c1cacf44
fix #7248
2024-06-12 14:26:35 -07:00
Nikolaj Bjorner
b831a589e5
fixes to #7250
2024-06-12 08:50:24 -07:00
Nikolaj Bjorner
49610f5159
fix #7246
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-06-06 08:11:19 +02:00
Nikolaj Bjorner
770c51ad2b
add m_replay_qhead to the trail
2024-05-31 11:54:50 +04:00
Nikolaj Bjorner
c0a7af4420
fix bugs with tracking premises in user propagator in sat/smt
2024-05-31 11:25:09 +04:00
Bruce Mitchener
904a50fe49
Fix compilation error in column_info ( #7235 )
...
Reference to `m_low_bound` should be `m_lower_bound`.
2024-05-27 09:19:29 +04:00
Jakob Rath
e454ae275c
intblast: fix translation of sign_ext ( #7230 )
2024-05-18 19:01:35 -07:00
Nuno Lopes
18a95d89c6
fix assertion failure when printing stats
...
It would crash when number of bin_lemmas == 0
2024-05-18 16:30:26 +01:00
Nikolaj Bjorner
cb50dcabda
fix #7229
2024-05-17 18:28:08 -07:00
Nuno Lopes
552068a71e
let the replayer stop when it encounters a C command with invalid args
2024-05-17 11:10:09 +01:00
Nikolaj Bjorner
8fe357f1f2
Nlsat simplify ( #7227 )
...
* dev branch for simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bugfixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix factorization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* separate out simplification functionality
* reorder initialization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reorder initialization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update README.md
* initial warppers for seq-map/seq-fold
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* expose fold as well
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add C++ bindings for sequence operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add abs function to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add parameter validation to ternary and 4-ary functions for API #7219
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add pre-processing and reorder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add pre-processing and reorder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-14 22:19:33 -07:00
Nikolaj Bjorner
e036a5bd9b
add parameter validation to ternary and 4-ary functions for API #7219
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-11 18:06:18 -07:00
Nikolaj Bjorner
efc893263a
add abs function to API
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-09 20:54:39 -07:00
Nikolaj Bjorner
b120745078
add C++ bindings for sequence operations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-09 20:20:05 -07:00
Nikolaj Bjorner
c7529d0b25
expose fold as well
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-09 14:56:18 -07:00
Nikolaj Bjorner
fc6c4c98e2
initial warppers for seq-map/seq-fold
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-09 14:52:49 -07:00
Nikolaj Bjorner
f9176fb4b7
Update README.md
2024-05-07 11:39:52 -07:00
Nikolaj Bjorner
8f4ffc7caf
add logging for first conflict
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-01 20:50:52 -07:00
Nikolaj Bjorner
2f02278227
add virtual destructor to z3::object class
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-01 16:35:25 -07:00
Nikolaj Bjorner
19eb7225ea
add virtual destructor to z3::object class
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-01 16:20:05 -07:00
Nikolaj Bjorner
231a985bf9
add virtual destructor to z3::object class
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-01 16:17:06 -07:00
Nikolaj Bjorner
04c55c34e5
fix unsoundness bug
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-05-01 14:45:15 -07:00
Nikolaj Bjorner
869643a551
fix memory leak
2024-05-01 10:07:37 -07:00
Nikolaj Bjorner
1ef4354080
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-30 17:52:00 -07:00
Nikolaj Bjorner
aa1a596394
add doc-string
2024-04-30 17:05:40 -07:00
Nikolaj Bjorner
29e724f787
add gc to lemmas, convert bounds constraints to lemmas, add simplification pre-processing beyond equality extraction
2024-04-30 17:05:21 -07:00
Nikolaj Bjorner
b0222cbdaa
temper warning messages from uninitalized pointers
2024-04-30 17:00:49 -07:00
Nikolaj Bjorner
4c070f9e76
add extra fields to nlsat-clause
2024-04-30 17:00:05 -07:00
Nikolaj Bjorner
39dc8861ee
expose comparisons with polynomials, incremental way to extract variables
2024-04-30 16:59:50 -07:00
Nikolaj Bjorner
bc577b93ae
refine precision before taking closest integral value.
2024-04-30 16:58:22 -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
cbef183ae5
type check equality injectivity axiom
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-20 14:57:04 -04:00
Nikolaj Bjorner
e184a9a711
fix translation of bvudiv
2024-04-20 07:32:52 -04:00
Nikolaj Bjorner
0368b52716
add missing expr
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-17 15:16:11 +02: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
43dd6a5436
include mutex
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-11 18:19:58 +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
7b8980f82d
fix regression introduced when testing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-09 11:17:03 -07:00
Nikolaj Bjorner
8d0e66b3e3
fix regression introduced when testing
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-09 11:16:34 -07:00
Nikolaj Bjorner
9a681b1a37
reorg sls
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-04-09 10:44:53 -07:00
