projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Introduce quantifiers inference manager (#5821)
[cvc5.git]
/
src
/
theory
/
fp
/
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
2018-05-24
Andres Noetzli
Fix compiler warnings (#1959)
tree
|
commitdiff
2018-05-14
Martin
Floating point theory solver based on SymFPU (#1895)
tree
|
commitdiff
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
tree
|
commitdiff
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
tree
|
commitdiff
2018-02-08
Tim King
Fixing more inconsistent usages of override. (#1575)
tree
|
commitdiff
2018-02-06
Tim King
Resolving warnings from -Winconsistent-missing-override...
tree
|
commitdiff
2018-01-27
Tim King
Removing structurally dead code. (#1540)
tree
|
commitdiff
2017-12-08
Andrew Reynolds
Make collect model info return a Bool (#1421)
tree
|
commitdiff
2017-10-10
Martin
Add skeleton of the FP theory solver (#1130)
tree
|
commitdiff
2017-10-03
Martin
Add 5 FP kinds for partial to total fn conversion ...
tree
|
commitdiff
2017-10-02
Tim King
Removing throw specifiers from TypeEnumeratorBase's...
tree
|
commitdiff
2017-09-27
Martin Brain
Fix type checking of to_real (#1127)
tree
|
commitdiff
2017-09-27
Martin Brain
Improve FP rewriter: const folding, other (#1126)
tree
|
commitdiff
2017-09-20
Martin
Add FP type enumerator and cardinality computer (#1104)
tree
|
commitdiff
2017-09-15
Martin
Make floating-point comparison operators chainable...
tree
|
commitdiff
2017-09-14
Martin
Floating point symfpu support (#1093)
tree
|
commitdiff
2017-07-07
Mathias Preiner
Update copyright headers.
tree
|
commitdiff
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-10-03
Tim King
Removing the throw specifiers from theory_fp_type_rules.h.
tree
|
commitdiff
2016-04-20
PaulMeng
update from the master
tree
|
commitdiff
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-04-04
Tim King
Updating the copyright headers and scripts.
tree
|
commitdiff
2016-01-28
Tim King
Adding listeners to Options.
tree
|
commitdiff
2016-01-06
Tim King
Add SmtGlobals Class
tree
|
commitdiff
2015-12-15
Tim King
Refactoring Options Handler & Library Cycle Breaking
tree
|
commitdiff
2015-05-12
barrettcw
Merge pull request #74 from finnhaedicke/namespace_minisat
tree
|
commitdiff
2015-04-23
Clark Barrett
Merge branch 'master' into google
tree
|
commitdiff
2015-04-21
Clark Barrett
Changes needed to compile at Google, plus some bug...
tree
|
commitdiff
2014-12-04
Martin Brain
Floating point infrastructure.
tree
|
commitdiff