Nikolaj Bjorner
|
e816d16724
|
fix #2527
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-31 10:09:52 -04:00 |
|
Nikolaj Bjorner
|
4c0db00a7b
|
fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-30 08:31:37 -03:00 |
|
Nikolaj Bjorner
|
de43e05102
|
fix overflow bug exposed by #2476
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-29 22:34:04 -03:00 |
|
Nikolaj Bjorner
|
20dc59e02d
|
fix #2523
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-28 12:28:33 -03:00 |
|
Nikolaj Bjorner
|
2e6908bd9e
|
fix #2509, fix issue with model inheritance exposed by #2483
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-27 10:48:22 -03:00 |
|
Nikolaj Bjorner
|
271cd2ac6b
|
disable expensive model validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-26 07:26:12 -03:00 |
|
Nikolaj Bjorner
|
75a40d8f8e
|
reorder fields, rename overload name clash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-25 16:01:39 -03:00 |
|
Nikolaj Bjorner
|
64f4c9794d
|
fix regressions during string fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-25 10:00:26 +01:00 |
|
Nikolaj Bjorner
|
0d9cd7bc2b
|
addressing misc. string bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-24 15:40:15 +01:00 |
|
Nikolaj Bjorner
|
a337a51374
|
fixes for #2513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-23 23:29:24 +03:00 |
|
Nikolaj Bjorner
|
de69b01e92
|
Lev's fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-23 23:29:24 +03:00 |
|
Nikolaj Bjorner
|
2b2f016f96
|
python for accessing lambda, switch to theory branching for QF_LRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-14 15:44:34 -07:00 |
|
Nikolaj Bjorner
|
520ea65f32
|
move towards theory phase selection, implement getitem on lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-14 15:44:33 -07:00 |
|
Nikolaj Bjorner
|
75962173ff
|
fix #2481
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-12 09:38:45 -07:00 |
|
Nikolaj Bjorner
|
9fa9aa09ff
|
fix #2468, adding assignment phase heuristic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-10 15:25:05 -07:00 |
|
Nikolaj Bjorner
|
8579a004d0
|
distribute concat over bvxor and bvor, #2470
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-07 15:14:58 -07:00 |
|
Nikolaj Bjorner
|
e950453685
|
force propagation for smt cubing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-06 14:19:16 -07:00 |
|
Nikolaj Bjorner
|
0af249d651
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-06 13:44:12 -07:00 |
|
Bruce Mitchener
|
077f518241
|
Fix -Wreorder warning.
|
2019-08-04 18:37:31 -07:00 |
|
Nikolaj Bjorner
|
bc3b0f6e33
|
introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-04 12:00:48 -07:00 |
|
Nikolaj Bjorner
|
01920abf46
|
introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-04 11:57:30 -07:00 |
|
Nikolaj Bjorner
|
59f69bbe0d
|
introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-04 11:56:03 -07:00 |
|
Nikolaj Bjorner
|
2d5714a5d4
|
fixing #2443 #2445 #2447 #2448
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 15:06:34 -07:00 |
|
Nikolaj Bjorner
|
584eee2cf4
|
fixing #2448 and #2445 and #2443
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 15:06:34 -07:00 |
|
Nikolaj Bjorner
|
c4480337c4
|
fixing #2448 and #2445 and #2443
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 15:06:34 -07:00 |
|
Nikolaj Bjorner
|
3d1c40ce23
|
fixing #2448
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 15:06:34 -07:00 |
|
Nikolaj Bjorner
|
0a29002c2f
|
return unknown if m_array_weak was used and result is satisfiable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 00:20:41 +08:00 |
|
Nikolaj Bjorner
|
e1fd167e01
|
remove stale assertions due to lambda #2446
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-30 14:35:09 +08:00 |
|
Nikolaj Bjorner
|
74631265b9
|
remove stale assertions due to lambda #2446
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-30 14:32:06 +08:00 |
|
Nikolaj Bjorner
|
e6df7b73aa
|
fix #2434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-25 09:40:18 -07:00 |
|
Nikolaj Bjorner
|
859512d937
|
fix #2431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 12:14:02 -07:00 |
|
Nikolaj Bjorner
|
019d78e219
|
fix #2422
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-24 09:51:04 -07:00 |
|
Nikolaj Bjorner
|
e593b5b2c8
|
fix #2415
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-20 16:23:01 -07:00 |
|
Nikolaj Bjorner
|
41ca956012
|
expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 13:45:13 -07:00 |
|
Nikolaj Bjorner
|
5820b16800
|
mark assumption literals to be skolem to hide them from models #2406
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 08:25:42 -07:00 |
|
Nikolaj Bjorner
|
1ba6d16c61
|
augment axiomatization for substr to fix #2366
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 08:38:33 +01:00 |
|
Nikolaj Bjorner
|
cfb4d289b8
|
fix #2325
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-11 10:34:35 +01:00 |
|
Nikolaj Bjorner
|
88aa689a70
|
fix #2387, add ite-hoist rewriting, allow assumptions to be compound expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-09 07:40:29 +01:00 |
|
Nikolaj Bjorner
|
cd93cdd819
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-09 07:40:29 +01:00 |
|
Nikolaj Bjorner
|
6d244ed2aa
|
internalize reflect
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-04 07:33:37 +07:00 |
|
Nikolaj Bjorner
|
8e2ad4e461
|
#2379 and #2380
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-04 07:08:47 +07:00 |
|
Nikolaj Bjorner
|
db87f2aab0
|
separate rewriter used by smt context from asserted formulas to avoid term substitution, exposed by #2370
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-02 15:28:21 +07:00 |
|
Nikolaj Bjorner
|
85b0722df0
|
ensure also negative lt are constrained
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-30 07:44:06 +03:00 |
|
Nikolaj Bjorner
|
1f0d162b7f
|
fix segfault #2360
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-30 00:54:48 +03:00 |
|
Nikolaj Bjorner
|
6e994f9279
|
temporarily disable delete
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-29 20:09:33 +03:00 |
|
Nikolaj Bjorner
|
335543b374
|
adding comparison #2360
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-28 21:14:58 -07:00 |
|
Nikolaj Bjorner
|
db274ebe01
|
relax condition for distributing extract over ite #2359
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-23 16:48:42 -07:00 |
|
Nikolaj Bjorner
|
b8734273c8
|
pydoc regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-22 17:49:46 -08:00 |
|
Nikolaj Bjorner
|
e0a44894cf
|
purge smt.timeout, use timeout instead to control solver timing #2354
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-21 16:56:24 +02:00 |
|
Nikolaj Bjorner
|
cbe52e298b
|
remove tracing, fix doctext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-06-21 15:08:26 +02:00 |
|