projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Reimplement support for relational triggers (#7063)
[cvc5.git]
/
src
/
theory
/
fp
/
2021-09-21
Andres Noetzli
Fix handling of conversions between FP and reals (...
tree
|
commitdiff
2021-09-13
Aina Niemetz
FP: Rename FpConverter to FpWordBlaster. (#7170)
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Enable caching in the theory inference manager...
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Use EnvObj::rewrite() and options() in theory_fp...
tree
|
commitdiff
2021-09-10
Aina Niemetz
FP: Do not send trivial lemmas. (#7167)
tree
|
commitdiff
2021-09-07
Andres Noetzli
Use `EnvObj` methods instead of `Theory` methods (...
tree
|
commitdiff
2021-08-17
Gereon Kremer
Push Env class into TheoryState (#7012)
tree
|
commitdiff
2021-08-16
Gereon Kremer
Make Theory class use Env (#7011)
tree
|
commitdiff
2021-07-23
Aina Niemetz
FP: Add option to word-blast more lazily. (#6904)
tree
|
commitdiff
2021-06-29
Aina Niemetz
FP: Refactor, rewrite and clean up word blasting. ...
tree
|
commitdiff
2021-06-23
Aina Niemetz
FP: Remove sections guarded with undefined macro SYMFPU...
tree
|
commitdiff
2021-06-16
Aina Niemetz
Make symfpu a required dependency. (#6749)
tree
|
commitdiff
2021-05-27
Aina Niemetz
FP: 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 Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-21
Andres Noetzli
Support braced-init-lists with `mkNode()` (#6580)
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Add more missing inference ids (#6313)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-04
Aina Niemetz
FP: Move removal of generic to_fp operations to rewrite...
tree
|
commitdiff
2021-05-04
Aina Niemetz
FP: Move type check from expandDefinitions. (#6479)
tree
|
commitdiff
2021-05-03
Aina Niemetz
FP: Rewrite to_fp conversion from signed bit-vector...
tree
|
commitdiff
2021-04-30
Aina Niemetz
Add parameter name for argument `isPreRewrite` for...
tree
|
commitdiff
2021-04-22
Andrew Reynolds
Move expand definition from Theory to TheoryRewriter...
tree
|
commitdiff
2021-04-20
Andrew Reynolds
Split FP expand definitions to own module (#6392)
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
tree
|
commitdiff
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove 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 Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-31
Aina Niemetz
FP: Move implementation of type rules from header to...
tree
|
commitdiff
2021-03-25
Aina Niemetz
FP: Refactor FloatingPointLiteral in preparation for...
tree
|
commitdiff
2021-03-21
Andrew Reynolds
Clean 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 Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove partial UDIV/UREM operators. (#6069)
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-01
Andrew Reynolds
Eliminate PREPROCESS lemma property (#5827)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Simplify lemma interface (#5819)
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Do not check FP at last call if not necessary (#5627)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-11-30
Aina Niemetz
fp_converter: Properly separate out symbolic glue code...
tree
|
commitdiff
2020-11-30
Andrew Reynolds
Remove includes for old API from internal code (#5536)
tree
|
commitdiff
2020-11-21
Aina Niemetz
Rename symfpu_literal.(h.in|cpp) -> floatingpoint_liter...
tree
|
commitdiff
2020-11-20
Aina Niemetz
RoundingMode: Rename enum values to conform to code...
tree
|
commitdiff
2020-11-20
Aina Niemetz
FloatingPoint: Separate out symFPU glue code. (#5492)
tree
|
commitdiff
2020-11-18
Aina Niemetz
FloatingPoint: Clean up and document header, format...
tree
|
commitdiff
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
tree
|
commitdiff
2020-09-23
Aina Niemetz
FP: Use Assert instead of AlwaysAssert in traits::...
tree
|
commitdiff
2020-09-22
Aina Niemetz
FP: Use Assert instead of PRECONDITION macro in convert...
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-08-31
Andrew Reynolds
Simplify 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 Reynolds
Extend the standard Theory template based on equality...
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use 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 Niemetz
Update copyright headers.
tree
|
commitdiff
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-04
Aina Niemetz
--fp-exp: Better warning message. (#3709)
tree
|
commitdiff
2019-12-18
Andres Noetzli
Avoid 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 Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-06-03
Andres Noetzli
Enable SymFPU assertions in production (#3036)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-05
Haniel Barbosa
fix fp issue (#2940)
tree
|
commitdiff
2019-04-04
Haniel Barbosa
Ignoring FP benchmarks with "unsafe" sizes unless optio...
tree
|
commitdiff
2019-04-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-04-01
Andres Noetzli
FP: Fix wrong model due to partial assignment (#2910)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-01-15
Andrew Reynolds
Fix unsound double abs rewrite rule for FP (#2792)
tree
|
commitdiff
2018-12-19
Andrew Reynolds
Fix issues with REWRITE_DONE in floating point rewriter...
tree
|
commitdiff
2018-11-21
Martin
Obvious 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 Niemetz
Fix compiler warnings. (#2585)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Remove unused CMakeLists.txt
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-08-28
Andres Noetzli
Remove throw specifiers in FP type checker (#2392)
tree
|
commitdiff
2018-08-28
Andres Noetzli
Remove dead code in fp_converter (#2388)
tree
|
commitdiff
2018-07-15
Andres Noetzli
Avoid ambiguous overloads in BitVector (#2169)
tree
|
commitdiff
2018-07-06
Martin
Feature/fp rewrite improvement (#2154)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-11
Andrew Reynolds
Fix equality conflicts reported by FP (#2064)
tree
|
commitdiff
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
tree
|
commitdiff
next