Nikolaj Bjorner
|
0ce1c34d81
|
fix #5065 - regression solving str.from_int equations now that it isn't injective any longer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-03-02 12:59:48 -08:00 |
|
Nikolaj Bjorner
|
4455f6caf8
|
move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail
|
2021-02-02 03:58:19 -08:00 |
|
Nikolaj Bjorner
|
b02c698284
|
align variable names with dimacs input
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-08 16:52:10 -08:00 |
|
Nikolaj Bjorner
|
cf4bf7b591
|
more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-02 18:44:53 -05:00 |
|
Bruce Mitchener
|
b7d1753843
|
Use override rather than virtual.
|
2018-02-09 21:19:27 +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 |
|
Christoph M. Wintersteiger
|
1724811e1b
|
qffp tactic cleaned up to be in line with the default behavior of other tactics.
|
2016-03-30 15:23:46 +01:00 |
|
Christoph M. Wintersteiger
|
cc04fdbd70
|
Added eager ackermannization to QF_FP, so that small numbers of unspecified operators are eliminated upfront.
|
2016-03-17 17:52:26 +00:00 |
|
Christoph M. Wintersteiger
|
cbf8bd8de1
|
Enabled proof & core production in fpa2bv and qffp.
|
2015-10-25 15:56:42 +00:00 |
|
Christoph M. Wintersteiger
|
f84d6bf5bb
|
Bugfix for QF_FP tactic
|
2015-06-12 12:58:07 +01:00 |
|
Christoph M. Wintersteiger
|
5ae2dd9c74
|
Bugfix for QF_FP default tactic.
|
2015-05-30 15:20:07 +01:00 |
|
Christoph M. Wintersteiger
|
ba88648468
|
Added has_fp_to_real probe to detect when QF_FP need QF_NRA.
|
2015-05-29 14:49:53 +01:00 |
|
Christoph M. Wintersteiger
|
85419ca503
|
Added branch into QF_NRA from QF_FP problems containing to_real terms.
|
2015-05-29 14:21:27 +01:00 |
|
Christoph M. Wintersteiger
|
6f575689b1
|
Added injection of auxiliary lemmas for fp.isNaN, so that the value propagation can pick up these values and propagate them.
Fixes #96.
|
2015-05-21 19:02:09 +01:00 |
|
Christoph M. Wintersteiger
|
5e60bcd920
|
FPA: fixes for the fpa_rewriter to enable model extraction and validation.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-02-06 16:53:31 +00:00 |
|
Christoph M. Wintersteiger
|
5344d6f3c0
|
various bugfixes and extensions for FPA
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-15 19:25:49 +00:00 |
|
Christoph M. Wintersteiger
|
0cedd32ea2
|
More renaming floats -> fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 13:47:26 +00:00 |
|
Christoph M. Wintersteiger
|
5e5758bb25
|
More float -> fpa renaming
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-08 13:37:18 +00:00 |
|