diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2e17d812c..69c4eabfd 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -23,7 +23,6 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt2/smt2_input.h" -#include "printer/sygus_print_callback.h" #include "util/bitvector.h" // ANTLR defines these, which is really bad! @@ -929,10 +928,6 @@ void Smt2::addSygusConstructorTerm( Trace("parser-sygus2") << "Purified operator " << op << ", #args/cargs=" << args.size() << "/" << cargs.size() << std::endl; - std::shared_ptr<SygusPrintCallback> spc; - // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>( - op.getExpr(), api::termVectorToExprs(args)); if (!args.empty()) { api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args); @@ -942,7 +937,7 @@ void Smt2::addSygusConstructorTerm( Trace("parser-sygus2") << "addSygusConstructor: operator " << op << std::endl; dt.getDatatype().addSygusConstructor( - op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc); + op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs)); } api::Term Smt2::purifySygusGTerm(api::Term term, |