| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-06-16 | Make symfpu a required dependency. (#6749) | Aina Niemetz | |
| 2021-04-14 | Rename public and private headers in src/include. (#6352) | Aina Niemetz | |
| 2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz | |
| 2021-04-09 | Rename CVC4_ macros to CVC5_. (#6327) | Aina Niemetz | |
| 2021-04-09 | Rename CVC4__ header guards to CVC5__. (#6326) | Aina Niemetz | |
| 2021-04-01 | FP: Factor out symfpu traits. (#6246) | Aina Niemetz | |
| This is in preparation for a MPFR floating-point literal implementation. We will need to have both literal kinds return a symFPU unpacked float via `getSymUF()` in order to be able to plug it into the fp_converter. For this, it makes sense to have the traits implemented and to be included separately, so that they can also be included in the MPFR implementation. | |||
| 2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz | |
| 2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz | |
| 2021-03-29 | FloatingPointLiteral: Constructor for special consts. (#6220) | Aina Niemetz | |
| This replaces static helpers for creating special consts with constructors. This is in preparation for a FP literal implementation using MPFR. In the next step, I'll introduce a FloatingPointLiteral base class, from which the specialization FloatingPointSymFPULiteral is derived. The MPFR implementation will also be derived from the base class. This is in order to make unit tests that compare between the two possible. Further, in the worst case, MPFR will have to use SymFPU for unsupported cases (to be determined). | |||
| 2021-03-26 | FloatingPointLiteral: Make constructors that shouldn't be used outside of ↵ | Aina Niemetz | |
| FloatingPoint(Literal) private. (#6211) | |||
| 2021-03-25 | FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206) | Aina Niemetz | |
| This pushes all symfpu specific parts from FloatingPoint into FloatingPointLiteral. FloatingPoint is now generic. An additional FloatingPointLiteral implementation using MPFR will be made configurable similiarly to how we handle Integers with either GMP or CLN backend. | |||
| 2021-03-22 | FP: Add documentation for FloatingPointLiteral constructors. (#6183) | Aina Niemetz | |
| 2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
| 2020-12-01 | Remove use of this-> in FP literal. (#5565) | Aina Niemetz | |
| 2020-11-20 | Rename symfpu_literal.(h.in|cpp) -> floatingpoint_literal_symfpu.(h.in|cpp). ↵ | Aina Niemetz | |
| (#5502) | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback