OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (...
authormakaimann <makaim@stanford.edu>
Mon, 2 Dec 2019 21:36:19 +0000 (13:36 -0800)
committerGitHub <noreply@github.com>
Mon, 2 Dec 2019 21:36:19 +0000 (13:36 -0800)
commit207de293b26cf7771814d3cf421e64fc6116434e
tree3b8af6d5d4504c182bd80df06330829dbcab2516
parentdc99f1c45f616a93ee84b2a6ba877518206bdbaf
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
15 files changed:
examples/api/bitvectors-new.cpp
examples/api/datatypes-new.cpp
examples/api/extract-new.cpp
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/cvc4cppkind.h
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/preprocessing/passes/ackermann.cpp
src/preprocessing/passes/ackermann.h
src/smt/smt_engine.cpp
src/theory/arith/arith_rewriter.cpp
test/unit/api/opterm_black.h
test/unit/api/solver_black.h
test/unit/api/term_black.h