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
|
8691ef1d4d
|
additional bit-vector propagators (#4695)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-18 12:38:29 -07:00 |
|
Nikolaj Bjorner
|
549753845e
|
bv and gc of literals (#4692)
* bv and gc of literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* overload
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* diseq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-17 14:24:07 -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
|
7327023c88
|
add variable replay, remove MacOS from Travis (#4681)
* 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>
* 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>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dbg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* drat and fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move ackerman functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* towards debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing file
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>
* remove csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* replay variables created by solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove old function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix scoped-limit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-08 05:57:07 -07:00 |
|
Nikolaj Bjorner
|
d02b0cde7a
|
running updates to bv_solver (#4674)
* 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>
* 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>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dbg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* drat and fresh
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move ackerman functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* towards debugability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing file
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>
* remove csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-07 20:35:32 -07:00 |
|
Nikolaj Bjorner
|
116390833b
|
prepare for theory plugins
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-02 10:42:18 -07:00 |
|
Nikolaj Bjorner
|
fa9cf0fa0c
|
mk-var during copy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-31 20:34:41 -07:00 |
|
Nikolaj Bjorner
|
ed7d969366
|
elaborate on smt/drat format outline, expose euf mode as config
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-31 19:29:23 -07:00 |
|
Nikolaj Bjorner
|
4d41db3028
|
adding euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-31 14:36:16 -07:00 |
|
Nikolaj Bjorner
|
bee3077640
|
free memory in egraph
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 20:13:46 -07:00 |
|
Nikolaj Bjorner
|
a003af494b
|
release nodes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 20:09:27 -07:00 |
|
Nikolaj Bjorner
|
bbe027f6a1
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 15:03:15 -07:00 |
|
Nikolaj Bjorner
|
25106866b5
|
fix dotnet build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 14:46:31 -07:00 |
|
Nikolaj Bjorner
|
727ea43b16
|
remove lazy push from theory_lra
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 12:07:14 -07:00 |
|
Nikolaj Bjorner
|
e8826bb20f
|
fix #4651
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-30 09:49:12 -07:00 |
|
Nikolaj Bjorner
|
86310a1a27
|
updated sat_smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-29 19:21:51 -07:00 |
|
Nikolaj Bjorner
|
e9a4e486ae
|
dbg
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-29 19:21:50 -07:00 |
|
Nikolaj Bjorner
|
79fc3f2375
|
warnings /errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-29 09:53:24 -07:00 |
|
Nikolaj Bjorner
|
60f8884dbd
|
sr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-28 15:10:52 -07:00 |
|
Nikolaj Bjorner
|
b8fb744935
|
reset caches
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-28 15:09:12 -07:00 |
|
Nikolaj Bjorner
|
93ee2a68a4
|
persist fields
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-28 13:41:50 -07:00 |
|
Nikolaj Bjorner
|
4244ce4aad
|
adding ack/model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-28 12:55:47 -07:00 |
|
Nikolaj Bjorner
|
1a36d44450
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-26 10:41:20 -07:00 |
|
Nikolaj Bjorner
|
c21a2fcf9f
|
sat solver setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-26 09:40:42 -07:00 |
|
Nikolaj Bjorner
|
ecd3315a74
|
add sat-euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-25 12:16:57 -07:00 |
|
Nikolaj Bjorner
|
65e6d942ac
|
euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-08-24 01:55:13 -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
|
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 |
|
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
|
16d34b9fcc
|
fix #4100
|
2020-04-26 13:30:13 -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
|
c70e9af09d
|
fix #3734
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-04 12:53:24 -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
|
e7ec842cf5
|
fix #3348
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-16 12:14:19 -07:00 |
|
Nikolaj Bjorner
|
3d7098ec85
|
fix #3137
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-09 07:15:06 +01:00 |
|
Nikolaj Bjorner
|
7d976e4f4d
|
fix #3120
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-06 06:52:38 +01:00 |
|
Nikolaj Bjorner
|
bd3024e837
|
fix #3161
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-05 17:37:38 +01:00 |
|
Nikolaj Bjorner
|
dd3e77107e
|
rename aig_simplifier to cut_simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 18:29:59 -08:00 |
|
Nikolaj Bjorner
|
a9d22d7409
|
fix #2918
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-01 14:09:40 -08:00 |
|
Nikolaj Bjorner
|
e0a41a18c3
|
add validation to aig_simplifier, start BIG-based masking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-11 20:47:38 -08:00 |
|
Nikolaj Bjorner
|
78a1736bd2
|
prepare symbols to be more abstract, update mbi, delay initialize some modules
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-10 12:02:08 -08:00 |
|
Nikolaj Bjorner
|
ca243428f8
|
make cutset maintainance incremental, expose option for goal2sat to populate aig
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-08 16:39:49 -08:00 |
|
Nikolaj Bjorner
|
57846e50fa
|
use variable id as level, separate cut-set updates, add missing reset in pdd
|
2020-01-08 02:15:45 -08:00 |
|
Nikolaj Bjorner
|
40a4326ad4
|
add anf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-05 16:46:49 -08:00 |
|
Nikolaj Bjorner
|
ca498e20d1
|
move value factories to model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-16 19:48:35 -07:00 |
|
Nikolaj Bjorner
|
185b01dd35
|
fix #2416
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-23 19:01:49 -07:00 |
|
Nikolaj Bjorner
|
41ca956012
|
expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-18 13:45:13 -07:00 |
|