projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Reimplement support for relational triggers (#7063)
[cvc5.git] / src / theory / fp /
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (... tree | commitdiff
2021-09-13 Aina NiemetzFP: Rename FpConverter to FpWordBlaster. (#7170) tree | commitdiff
2021-09-10 Aina NiemetzFP: Enable caching in the theory inference manager... tree | commitdiff
2021-09-10 Aina NiemetzFP: Use EnvObj::rewrite() and options() in theory_fp... tree | commitdiff
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167) tree | commitdiff
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) tree | commitdiff
2021-06-29 Aina NiemetzFP: Refactor, rewrite and clean up word blasting. ... tree | commitdiff
2021-06-23 Aina NiemetzFP: Remove sections guarded with undefined macro SYMFPU... tree | commitdiff
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) tree | commitdiff
2021-05-27 Aina NiemetzFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD... tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-21 Andres NoetzliSupport braced-init-lists with `mkNode()` (#6580) tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-19 Andrew ReynoldsAdd more missing inference ids (#6313) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-04 Aina NiemetzFP: Move removal of generic to_fp operations to rewrite... tree | commitdiff
2021-05-04 Aina NiemetzFP: Move type check from expandDefinitions. (#6479) tree | commitdiff
2021-05-03 Aina NiemetzFP: Rewrite to_fp conversion from signed bit-vector... tree | commitdiff
2021-04-30 Aina NiemetzAdd parameter name for argument `isPreRewrite` for... tree | commitdiff
2021-04-22 Andrew ReynoldsMove expand definition from Theory to TheoryRewriter... tree | commitdiff
2021-04-20 Andrew ReynoldsSplit FP expand definitions to own module (#6392) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-31 Aina NiemetzFP: Move implementation of type rules from header to... tree | commitdiff
2021-03-25 Aina NiemetzFP: Refactor FloatingPointLiteral in preparation for... tree | commitdiff
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827) tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-30 Aina Niemetzfp_converter: Properly separate out symbolic glue code... tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... tree | commitdiff
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... tree | commitdiff
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492) tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-09-23 Aina NiemetzFP: Use Assert instead of AlwaysAssert in traits::... tree | commitdiff
2020-09-22 Aina NiemetzFP: Use Assert instead of PRECONDITION macro in convert... tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... tree | commitdiff
2020-08-28 Andrew Reynolds(new theory) Update TheoryFP to the new interface ... tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-04 Aina Niemetz--fp-exp: Better warning message. (#3709) tree | commitdiff
2019-12-18 Andres NoetzliAvoid calling rewriter from type checker (#3548) tree | commitdiff
2019-12-13 Aina Niemetz FP converter: convert: Use std::vector as instead... tree | commitdiff
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-06-03 Andres NoetzliEnable SymFPU assertions in production (#3036) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-05 Haniel Barbosafix fp issue (#2940) tree | commitdiff
2019-04-04 Haniel BarbosaIgnoring FP benchmarks with "unsafe" sizes unless optio... tree | commitdiff
2019-04-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-04-01 Andres NoetzliFP: Fix wrong model due to partial assignment (#2910) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-01-15 Andrew Reynolds Fix unsound double abs rewrite rule for FP (#2792) tree | commitdiff
2018-12-19 Andrew ReynoldsFix issues with REWRITE_DONE in floating point rewriter... tree | commitdiff
2018-11-21 MartinObvious rewrites to floating-point < and <=. (#2706) tree | commitdiff
2018-11-21 Andrew Reynolds Fix type enumerator for FP (#2717) tree | commitdiff
2018-10-04 Aina NiemetzFix compiler warnings. (#2585) tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-08-28 Andres NoetzliRemove throw specifiers in FP type checker (#2392) tree | commitdiff
2018-08-28 Andres NoetzliRemove dead code in fp_converter (#2388) tree | commitdiff
2018-07-15 Andres NoetzliAvoid ambiguous overloads in BitVector (#2169) tree | commitdiff
2018-07-06 MartinFeature/fp rewrite improvement (#2154) tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-06-11 Andrew ReynoldsFix equality conflicts reported by FP (#2064) tree | commitdiff
2018-06-04 Andrew ReynoldsEnable cegqi (with model values) for floating point... tree | commitdiff
next