diff options
34 files changed, 127 insertions, 575 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 278632a90..af2d0b782 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -116,8 +116,6 @@ libcvc4_add_sources( printer/printer.h printer/smt2/smt2_printer.cpp printer/smt2/smt2_printer.h - printer/sygus_print_callback.cpp - printer/sygus_print_callback.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h proof/arith_proof.cpp @@ -987,7 +985,6 @@ install(FILES DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/parser) install(FILES - printer/sygus_print_callback.h DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/printer) install(FILES diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 456e5a606..fcf0c028e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -49,7 +49,6 @@ #include "options/main_options.h" #include "options/options.h" #include "options/smt_options.h" -#include "printer/sygus_print_callback.h" #include "smt/model.h" #include "smt/smt_engine.h" #include "theory/logic_info.h" @@ -2553,10 +2552,6 @@ void Grammar::addSygusConstructorTerm( Term op = purifySygusGTerm(term, args, cargs, ntsToUnres); std::stringstream ssCName; ssCName << op.getKind(); - std::shared_ptr<SygusPrintCallback> spc; - // callback prints as the expression - spc = std::make_shared<printer::SygusExprPrintCallback>( - *op.d_expr, termVectorToExprs(args)); if (!args.empty()) { Term lbvl = Term(d_solver, @@ -2568,7 +2563,7 @@ void Grammar::addSygusConstructorTerm( {*lbvl.d_expr, *op.d_expr})); } dt.d_dtype->addSygusConstructor( - *op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc); + *op.d_expr, ssCName.str(), sortVectorToTypes(cargs)); } Term Grammar::purifySygusGTerm( diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 5a48a0220..9ec3ac5fd 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -266,7 +266,6 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ void Datatype::addSygusConstructor(Expr op, const std::string& cname, const std::vector<Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc, int weight) { // avoid name clashes @@ -275,7 +274,7 @@ void Datatype::addSygusConstructor(Expr op, std::string name = ss.str(); unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); DatatypeConstructor c(name, cweight); - c.setSygus(op, spc); + c.setSygus(op); for( unsigned j=0; j<cargs.size(); j++ ){ Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; std::stringstream sname; @@ -288,12 +287,11 @@ void Datatype::addSygusConstructor(Expr op, void Datatype::addSygusConstructor(Kind k, const std::string& cname, const std::vector<Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc, int weight) { ExprManagerScope ems(*d_em); Expr op = d_em->operatorOf(k); - addSygusConstructor(op, cname, cargs, spc, weight); + addSygusConstructor(op, cname, cargs, weight); } void Datatype::setTuple() { @@ -526,15 +524,12 @@ DatatypeConstructor::DatatypeConstructor(std::string name, unsigned weight) d_internal = std::make_shared<DTypeConstructor>(name, weight); } -void DatatypeConstructor::setSygus(Expr op, - std::shared_ptr<SygusPrintCallback> spc) +void DatatypeConstructor::setSygus(Expr op) { PrettyCheckArgument( !isResolved(), this, "cannot modify a finalized Datatype constructor"); Node opn = Node::fromExpr(op); d_internal->setSygus(op); - // print callback lives at the expression level currently - d_sygus_pc = spc; } const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs() @@ -626,13 +621,6 @@ unsigned DatatypeConstructor::getWeight() const return d_internal->getWeight(); } -std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const -{ - PrettyCheckArgument( - isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_pc; -} - Cardinality DatatypeConstructor::getCardinality(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 0da4c9f51..54095050f 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -171,32 +171,6 @@ class CVC4_PUBLIC DatatypeConstructorArg { DatatypeConstructorArg(std::string name, Expr selector); };/* class DatatypeConstructorArg */ -class Printer; - -/** sygus datatype constructor printer - * - * This is a virtual class that is used to specify - * a custom printing callback for sygus terms. This is - * useful for sygus grammars that include defined - * functions or let expressions. - */ -class CVC4_PUBLIC SygusPrintCallback -{ - public: - SygusPrintCallback() {} - virtual ~SygusPrintCallback() {} - /** - * Writes the term that sygus datatype expression e - * encodes to stream out. p is the printer that - * requested that expression e be written on output - * stream out. Calls may be made to p to print - * subterms of e. - */ - virtual void toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const = 0; -}; - class DTypeConstructor; /** @@ -284,14 +258,6 @@ class CVC4_PUBLIC DatatypeConstructor { * of the form (lambda (x) x). */ bool isSygusIdFunc() const; - /** get sygus print callback - * - * This class stores custom ways of printing - * sygus datatype constructors, for instance, - * to handle defined or let expressions that - * appear in user-provided grammars. - */ - std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const; /** get weight * * Get the weight of this constructor. This value is used when computing the @@ -428,7 +394,7 @@ class CVC4_PUBLIC DatatypeConstructor { * operator op. spc is the sygus callback of this datatype constructor, * which is stored in a shared pointer. */ - void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc); + void setSygus(Expr op); /** * Get the list of arguments to this constructor. @@ -445,8 +411,6 @@ class CVC4_PUBLIC DatatypeConstructor { Expr d_constructor; /** the arguments of this constructor */ std::vector<DatatypeConstructorArg> d_args; - /** sygus print callback */ - std::shared_ptr<SygusPrintCallback> d_sygus_pc; };/* class DatatypeConstructor */ class DType; @@ -595,8 +559,6 @@ class CVC4_PUBLIC Datatype { * this constructor encodes * cname : the name of the constructor (for printing only) * cargs : the arguments of the constructor - * spc : an (optional) callback that is used for custom printing. This is - * to accomodate user-provided grammars in the sygus format. * * It should be the case that cargs are sygus datatypes that * encode the arguments of op. For example, a sygus constructor @@ -611,7 +573,6 @@ class CVC4_PUBLIC Datatype { void addSygusConstructor(Expr op, const std::string& cname, const std::vector<Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** * Same as above, with builtin kind k. @@ -619,7 +580,6 @@ class CVC4_PUBLIC Datatype { void addSygusConstructor(Kind k, const std::string& cname, const std::vector<Type>& cargs, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** set that this datatype is a tuple */ diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index d14f0d1a7..1efea4e15 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -14,8 +14,6 @@ #include "expr/sygus_datatype.h" -#include "printer/sygus_print_callback.h" - using namespace CVC4::kind; namespace CVC4 { @@ -30,14 +28,12 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); } void SygusDatatype::addConstructor(Node op, const std::string& name, const std::vector<TypeNode>& argTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { d_cons.push_back(SygusDatatypeConstructor()); d_cons.back().d_op = op; d_cons.back().d_name = name; d_cons.back().d_argTypes = argTypes; - d_cons.back().d_pc = spc; d_cons.back().d_weight = weight; } @@ -54,15 +50,14 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn) std::vector<TypeNode> builtinArg; builtinArg.push_back(tn); addConstructor( - av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0); + av, cname, builtinArg, 0); } void SygusDatatype::addConstructor(Kind k, const std::vector<TypeNode>& argTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { NodeManager* nm = NodeManager::currentNM(); - addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight); + addConstructor(nm->operatorOf(k), kindToString(k), argTypes, weight); } size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); } @@ -97,7 +92,6 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType, d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(), d_cons[i].d_name, cargs, - d_cons[i].d_pc, d_cons[i].d_weight); } Trace("sygus-type-cons") << "...built datatype " << d_dt << " "; diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index 1bf74d8d3..4342aa291 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -45,8 +45,6 @@ class SygusDatatypeConstructor std::string d_name; /** List of argument types. */ std::vector<TypeNode> d_argTypes; - /** Print callback of the constructor. */ - std::shared_ptr<SygusPrintCallback> d_pc; /** Weight of the constructor. */ int d_weight; }; @@ -89,7 +87,6 @@ class SygusDatatype void addConstructor(Node op, const std::string& name, const std::vector<TypeNode>& argTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** * Add constructor that encodes an application of builtin kind k. Like above, @@ -98,7 +95,6 @@ class SygusDatatype */ void addConstructor(Kind k, const std::vector<TypeNode>& argTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** * This adds a constructor that corresponds to the any constant constructor diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ff6bdbde0..c97a24d6d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -661,6 +661,15 @@ bool TypeNode::isCodatatype() const return false; } +bool TypeNode::isSygusDatatype() const +{ + if (isDatatype()) + { + return getDType().isSygus(); + } + return false; +} + std::string TypeNode::toString() const { std::stringstream ss; OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 12c96d307..f957fe0d0 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -639,6 +639,9 @@ public: /** Is this a fully instantiated datatype type */ bool isInstantiatedDatatype() const; + /** Is this a sygus datatype type */ + bool isSygusDatatype() const; + /** * Get instantiated datatype type. The type on which this method is called * should be a parametric datatype whose parameter list is the same size as 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, diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 699899c1e..d0ebe5f19 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -20,7 +20,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "printer/sygus_print_callback.h" #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" @@ -344,7 +343,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( sdts[i].addConstructor(lambdaOp, sscs.str(), argListc, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); } // recursive apply @@ -413,7 +411,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( sdttl.addConstructor(lambdaOp, ssc.str(), argList, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); Trace("srs-input-debug") << "Grammar for subterm " << n << " is: " << std::endl; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5d54759b9..67dbe1036 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -69,14 +69,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) } } -void Printer::toStreamSygus(std::ostream& out, TNode n) const -{ - // no sygus-specific printing associated with this printer, - // just print the original term, without letification (the fifth argument is - // set to 0). - toStream(out, n, -1, false, 0); -} - void Printer::toStream(std::ostream& out, const Model& m) const { for(size_t i = 0; i < m.getNumCommands(); ++i) { diff --git a/src/printer/printer.h b/src/printer/printer.h index b18e318ee..fd788209c 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -65,21 +65,6 @@ class Printer /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const; - /** - * Write the term that sygus datatype term n - * encodes to a stream with this Printer. - * For example, consider the datatype term - * (C_plus (C_minus C_x C_0) C_y) - * where C_plus, C_minus, C_x, C_0, C_y are constructors - * whose sygus operators are PLUS, MINUS, x, 0, y. - * In this case, this method is equivalent to printing - * the integer term: - * (PLUS (MINUS x 0) y) - * This method may make calls to sygus printing callback - * methods stored in sygus datatype constructors. - */ - virtual void toStreamSygus(std::ostream& out, TNode n) const; - protected: /** Derived classes can construct, but no one else. */ Printer() {} diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 49f786f78..23503ea28 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -35,6 +35,7 @@ #include "smt_util/boolean_simplification.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/substitutions.h" #include "theory/theory_model.h" #include "util/smt2_quote_string.h" @@ -1493,51 +1494,6 @@ void Smt2Printer::toStream(std::ostream& out, } } -void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const -{ - if (n.getKind() == kind::APPLY_CONSTRUCTOR) - { - TypeNode tn = n.getType(); - const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); - if (dt.isSygus()) - { - int cIndex = Datatype::indexOf(n.getOperator().toExpr()); - Assert(!dt[cIndex].getSygusOp().isNull()); - SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback().get(); - if (spc != nullptr && options::sygusPrintCallbacks()) - { - spc->toStreamSygus(this, out, n.toExpr()); - } - else - { - if (n.getNumChildren() > 0) - { - out << "("; - } - // print operator without letification (the fifth argument is set to 0). - toStream(out, dt[cIndex].getSygusOp(), -1, false, 0); - if (n.getNumChildren() > 0) - { - for (Node nc : n) - { - out << " "; - toStreamSygus(out, nc); - } - out << ")"; - } - } - return; - } - } - Node p = n.getAttribute(theory::SygusPrintProxyAttribute()); - if (p.isNull()) - { - p = n; - } - // cannot convert term to analog, print original, without letification. - toStream(out, p, -1, false, 0); -} - static void toStream(std::ostream& out, const AssertCommand* c) { out << "(assert " << c->getExpr() << ")"; @@ -2066,8 +2022,6 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t) // name // sygus type // constructors in order - Printer* sygus_printer = - Printer::getPrinter(language::output::LANG_SYGUS_V2); do { Type curr = typesToPrint.front(); @@ -2100,8 +2054,8 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t) } } Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren); - // now, print it - sygus_printer->toStreamSygus(types_list, consToPrint); + // now, print it using the conversion to builtin with external + types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, true); types_list << ' '; } types_list << "))\n"; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 398e510cb..640521a67 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -57,11 +57,6 @@ class Smt2Printer : public CVC4::Printer { * with the core (UnsatCore::getSmtEngine) for printing named assertions. */ void toStream(std::ostream& out, const UnsatCore& core) const override; - /** - * Write the term that sygus datatype term node n - * encodes to a stream with this Printer. - */ - void toStreamSygus(std::ostream& out, TNode n) const override; private: void toStream( diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp deleted file mode 100644 index a15bde3c3..000000000 --- a/src/printer/sygus_print_callback.cpp +++ /dev/null @@ -1,142 +0,0 @@ -/********************* */ -/*! \file sygus_print_callback.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of sygus print callbacks - **/ - -#include "printer/sygus_print_callback.h" - -#include "expr/node.h" -#include "printer/printer.h" - -using namespace CVC4::kind; -using namespace std; - -namespace CVC4 { -namespace printer { - -SygusExprPrintCallback::SygusExprPrintCallback(Expr body, - const std::vector<Expr>& args) - : d_body(body), d_body_argument(-1) -{ - d_args.insert(d_args.end(), args.begin(), args.end()); - for (unsigned i = 0, size = d_args.size(); i < size; i++) - { - if (d_args[i] == d_body) - { - d_body_argument = static_cast<int>(i); - } - } -} - -void SygusExprPrintCallback::doStrReplace(std::string& str, - const std::string& oldStr, - const std::string& newStr) const -{ - size_t pos = 0; - while ((pos = str.find(oldStr, pos)) != std::string::npos) - { - str.replace(pos, oldStr.length(), newStr); - pos += newStr.length(); - } -} - -void SygusExprPrintCallback::toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const -{ - // optimization: if body is equal to an argument, then just print that one - if (d_body_argument >= 0) - { - p->toStreamSygus(out, Node::fromExpr(e[d_body_argument])); - } - else - { - // make substitution - std::vector<Node> vars; - std::vector<Node> subs; - for (unsigned i = 0, size = d_args.size(); i < size; i++) - { - vars.push_back(Node::fromExpr(d_args[i])); - std::stringstream ss; - ss << "_setpc_var_" << i; - Node lv = NodeManager::currentNM()->mkBoundVar( - ss.str(), TypeNode::fromType(d_args[i].getType())); - subs.push_back(lv); - } - - // the substituted body should be a non-sygus term - Node sbody = Node::fromExpr(d_body); - sbody = - sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - - // print to stream without letification - std::stringstream body_out; - p->toStream(body_out, sbody, -1, false, 0); - - // do string substitution - Assert(e.getNumChildren() == d_args.size()); - std::string str_body = body_out.str(); - for (unsigned i = 0, size = d_args.size(); i < size; i++) - { - std::stringstream old_str; - old_str << subs[i]; - std::stringstream new_str; - p->toStreamSygus(new_str, Node::fromExpr(e[i])); - doStrReplace(str_body, old_str.str().c_str(), new_str.str().c_str()); - } - out << str_body; - } -} - -SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name) - : d_name(name) -{ -} - -void SygusNamedPrintCallback::toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const -{ - if (e.getNumChildren() > 0) - { - out << "("; - } - out << d_name; - if (e.getNumChildren() > 0) - { - for (Expr ec : e) - { - out << " "; - p->toStreamSygus(out, ec); - } - out << ")"; - } -} - -void SygusEmptyPrintCallback::toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const -{ - if (e.getNumChildren() == 1) - { - p->toStreamSygus(out, e[0]); - } - else - { - Assert(false); - } -} - -std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr; - -} /* CVC4::printer namespace */ -} /* CVC4 namespace */ diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h deleted file mode 100644 index 925c80ae8..000000000 --- a/src/printer/sygus_print_callback.h +++ /dev/null @@ -1,136 +0,0 @@ -/********************* */ -/*! \file sygus_print_callback.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief sygus print callback functions - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H -#define CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H - -#include <vector> - -#include "expr/datatype.h" -#include "expr/expr.h" - -namespace CVC4 { -namespace printer { - -/** sygus expression constructor printer - * - * This class is used for printing sygus datatype constructor terms whose top - * symbol is an expression, such as a custom defined lambda. For example, for - * sygus grammar: - * A -> (+ x A B) | x | y - * B -> 0 | 1 - * The first constructor, call it C_f for A takes two arguments (A, B) and has - * sygus operator - * (lambda ((z Int) (w Int)) (+ x z w)) - * For this operator, we set a print callback that prints, e.g. the term - * C_f( t1, t2 ) - * is printed as: - * "(+ x [out1] [out2])" - * where out1 is the result of p->toStreamSygus(out,t1) and - * out2 is the result of p->toStreamSygus(out,t2). - */ -class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback -{ - public: - SygusExprPrintCallback(Expr body, const std::vector<Expr>& args); - ~SygusExprPrintCallback() {} - /** print sygus term e on output out using printer p */ - virtual void toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const override; - - protected: - /** body of the sygus term */ - Expr d_body; - /** arguments */ - std::vector<Expr> d_args; - /** body argument */ - int d_body_argument; - /** do string replace - * - * Replaces all occurrences of oldStr with newStr in str. - */ - void doStrReplace(std::string& str, - const std::string& oldStr, - const std::string& newStr) const; -}; - -/** sygus named constructor printer - * - * This callback is used for explicitly naming - * the builtin term that a sygus datatype constructor - * should be printed as. This is used for printing - * terms in sygus grammars that involve defined - * functions. For example, for grammar : - * A -> f( A ) | 0 - * where f is defined as: - * (define-fun ((x Int)) Int (+ x 1)) - * this class can be used as a callback for printing - * the first sygus datatype constructor f, where we use - * analog operator (lambda (x) (+ x 1)). - */ -class CVC4_PUBLIC SygusNamedPrintCallback : public SygusPrintCallback -{ - public: - SygusNamedPrintCallback(std::string name); - ~SygusNamedPrintCallback() {} - /** print sygus term e on output out using printer p */ - virtual void toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const override; - - private: - /** the defined function name */ - std::string d_name; -}; - -/** sygus empty printer - * - * This callback is used for printing constructors whose operators are - * implicit, such as identity functions. For example, for grammar : - * A -> B - * B -> x | 0 | 1 - * The first constructor of A, call it cons, has sygus operator (lambda (x) x). - * Call toStreamSygus on cons( t ) should call toStreamSygus on t directly. - */ -class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback -{ - public: - SygusEmptyPrintCallback() {} - ~SygusEmptyPrintCallback() {} - /** print sygus term e on output out using printer p */ - virtual void toStreamSygus(const Printer* p, - std::ostream& out, - Expr e) const override; - /* Retrieves empty callback pointer */ - static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC() - { - if (!d_empty_pc) - { - d_empty_pc = std::make_shared<SygusEmptyPrintCallback>(); - } - return d_empty_pc; - } - - private: - /* empty callback object */ - static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc; -}; - -} /* CVC4::printer namespace */ -} /* CVC4 namespace */ - -#endif /* CVC4__PRINTER__SYGUS_PRINT_CALLBACK_H */ diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 3caee52f9..e95b66bd7 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -19,7 +19,6 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/evaluator.h" @@ -327,9 +326,18 @@ struct SygusToBuiltinTermAttributeId typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node> SygusToBuiltinTermAttribute; +// A variant of the above attribute for cases where we introduce a fresh +// variable. This is to support sygusToBuiltin on non-constant sygus terms, +// where sygus variables should be mapped to canonical builtin variables. +// It is important to cache this so that sygusToBuiltin is deterministic. +struct SygusToBuiltinVarAttributeId +{ +}; +typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node> + SygusToBuiltinVarAttribute; + Node sygusToBuiltin(Node n, bool isExternal) { - Assert(n.isConst()); std::unordered_map<TNode, Node, TNodeHashFunction> visited; std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; std::vector<TNode> visit; @@ -343,6 +351,9 @@ Node sygusToBuiltin(Node n, bool isExternal) it = visited.find(cur); if (it == visited.end()) { + // Notice this condition succeeds in roughly 99% of the executions of this + // method (based on our coverage tests), hence the else if / else cases + // below do not significantly impact performance. if (cur.getKind() == APPLY_CONSTRUCTOR) { if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute())) @@ -359,6 +370,27 @@ Node sygusToBuiltin(Node n, bool isExternal) } } } + else if (cur.getType().isSygusDatatype()) + { + Assert (cur.isVar()); + if (cur.hasAttribute(SygusToBuiltinVarAttribute())) + { + // use the previously constructed variable for it + visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute()); + } + else + { + std::stringstream ss; + ss << cur; + const DType& dt = cur.getType().getDType(); + // make a fresh variable + NodeManager * nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), dt.getSygusType()); + SygusToBuiltinVarAttribute stbv; + cur.setAttribute(stbv, var); + visited[cur] = var; + } + } else { // non-datatypes are themselves @@ -664,28 +696,10 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, << " Arg #" << k << ": " << argtNew << std::endl; cargs.push_back(argtNew); } - // callback prints as the expression - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> args; - if (op.getKind() == LAMBDA) - { - Node opBody = op[1]; - for (const Node& v : op[0]) - { - args.push_back(v.toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>( - opBody.toExpr(), args); - } - else if (cargs.empty()) - { - spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(), - args); - } std::stringstream ss; ss << ops.getKind(); Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; - sdts.back().addConstructor(ops, ss.str(), cargs, spc); + sdts.back().addConstructor(ops, ss.str(), cargs); } Trace("dtsygus-gen-debug") << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 593577b8e..88ee6d33b 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -145,7 +145,7 @@ Node applySygusArgs(const DType& dt, const std::vector<Node>& args); /** Sygus to builtin * - * This method converts a constant term of SyGuS datatype type to its builtin + * This method converts a term n of SyGuS datatype type to its builtin * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y * respectively. @@ -154,8 +154,12 @@ Node applySygusArgs(const DType& dt, * that was provided. This includes the use of defined functions. This argument * should typically be false, unless we are e.g. exporting the value of the * term as a final solution. + * + * If n is not constant, then its non-constant subterms that have sygus + * datatype types are replaced by fresh variables (of the same name, if that + * subterm is a variable, and having arbitrary name otherwise). */ -Node sygusToBuiltin(Node c, bool isExternal = false); +Node sygusToBuiltin(Node n, bool isExternal = false); /** Sygus to builtin eval * * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index fda08bb0e..c279f0558 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1566,8 +1566,7 @@ void SygusExtension::check( std::vector< Node >& lemmas ) { { Trace("dt-sygus") << "* DT model : " << prog << " -> "; std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, progv); + quantifiers::TermDbSygus::toStreamSygus(ss, progv); Trace("dt-sygus") << ss.str() << std::endl; } // first check that the value progv for prog is what we expected diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index cabd78643..4593f36f1 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -202,10 +202,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, out << "(" << (verified ? "" : "candidate-") << "rewrite "; if (d_using_sygus) { - Printer* p = Printer::getPrinter(options::outputLanguage()); - p->toStreamSygus(out, sol); + TermDbSygus::toStreamSygus(out, sol); out << " "; - p->toStreamSygus(out, eq_sol); + TermDbSygus::toStreamSygus(out, eq_sol); } else { diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index c89fc6424..45b627ba4 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -163,12 +163,11 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) } if (Trace.isOn("sygus-rr-filter")) { - Printer* p = Printer::getPrinter(options::outputLanguage()); std::stringstream ss; ss << "(redundant-rewrite "; - p->toStreamSygus(ss, n); + TermDbSygus::toStreamSygus(ss, n); ss << " "; - p->toStreamSygus(ss, eq_n); + TermDbSygus::toStreamSygus(ss, eq_n); ss << ")"; Trace("sygus-rr-filter") << ss.str() << std::endl; } diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index de75af083..dcdd89c1b 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -297,11 +297,10 @@ bool CegisCoreConnective::constructSolution( { Trace("sygus-ccore") << "CegisCoreConnective: Construct candidate solutions..." << std::endl; - Printer* p = Printer::getPrinter(options::outputLanguage()); for (unsigned i = 0, size = candidates.size(); i < size; i++) { std::stringstream ss; - p->toStreamSygus(ss, candidate_values[i]); + TermDbSygus::toStreamSygus(ss, candidate_values[i]); Trace("sygus-ccore") << " " << candidates[i] << " -> " << ss.str() << std::endl; } diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 64e604d0b..91df9d0d6 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -97,7 +97,7 @@ void EnumStreamPermutation::reset(Node value) for (const Node& var : p.second) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var); + TermDbSygus::toStreamSygus(ss, var); Trace("synth-stream-concrete") << " " << ss.str(); } Trace("synth-stream-concrete") << " ]"; @@ -111,7 +111,7 @@ Node EnumStreamPermutation::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value); + TermDbSygus::toStreamSygus(ss, d_value); Trace("synth-stream-concrete") << " ....streaming next permutation for value : " << ss.str() << " with " << d_perm_state_class.size() << " permutation classes\n"; @@ -203,8 +203,7 @@ Node EnumStreamPermutation::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, perm_value); + TermDbSygus::toStreamSygus(ss, perm_value); Trace("synth-stream-concrete") << " ....return new perm " << ss.str() << "\n"; } @@ -291,8 +290,7 @@ void EnumStreamPermutation::PermutationState::getLastPerm( if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, d_vars[d_last_perm[i]]); + TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]); Trace("synth-stream-concrete") << " " << ss.str(); } vars.push_back(d_vars[d_last_perm[i]]); @@ -373,7 +371,7 @@ void EnumStreamSubstitution::resetValue(Node value) if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value); + TermDbSygus::toStreamSygus(ss, value); Trace("synth-stream-concrete") << " * Streaming concrete: registering value " << ss.str() << "\n"; } @@ -402,7 +400,7 @@ void EnumStreamSubstitution::resetValue(Node value) for (const Node& var : p.second) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var); + TermDbSygus::toStreamSygus(ss, var); Trace("synth-stream-concrete") << " " << ss.str(); } Trace("synth-stream-concrete") << " ]"; @@ -416,7 +414,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value); + TermDbSygus::toStreamSygus(ss, d_value); Trace("synth-stream-concrete") << " ..streaming next combination of " << ss.str() << "\n"; } @@ -471,7 +469,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete-debug")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last); + TermDbSygus::toStreamSygus(ss, d_last); Trace("synth-stream-concrete-debug") << " ..using base perm " << ss.str() << "\n"; } @@ -521,8 +519,7 @@ Node EnumStreamSubstitution::getNext() if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); + TermDbSygus::toStreamSygus(ss, comb_value); Trace("synth-stream-concrete") << " ....register new comb value " << ss.str() << " with rewritten form " << builtin_comb_value @@ -531,20 +528,21 @@ Node EnumStreamSubstitution::getNext() if (!builtin_comb_value.isConst() && !d_comb_values.insert(builtin_comb_value).second) { - std::stringstream ss, ss1; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); - Trace("synth-stream-concrete") - << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value - << "\n ..excluding all other concretizations (had " - << d_comb_values.size() << " already)\n\n"; + if (Trace.isOn("synth-stream-concrete")) + { + std::stringstream ss, ss1; + TermDbSygus::toStreamSygus(ss, comb_value); + Trace("synth-stream-concrete") + << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value + << "\n ..excluding all other concretizations (had " + << d_comb_values.size() << " already)\n\n"; + } return Node::null(); } if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, comb_value); + TermDbSygus::toStreamSygus(ss, comb_value); Trace("synth-stream-concrete") << " ..return new comb " << ss.str() << "\n\n"; } @@ -581,8 +579,7 @@ void EnumStreamSubstitution::CombinationState::getLastComb( if (Trace.isOn("synth-stream-concrete")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, d_vars[d_last_comb[i]]); + TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]); Trace("synth-stream-concrete") << " " << ss.str(); } vars.push_back(d_vars[d_last_comb[i]]); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index b71a92260..ee37d7b4b 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,7 +19,6 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "printer/sygus_print_callback.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index cb30a408e..bd5f7ae50 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,7 +18,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" @@ -492,7 +491,7 @@ bool CegGrammarConstructor::isHandledType(TypeNode t) } Node CegGrammarConstructor::createLambdaWithZeroArg( - Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc) + Kind k, TypeNode bArgType) { NodeManager* nm = NodeManager::currentNM(); std::vector<Node> opLArgs; @@ -513,9 +512,6 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( zarg = bv::utils::mkZero(size); } Node body = nm->mkNode(k, zarg, opLArgs.back()); - // use a print callback since we do not want to print the lambda - spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(), - opLArgsExpr); // create operator Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body); Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n"; @@ -1137,15 +1133,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial); - // use a print callback since we do not want to print the lambda - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> opLArgsExpr; - for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++) - { - opLArgsExpr.push_back(opLArgs[j].toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>( - monomial.toExpr(), opLArgsExpr); // add it as a constructor std::stringstream ssop; ssop << "monomial_" << sdc.d_name; @@ -1153,7 +1140,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // a generalization of a non-Boolean variable (which has weight 0). // This ensures that e.g. ( c1*x >= 0 ) has the same weight as // ( x >= 0 ). - sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc, 0); + sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, 0); } } if (polynomialGrammar) @@ -1167,14 +1154,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Assert(sumChildren.size() > 1); Node ops = nm->mkNode(PLUS, sumChildren); Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> lambdaVarsExpr; - for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++) - { - lambdaVarsExpr.push_back(lambdaVars[j].toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(), - lambdaVarsExpr); Trace("sygus-grammar-def") << "any term operator is " << op << std::endl; // make the any term datatype, add to back // do not consider the exclusion criteria of the generator @@ -1182,7 +1161,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // a simultaneous generalization of set of non-Boolean variables. // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as // e.g. ( x >= 0 ) or ( y >= 0 ). - sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0); + sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, 0); // mark that predicates should be of the form (= pol 0) and (<= pol 0) itgat->second.second = true; } @@ -1223,7 +1202,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; std::vector<TypeNode> cargsEmpty; // make boolean variables weight as non-nullary constructors - sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, nullptr, 1); + sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, 1); } } // add constants @@ -1270,8 +1249,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // predicates if (zarg) { - std::shared_ptr<SygusPrintCallback> spc; - Node op = createLambdaWithZeroArg(k, types[i], spc); + Node op = createLambdaWithZeroArg(k, types[i]); ss << "eq_" << types[i]; sdtBool.addConstructor(op, ss.str(), cargs); } @@ -1283,7 +1261,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.pop_back(); } // type specific predicates - std::shared_ptr<SygusPrintCallback> spc; std::stringstream ssop; if (types[i].isReal()) { @@ -1291,7 +1268,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for " << k << std::endl; if (zarg) { - Node op = createLambdaWithZeroArg(kind, types[i], spc); + Node op = createLambdaWithZeroArg(kind, types[i]); ssop << "leq_" << types[i]; sdtBool.addConstructor(op, ssop.str(), cargs); } @@ -1307,7 +1284,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for " << k << std::endl; if (zarg) { - Node op = createLambdaWithZeroArg(kind, types[i], spc); + Node op = createLambdaWithZeroArg(kind, types[i]); ssop << "leq_" << types[i]; sdtBool.addConstructor(op, ssop.str(), cargs); } @@ -1522,22 +1499,20 @@ void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( Node op, const std::string& name, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { if (shouldInclude(op)) { - d_sdt.addConstructor(op, name, consTypes, spc, weight); + d_sdt.addConstructor(op, name, consTypes, weight); } } void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor( Kind k, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc, int weight) { NodeManager* nm = NodeManager::currentNM(); - addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight); + addConstructor(nm->operatorOf(k), kindToString(k), consTypes, weight); } bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index b0c575809..fd7f84484 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -200,7 +200,6 @@ public: void addConstructor(Node op, const std::string& name, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** * Possibly add a constructor to d_sdt, based on the criteria mentioned @@ -208,7 +207,6 @@ public: */ void addConstructor(Kind k, const std::vector<TypeNode>& consTypes, - std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); /** Should we include constructor with operator op? */ bool shouldInclude(Node op) const; @@ -260,13 +258,9 @@ public: * and an extra zero argument of that same type. For example, for k = LEQ and * bArgType = Int, the operator will be lambda x : Int. x + 0. Currently the * supported input types are Real (thus also Int) and BitVector. - * - * This method also creates a print callback for the operator, saved via the - * argument spc, if the caller wishes to not print the lambda. */ static Node createLambdaWithZeroArg(Kind k, - TypeNode bArgType, - std::shared_ptr<SygusPrintCallback> spc); + TypeNode bArgType); //---------------- end grammar construction }; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 819dd6de9..939256b2b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -18,7 +18,6 @@ #include "expr/datatype.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" -#include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -84,8 +83,7 @@ SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn) void SygusGrammarNorm::TypeObject::addConsInfo( SygusGrammarNorm* sygus_norm, - const DTypeConstructor& cons, - std::shared_ptr<SygusPrintCallback> spc) + const DTypeConstructor& cons) { Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n"; /* Recover the sygus operator to not lose reference to the original @@ -107,7 +105,7 @@ void SygusGrammarNorm::TypeObject::addConsInfo( } d_sdt.addConstructor( - sygus_op, cons.getName(), consTypes, spc, cons.getWeight()); + sygus_op, cons.getName(), consTypes, cons.getWeight()); } void SygusGrammarNorm::TypeObject::initializeDatatype( @@ -225,7 +223,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, to.d_sdt.addConstructor(iden_op, "id", ctypes, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); Trace("sygus-grammar-normalize-chain") << "\tAdding " << t << " to " << to.d_unres_tn << "\n"; @@ -267,7 +264,6 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm, to.d_sdt.addConstructor(iden_op, "id_next", ctypes, - printer::SygusEmptyPrintCallback::getEmptyPC(), 0); } @@ -472,7 +468,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, { unsigned oi = op_pos[i]; Assert(oi < dt.getNumConstructors()); - to.addConsInfo(this, dt[oi], dtt[oi].getSygusPrintCallback()); + to.addConsInfo(this, dt[oi]); } /* Build normalize datatype */ if (Trace.isOn("sygus-grammar-normalize")) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 7b635884b..5994d0e7d 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -198,8 +198,7 @@ class SygusGrammarNorm * The types of the arguments of "cons" are recursively normalized */ void addConsInfo(SygusGrammarNorm* sygus_norm, - const DTypeConstructor& cons, - std::shared_ptr<SygusPrintCallback> spc); + const DTypeConstructor& cons); /** initializes a datatype with the information in the type object * diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 77b193a75..42572a0c7 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -21,7 +21,6 @@ #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "options/smt_options.h" -#include "printer/sygus_print_callback.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index cff8f581d..3e632fc56 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -129,11 +129,10 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (Trace.isOn("sygus-repair-const")) { Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl; - Printer* p = Printer::getPrinter(options::outputLanguage()); for (unsigned i = 0, size = candidates.size(); i < size; i++) { std::stringstream ss; - p->toStreamSygus(ss, candidate_values[i]); + TermDbSygus::toStreamSygus(ss, candidate_values[i]); Trace("sygus-repair-const") << " " << candidates[i] << " -> " << ss.str() << std::endl; } @@ -151,9 +150,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody, cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles); if (Trace.isOn("sygus-repair-const")) { - Printer* p = Printer::getPrinter(options::outputLanguage()); std::stringstream ss; - p->toStreamSygus(ss, cv); + TermDbSygus::toStreamSygus(ss, cv); Trace("sygus-repair-const") << "Solution #" << i << " : " << ss.str() << std::endl; if (skeleton == cv) @@ -163,7 +161,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, else { std::stringstream sss; - p->toStreamSygus(sss, skeleton); + TermDbSygus::toStreamSygus(sss, skeleton); Trace("sygus-repair-const") << "...inferred skeleton : " << sss.str() << std::endl; } @@ -269,8 +267,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine")) { std::stringstream sss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(sss, repair_cv[i]); + TermDbSygus::toStreamSygus(sss, repair_cv[i]); ss << " * " << candidates[i] << " -> " << sss.str() << std::endl; } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 9fb0702b1..86cb69f48 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -713,8 +713,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, if (Trace.isOn("sygus-unif-sol")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, hd_mv[e]); + TermDbSygus::toStreamSygus(ss, hd_mv[e]); Trace("sygus-unif-sol") << " add evaluation head (" << hd_counter << "/" << d_hds.size() << "): " << e << " -> " << ss.str() << std::endl; @@ -766,7 +765,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, if (Trace.isOn("sygus-unif-sol")) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv); + TermDbSygus::toStreamSygus(ss, cv); Trace("sygus-unif-sol") << " add condition (" << c_counter << "/" << d_conds.size() << "): " << ce << " -> " << ss.str() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6ade49b6d..9608de743 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -373,7 +373,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) for (const Node& fc : fail_cvs) { std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc); + TermDbSygus::toStreamSygus(ss, fc); Trace("sygus-engine") << ss.str() << " "; } Trace("sygus-engine") << std::endl; @@ -434,7 +434,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv; TypeNode tn = onv.getType(); std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + TermDbSygus::toStreamSygus(ss, onv); if (printDebug) { sygusEnumOut << " " << ss.str(); @@ -559,7 +559,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Node v = candidate_values[i]; std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, v); + TermDbSygus::toStreamSygus(ss, v); out << "(" << d_quant[0][i] << " " << ss.str() << ")"; } out << ")" << std::endl; @@ -1193,8 +1193,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } else { - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(out, sol); + Node bsol = datatypes::utils::sygusToBuiltin(sol, true); + out << bsol; } out << ")" << std::endl; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ac1c7d342..c2a02e715 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -723,19 +723,18 @@ void TermDbSygus::toStreamSygus(const char* c, Node n) { if (Trace.isOn(c)) { - if (n.isNull()) - { - Trace(c) << n; - } - else - { - std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); - Trace(c) << ss.str(); - } + std::stringstream ss; + toStreamSygus(ss, n); + Trace(c) << ss.str(); } } +void TermDbSygus::toStreamSygus(std::ostream& out, Node n) +{ + // use external conversion + out << datatypes::utils::sygusToBuiltin(n, true); +} + SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) { AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end()); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 97cdc6ddd..921b08de5 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -310,7 +310,9 @@ class TermDbSygus { /** print to sygus stream n on trace c */ static void toStreamSygus(const char* c, Node n); - + /** print to sygus stream n on output out */ + static void toStreamSygus(std::ostream& out, Node n); + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; |