Nikolaj Bjorner
|
493671aa72
|
fix #3520
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:58:06 -07:00 |
|
Nikolaj Bjorner
|
498864c582
|
adding dump facility for cancelation #2095, easing dimacs in/out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-01-24 12:21:23 -08:00 |
|
Bruce Mitchener
|
cdfc19a885
|
Use nullptr.
|
2018-10-02 09:11:19 +07:00 |
|
Nikolaj Bjorner
|
fdcedee887
|
hardening pop abuse and exception safety for #1776
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-30 09:56:16 -07:00 |
|
Nikolaj Bjorner
|
bfeb15b876
|
move to list of clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-14 16:08:50 -07:00 |
|
Arie Gurfinkel
|
26339119e4
|
solver::check_sat_cc : check_sat assuming cube and clause
Extends check_sat with an ability to assume a single clause in
addition to assuming a cube of assumptions
|
2018-06-14 16:08:50 -07:00 |
|
Nikolaj Bjorner
|
fa0c75e76e
|
rename to core2 to avoid overloaded virtual
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-07 15:13:13 -08:00 |
|
Nikolaj Bjorner
|
5a8154c156
|
fix errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-07 14:47:16 -08:00 |
|
Nikolaj Bjorner
|
0d15b6abb7
|
add stubs for converting assertions, consolidate filter_model_converter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-17 14:51:13 -08: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
|
8d2b70a5e2
|
better encodings for at-most-1, #755
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-10 23:46:03 -07:00 |
|
Christoph M. Wintersteiger
|
f54a7db108
|
Added debug traces.
|
2016-08-09 16:36:49 +01:00 |
|
Nikolaj Bjorner
|
8221a09659
|
fast path for antecedent extraction in smt_context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-28 16:49:19 -07:00 |
|
Nikolaj Bjorner
|
ec565ae7a0
|
fixes to #596 and #592: use exponential step increments on integer problems, align int.to.str with canonizer and disequality checker
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-17 01:00:42 -07:00 |
|
Nikolaj Bjorner
|
3d7eb12117
|
tracking use of assumptions in tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-09 21:33:08 -08:00 |
|
Ken McMillan
|
51aa10821e
|
fixed pop issue and interpolation proof mode issue
|
2014-08-26 13:46:53 -07:00 |
|
Leonardo de Moura
|
8198e62cbd
|
solver factories, cleanup solver API, simplified strategic solver, added combined solver
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-11 17:47:27 -08:00 |
|
Leonardo de Moura
|
8d6a091083
|
fixed bugs found in regression tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-07 07:36:40 -08:00 |
|
Leonardo de Moura
|
e2f6a65aa2
|
added support for named assertions
|
2012-11-02 14:00:43 -07:00 |
|
Leonardo de Moura
|
e1eb3ee8ee
|
fixed bug in solver_na2as
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-02 11:36:59 -07:00 |
|
Leonardo de Moura
|
33c165490c
|
fixed solver_na2as
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-02 09:43:07 -07:00 |
|
Leonardo de Moura
|
d545f187f8
|
working on named assertions support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-02 08:28:34 -07:00 |
|