diff options
author | makaimann <makaim@stanford.edu> | 2020-02-18 20:11:52 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-18 22:11:52 -0600 |
commit | 0398c53a582a3242ef89dceae59d00137f17df79 (patch) | |
tree | c12805bb0ed7b81506c912d11f8b0da7c2945fcc /examples | |
parent | 8e4dbbe1ef9a82622a784f0a905d01ce4fdc1e7d (diff) |
Change datatype selector/constructor/tester to terms (#3773)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/datatypes-new.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 43f97796e..c5773fa72 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -36,9 +36,11 @@ 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(consList.getConstructorTerm("cons"), - slv.mkReal(0), - slv.mkTerm(consList.getConstructorTerm("nil"))); + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl << "sort of cons is " @@ -51,7 +53,8 @@ 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(consList["cons"].getSelectorTerm("head"), t); + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -116,7 +119,8 @@ 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(paramConsList["cons"].getSelectorTerm("head"), a); + Term head_a = slv.mkTerm( + APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " |