Nikolaj Bjorner
|
669a1d63da
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-03-18 16:36:16 -07:00 |
|
Nikolaj Bjorner
|
6010d751ed
|
fix #5903
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-03-18 16:21:47 -07:00 |
|
Hari Govind V K
|
f26c12a9ad
|
fix #5882. Use model true when inlining (#5892)
|
2022-03-09 12:31:39 -08:00 |
|
Nikolaj Bjorner
|
bbadd17d56
|
fix #5874
|
2022-03-02 08:46:28 -08:00 |
|
Nikolaj Bjorner
|
2b6dadcbc6
|
fix #5869
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2022-02-28 17:02:13 -08:00 |
|
Nikolaj Bjorner
|
7f149a36d7
|
refining model update rules for del_rule #5865 #5866
|
2022-02-25 08:03:46 -08: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 |
|
Nuno Lopes
|
23e6adcad3
|
fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string
|
2020-07-11 20:24:45 +01:00 |
|
Nikolaj Bjorner
|
a884201d62
|
remove using insert_if_not_there2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-25 15:08:51 -07:00 |
|
Nikolaj Bjorner
|
1fce2905ec
|
fix #3832
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-09 19:38:08 -07:00 |
|
Nikolaj Bjorner
|
b889b110ee
|
bool_vector, some spacer tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-05 12:59:04 -07:00 |
|
Arie Gurfinkel
|
9109968e55
|
Cleanup fixedpoint options
Replace pdr options with spacer
Repace fixedpoint module with fp
|
2018-06-14 16:08:52 -07:00 |
|
Nikolaj Bjorner
|
9279cbfbac
|
don't reinit assumptions when the solver is unsat. fixes #1502
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-24 16:30:08 +09:00 |
|
Nikolaj Bjorner
|
7b6f51941c
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-21 22:18:47 +09:00 |
|
Nikolaj Bjorner
|
54b00f357b
|
fix rule inlining, add WithParams to pass parameters directly to python API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-02-21 21:57:54 +09:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Nikolaj Bjorner
|
2c97eb1393
|
include information whether rule is reachable in del_rule model converter for simpler model presentation #1241
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-15 11:46:28 -08:00 |
|
Nikolaj Bjorner
|
2b82fd5d0c
|
updated include directives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-01 10:51:47 -07: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 |
|
Arie Gurfinkel
|
af28057980
|
preserve dl rule names during xforms
|
2017-06-20 22:23:55 -04:00 |
|
Nikolaj Bjorner
|
22808a039d
|
working on udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-21 20:25:11 -07:00 |
|
Nikolaj Bjorner
|
c09903288f
|
have free variable utility use a class for more efficient re-use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-09-15 16:14:22 -07:00 |
|
Nikolaj Bjorner
|
ddbff6f77b
|
revamp configuration parameter names for fixedpoint
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-08-18 01:03:11 -07:00 |
|
Nikolaj Bjorner
|
4957e71408
|
make get_vars populate all indices with sorts even if variable does not occur in rule. This makes the use of get_vars less prone to callers having to double check for null pointers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-07-21 17:12:39 +02:00 |
|
Nikolaj Bjorner
|
d6de73a2d1
|
fix model converter in inliner. Bug reported by Sagar Chaki
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-07-06 18:11:57 +02:00 |
|
Nikolaj Bjorner
|
084a6f35eb
|
fix bug reported by Nuno Lopes: inlining is unsound for negated predicates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-01-02 17:37:35 -08:00 |
|
Nikolaj Bjorner
|
716663b04a
|
avoid creating full tables when negated variables are unitary, add lazy table infrastructure, fix coi_filter for relations, reduce dependencies on fixedpoing_parameters.hpp header file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-09-08 05:52:18 -07:00 |
|
Nikolaj Bjorner
|
0d56499e2d
|
re-organize muz_qe into separate units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2013-08-28 21:20:24 -07:00 |
|