Nikolaj Bjorner
|
d6298b089d
|
Merge pull request #1799 from c-cube/fix-union-find
fix(union-find): keep values and representative in consistent order
|
2018-08-18 05:51:01 -07:00 |
|
Simon Cruanes
|
5141f05e6d
|
fix(union-find): keep values and representative in consistent order
the merge handlers should be called with r1,r2,v1,v2 or r2,r1,v2,v1
but not a mix
|
2018-08-17 14:58:44 -05:00 |
|
Nikolaj Bjorner
|
12f9336fec
|
disable unused macros
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-15 22:44:07 -07:00 |
|
Nikolaj Bjorner
|
056ec2d5c4
|
remove inc file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-15 22:27:07 -07:00 |
|
Nikolaj Bjorner
|
2b2f193f2b
|
remove dependency on ARRAYSIZE for issue #1616
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-15 22:26:14 -07:00 |
|
Nikolaj Bjorner
|
fd5cfbe402
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-15 10:38:23 -07:00 |
|
Nikolaj Bjorner
|
03bd010b05
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 21:19:06 -07:00 |
|
Nikolaj Bjorner
|
d67bfd78b9
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 21:15:55 -07:00 |
|
Nikolaj Bjorner
|
40a79694ea
|
add job/resource axioms on demand
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 16:33:34 -07:00 |
|
Nikolaj Bjorner
|
2839f64f0d
|
rename to csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 11:05:55 -07:00 |
|
Nikolaj Bjorner
|
a478f95999
|
remove debug assert
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 10:56:52 -07:00 |
|
Nikolaj Bjorner
|
502c071266
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 09:57:06 -07:00 |
|
Nikolaj Bjorner
|
d55fe1ac59
|
na'
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-14 09:41:43 -07:00 |
|
Nikolaj Bjorner
|
a096ec648c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-13 17:11:22 -07:00 |
|
Nikolaj Bjorner
|
540baa88f4
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-13 17:08:34 -07:00 |
|
Nikolaj Bjorner
|
3478b8b924
|
add js-model interfacing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-12 18:14:06 -07:00 |
|
Nikolaj Bjorner
|
0af00e62de
|
abstract arithmetic value extraction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-12 12:42:26 -07:00 |
|
Nikolaj Bjorner
|
abd902d58c
|
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-11 18:14:32 -07:00 |
|
Nikolaj Bjorner
|
95963f71f4
|
fix bug introduced in fix of #1798
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-11 17:18:11 -07:00 |
|
Nikolaj Bjorner
|
d270df67f7
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-08-11 13:33:35 -07:00 |
|
Nikolaj Bjorner
|
96d3b98a44
|
fix #1783, wronge clausification of negated pb inequalities. Signs were ignored
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-11 13:33:09 -07:00 |
|
Nikolaj Bjorner
|
8de8c4cade
|
fix #1798
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-11 11:41:06 -07:00 |
|
Nikolaj Bjorner
|
55f15b0921
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-10 17:52:34 -07:00 |
|
Nikolaj Bjorner
|
a13b6a99d6
|
Merge pull request #1797 from c-cube/conf-dt-lazy-split
expose the configuration param for datatype case splits
|
2018-08-10 16:09:13 -07:00 |
|
Simon Cruanes
|
0aca1ad4c1
|
feat(smt/dt): expose the configuration param for datatype case splits
|
2018-08-10 17:37:23 -05:00 |
|
Nikolaj Bjorner
|
baeff82e59
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-10 09:46:21 -07:00 |
|
Nikolaj Bjorner
|
0d8de8f65f
|
add theory outlline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-09 20:19:26 -07:00 |
|
Nikolaj Bjorner
|
2b968f9e63
|
initial decl plugin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-09 15:29:39 -07:00 |
|
Nikolaj Bjorner
|
d5b2059fdb
|
Merge pull request #1796 from mtrberzi/issue1726-2
fix contains/indexof heuristic precondition and re.loop handling
|
2018-08-07 16:03:13 -07:00 |
|
Murphy Berzish
|
c65dbaea90
|
z3str3: fix contains-indexof precondition
|
2018-08-07 15:12:37 -04:00 |
|
Murphy Berzish
|
7a84486df2
|
Merge branch 'master' into develop
|
2018-08-07 12:57:02 -04:00 |
|
Nikolaj Bjorner
|
8b4e1c1209
|
fix #1793
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-06 18:13:26 -07:00 |
|
Nikolaj Bjorner
|
84c7df75d6
|
record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-06 16:21:27 -07:00 |
|
Nikolaj Bjorner
|
24b6ff90cd
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-08-05 13:49:42 -07:00 |
|
Nikolaj Bjorner
|
a3c692c05f
|
fix include paths
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 13:49:26 -07:00 |
|
Nikolaj Bjorner
|
a33a1ab92b
|
Merge pull request #1790 from NikolajBjorner/master
bmc improvements, move fd_solver to self-contained directory
|
2018-08-05 10:35:39 -07:00 |
|
Nikolaj Bjorner
|
60110bb289
|
reduce dependencies in CMakeLists file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 10:34:13 -07:00 |
|
Nikolaj Bjorner
|
6400da63ab
|
missing file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 10:10:52 -07:00 |
|
Nikolaj Bjorner
|
74efe253a0
|
fix header files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 10:09:23 -07:00 |
|
Nikolaj Bjorner
|
d47e06732c
|
bmc improvements, move fd_solver to self-contained directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 10:02:15 -07:00 |
|
Nikolaj Bjorner
|
e041ebbe80
|
bmc improvements, move fd_solver to self-contained directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-05 10:00:49 -07:00 |
|
Nikolaj Bjorner
|
fd09b1a7d0
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-08-03 22:14:28 -07:00 |
|
Nikolaj Bjorner
|
c247abfc65
|
prepare js output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-03 22:13:25 -07:00 |
|
Nikolaj Bjorner
|
f306f75e36
|
harness internalization and API for #1776
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-02 20:18:27 -07:00 |
|
Nikolaj Bjorner
|
51610842b9
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-02 10:41:53 -07:00 |
|
Nikolaj Bjorner
|
7bd4a313dd
|
expr utilities for pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-02 10:41:07 -07:00 |
|
Nikolaj Bjorner
|
fed977b492
|
fix #1782
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-02 10:08:16 -07:00 |
|
Nikolaj Bjorner
|
39333273a5
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-08-01 17:31:20 -07:00 |
|
Nikolaj Bjorner
|
8b08821112
|
fix #1784, fix #1783
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-01 17:31:14 -07:00 |
|
Lev Nachmanson
|
ed44ffd54d
|
Merge pull request #1781 from levnach/master
unroll static_matrix to avoid dead cells
|
2018-08-01 15:03:39 -07:00 |
|