Nikolaj Bjorner
a74c01c8b9
#5528
2021-09-01 20:39:54 -07:00
Nikolaj Bjorner
b1002638ab
#5324
2021-06-06 21:14:17 -07:00
Nikolaj Bjorner
eed87807c5
#5324
2021-06-06 10:41:10 -07:00
Nikolaj Bjorner
0810720267
#5223
2021-05-02 10:30:35 -07:00
Nikolaj Bjorner
5cfe273460
#5211
...
```
(declare-fun v5 () Bool)
(declare-fun i1 () Int)
(declare-fun i2 () Int)
(declare-fun i4 () Int)
(declare-fun i5 () Int)
(declare-fun i6 () Int)
(declare-fun i9 () Int)
(declare-fun i10 () Int)
(assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
(check-sat)
```
2021-04-22 22:10:39 -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
Nikolaj Bjorner
974ef3c147
port equality propagation changes to new core
2021-03-28 16:15:04 -07:00
Nikolaj Bjorner
a152bb1e80
remove template Context dependency in every trail object
2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
4d55f83654
misc
2020-12-04 16:59:13 -08:00
Nikolaj Bjorner
12198d13ac
fix #4794
2020-12-02 12:24:35 -08:00
Nikolaj Bjorner
620204bbb4
use value function in lar_solver ( #4771 )
...
* use value function in lar_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add missing return
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* check_feasible is called after column is added for fixed variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
2020-11-03 01:08:24 -08:00
Nikolaj Bjorner
fb6e7e146b
test mbi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-30 17:03:04 -07:00
Nikolaj Bjorner
8d76470a8a
fixes to mostly solver arith/euf and backtracking scopes
2020-10-26 11:06:41 -07:00
Nikolaj Bjorner
1ee2ba2a9b
mbqi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-26 11:06:40 -07: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
44679d8f5b
arith_solver ( #4733 )
...
* porting arithmetic solver
* integrating arithmetic
* lp
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>
2020-10-16 10:49:46 -07:00
Nikolaj Bjorner
07deb6ee88
remove pragma once
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-10-12 13:22:37 -07:00
Nikolaj Bjorner
4f0c743e2b
add stubs for arithmetic
2020-10-12 11:24:08 -07:00
