From 207de293b26cf7771814d3cf421e64fc6116434e Mon Sep 17 00:00:00 2001 From: makaimann Date: Mon, 2 Dec 2019 13:36:19 -0800 Subject: 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 * Comment comment suggestion Co-Authored-By: Aina Niemetz * 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 --- src/preprocessing/passes/ackermann.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/preprocessing/passes/ackermann.h') diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 8f27cab25..410dde8b9 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -55,8 +55,8 @@ class Ackermann : public PreprocessingPass * occurring in the input formula, add the following lemma: * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; private: /* Map each function to a set of terms associated with it */ -- cgit v1.2.3