summaryrefslogtreecommitdiff
path: root/src/theory/fp
AgeCommit message (Expand)Author
2021-09-20Fix handling of conversions between FP and reals (#7149)Andres Noetzli
2021-09-13FP: Rename FpConverter to FpWordBlaster. (#7170)Aina Niemetz
2021-09-10FP: Enable caching in the theory inference manager. (#7168)Aina Niemetz
2021-09-10FP: Use EnvObj::rewrite() and options() in theory_fp. (#7169)Aina Niemetz
2021-09-10FP: Do not send trivial lemmas. (#7167)Aina Niemetz
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-07-23FP: Add option to word-blast more lazily. (#6904)Aina Niemetz
2021-06-29FP: Refactor, rewrite and clean up word blasting. (#6802)Aina Niemetz
2021-06-23FP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)Aina Niemetz
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-05-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-21Support braced-init-lists with `mkNode()` (#6580)Andres Noetzli
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-04FP: Move removal of generic to_fp operations to rewriter. (#6480)Aina Niemetz
2021-05-04FP: Move type check from expandDefinitions. (#6479)Aina Niemetz
2021-05-03FP: Rewrite to_fp conversion from signed bit-vector. (#6472)Aina Niemetz
2021-04-30Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)Aina Niemetz
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-20Split FP expand definitions to own module (#6392)Andrew Reynolds
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
2021-04-05[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)Haniel Barbosa
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31FP: Move implementation of type rules from header to .cpp file. (#6241)Aina Niemetz
2021-03-25FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)Aina Niemetz
2021-03-21Clean up remaining raw uses of output channel (#6161)Andrew Reynolds
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-01Eliminate PREPROCESS lemma property (#5827)Andrew Reynolds
2021-01-28Simplify lemma interface (#5819)Andrew Reynolds
2020-12-08Do not check FP at last call if not necessary (#5627)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-11-30fp_converter: Properly separate out symbolic glue code. (#5501)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback