Nikolaj Bjorner
|
115203e87c
|
fixes to sat.euf ematching #5573
|
2021-10-16 15:52:37 -07:00 |
|
Nikolaj Bjorner
|
52032b9ef8
|
#5467
|
2021-10-12 10:16:15 -07:00 |
|
Nikolaj Bjorner
|
2973d3bdc1
|
fix #5392
|
2021-07-07 23:43:30 +02:00 |
|
Nikolaj Bjorner
|
00deb12238
|
signed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-05-21 15:51:27 -07:00 |
|
Nikolaj Bjorner
|
03d2c5f3d0
|
consolidate literals
|
2021-05-20 12:58:27 -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
|
0b0efa83ca
|
debugging #5127
|
2021-04-06 20:09:50 -07:00 |
|
Nikolaj Bjorner
|
026065ff71
|
streamline pb solver interface and naming after removal of xor
|
2021-02-28 12:32:04 -08:00 |
|
Nikolaj Bjorner
|
be50f38903
|
enforce sign coherence #4740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 14:30:00 -08:00 |
|
Nikolaj Bjorner
|
638ef9ed03
|
enforce sign coherence #4740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 14:28:49 -08:00 |
|
Nikolaj Bjorner
|
c07cfc0e69
|
include path to thread and guard by SINGLE_THREAD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-29 16:43:15 -07:00 |
|
Nikolaj Bjorner
|
ac4bcb9034
|
update logging for lemmas
|
2020-10-29 15:09:23 -07:00 |
|
Nikolaj Bjorner
|
601ba2a361
|
#4765
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-10-29 12:10:00 -07:00 |
|
Nikolaj Bjorner
|
367e5fdd52
|
delay internalize (#4714)
* adding array solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use default in model construction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* debug delay internalization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* get rid of implied values and bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* redo egraph
* remove out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-28 19:24:16 -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
|
2d52367368
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-09-15 16:45:11 -07:00 |
|
Nikolaj Bjorner
|
80cc45c5c1
|
display justifications compactly for tracing #4575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-08 13:32:41 -07:00 |
|
Nikolaj Bjorner
|
ee9c797822
|
address #3886 and #3891 by revamping nl_arith decoupling of monomial analysis and access
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-10 01:33:46 -07:00 |
|
Nikolaj Bjorner
|
066413516f
|
disable temp debug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-09 19:39:31 -07:00 |
|
Nikolaj Bjorner
|
c4b52edb29
|
add back assertion for #3849
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-09 18:08:40 -07:00 |
|
Nikolaj Bjorner
|
ee8aa50750
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Nikolaj Bjorner
|
e16c62d6e2
|
don't reset core after it has been populated for the cut #3451 and presumably other bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-25 19:43:55 -07:00 |
|
Lev Nachmanson
|
c562a1f883
|
remove debug code and improve printing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-02-04 16:08:24 -08:00 |
|
Nikolaj Bjorner
|
5f2720562b
|
adding threads to smt core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-01-31 17:08:53 -08:00 |
|
Lev Nachmanson
|
882b8ee63b
|
NB's review
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
f5c8ead995
|
port Grobner
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
3e0cf4b96d
|
port Grobner: fixes in nex simplifications
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
8eaa2bfb02
|
sort nla_expr
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
97ef190f4f
|
full recursion on horner, not finished
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
73e63e1ad9
|
fix a bug in nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
e49dbbe465
|
fix ordered lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
54ba889b7b
|
debug order lemma, introduce sign for factors
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
b32f2703d4
|
fix in emonomials
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Lev Nachmanson
|
8cdf754990
|
debug emons
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-01-28 10:04:21 -08:00 |
|
Nikolaj Bjorner
|
7e415c1b69
|
update to logging
|
2019-12-04 23:08:41 +03:00 |
|
Nikolaj Bjorner
|
2f6a9ba39b
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-12-03 20:34:56 +01:00 |
|
Nikolaj Bjorner
|
23029daf5e
|
investigating relevancy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-11-05 17:16:30 +01:00 |
|
Nikolaj Bjorner
|
e816d16724
|
fix #2527
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-31 10:09:52 -04:00 |
|
Nikolaj Bjorner
|
a337a51374
|
fixes for #2513
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-23 23:29:24 +03:00 |
|
Nikolaj Bjorner
|
48fc3d752e
|
add clause proof module, small improvements to bapa
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-30 15:49:19 -07:00 |
|
Nikolaj Bjorner
|
94dae2da3a
|
fix fourth bug produced by repros by Mark Dunlop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-27 18:11:18 -08:00 |
|
Nikolaj Bjorner
|
442e47dfce
|
fix datatype occurs check bug reported by Gerhard Schellhorn
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-17 16:34:26 -08:00 |
|
Nikolaj Bjorner
|
f2e636c598
|
record simplified input clauses as lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-16 16:37:21 -08:00 |
|
Nikolaj Bjorner
|
0b84c60886
|
fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-14 01:25:25 -08:00 |
|
Nikolaj Bjorner
|
f8a3300026
|
introduce proxies to differentiate from arithmetical variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-12-29 11:13:15 +08:00 |
|
Nikolaj Bjorner
|
184ae7211e
|
fix #1897
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-23 10:00:57 -07:00 |
|
Nikolaj Bjorner
|
4ffd860375
|
narrowing incorrect lemma generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-11 11:31:19 -07:00 |
|
Nikolaj Bjorner
|
1cb3f7c792
|
fixing #1520
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-28 18:03:13 -07:00 |
|
Nikolaj Bjorner
|
e39107c682
|
turn lemma-id into an attribute on the cotext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-10 21:26:51 -07:00 |
|
Nikolaj Bjorner
|
5e5f46f0f8
|
handle cancelation from nra_solver gracefully
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-10 17:34:45 -07:00 |
|