Nikolaj Bjorner
|
33525007ab
|
try #4984
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-31 22:15:00 -08:00 |
|
|
Nikolaj Bjorner
|
46f754c43d
|
add priority queue to instantiation
|
2021-01-31 16:17:52 -08:00 |
|
|
Nikolaj Bjorner
|
4af9132f2e
|
more ematching
|
2021-01-29 13:39:14 -08:00 |
|
|
Nikolaj Bjorner
|
f48fb8d3e8
|
it just works
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 11:12:05 -08:00 |
|
|
Nikolaj Bjorner
|
8a229bf684
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-27 22:39:02 -08:00 |
|
|
Nikolaj Bjorner
|
579caab025
|
na
|
2021-01-27 19:35:34 -08:00 |
|
|
Nikolaj Bjorner
|
680b185872
|
adding ematching engine, fixing seq_unicode
|
2021-01-22 17:10:45 -08:00 |
|
|
Nikolaj Bjorner
|
60ef60dff8
|
euf solver updates
|
2021-01-07 17:32:04 -08:00 |
|
|
Nikolaj Bjorner
|
374ae52d70
|
testing mbi
|
2020-12-26 13:49:59 -08:00 |
|
|
Nikolaj Bjorner
|
ab199dedf9
|
debug arith/mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-02 12:13:19 -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
|
2f756da294
|
adding dt-solver (#4739)
* 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
|
2020-10-18 15:28:21 -07:00 |
|
|
Nikolaj Bjorner
|
72b1e8a714
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-12 13:36:40 -07:00 |
|
|
Nikolaj Bjorner
|
1131fedb23
|
finish front-matter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-05 17:14:03 -07:00 |
|
|
Nikolaj Bjorner
|
fa58a36b9f
|
model refactor (#4723)
* refactor model fixing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing cond macro
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add macros dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* deps and debug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add dependency to normal forms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* compile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix leal regression
* complete model fixer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fold back private functionality to model_finder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* avoid duplicate fixed callbacks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-05 14:13:05 -07:00 |
|
Nuno Lopes
|
458572323a
|
remove unneded #pragma once
|
2020-09-30 11:36:16 +01:00 |
|
|
Nikolaj Bjorner
|
1d199b707b
|
connect mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-29 23:51:31 -07:00 |
|
|
Nikolaj Bjorner
|
5df2715064
|
q
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-29 13:43:51 -07:00 |
|