diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 463fe74df..53242f077 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -46,6 +46,7 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_algorithm.h" +#include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/sequence.h" #include "expr/type_node.h" @@ -3960,7 +3961,7 @@ Term Grammar::purifySygusGTerm( if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator so we should provide the op - NodeBuilder<> nb(term.d_node->getKind()); + NodeBuilder nb(term.d_node->getKind()); nb << term.d_node->getOperator(); nb.append(Term::termVectorToNodes(pchildren)); nret = nb.constructNode(); @@ -4348,7 +4349,7 @@ Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const const cvc5::Kind int_kind = extToIntKind(op.d_kind); std::vector<Node> echildren = Term::termVectorToNodes(children); - NodeBuilder<> nb(int_kind); + NodeBuilder nb(int_kind); nb << *op.d_node; nb.append(echildren); Node res = nb.constructNode(); @@ -5547,7 +5548,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, Sort s = mkTupleSortHelper(sorts); Datatype dt = s.getDatatype(); - NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR)); + NodeBuilder nb(extToIntKind(APPLY_CONSTRUCTOR)); nb << *dt[0].getConstructorTerm().d_node; nb.append(args); Node res = nb.constructNode(); |