diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/printer.cpp | 18 | ||||
-rw-r--r-- | src/printer/printer.h | 8 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 37 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 8 | ||||
-rw-r--r-- | src/smt/command.cpp | 16 | ||||
-rw-r--r-- | src/smt/command.h | 19 | ||||
-rw-r--r-- | src/smt/dump.h | 11 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 33 |
8 files changed, 125 insertions, 25 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 67dbe1036..4b1fbbe22 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -117,5 +117,23 @@ Printer* Printer::getPrinter(OutputLanguage lang) return d_printers[lang].get(); } +/** + * Write an error to `out` stating that command `name` is not supported by this + * printer. + */ +void printUnknownCommand(std::ostream& out, const std::string& name) +{ + out << "ERROR: don't know how to print " << name << " command" << std::endl; +} + +void Printer::toStreamCmdSynthFun(std::ostream& out, + const std::string& sym, + const std::vector<Node>& vars, + TypeNode range, + bool isInv, + TypeNode sygusType) +{ + printUnknownCommand(out, "synth-fun"); +} }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index fd788209c..918a95729 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -65,6 +65,14 @@ class Printer /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const; + /** Print synth-fun command */ + virtual void toStreamCmdSynthFun(std::ostream& out, + const std::string& sym, + const std::vector<Node>& vars, + TypeNode range, + bool isInv, + TypeNode sygusType); + 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 b92490ae2..96a7f634d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1304,7 +1304,6 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream<CommentCommand>(out, c, d_variant) || tryToStream<EmptyCommand>(out, c) || tryToStream<EchoCommand>(out, c, d_variant) - || tryToStream<SynthFunCommand>(out, c) || tryToStream<DeclareSygusFunctionCommand>(out, c) || tryToStream<DeclareSygusVarCommand>(out, c) || tryToStream<SygusConstraintCommand>(out, c) @@ -2019,16 +2018,15 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) -------------------------------------------------------------------------- */ -static void toStreamSygusGrammar(std::ostream& out, const Type& t) +static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t) { - if (!t.isNull() && t.isDatatype() - && TypeNode::fromType(t).getDType().isSygus()) + if (!t.isNull() && t.isDatatype() && t.getDType().isSygus()) { std::stringstream types_predecl, types_list; std::set<TypeNode> grammarTypes; std::list<TypeNode> typesToPrint; - grammarTypes.insert(TypeNode::fromType(t)); - typesToPrint.push_back(TypeNode::fromType(t)); + grammarTypes.insert(t); + typesToPrint.push_back(t); NodeManager* nm = NodeManager::currentNM(); // for each datatype in grammar // name @@ -2067,7 +2065,8 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t) } Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren); // now, print it using the conversion to builtin with external - types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, true); + types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint, + true); types_list << ' '; } types_list << "))\n"; @@ -2077,35 +2076,39 @@ static void toStreamSygusGrammar(std::ostream& out, const Type& t) } } -static void toStream(std::ostream& out, const SynthFunCommand* c) +void Smt2Printer::toStreamCmdSynthFun(std::ostream& out, + const std::string& sym, + const std::vector<Node>& vars, + TypeNode range, + bool isInv, + TypeNode sygusType) { - out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) + out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym) << ' '; - const std::vector<api::Term>& vars = c->getVars(); out << '('; if (!vars.empty()) { // print variable list - std::vector<api::Term>::const_iterator i = vars.begin(), i_end = vars.end(); - out << '(' << *i << ' ' << i->getSort() << ')'; + std::vector<Node>::const_iterator i = vars.cbegin(), i_end = vars.cend(); + out << '(' << *i << ' ' << i->getType() << ')'; ++i; while (i != i_end) { - out << " (" << *i << ' ' << i->getSort() << ')'; + out << " (" << *i << ' ' << i->getType() << ')'; ++i; } } out << ')'; // if not invariant-to-synthesize, print return type - if (!c->isInv()) + if (!isInv) { - out << ' ' << c->getSort(); + out << ' ' << range; } out << '\n'; // print grammar, if any - if (c->getGrammar() != nullptr) + if (sygusType != TypeNode::null()) { - out << *c->getGrammar(); + toStreamSygusGrammar(out, sygusType); } out << ')'; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 640521a67..cb1ffe9bd 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -58,6 +58,14 @@ class Smt2Printer : public CVC4::Printer { */ void toStream(std::ostream& out, const UnsatCore& core) const override; + /** Print synth fun command */ + void toStreamCmdSynthFun(std::ostream& out, + const std::string& sym, + const std::vector<Node>& vars, + TypeNode range, + bool isInv, + TypeNode sygusType) override; + private: void toStream( std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 4d8f6d910..f5c997318 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -719,6 +719,22 @@ std::string SynthFunCommand::getCommandName() const return d_isInv ? "synth-inv" : "synth-fun"; } +void SynthFunCommand::toStream(std::ostream& out, + int toDepth, + bool types, + size_t dag, + OutputLanguage language) const +{ + std::vector<Node> nodeVars = termVectorToNodes(d_vars); + Printer::getPrinter(language)->toStreamCmdSynthFun( + out, + d_symbol, + nodeVars, + TypeNode::fromType(d_sort.getType()), + d_isInv, + TypeNode::fromType(d_grammar->resolve().getType())); +} + /* -------------------------------------------------------------------------- */ /* class SygusConstraintCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 1674e0a62..fb7660b70 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -205,11 +205,12 @@ class CVC4_PUBLIC Command virtual void invoke(SmtEngine* smtEngine) = 0; virtual void invoke(SmtEngine* smtEngine, std::ostream& out); - void toStream(std::ostream& out, - int toDepth = -1, - bool types = false, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const; + virtual void toStream( + std::ostream& out, + int toDepth = -1, + bool types = false, + size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const; std::string toString() const; @@ -748,6 +749,14 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand /** returns this command's name */ std::string getCommandName() const override; + /** prints the Synth-fun command */ + void toStream( + std::ostream& out, + int toDepth = -1, + bool types = false, + size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const override; + protected: /** the function-to-synthesize */ api::Term d_fun; diff --git a/src/smt/dump.h b/src/smt/dump.h index 050935422..693baede2 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -40,6 +40,17 @@ class CVC4_PUBLIC CVC4dumpstream return *this; } + // Note(abdoo8080): temporarily overloading operator<< for strings to allow us + // to print commands provided as strings + CVC4dumpstream& operator<<(const std::string& str) + { + if (d_os != nullptr) + { + (*d_os) << str << std::endl; + } + return *this; + } + private: std::ostream* d_os; }; /* class CVC4dumpstream */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 13865b2ec..7f6d3db9d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1324,9 +1324,36 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; - // dumping SynthFunCommand from smt-engine is currently broken (please take at - // CVC4/cvc4-projects#211) - // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); + + // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot + // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we + // must print the command using the Node-level utility method for now. + + if (Dump.isOn("raw-benchmark")) + { + std::vector<Node> nodeVars; + nodeVars.reserve(vars.size()); + for (const Expr& var : vars) + { + nodeVars.push_back(Node::fromExpr(var)); + } + + std::stringstream ss; + + Printer::getPrinter(options::outputLanguage()) + ->toStreamCmdSynthFun( + ss, + id, + nodeVars, + func.getType().isFunction() + ? TypeNode::fromType(func.getType()).getRangeType() + : TypeNode::fromType(func.getType()), + isInv, + TypeNode::fromType(sygusType)); + + Dump("raw-benchmark") << ss.str(); + } + // sygus conjecture is now stale setSygusConjectureStale(); } |