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 /examples | |
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 'examples')
-rw-r--r-- | examples/api/bitvectors-new.cpp | 4 | ||||
-rw-r--r-- | examples/api/datatypes-new.cpp | 14 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 16 |
3 files changed, 15 insertions, 19 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index 58912a1bb..4578da733 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -114,8 +114,8 @@ int main() cout << " CVC4: " << slv.checkValidAssuming(v) << endl; // Assert that a is odd - OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a); + Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); cout << "Assert " << a_odd << endl; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index efbd33645..9ff05ac0d 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -36,11 +36,9 @@ void test(Solver& slv, Sort& consListSort) // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Term t = slv.mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - slv.mkReal(0), - slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + Term t = slv.mkTerm(consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl << "sort of cons is " @@ -53,8 +51,7 @@ void test(Solver& slv, Sort& consListSort) // Here we first get the DatatypeConstructor for cons (with // consList["cons"]) in order to get the "head" selector symbol // to apply. - Term t2 = - slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); + Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -118,8 +115,7 @@ void test(Solver& slv, Sort& consListSort) Term a = slv.mkConst(paramConsIntListSort, "a"); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Term head_a = slv.mkTerm( - APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a); std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 0cb885b2c..0f0f8243a 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -30,17 +30,17 @@ int main() Term x = slv.mkConst(bitvector32, "a"); - OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); - Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x); + Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); - OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); - Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x); + Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); - OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); - Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x); + Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); - OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x); + Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; |