diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b965d55a6..49ef2336c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.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" @@ -3956,7 +3957,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(); @@ -4344,7 +4345,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(); @@ -5543,7 +5544,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(); |