Nikolaj Bjorner
|
ecb43ccca2
|
update smt logging format to follow SAT solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-20 20:00:20 -07:00 |
|
Nikolaj Bjorner
|
c41abf2241
|
fix #4624 #4633 #4632 #4631
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-13 08:36:16 -07:00 |
|
Nikolaj Bjorner
|
59d8895d15
|
add accessors for implied values to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-28 19:46:39 -07:00 |
|
Nikolaj Bjorner
|
ac39ddb43f
|
flush gmc for sat-preprocessor model bug #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-26 14:30:48 -07:00 |
|
Nikolaj Bjorner
|
45855fce06
|
fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-22 10:45:29 -07:00 |
|
Nikolaj Bjorner
|
dd5e2e8930
|
check for 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-22 10:44:00 -07:00 |
|
Nuno Lopes
|
bb26f219fe
|
remove unneeded constructors (last round)
|
2020-07-12 17:41:57 +01:00 |
|
Nuno Lopes
|
23e6adcad3
|
fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string
|
2020-07-11 20:24:45 +01:00 |
|
Nikolaj Bjorner
|
ec3066c28a
|
#4532 - arithmetic using SAT for interpreted atoms such as (< 0 0)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 11:43:32 -07:00 |
|
Nikolaj Bjorner
|
d0e20e44ff
|
booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 15:56:30 -07:00 |
|
Nikolaj Bjorner
|
85cb0293f5
|
fix #4541
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-24 20:26:59 -07:00 |
|
Jack Yao
|
55cd1e996c
|
add sat option for doing a global simplification before the bounded search and the main CDCL search loop. The option is also used for the sat-preprocess tacitc (#4514)
Co-authored-by: rainoftime <rainoftime@gmail.com>
|
2020-06-12 16:45:50 -07:00 |
|
Nikolaj Bjorner
|
5f9973d8c4
|
fix #4508
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-07 16:28:53 -07:00 |
|
Nikolaj Bjorner
|
e52eed325c
|
close #4450
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-04 09:22:38 -07:00 |
|
Nuno Lopes
|
7ac2791482
|
remove a bunch of constructors to avoid copies
still not enough to guarantee that vector::expand doesnt copy (WIP)
|
2020-06-03 17:09:27 +01:00 |
|
Nikolaj Bjorner
|
ea1f50b77e
|
simplify extended contains patterns
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-28 19:11:29 -07:00 |
|
Nuno Lopes
|
903725314c
|
fix gcc 9/10 warnings
|
2020-05-23 16:39:09 +01:00 |
|
Alexey Vishnyakov
|
3b0c40044f
|
SINGLE_THREAD: do not use pthread if possible (#4382)
|
2020-05-19 09:45:41 -07:00 |
|
Nikolaj Bjorner
|
f538ee3fe2
|
another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:07:39 -07:00 |
|
Nikolaj Bjorner
|
73fa5995d4
|
fix #4316
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-13 19:35:17 -07:00 |
|
Nikolaj Bjorner
|
603b5552fa
|
port progation from cons branch
|
2020-05-06 12:21:01 -07:00 |
|
Nikolaj Bjorner
|
b81ab94db7
|
pipeline with release mode (#4206)
* pipeline with release mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-04 12:30:03 -07:00 |
|
Nikolaj Bjorner
|
5e4276b0bd
|
fix #4197
|
2020-05-03 10:26:11 -07:00 |
|
Nikolaj Bjorner
|
71e9bf1053
|
initialize local variable
|
2020-04-28 16:36:53 -07:00 |
|
Nikolaj Bjorner
|
16d34b9fcc
|
fix #4100
|
2020-04-26 13:30:13 -07:00 |
|
Nikolaj Bjorner
|
95a78b2450
|
updates to seq and bug fixes (#4056)
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4037
* nicer output for skolem functions
* more overhaul of seq, some bug fixes
* na
* added offset_eq file
* na
* fix #4044
* fix #4040
* fix #4045
* updated ignore
* new rewrites for indexof based on #4036
* add shortcuts
* updated ne solver for seq, fix #4025
* use pair vectors for equalities that are reduced by seq_rewriter
* use erase_and_swap
* remove unit-walk
* na
* add check for #3200
* nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* name a type
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove fp check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove unsound axiom instantiation for non-contains
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix rewrites
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4053
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4052
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 13:18:55 -07:00 |
|
Nikolaj Bjorner
|
5e0c34cae2
|
fix #3953
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 09:43:03 -07:00 |
|
Nikolaj Bjorner
|
b4e7730034
|
fix #3938
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 13:05:53 -07:00 |
|
Nikolaj Bjorner
|
9b609af8fc
|
fix #3924
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 16:19:54 -07:00 |
|
Nikolaj Bjorner
|
c85113acdb
|
fix #3928
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 15:25:08 -07:00 |
|
Nikolaj Bjorner
|
b42b329d6c
|
initialize best-phase-size #3897
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-10 12:04:55 -07:00 |
|
Nikolaj Bjorner
|
bd0620f245
|
fix #3815
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-06 19:28:51 -07:00 |
|
Nuno Lopes
|
346d852bbd
|
fix build
|
2020-04-06 11:19:04 +01:00 |
|
Nikolaj Bjorner
|
b9c9687caf
|
bool_vector
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 18:14:56 -07:00 |
|
Nikolaj Bjorner
|
da6297f31f
|
bool_vector
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 17:41:19 -07:00 |
|
Nikolaj Bjorner
|
b889b110ee
|
bool_vector, some spacer tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 12:59:04 -07:00 |
|
Nikolaj Bjorner
|
1949a978ce
|
fix #3760
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 11:39:25 -07:00 |
|
Nikolaj Bjorner
|
7e8753cd3f
|
fix #3726
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 18:48:09 -07:00 |
|
Nikolaj Bjorner
|
031b3a55ef
|
fix #3733 persist uninterpreted atoms across calls to incremental sat solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 13:11:39 -07:00 |
|
Nikolaj Bjorner
|
c70e9af09d
|
fix #3734
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 12:53:24 -07:00 |
|
Nikolaj Bjorner
|
6f65051f2c
|
silence some build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 17:11:34 -07:00 |
|
Nikolaj Bjorner
|
426e4cc75c
|
fix #3557
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 16:37:59 -07:00 |
|
Nikolaj Bjorner
|
0b856638e9
|
fix #3721
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 15:31:44 -07:00 |
|
Nikolaj Bjorner
|
9092cdc3a5
|
remove stdout
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 10:42:17 -07:00 |
|
Nikolaj Bjorner
|
50624723af
|
fix #3704
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 10:38:31 -07:00 |
|
Nikolaj Bjorner
|
26192e848c
|
fix #3675
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-02 17:41:06 -07:00 |
|
Nikolaj Bjorner
|
8290cfadcc
|
fix #3694
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-02 08:05:43 -07:00 |
|
Nikolaj Bjorner
|
9109a29a15
|
fix #3653 cubing could convert internal variables to external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-01 11:42:20 -07:00 |
|
Nikolaj Bjorner
|
3574a95e50
|
fix #3647
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-01 03:52:59 -07:00 |
|
Nikolaj Bjorner
|
9d759a187e
|
fix #3643
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-01 00:19:05 -07:00 |
|