diff options
| author | makaimann <makaim@stanford.edu> | 2019-12-02 13:36:19 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-02 13:36:19 -0800 |
| commit | 207de293b26cf7771814d3cf421e64fc6116434e (patch) | |
| tree | 3b8af6d5d4504c182bd80df06330829dbcab2516 /src/preprocessing/passes/ackermann.cpp | |
| parent | dc99f1c45f616a93ee84b2a6ba877518206bdbaf (diff) | |
OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (#3355)
* Treat uninterpreted functions as a child in Term iteration
* Remove unnecessary const_iterator constructor
* Add parameter comments to const_iterator constructor
* Use operator[] instead of storing a vector of Expr children
* Switch pos member variable from int to uint32_t
* Add comment about how UFs are treated in iteration
* Allow OpTerm to contain a single Kind, update OpTerm construction
* Update mkTerm to use only an OpTerm (and not also a Kind)
* Remove unnecessary function checkMkOpTerm
* Update mkOpTerm comments to not use _OP Kinds
* Update examples to use new mkTerm
* First pass on fixing unit test
* Override kind for Constructor and Selector Terms
* More fixes to unit tests
* Updates to parser
* Remove old assert (for Kind, OpTerm pattern which was removed)
* Remove *_OP kinds from public API
* Add hasOpTerm and getOpTerm methods to Term
* Add test for UF iteration
* Add unit test for getOpTerm
* Move OpTerm implementation above Term implemenation to match header file
Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.
* Fix mkTerm in datatypes-new.cpp example
* Use helper function for creating term from Kind to avoid nested API calls
* Rename: OpTerm->Op in API
* Update OpTerm->Op in examples/tests/parser
* Add case for APPLY_TESTER
* operator term -> operator
* Update src/api/cvc4cpp.h
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Comment comment suggestion
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add not-null checks and implement Op from a single Kind constructor
* Undo sed mistake for OpTerm replacement
* Add 'd_' prefix to member vars
* Fix comment and remove old commented-out code
* Formatting
* Revert "Formatting"
This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.
* More fixes for sed mistakes
* Minor formatting
* Undo changes in CVC parser
* Add isIndexed and prefix with d_
* Create helper function for isIndexed to avoid calling API functions in other API functions
Diffstat (limited to 'src/preprocessing/passes/ackermann.cpp')
| -rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 4b5873e80..87c7fa2ce 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -35,8 +35,7 @@ namespace passes { /* -------------------------------------------------------------------------- */ -namespace -{ +namespace { void addLemmaForPair(TNode args1, TNode args2, @@ -219,7 +218,6 @@ PreprocessingPassResult Ackermann::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } - /* -------------------------------------------------------------------------- */ } // namespace passes |