summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/printer/printer.cpp18
-rw-r--r--src/printer/printer.h8
-rw-r--r--src/printer/smt2/smt2_printer.cpp37
-rw-r--r--src/printer/smt2/smt2_printer.h8
-rw-r--r--src/smt/command.cpp16
-rw-r--r--src/smt/command.h19
-rw-r--r--src/smt/dump.h11
-rw-r--r--src/smt/smt_engine.cpp33
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback