diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 14:12:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-14 14:12:18 -0500 |
| commit | 14d32d598e9daa97cf1a29ff893caac2989baec4 (patch) | |
| tree | f37a48a15db69e6423a3149c1a2e91687b870542 /src/parser/smt2 | |
| parent | 455fed0b388ff9c534391eb88f8c2a336fa42f07 (diff) | |
Remove sygus print callback (#4727)
This removes sygus print callbacks, since they are no longer necessary to support the sygus v1 parser.
This involved generalizing the scope of the datatype utility sygusToBuiltin. Now, printing "as sygus" simply is accomplished by doing sygusToBuiltin conversion and then calling the printer on the builtin term.
This is required for further work towards eliminating the Expr layer.
FYI @4tXJ7f
Diffstat (limited to 'src/parser/smt2')
| -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, |