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
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
d0e20e44ff
booyah
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
8dac9b7b94
fix #3814
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-07 10:40:36 -07:00
Bruce Mitchener
e570940662
Prefer using empty rather than size comparisons.
2018-11-27 21:42:04 +07:00
Arie Gurfinkel
3a01fd791b
Replace rule API
2018-09-04 21:49:59 -04: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
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
4bbe1d4674
remove unused min-aggregate
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-04 09:23:36 -08:00
Nikolaj Bjorner
4bc044c982
update header guards to be C++ style. Fixes issue #9
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Alex Horn
132f984d51
Add syntactical min checker
...
The purpose of this patch is to find out more about the "shape" of
the constraints in our benchmarks. In particular, we would like to
determine whether aggregation and negation, together, appear in
recursive rules.
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
2015-06-10 20:19:14 +01:00
Alex Horn
140fb7942d
Add datalog infrastructure for min aggregation function
...
This patch adds an instruction to the datalog interpreter and
constructs a new AST node for min aggregation functions.
The compiler is currently still work in progress and depends on
changes made to the handling of simple joins and the preprocessor.
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
2015-06-10 18:14:14 +01:00
Nikolaj Bjorner
c09903288f
have free variable utility use a class for more efficient re-use
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 16:14:22 -07:00
Nikolaj Bjorner
e4338f085b
re-organization of muz
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-08-28 22:11:33 -07:00
