Nikolaj Bjorner
|
3a70b6aab4
|
fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-13 11:12:27 -07:00 |
|
Nikolaj Bjorner
|
709a5d9524
|
fix bug: & -> &&
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-24 16:09:12 -07:00 |
|
Nikolaj Bjorner
|
05a784fa9e
|
fix issue #535
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-24 08:16:19 -07:00 |
|
Zephyr Pellerin
|
b13db1e82e
|
Bugfix for arith_rewriter single operand division
|
2016-03-04 18:26:00 -08:00 |
|
Nikolaj Bjorner
|
baee4225a7
|
reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-11 16:21:24 -08:00 |
|
Nikolaj Bjorner
|
035f2bb0da
|
disable unsound simplification of root objects, and incorrect evaluation of negative even roots
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-09 08:41:59 -08:00 |
|
Christoph M. Wintersteiger
|
bd94b59a92
|
Bugfix for arith rewriter to avoid rewriting loops.
|
2015-11-03 13:00:10 +00:00 |
|
Christoph M. Wintersteiger
|
27140c527c
|
trailing whitespace
|
2015-11-03 12:56:29 +00:00 |
|
Nikolaj Bjorner
|
7838213675
|
eliminate to_real coersions to make mixed integer problems easier to digest. Issue #277
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-10-30 15:12:21 -07:00 |
|
Nikolaj Bjorner
|
23313e5bdc
|
remove unsound simplification for rem. Codeplex Issue 76
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-03-02 17:24:40 -08:00 |
|
Leonardo de Moura
|
97bf9418f7
|
Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-02-20 13:41:08 -08:00 |
|
Leonardo de Moura
|
c4f762028f
|
Add support for abs (absolute value) function in theory arith (it is part of the SMT-LIB 2.0 standard)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-02-03 15:28:56 -08:00 |
|
Leonardo de Moura
|
a99b8fe797
|
exposed rewriter parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-12-02 22:03:30 -08:00 |
|
Leonardo de Moura
|
cf28cbab0a
|
saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-29 17:19:12 -08:00 |
|
Leonardo de Moura
|
0a4446ae26
|
reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-23 22:14:35 -07:00 |
|