Nuno Lopes
|
689e2d41de
|
remove a bunch of unneeded memory allocations
|
2022-02-25 16:08:23 +00:00 |
|
Nikolaj Bjorner
|
6a412f7f04
|
allow to pass Booleans as arguments to arithmetic expressions
|
2022-01-31 12:00:54 -08:00 |
|
|
Nikolaj Bjorner
|
c2595b9bc8
|
#5379
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-07-06 18:58:27 +02:00 |
|
Nuno Lopes
|
5a66dfad2a
|
change parameter::hash so that the least significant bits arent overriden
the 3rd bit was being stuck by the parameter kind, leading to increased number of hash collisions
|
2021-05-27 09:38:21 +01:00 |
|
|
Nuno Lopes
|
36ca98cbbe
|
ast: remove 2 default constructors
|
2021-05-24 14:59:03 +01:00 |
|
|
Nuno Lopes
|
f8406623b4
|
switch parameter to an std::variant
plus fix mem leak & move constructor for zstrings
|
2021-05-23 13:07:29 +01:00 |
|
|
Nikolaj Bjorner
|
20a67e47ca
|
remove symbol -> zstring -> symbol round-trips
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-05-22 13:12:49 -07:00 |
|
|
Nikolaj Bjorner
|
4a6083836a
|
call it data instead of c_ptr for approaching C++11 std::vector convention.
|
2021-04-13 18:17:35 -07:00 |
|
|
Nuno Lopes
|
a6ef99d56e
|
constify ids of builtin AST families + remove some dead code
|
2021-04-04 18:13:52 +01:00 |
|
|
Nikolaj Bjorner
|
9098084217
|
reduce overhead of creating seq-plugin, enable parameter cleanup for #5095
|
2021-03-15 11:54:44 -07:00 |
|
|
Nikolaj Bjorner
|
8f577d3943
|
remove ast_manager get_sort method entirely
|
2021-02-02 13:57:01 -08:00 |
|
|
Nikolaj Bjorner
|
3ae4c6e9de
|
refactor get_sort
|
2021-02-02 04:45:54 -08:00 |
|
|
Nikolaj Bjorner
|
4455f6caf8
|
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
|
2021-02-02 03:58:19 -08:00 |
|
|
Nikolaj Bjorner
|
6c9bdc949e
|
fix #4848
|
2020-12-07 05:59:55 -08:00 |
|
|
Nikolaj Bjorner
|
768e2c1d0d
|
tune hoist-rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 11:25:17 -08:00 |
|
|
Nikolaj Bjorner
|
72d407a49f
|
mbp (#4741)
* adding dt-solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move mbp to self-contained module
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Create CMakeLists.txt
* dt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename to bool_var2expr to indicate type class
* mbp
* na
* add projection
* na
* na
* na
* na
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* deps
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* testing arith/q
* na
* newline for model printing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-21 15:48:40 -07:00 |
|
|
Nikolaj Bjorner
|
1d8d58710c
|
fix #4725
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-06 08:41:30 -07:00 |
|
|
Nikolaj Bjorner
|
518296dbc1
|
some compile warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-30 15:59:42 -07:00 |
|
|
Nikolaj Bjorner
|
6f63f8761c
|
optimizations to bv-solver and euf-egraph (#4698)
* additional bit-vector propagators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename restrict (not a keyword, but well) #4694, tune euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add pb rewriting to pb2bv #4697
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-20 06:47:27 -07:00 |
|
|
Nikolaj Bjorner
|
6a4261d1af
|
debugging bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-15 15:37:31 -07:00 |
|
|
Nikolaj Bjorner
|
796e2fd9eb
|
arrays (#4684)
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fill
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update drat and fix euf bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* const qualifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reorg ba
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reorg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-13 19:29:59 -07:00 |
|
|
Nikolaj Bjorner
|
59e388ece1
|
handle bind proof constructor and print lambda
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-04 11:59:59 -07:00 |
|
|
Nikolaj Bjorner
|
d3e20d41b2
|
fix $4457
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-02 18:31:28 -07:00 |
|
|
Nikolaj Bjorner
|
9da0b61d30
|
na
|
2020-05-21 21:04:48 -07:00 |
|
|
Nikolaj Bjorner
|
1be22a80f6
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 17:20:18 -07:00 |
|
|
Nikolaj Bjorner
|
884a68251b
|
fix #4266
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 16:53:59 -07:00 |
|
|
Nikolaj Bjorner
|
4938ea7be6
|
fix #4123
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-27 11:44:25 -07:00 |
|
|
Nikolaj Bjorner
|
735888145e
|
fix #4112
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-26 21:04:28 -07:00 |
|
|
Nikolaj Bjorner
|
f9193809ea
|
add recfun rewriting, remove quantifier based recfun
|
2020-04-26 12:59:51 -07:00 |
|
|
Nikolaj Bjorner
|
6a5695463f
|
fix #3943
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 12:58:18 -07:00 |
|
|
Nikolaj Bjorner
|
b066f562c6
|
fix #3904
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 12:50:12 -07:00 |
|
|
Nikolaj Bjorner
|
77e7dcb3c3
|
fix #3874
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-08 16:32:57 -07:00 |
|
|
Nikolaj Bjorner
|
6e8d9001dc
|
fix #3843
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-08 11:08:45 -07:00 |
|
|
Nikolaj Bjorner
|
40aa2f7cb2
|
fix 3838 fix #3837
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-08 05:49:24 -07:00 |
|
|
Nikolaj Bjorner
|
550852bc62
|
fix #3765
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 13:49:26 -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
|
eacde16b3e
|
fix #3199
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 23:55:44 -07:00 |
|
|
Nikolaj Bjorner
|
121a6de32c
|
fix #3748
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 13:22:30 -07:00 |
|
Lev Nachmanson
|
cf3f06ee26
|
use scoped interval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-02 15:58:46 -07:00 |
|
|
Nikolaj Bjorner
|
c6b4641050
|
fix #3649
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-01 10:56:27 -07:00 |
|
|
Nikolaj Bjorner
|
e9bc8e2433
|
fix #3642
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-31 23:38:07 -07:00 |
|
|
Nikolaj Bjorner
|
8a961a5ce9
|
fix #3554
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 15:02:55 -07:00 |
|
|
Nikolaj Bjorner
|
fe81de6d39
|
fix #3555
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:37:38 -07:00 |
|
|
Nikolaj Bjorner
|
f8dcaa8885
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 10:23:00 -07:00 |
|
|
Nikolaj Bjorner
|
c165f69248
|
fix #3525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
|
Nikolaj Bjorner
|
70a1786061
|
scoping th solver to avoid memory leak during cancellation exposed by #3431
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 14:14:45 -07:00 |
|
|
Nikolaj Bjorner
|
d6a2e7ac15
|
fix #3433
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 13:21:48 -07:00 |
|
|
Nikolaj Bjorner
|
6c1d0f6ea0
|
fix #3438
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-22 11:27:20 -07:00 |
|
|
Nikolaj Bjorner
|
c613ab0ba0
|
fix #3286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-14 11:42:26 -07:00 |
|
|
Nikolaj Bjorner
|
31c3ac016a
|
fix #3275
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-13 13:55:12 -07:00 |
|