summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.h6
-rw-r--r--src/printer/ast/ast_printer.cpp253
-rw-r--r--src/printer/ast/ast_printer.h148
-rw-r--r--src/printer/cvc/cvc_printer.cpp380
-rw-r--r--src/printer/cvc/cvc_printer.h150
-rw-r--r--src/printer/printer.cpp310
-rw-r--r--src/printer/printer.h213
-rw-r--r--src/printer/smt2/smt2_printer.cpp451
-rw-r--r--src/printer/smt2/smt2_printer.h190
-rw-r--r--src/printer/tptp/tptp_printer.cpp9
-rw-r--r--src/printer/tptp/tptp_printer.h23
-rw-r--r--src/smt/command.cpp583
-rw-r--r--src/smt/command.h336
13 files changed, 2305 insertions, 747 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 7e91b3b99..6c84b73bc 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -44,6 +44,8 @@ class Datatype;
class DatatypeConstructor;
class DatatypeConstructorArg;
class ExprManager;
+class GetAbductCommand;
+class GetInterpolCommand;
class NodeManager;
class SmtEngine;
class SynthFunCommand;
@@ -1950,8 +1952,10 @@ std::ostream& operator<<(std::ostream& out,
*/
class CVC4_PUBLIC Grammar
{
- friend class Solver;
+ friend class CVC4::GetAbductCommand;
+ friend class CVC4::GetInterpolCommand;
friend class CVC4::SynthFunCommand;
+ friend class Solver;
public:
/**
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 1923594f3..d4f28c186 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -132,55 +132,6 @@ void AstPrinter::toStream(std::ostream& out,
template <class T>
static bool tryToStream(std::ostream& out, const Command* c);
-void AstPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if(tryToStream<EmptyCommand>(out, c) ||
- tryToStream<AssertCommand>(out, c) ||
- tryToStream<PushCommand>(out, c) ||
- tryToStream<PopCommand>(out, c) ||
- tryToStream<CheckSatCommand>(out, c) ||
- tryToStream<CheckSatAssumingCommand>(out, c) ||
- tryToStream<QueryCommand>(out, c) ||
- tryToStream<ResetCommand>(out, c) ||
- tryToStream<ResetAssertionsCommand>(out, c) ||
- tryToStream<QuitCommand>(out, c) ||
- tryToStream<DeclarationSequence>(out, c) ||
- tryToStream<CommandSequence>(out, c) ||
- tryToStream<DeclareFunctionCommand>(out, c) ||
- tryToStream<DeclareTypeCommand>(out, c) ||
- tryToStream<DefineTypeCommand>(out, c) ||
- tryToStream<DefineNamedFunctionCommand>(out, c) ||
- tryToStream<DefineFunctionCommand>(out, c) ||
- tryToStream<SimplifyCommand>(out, c) ||
- tryToStream<GetValueCommand>(out, c) ||
- tryToStream<GetModelCommand>(out, c) ||
- tryToStream<GetAssignmentCommand>(out, c) ||
- tryToStream<GetAssertionsCommand>(out, c) ||
- tryToStream<GetProofCommand>(out, c) ||
- tryToStream<SetBenchmarkStatusCommand>(out, c) ||
- tryToStream<SetBenchmarkLogicCommand>(out, c) ||
- tryToStream<SetInfoCommand>(out, c) ||
- tryToStream<GetInfoCommand>(out, c) ||
- tryToStream<SetOptionCommand>(out, c) ||
- tryToStream<GetOptionCommand>(out, c) ||
- tryToStream<DatatypeDeclarationCommand>(out, c) ||
- tryToStream<CommentCommand>(out, c)) {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* AstPrinter::toStream(Command*) */
-
template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s);
@@ -211,198 +162,236 @@ void AstPrinter::toStream(std::ostream& out,
Unreachable();
}
-static void toStream(std::ostream& out, const EmptyCommand* c)
+void AstPrinter::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
{
- out << "EmptyCommand(" << c->getName() << ")";
+ out << "EmptyCommand(" << name << ')';
}
-static void toStream(std::ostream& out, const AssertCommand* c)
+void AstPrinter::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- out << "Assert(" << c->getExpr() << ")";
+ out << "EchoCommand(" << output << ')';
}
-static void toStream(std::ostream& out, const PushCommand* c)
+void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "Push()";
+ out << "Assert(" << n << ')';
}
-static void toStream(std::ostream& out, const PopCommand* c) { out << "Pop()"; }
+void AstPrinter::toStreamCmdPush(std::ostream& out) const { out << "Push()"; }
+
+void AstPrinter::toStreamCmdPop(std::ostream& out) const { out << "Pop()"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(e.isNull()) {
+ if (n.isNull())
+ {
out << "CheckSat()";
- } else {
- out << "CheckSat(" << e << ")";
+ }
+ else
+ {
+ out << "CheckSat(" << n << ')';
}
}
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void AstPrinter::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
- const vector<Expr>& terms = c->getTerms();
out << "CheckSatAssuming( << ";
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
out << ">> )";
}
-static void toStream(std::ostream& out, const QueryCommand* c)
+void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
- out << "Query(" << c->getExpr() << ')';
+ out << "Query(" << n << ')';
}
-static void toStream(std::ostream& out, const ResetCommand* c)
-{
- out << "Reset()";
-}
+void AstPrinter::toStreamCmdReset(std::ostream& out) const { out << "Reset()"; }
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "ResetAssertions()";
}
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
- out << "Quit()";
-}
+void AstPrinter::toStreamCmdQuit(std::ostream& out) const { out << "Quit()"; }
-static void toStream(std::ostream& out, const DeclarationSequence* c)
+void AstPrinter::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
out << "DeclarationSequence[" << endl;
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
out << "]";
}
-static void toStream(std::ostream& out, const CommandSequence* c)
+void AstPrinter::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
out << "CommandSequence[" << endl;
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
out << "]";
}
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- out << "Declare(" << c->getSymbol() << "," << c->getType() << ")";
+ out << "Declare(" << id << "," << type << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const std::vector<Expr>& formals = c->getFormals();
- Expr formula = c->getFormula();
- out << "DefineFunction( \"" << func << "\", [";
- if(formals.size() > 0) {
- copy( formals.begin(), formals.end() - 1,
- ostream_iterator<Expr>(out, ", ") );
+ out << "DefineFunction( \"" << id << "\", [";
+ if (formals.size() > 0)
+ {
+ copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
out << formals.back();
}
out << "], << " << formula << " >> )";
}
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << ","
- << c->getType() << ")";
+ out << "DeclareType(" << id << "," << arity << "," << type << ')';
}
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void AstPrinter::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- const vector<Type>& params = c->getParameters();
- out << "DefineType(" << c->getSymbol() << ",[";
- if(params.size() > 0) {
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(out, ", ") );
+ out << "DefineType(" << id << ",[";
+ if (params.size() > 0)
+ {
+ copy(params.begin(),
+ params.end() - 1,
+ ostream_iterator<TypeNode>(out, ", "));
out << params.back();
}
- out << "]," << c->getType() << ")";
+ out << "]," << t << ')';
}
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
out << "DefineNamedFunction( ";
- toStream(out, static_cast<const DefineFunctionCommand*>(c));
- out << " )";
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
+ out << " )" << std::endl;
}
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "Simplify( << " << c->getTerm() << " >> )";
+ out << "Simplify( << " << n << " >> )";
}
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void AstPrinter::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
out << "GetValue( << ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
out << ">> )";
}
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
{
out << "GetModel()";
}
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "GetAssignment()";
}
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+
+void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "GetAssertions()";
}
-static void toStream(std::ostream& out, const GetProofCommand* c)
+
+void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
{
out << "GetProof()";
}
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c)
+
+void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
- out << "SetBenchmarkStatus(" << c->getStatus() << ")";
+ out << "GetUnsatCore()";
}
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "SetBenchmarkLogic(" << c->getLogic() << ")";
+ out << "SetBenchmarkStatus(" << status << ')';
}
-static void toStream(std::ostream& out, const SetInfoCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
+ out << "SetBenchmarkLogic(" << logic << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "GetInfo(" << c->getFlag() << ")";
+ out << "SetInfo(" << flag << ", " << sexpr << ')';
}
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+
+void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
+{
+ out << "GetInfo(" << flag << ')';
+}
+
+void AstPrinter::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
+ out << "SetOption(" << flag << ", " << sexpr << ')';
}
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void AstPrinter::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "GetOption(" << c->getFlag() << ")";
+ out << "GetOption(" << flag << ')';
}
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c)
+void AstPrinter::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const vector<Type>& datatypes = c->getDatatypes();
out << "DatatypeDeclarationCommand([";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
out << t << ";" << endl;
}
out << "])";
}
-static void toStream(std::ostream& out, const CommentCommand* c)
+void AstPrinter::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- out << "CommentCommand([" << c->getComment() << "])";
+ out << "CommentCommand([" << comment << "])";
}
template <class T>
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 2fd7da749..17e052037 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -27,7 +27,8 @@ namespace CVC4 {
namespace printer {
namespace ast {
-class AstPrinter : public CVC4::Printer {
+class AstPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
@@ -35,23 +36,150 @@ class AstPrinter : public CVC4::Printer {
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
private:
void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
void toStream(std::ostream& out,
const Model& m,
const Command* c) const override;
-};/* class AstPrinter */
+}; /* class AstPrinter */
-}/* CVC4::printer::ast namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace ast
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__AST_PRINTER_H */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 243592456..8120d1d88 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1038,57 +1038,6 @@ void CvcPrinter::toStream(
template <class T>
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
-void CvcPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
- tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
- tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) ||
- tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
- tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
- tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
- tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
- tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
- tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
- tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
- tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* CvcPrinter::toStream(Command*) */
-
template <class T>
static bool tryToStream(std::ostream& out,
const CommandStatus* s,
@@ -1245,294 +1194,316 @@ void CvcPrinter::toStream(std::ostream& out,
}
}
-static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "ASSERT " << c->getExpr() << ";";
+ out << "ASSERT " << n << ';';
}
-static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
-{
- out << "PUSH;";
-}
+void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; }
-static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
-{
- out << "POP;";
-}
+void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << "PUSH; ";
}
- if(!e.isNull()) {
- out << "CHECKSAT " << e << ";";
- } else {
+ if (!n.isNull())
+ {
+ out << "CHECKSAT " << n << ';';
+ }
+ else
+ {
out << "CHECKSAT;";
}
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << " POP;";
}
}
-static void toStream(std::ostream& out,
- const CheckSatAssumingCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
- const vector<Expr>& exprs = c->getTerms();
- if (cvc3Mode)
+ if (d_cvc3Mode)
{
out << "PUSH; ";
}
out << "CHECKSAT";
- if (exprs.size() > 0)
+ if (nodes.size() > 0)
{
- out << " " << exprs[0];
- for (size_t i = 1, n = exprs.size(); i < n; ++i)
+ out << ' ' << nodes[0];
+ for (size_t i = 1, n = nodes.size(); i < n; ++i)
{
- out << " AND " << exprs[i];
+ out << " AND " << nodes[i];
}
}
- out << ";";
- if (cvc3Mode)
+ out << ';';
+ if (d_cvc3Mode)
{
out << " POP;";
}
}
-static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << "PUSH; ";
}
- if(!e.isNull()) {
- out << "QUERY " << e << ";";
- } else {
+ if (!n.isNull())
+ {
+ out << "QUERY " << n << ';';
+ }
+ else
+ {
out << "QUERY TRUE;";
}
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << " POP;";
}
}
-static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
-{
- out << "RESET;";
-}
+void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; }
-static void toStream(std::ostream& out,
- const ResetAssertionsCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "RESET ASSERTIONS;";
}
-static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
{
- //out << "EXIT;";
+ // out << "EXIT;";
}
-static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
}
-static void toStream(std::ostream& out,
- const DeclarationSequence* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- DeclarationSequence::const_iterator i = c->begin();
- for(;;) {
+ DeclarationSequence::const_iterator i = sequence.cbegin();
+ for (;;)
+ {
DeclarationDefinitionCommand* dd =
- static_cast<DeclarationDefinitionCommand*>(*i++);
- if(i != c->end()) {
+ static_cast<DeclarationDefinitionCommand*>(*i++);
+ if (i != sequence.cend())
+ {
out << dd->getSymbol() << ", ";
- } else {
+ }
+ else
+ {
out << *dd;
break;
}
}
}
-static void toStream(std::ostream& out,
- const DeclareFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- out << c->getSymbol() << " : " << c->getType() << ";";
+ out << id << " : " << type << ';';
}
-static void toStream(std::ostream& out,
- const DefineFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const vector<Expr>& formals = c->getFormals();
- Expr formula = c->getFormula();
- out << func << " : " << func.getType() << " = ";
- if(formals.size() > 0) {
+ std::vector<TypeNode> sorts;
+ sorts.reserve(formals.size() + 1);
+ for (const Node& n : formals)
+ {
+ sorts.push_back(n.getType());
+ }
+ sorts.push_back(range);
+
+ out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts)
+ << " = ";
+ if (formals.size() > 0)
+ {
out << "LAMBDA(";
- vector<Expr>::const_iterator i = formals.begin();
- while(i != formals.end()) {
+ vector<Node>::const_iterator i = formals.cbegin();
+ while (i != formals.end())
+ {
out << (*i) << ":" << (*i).getType();
- if(++i != formals.end()) {
+ if (++i != formals.end())
+ {
out << ", ";
}
}
out << "): ";
}
- out << formula << ";";
+ out << formula << ';';
}
-static void toStream(std::ostream& out,
- const DeclareTypeCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- if(c->getArity() > 0) {
- //TODO?
+ if (arity > 0)
+ {
+ // TODO?
out << "ERROR: Don't know how to print parameterized type declaration "
- "in CVC language." << endl;
- } else {
- out << c->getSymbol() << " : TYPE;";
+ "in CVC language."
+ << std::endl;
+ }
+ else
+ {
+ out << id << " : TYPE;";
}
}
-static void toStream(std::ostream& out,
- const DefineTypeCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- if(c->getParameters().size() > 0) {
+ if (params.size() > 0)
+ {
out << "ERROR: Don't know how to print parameterized type definition "
- "in CVC language:" << endl << c->toString() << endl;
- } else {
- out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
+ "in CVC language:"
+ << std::endl;
+ }
+ else
+ {
+ out << id << " : TYPE = " << t << ';';
}
}
-static void toStream(std::ostream& out,
- const DefineNamedFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
}
-static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "TRANSFORM " << c->getTerm() << ";";
+ out << "TRANSFORM " << n << ';';
}
-static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
- const vector<Expr>& terms = c->getTerms();
- Assert(!terms.empty());
+ Assert(!nodes.empty());
out << "GET_VALUE ";
- copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
- out << terms.back() << ";";
+ copy(nodes.begin(),
+ nodes.end() - 1,
+ ostream_iterator<Node>(out, ";\nGET_VALUE "));
+ out << nodes.back() << ';';
}
-static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
{
out << "COUNTERMODEL;";
}
-static void toStream(std::ostream& out,
- const GetAssignmentCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "% (get-assignment)";
}
-static void toStream(std::ostream& out,
- const GetAssertionsCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "WHERE;";
}
-static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
{
out << "DUMP_PROOF;";
}
-static void toStream(std::ostream& out,
- const GetUnsatCoreCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
out << "DUMP_UNSAT_CORE;";
}
-static void toStream(std::ostream& out,
- const SetBenchmarkStatusCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "% (set-info :status " << c->getStatus() << ")";
+ out << "% (set-info :status " << status << ')';
}
-static void toStream(std::ostream& out,
- const SetBenchmarkLogicCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
+ out << "OPTION \"logic\" \"" << logic << "\";";
}
-static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "% (set-info " << c->getFlag() << " ";
+ out << "% (set-info " << flag << ' ';
OutputLanguage language =
- cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
- SExpr::toStream(out, c->getSExpr(), language);
- out << ")";
+ d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+ SExpr::toStream(out, sexpr, language);
+ out << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
{
- out << "% (get-info " << c->getFlag() << ")";
+ out << "% (get-info " << flag << ')';
}
-static void toStream(std::ostream& out,
- const SetOptionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "OPTION \"" << c->getFlag() << "\" ";
- SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
- out << ";";
+ out << "OPTION \"" << flag << "\" ";
+ SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
+ out << ';';
}
-static void toStream(std::ostream& out,
- const GetOptionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "% (get-option " << c->getFlag() << ")";
+ out << "% (get-option " << flag << ')';
}
-static void toStream(std::ostream& out,
- const DatatypeDeclarationCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const vector<Type>& datatypes = c->getDatatypes();
Assert(!datatypes.empty() && datatypes[0].isDatatype());
- const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType();
- //do not print tuple/datatype internal declarations
+ const DType& dt0 = datatypes[0].getDType();
+ // do not print tuple/datatype internal declarations
if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
{
out << "DATATYPE" << endl;
bool firstDatatype = true;
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
- if(! firstDatatype) {
+ if (!firstDatatype)
+ {
out << ',' << endl;
}
- const DType& dt = TypeNode::fromType(t).getDType();
+ const DType& dt = t.getDType();
out << " " << dt.getName();
- if(dt.isParametric()) {
+ if (dt.isParametric())
+ {
out << '[';
- for(size_t j = 0; j < dt.getNumParameters(); ++j) {
- if(j > 0) {
+ for (size_t j = 0; j < dt.getNumParameters(); ++j)
+ {
+ if (j > 0)
+ {
out << ',';
}
out << dt.getParameter(j);
@@ -1578,16 +1549,21 @@ static void toStream(std::ostream& out,
}
}
-static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- out << "% " << c->getComment();
+ out << "% " << comment;
}
-static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
+void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
+{
+}
-static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- out << "ECHO \"" << c->getOutput() << "\";";
+ out << "ECHO \"" << output << "\";";
}
template <class T>
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index f5a06a082..0fd3d3a49 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -27,23 +27,151 @@ namespace CVC4 {
namespace printer {
namespace cvc {
-class CvcPrinter : public CVC4::Printer {
+class CvcPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
- CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
+ CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {}
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
private:
void toStream(
std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
@@ -52,10 +180,10 @@ class CvcPrinter : public CVC4::Printer {
const Command* c) const override;
bool d_cvc3Mode;
-};/* class CvcPrinter */
+}; /* class CvcPrinter */
-}/* CVC4::printer::cvc namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace cvc
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__CVC_PRINTER_H */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 4b1fbbe22..0e7550518 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -85,8 +85,7 @@ void Printer::toStream(std::ostream& out, const Model& m) const
void Printer::toStream(std::ostream& out, const UnsatCore& core) const
{
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
- AssertCommand cmd(*i);
- toStream(out, &cmd, -1, false, -1);
+ toStreamCmdAssert(out, Node::fromExpr(*i));
out << std::endl;
}
}/* Printer::toStream(UnsatCore) */
@@ -117,23 +116,316 @@ 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)
+void Printer::printUnknownCommand(std::ostream& out,
+ const std::string& name) const
{
out << "ERROR: don't know how to print " << name << " command" << std::endl;
}
+void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
+{
+ printUnknownCommand(out, "empty");
+}
+
+void Printer::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
+{
+ printUnknownCommand(out, "echo");
+}
+
+void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "assert");
+}
+
+void Printer::toStreamCmdPush(std::ostream& out) const
+{
+ printUnknownCommand(out, "push");
+}
+
+void Printer::toStreamCmdPop(std::ostream& out) const
+{
+ printUnknownCommand(out, "pop");
+}
+
+void Printer::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-fun");
+}
+
+void Printer::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-sort");
+}
+
+void Printer::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
+{
+ printUnknownCommand(out, "define-sort");
+}
+
+void Printer::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
+{
+ printUnknownCommand(out, "define-fun");
+}
+
+void Printer::toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
+{
+ printUnknownCommand(out, "define-named-function");
+}
+
+void Printer::toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const
+{
+ printUnknownCommand(out, "define-fun-rec");
+}
+
+void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
+ const std::string& attr,
+ Node n) const
+{
+ printUnknownCommand(out, "set-user-attribute");
+}
+
+void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "check-sat");
+}
+
+void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "check-sat-assuming");
+}
+
+void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "query");
+}
+
+void Printer::toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-var");
+}
+
void Printer::toStreamCmdSynthFun(std::ostream& out,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType)
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun");
+}
+
+void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "constraint");
+}
+
+void Printer::toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const
+{
+ printUnknownCommand(out, "inv-constraint");
+}
+
+void Printer::toStreamCmdCheckSynth(std::ostream& out) const
+{
+ printUnknownCommand(out, "check-synth");
+}
+
+void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "simplify");
+}
+
+void Printer::toStreamCmdExpandDefinitions(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "expand-definitions");
+}
+
+void Printer::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "get-value");
+}
+
+void Printer::toStreamCmdGetAssignment(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-assignment");
+}
+
+void Printer::toStreamCmdGetModel(std::ostream& out) const
+{
+ printUnknownCommand(out, "ge-model");
+}
+
+void Printer::toStreamCmdBlockModel(std::ostream& out) const
+{
+ printUnknownCommand(out, "block-model");
+}
+
+void Printer::toStreamCmdBlockModelValues(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "block-model-values");
+}
+
+void Printer::toStreamCmdGetProof(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-proof");
+}
+
+void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-instantiations");
+}
+
+void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-synth-solution");
+}
+
+void Printer::toStreamCmdGetInterpol(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, "get-interpol");
+}
+
+void Printer::toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, "get-abduct");
+}
+
+void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
+ Node n) const
+{
+ printUnknownCommand(out, "get-quantifier-elimination");
+}
+
+void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-unsat-assumption");
+}
+
+void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-unsat-core");
+}
+
+void Printer::toStreamCmdGetAssertions(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-assertions");
+}
+
+void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
+{
+ printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
+{
+ printUnknownCommand(out, "set-logic");
+}
+
+void Printer::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
+{
+ printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
+{
+ printUnknownCommand(out, "get-info");
+}
+
+void Printer::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
+{
+ printUnknownCommand(out, "set-option");
+}
+
+void Printer::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
+{
+ printUnknownCommand(out, "get-option");
+}
+
+void Printer::toStreamCmdSetExpressionName(std::ostream& out,
+ Node n,
+ const std::string& name) const
+{
+ printUnknownCommand(out, "set-expression-name");
+}
+
+void Printer::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
+{
+ printUnknownCommand(
+ out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
+}
+
+void Printer::toStreamCmdReset(std::ostream& out) const
+{
+ printUnknownCommand(out, "reset");
+}
+
+void Printer::toStreamCmdResetAssertions(std::ostream& out) const
+{
+ printUnknownCommand(out, "reset-assertions");
+}
+
+void Printer::toStreamCmdQuit(std::ostream& out) const
+{
+ printUnknownCommand(out, "quit");
+}
+
+void Printer::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
+{
+ printUnknownCommand(out, "comment");
+}
+
+void Printer::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
+{
+ printUnknownCommand(out, "sequence");
+}
+
+void Printer::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- printUnknownCommand(out, "synth-fun");
+ printUnknownCommand(out, "sequence");
}
}/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 918a95729..3b737ec5f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -49,13 +49,6 @@ class Printer
bool types,
size_t dag) const = 0;
- /** Write a Command out to a stream with this Printer. */
- virtual void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const = 0;
-
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
@@ -65,13 +58,211 @@ class Printer
/** Write an UnsatCore out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const UnsatCore& core) const;
+ /** Print empty command */
+ virtual void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const;
+
+ /** Print echo command */
+ virtual void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const;
+
+ /** Print assert command */
+ virtual void toStreamCmdAssert(std::ostream& out, Node n) const;
+
+ /** Print push command */
+ virtual void toStreamCmdPush(std::ostream& out) const;
+
+ /** Print pop command */
+ virtual void toStreamCmdPop(std::ostream& out) const;
+
+ /** Print declare-fun command */
+ virtual void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const;
+
+ /** Print declare-sort command */
+ virtual void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const;
+
+ /** Print define-sort command */
+ virtual void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const;
+
+ /** Print define-fun command */
+ virtual void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const;
+
+ /** Print define-named-fun command */
+ virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const;
+
+ /** Print define-fun-rec command */
+ virtual void toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const;
+
+ /** Print set-user-attribute command */
+ void toStreamCmdSetUserAttribute(std::ostream& out,
+ const std::string& attr,
+ Node n) const;
+
+ /** Print check-sat command */
+ virtual void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const;
+
+ /** Print check-sat-assuming command */
+ virtual void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const;
+
+ /** Print query command */
+ virtual void toStreamCmdQuery(std::ostream& out, Node n) const;
+
+ /** Print declare-var command */
+ virtual void toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) 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);
+ TypeNode sygusType) const;
+
+ /** Print constraint command */
+ virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
+
+ /** Print inv-constraint command */
+ virtual void toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
+
+ /** Print check-synth command */
+ virtual void toStreamCmdCheckSynth(std::ostream& out) const;
+
+ /** Print simplify command */
+ virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
+
+ /** Print expand-definitions command */
+ void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const;
+
+ /** Print get-value command */
+ virtual void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const;
+
+ /** Print get-assignment command */
+ virtual void toStreamCmdGetAssignment(std::ostream& out) const;
+
+ /** Print get-model command */
+ virtual void toStreamCmdGetModel(std::ostream& out) const;
+
+ /** Print block-model command */
+ void toStreamCmdBlockModel(std::ostream& out) const;
+
+ /** Print block-model-values command */
+ void toStreamCmdBlockModelValues(std::ostream& out,
+ const std::vector<Node>& nodes) const;
+
+ /** Print get-proof command */
+ virtual void toStreamCmdGetProof(std::ostream& out) const;
+
+ /** Print get-instantiations command */
+ void toStreamCmdGetInstantiations(std::ostream& out) const;
+
+ /** Print get-synth-solution command */
+ void toStreamCmdGetSynthSolution(std::ostream& out) const;
+
+ /** Print get-interpol command */
+ void toStreamCmdGetInterpol(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const;
+
+ /** Print get-abduct command */
+ virtual void toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const;
+
+ /** Print get-quantifier-elimination command */
+ void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
+
+ /** Print get-unsat-assumptions command */
+ virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;
+
+ /** Print get-unsat-core command */
+ virtual void toStreamCmdGetUnsatCore(std::ostream& out) const;
+
+ /** Print get-assertions command */
+ virtual void toStreamCmdGetAssertions(std::ostream& out) const;
+
+ /** Print set-info :status command */
+ virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const;
+
+ /** Print set-logic command */
+ virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const;
+
+ /** Print set-info command */
+ virtual void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const;
+
+ /** Print get-info command */
+ virtual void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const;
+
+ /** Print set-option command */
+ virtual void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const;
+
+ /** Print get-option command */
+ virtual void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const;
+
+ /** Print set-expression-name command */
+ void toStreamCmdSetExpressionName(std::ostream& out,
+ Node n,
+ const std::string& name) const;
+
+ /** Print declare-datatype(s) command */
+ virtual void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const;
+
+ /** Print reset command */
+ virtual void toStreamCmdReset(std::ostream& out) const;
+
+ /** Print reset-assertions command */
+ virtual void toStreamCmdResetAssertions(std::ostream& out) const;
+
+ /** Print quit command */
+ virtual void toStreamCmdQuit(std::ostream& out) const;
+
+ /** Print comment command */
+ virtual void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const;
+
+ /** Print command sequence command */
+ virtual void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const;
+
+ /** Print declaration sequence command */
+ virtual void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const;
protected:
/** Derived classes can construct, but no one else. */
@@ -91,6 +282,12 @@ class Printer
getPrinter(lang)->toStream(out, m, c);
}
+ /**
+ * Write an error to `out` stating that command `name` is not supported by
+ * this printer.
+ */
+ void printUnknownCommand(std::ostream& out, const std::string& name) const;
+
private:
/** Disallow copy, assignment */
Printer(const Printer&) = delete;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 96a7f634d..3d76c81dc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1261,65 +1261,6 @@ static bool tryToStream(std::ostream& out, const Command* c);
template <class T>
static bool tryToStream(std::ostream& out, const Command* c, Variant v);
-void Smt2Printer::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
- || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c)
- || tryToStream<CheckSatAssumingCommand>(out, c)
- || tryToStream<QueryCommand>(out, c, d_variant)
- || tryToStream<ResetCommand>(out, c)
- || tryToStream<ResetAssertionsCommand>(out, c)
- || tryToStream<QuitCommand>(out, c)
- || tryToStream<DeclarationSequence>(out, c)
- || tryToStream<CommandSequence>(out, c)
- || tryToStream<DeclareFunctionCommand>(out, c)
- || tryToStream<DeclareTypeCommand>(out, c)
- || tryToStream<DefineTypeCommand>(out, c)
- || tryToStream<DefineNamedFunctionCommand>(out, c)
- || tryToStream<DefineFunctionCommand>(out, c)
- || tryToStream<DefineFunctionRecCommand>(out, c)
- || tryToStream<SimplifyCommand>(out, c)
- || tryToStream<GetValueCommand>(out, c)
- || tryToStream<GetModelCommand>(out, c)
- || tryToStream<GetAssignmentCommand>(out, c)
- || tryToStream<GetAssertionsCommand>(out, c)
- || tryToStream<GetProofCommand>(out, c)
- || tryToStream<GetUnsatAssumptionsCommand>(out, c)
- || tryToStream<GetUnsatCoreCommand>(out, c)
- || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
- || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
- || tryToStream<SetInfoCommand>(out, c, d_variant)
- || tryToStream<GetInfoCommand>(out, c)
- || tryToStream<SetOptionCommand>(out, c)
- || tryToStream<GetOptionCommand>(out, c)
- || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
- || tryToStream<CommentCommand>(out, c, d_variant)
- || tryToStream<EmptyCommand>(out, c)
- || tryToStream<EchoCommand>(out, c, d_variant)
- || tryToStream<DeclareSygusFunctionCommand>(out, c)
- || tryToStream<DeclareSygusVarCommand>(out, c)
- || tryToStream<SygusConstraintCommand>(out, c)
- || tryToStream<SygusInvConstraintCommand>(out, c)
- || tryToStream<CheckSynthCommand>(out, c)
- || tryToStream<GetAbductCommand>(out, c))
- {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* Smt2Printer::toStream(Command*) */
-
-
static std::string quoteSymbol(TNode n) {
std::stringstream ss;
ss << n;
@@ -1494,7 +1435,7 @@ void Smt2Printer::toStream(std::ostream& out,
else if (const DatatypeDeclarationCommand* datatype_declaration_command =
dynamic_cast<const DatatypeDeclarationCommand*>(command))
{
- toStream(out, datatype_declaration_command, -1, false, 1);
+ out << datatype_declaration_command;
}
else
{
@@ -1502,147 +1443,156 @@ void Smt2Printer::toStream(std::ostream& out,
}
}
-static void toStream(std::ostream& out, const AssertCommand* c)
+void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "(assert " << c->getExpr() << ")";
+ out << "(assert " << n << ')';
}
-static void toStream(std::ostream& out, const PushCommand* c)
+void Smt2Printer::toStreamCmdPush(std::ostream& out) const
{
out << "(push 1)";
}
-static void toStream(std::ostream& out, const PopCommand* c)
-{
- out << "(pop 1)";
-}
+void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) {
- out << PushCommand() << endl
- << AssertCommand(e) << endl
- << CheckSatCommand() << endl
- << PopCommand();
- } else {
+ if (!n.isNull())
+ {
+ toStreamCmdPush(out);
+ out << std::endl;
+ toStreamCmdAssert(out, n);
+ out << std::endl;
+ toStreamCmdCheckSat(out);
+ out << std::endl;
+ toStreamCmdPop(out);
+ }
+ else
+ {
out << "(check-sat)";
}
}
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void Smt2Printer::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
out << "(check-sat-assuming ( ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
out << "))";
}
-static void toStream(std::ostream& out, const QueryCommand* c, Variant v)
+void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(!e.isNull()) {
- if (v == smt2_0_variant)
+ if (!n.isNull())
+ {
+ if (d_variant == smt2_0_variant)
{
- out << PushCommand() << endl
- << AssertCommand(BooleanSimplification::negate(e)) << endl
- << CheckSatCommand() << endl
- << PopCommand();
+ toStreamCmdCheckSat(out, BooleanSimplification::negate(n));
}
else
{
- out << CheckSatAssumingCommand(e.notExpr()) << endl;
+ toStreamCmdCheckSatAssuming(out, {n});
}
- } else {
- out << "(check-sat)";
+ }
+ else
+ {
+ toStreamCmdCheckSat(out);
}
}
-static void toStream(std::ostream& out, const ResetCommand* c)
+void Smt2Printer::toStreamCmdReset(std::ostream& out) const
{
out << "(reset)";
}
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "(reset-assertions)";
}
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
- out << "(exit)";
-}
+void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
-static void toStream(std::ostream& out, const CommandSequence* c)
+void Smt2Printer::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- CommandSequence::const_iterator i = c->begin();
- if(i != c->end()) {
- for(;;) {
+ CommandSequence::const_iterator i = sequence.cbegin();
+ if (i != sequence.cend())
+ {
+ for (;;)
+ {
out << *i;
- if(++i != c->end()) {
+ if (++i != sequence.cend())
+ {
out << endl;
- } else {
+ }
+ else
+ {
break;
}
}
}
}
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void Smt2Printer::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
+{
+ toStreamCmdCommandSequence(out, sequence);
+}
+
+void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- Type type = c->getType();
- out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
- if(type.isFunction()) {
- FunctionType ft = type;
- const vector<Type> argTypes = ft.getArgTypes();
- if(argTypes.size() > 0) {
- copy( argTypes.begin(), argTypes.end() - 1,
- ostream_iterator<Type>(out, " ") );
+ out << "(declare-fun " << CVC4::quoteSymbol(id) << " (";
+ if (type.isFunction())
+ {
+ const vector<TypeNode> argTypes = type.getArgTypes();
+ if (argTypes.size() > 0)
+ {
+ copy(argTypes.begin(),
+ argTypes.end() - 1,
+ ostream_iterator<TypeNode>(out, " "));
out << argTypes.back();
}
- type = ft.getRangeType();
+ type = type.getRangeType();
}
- out << ") " << type << ")";
+ out << ") " << type << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const vector<Expr>* formals = &c->getFormals();
- out << "(define-fun " << func << " (";
- Type type = func.getType();
- Expr formula = c->getFormula();
- if(type.isFunction()) {
- vector<Expr> f;
- if(formals->empty()) {
- const vector<Type>& params = FunctionType(type).getArgTypes();
- for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
- f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
- NodeManager::SKOLEM_NO_NOTIFY).toExpr());
- }
- formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
- formals = &f;
- }
- vector<Expr>::const_iterator i = formals->begin();
- for(;;) {
+ out << "(define-fun " << id << " (";
+ if (!formals.empty())
+ {
+ vector<Node>::const_iterator i = formals.cbegin();
+ for (;;)
+ {
out << "(" << (*i) << " " << (*i).getType() << ")";
++i;
- if(i != formals->end()) {
+ if (i != formals.cend())
+ {
out << " ";
- } else {
+ }
+ else
+ {
break;
}
}
- type = FunctionType(type).getRangeType();
}
- out << ") " << type << " " << formula << ")";
+ out << ") " << range << ' ' << formula << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
+void Smt2Printer::toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const
{
- const vector<api::Term>& funcs = c->getFunctions();
- const vector<vector<api::Term> >& formals = c->getFormals();
out << "(define-fun";
if (funcs.size() > 1)
{
@@ -1665,10 +1615,10 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
}
out << funcs[i] << " (";
// print its type signature
- vector<api::Term>::const_iterator itf = formals[i].begin();
+ vector<Node>::const_iterator itf = formals[i].cbegin();
for (;;)
{
- out << "(" << (*itf) << " " << (*itf).getSort() << ")";
+ out << "(" << (*itf) << " " << (*itf).getType() << ")";
++itf;
if (itf != formals[i].end())
{
@@ -1679,8 +1629,8 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
break;
}
}
- api::Sort type = funcs[i].getSort();
- type = type.getFunctionCodomainSort();
+ TypeNode type = funcs[i].getType();
+ type = type.getRangeType();
out << ") " << type;
if (funcs.size() > 1)
{
@@ -1691,7 +1641,6 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
{
out << ") (";
}
- const vector<api::Term>& formulas = c->getFormulas();
for (unsigned i = 0, size = formulas.size(); i < size; i++)
{
if (i > 0)
@@ -1744,115 +1693,129 @@ static void toStreamRational(std::ostream& out,
}
}
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- out << "(declare-sort " << CVC4::quoteSymbol(c->getSymbol()) << " "
- << c->getArity() << ")";
+ out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")";
}
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- const vector<Type>& params = c->getParameters();
- out << "(define-sort " << c->getSymbol() << " (";
- if(params.size() > 0) {
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(out, " ") );
+ out << "(define-sort " << CVC4::quoteSymbol(id) << " (";
+ if (params.size() > 0)
+ {
+ copy(
+ params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
out << params.back();
}
- out << ") " << c->getType() << ")";
+ out << ") " << t << ")";
}
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
out << "DefineNamedFunction( ";
- toStream(out, static_cast<const DefineFunctionCommand*>(c));
- out << " )";
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
+ out << " )" << std::endl;
- out << "ERROR: don't know how to output define-named-function command" << endl;
+ printUnknownCommand(out, "define-named-function");
}
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "(simplify " << c->getTerm() << ")";
+ out << "(simplify " << n << ')';
}
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
out << "(get-value ( ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
out << "))";
}
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
{
out << "(get-model)";
}
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "(get-assignment)";
}
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "(get-assertions)";
}
-static void toStream(std::ostream& out, const GetProofCommand* c)
+void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
{
out << "(get-proof)";
}
-static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
{
out << "(get-unsat-assumptions)";
}
-static void toStream(std::ostream& out, const GetUnsatCoreCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
{
out << "(get-unsat-core)";
}
-static void toStream(std::ostream& out,
- const SetBenchmarkStatusCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "(set-info :status " << c->getStatus() << ")";
+ out << "(set-info :status " << status << ')';
}
-static void toStream(std::ostream& out,
- const SetBenchmarkLogicCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "(set-logic " << c->getLogic() << ")";
+ out << "(set-logic " << logic << ')';
}
-static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "(set-info :" << c->getFlag() << " ";
- SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
- out << ")";
+ out << "(set-info :" << flag << ' ';
+ SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
+ out << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
{
- out << "(get-info :" << c->getFlag() << ")";
+ out << "(get-info :" << flag << ')';
}
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "(set-option :" << c->getFlag() << " ";
- SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
- out << ")";
+ out << "(set-option :" << flag << ' ';
+ SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
+ out << ')';
}
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "(get-option :" << c->getFlag() << ")";
+ out << "(get-option :" << flag << ')';
}
-static void toStream(std::ostream& out, const DType& dt)
+void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
{
for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
@@ -1871,14 +1834,12 @@ static void toStream(std::ostream& out, const DType& dt)
}
}
-static void toStream(std::ostream& out,
- const DatatypeDeclarationCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const std::vector<Type>& datatypes = c->getDatatypes();
Assert(!datatypes.empty());
Assert(datatypes[0].isDatatype());
- const DType& d0 = TypeNode::fromType(datatypes[0]).getDType();
+ const DType& d0 = datatypes[0].getDType();
if (d0.isTuple())
{
// not necessary to print tuples
@@ -1891,21 +1852,21 @@ static void toStream(std::ostream& out,
out << "co";
}
out << "datatypes";
- if (isVariant_2_6(v))
+ if (isVariant_2_6(d_variant))
{
out << " (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& d = TypeNode::fromType(t).getDType();
+ const DType& d = t.getDType();
out << "(" << CVC4::quoteSymbol(d.getName());
out << " " << d.getNumParameters() << ")";
}
out << ") (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& d = TypeNode::fromType(t).getDType();
+ const DType& d = t.getDType();
if (d.isParametric())
{
out << "(par (";
@@ -1937,7 +1898,7 @@ static void toStream(std::ostream& out,
for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
{
Assert(datatypes[j].isDatatype());
- const DType& dj = TypeNode::fromType(datatypes[j]).getDType();
+ const DType& dj = datatypes[j].getDType();
if (dj.getNumParameters() != nparam)
{
success = false;
@@ -1974,10 +1935,10 @@ static void toStream(std::ostream& out,
out << std::endl;
}
out << ") (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& dt = TypeNode::fromType(t).getDType();
+ const DType& dt = t.getDType();
out << "(" << CVC4::quoteSymbol(dt.getName()) << " ";
toStream(out, dt);
out << ")";
@@ -1987,26 +1948,33 @@ static void toStream(std::ostream& out,
out << ")" << endl;
}
-static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
+void Smt2Printer::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- string s = c->getComment();
+ std::string s = comment;
size_t pos = 0;
- while((pos = s.find_first_of('"', pos)) != string::npos) {
- s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+ while ((pos = s.find_first_of('"', pos)) != string::npos)
+ {
+ s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(set-info :notes \"" << s << "\")";
}
-static void toStream(std::ostream& out, const EmptyCommand* c) {}
+void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
+{
+}
-static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- std::string s = c->getOutput();
+ std::string s = output;
// escape all double-quotes
size_t pos = 0;
- while((pos = s.find('"', pos)) != string::npos) {
- s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+ while ((pos = s.find('"', pos)) != string::npos)
+ {
+ s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(echo \"" << s << "\")";
@@ -2081,7 +2049,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType)
+ TypeNode sygusType) const
{
out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym)
<< ' ';
@@ -2113,60 +2081,43 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
out << ')';
}
-static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
-{
- out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol());
-
- FunctionType ft = c->getType();
- stringstream ss;
-
- for (const Type& i : ft.getArgTypes())
- {
- ss << i << ' ';
- }
-
- string argTypes = ss.str();
- argTypes.pop_back();
-
- out << " (" << argTypes << ") " << ft.getRangeType() << ')';
-}
-
-static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
+void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const
{
- out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
- << ')';
+ out << "(declare-var " << var << ' ' << type << ')';
}
-static void toStream(std::ostream& out, const SygusConstraintCommand* c)
+void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
{
- out << '(' << c->getCommandName() << ' ' << c->getExpr() << ')';
+ out << "(constraint " << n << ')';
}
-static void toStream(std::ostream& out, const SygusInvConstraintCommand* c)
+void Smt2Printer::toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const
{
- out << '(' << c->getCommandName() << ' ';
- copy(c->getPredicates().cbegin(),
- c->getPredicates().cend(),
- std::ostream_iterator<Expr>(out, " "));
- out << ')';
+ out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
+ << ')';
}
-static void toStream(std::ostream& out, const CheckSynthCommand* c)
+void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
{
- out << '(' << c->getCommandName() << ')';
+ out << "(check-synth)";
}
-static void toStream(std::ostream& out, const GetAbductCommand* c)
+void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
{
- out << '(';
- out << c->getCommandName() << ' ';
- out << c->getAbductName() << ' ';
- out << c->getConjecture();
+ out << "(get-abduct ";
+ out << name << ' ';
+ out << conj << ' ';
// print grammar, if any
- if (c->getGrammar() != nullptr)
+ if (!sygusType.isNull())
{
- out << *c->getGrammar();
+ toStreamSygusGrammar(out, sygusType);
}
out << ')';
}
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index cb1ffe9bd..6b57823a4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -35,20 +35,17 @@ enum Variant
// support for the string standard
sygus_variant // variant for sygus
}; /* enum Variant */
-class Smt2Printer : public CVC4::Printer {
+
+class Smt2Printer : public CVC4::Printer
+{
public:
- Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
+ Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
/**
@@ -58,13 +55,179 @@ class Smt2Printer : public CVC4::Printer {
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
- /** Print synth fun command */
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-fun-rec command */
+ void toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print declare-var command */
+ void toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) 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;
+ TypeNode sygusType) const override;
+
+ /** Print constraint command */
+ void toStreamCmdConstraint(std::ostream& out, Node n) const override;
+
+ /** Print inv-constraint command */
+ void toStreamCmdInvConstraint(std::ostream& out,
+ Node inv,
+ Node pre,
+ Node trans,
+ Node post) const override;
+
+ /** Print check-synth command */
+ void toStreamCmdCheckSynth(std::ostream& out) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-abduct command */
+ void toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const override;
+
+ /** Print get-unsat-assumptions command */
+ void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
void toStream(
@@ -73,12 +236,13 @@ class Smt2Printer : public CVC4::Printer {
const Model& m,
const Command* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
+ void toStream(std::ostream& out, const DType& dt) const;
Variant d_variant;
-};/* class Smt2Printer */
+}; /* class Smt2Printer */
-}/* CVC4::printer::smt2 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace smt2
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index f1c1089ad..c4623f76a 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -39,15 +39,6 @@ void TptpPrinter::toStream(
n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
}/* TptpPrinter::toStream() */
-void TptpPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* TptpPrinter::toStream() */
-
void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
{
s->toStream(out, language::output::LANG_SMTLIB_V2_5);
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index d183a19d0..6682b495e 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -27,7 +27,8 @@ namespace CVC4 {
namespace printer {
namespace tptp {
-class TptpPrinter : public CVC4::Printer {
+class TptpPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
@@ -35,27 +36,23 @@ class TptpPrinter : public CVC4::Printer {
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
/** print unsat core to stream
- * We use the expression names stored in the SMT engine associated with the unsat core
- * with UnsatCore::getSmtEngine.
- */
+ * We use the expression names stored in the SMT engine associated with the
+ * unsat core with UnsatCore::getSmtEngine.
+ */
void toStream(std::ostream& out, const UnsatCore& core) const override;
private:
void toStream(std::ostream& out,
const Model& m,
const Command* c) const override;
-};/* class TptpPrinter */
-}/* CVC4::printer::tptp namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}; /* class TptpPrinter */
+
+} // namespace tptp
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__TPTP_PRINTER_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2383167a6..99e0a6c25 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -105,6 +105,34 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
}
}
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
+{
+ std::vector<Node> nodes;
+ nodes.reserve(exprs.size());
+
+ for (Expr e : exprs)
+ {
+ nodes.push_back(Node::fromExpr(e));
+ }
+
+ return nodes;
+}
+
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
+{
+ std::vector<TypeNode> typeNodes;
+ typeNodes.reserve(types.size());
+
+ for (Type t : types)
+ {
+ typeNodes.push_back(TypeNode::fromType(t));
+ }
+
+ return typeNodes;
+}
+
/* -------------------------------------------------------------------------- */
/* class CommandPrintSuccess */
/* -------------------------------------------------------------------------- */
@@ -194,15 +222,6 @@ std::string Command::toString() const
return ss.str();
}
-void Command::toStream(std::ostream& out,
- int toDepth,
- bool types,
- size_t dag,
- OutputLanguage language) const
-{
- Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag);
-}
-
void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
{
Printer::getPrinter(language)->toStream(out, this);
@@ -240,6 +259,15 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager,
Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
std::string EmptyCommand::getCommandName() const { return "empty"; }
+void EmptyCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
+}
+
/* -------------------------------------------------------------------------- */
/* class EchoCommand */
/* -------------------------------------------------------------------------- */
@@ -273,6 +301,15 @@ Command* EchoCommand::exportTo(ExprManager* exprManager,
Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
std::string EchoCommand::getCommandName() const { return "echo"; }
+void EchoCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
+}
+
/* -------------------------------------------------------------------------- */
/* class AssertCommand */
/* -------------------------------------------------------------------------- */
@@ -314,6 +351,15 @@ Command* AssertCommand::clone() const
std::string AssertCommand::getCommandName() const { return "assert"; }
+void AssertCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdAssert(out, Node::fromExpr(d_expr));
+}
+
/* -------------------------------------------------------------------------- */
/* class PushCommand */
/* -------------------------------------------------------------------------- */
@@ -344,6 +390,15 @@ Command* PushCommand::exportTo(ExprManager* exprManager,
Command* PushCommand::clone() const { return new PushCommand(); }
std::string PushCommand::getCommandName() const { return "push"; }
+void PushCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdPush(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class PopCommand */
/* -------------------------------------------------------------------------- */
@@ -374,6 +429,15 @@ Command* PopCommand::exportTo(ExprManager* exprManager,
Command* PopCommand::clone() const { return new PopCommand(); }
std::string PopCommand::getCommandName() const { return "pop"; }
+void PopCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdPop(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class CheckSatCommand */
/* -------------------------------------------------------------------------- */
@@ -430,6 +494,16 @@ Command* CheckSatCommand::clone() const
std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
+void CheckSatCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCheckSat(out,
+ Node::fromExpr(d_expr));
+}
+
/* -------------------------------------------------------------------------- */
/* class CheckSatAssumingCommand */
/* -------------------------------------------------------------------------- */
@@ -505,6 +579,21 @@ std::string CheckSatAssumingCommand::getCommandName() const
return "check-sat-assuming";
}
+void CheckSatAssumingCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ std::vector<Node> nodes;
+ nodes.reserve(d_terms.size());
+ for (const Expr& e : d_terms)
+ {
+ nodes.push_back(Node::fromExpr(e));
+ }
+ Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(out, nodes);
+}
+
/* -------------------------------------------------------------------------- */
/* class QueryCommand */
/* -------------------------------------------------------------------------- */
@@ -559,6 +648,15 @@ Command* QueryCommand::clone() const
std::string QueryCommand::getCommandName() const { return "query"; }
+void QueryCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr);
+}
+
/* -------------------------------------------------------------------------- */
/* class DeclareSygusVarCommand */
/* -------------------------------------------------------------------------- */
@@ -605,51 +703,14 @@ std::string DeclareSygusVarCommand::getCommandName() const
return "declare-var";
}
-/* -------------------------------------------------------------------------- */
-/* class DeclareSygusFunctionCommand */
-/* -------------------------------------------------------------------------- */
-
-DeclareSygusFunctionCommand::DeclareSygusFunctionCommand(const std::string& id,
- Expr func,
- Type t)
- : DeclarationDefinitionCommand(id), d_func(func), d_type(t)
-{
-}
-
-Expr DeclareSygusFunctionCommand::getFunction() const { return d_func; }
-Type DeclareSygusFunctionCommand::getType() const { return d_type; }
-
-void DeclareSygusFunctionCommand::invoke(SmtEngine* smtEngine)
-{
- try
- {
- smtEngine->declareSygusVar(
- d_symbol, Node::fromExpr(d_func), TypeNode::fromType(d_type));
- d_commandStatus = CommandSuccess::instance();
- }
- catch (exception& e)
- {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-Command* DeclareSygusFunctionCommand::exportTo(
- ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+void DeclareSygusVarCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
{
- return new DeclareSygusFunctionCommand(
- d_symbol,
- d_func.exportTo(exprManager, variableMap),
- d_type.exportTo(exprManager, variableMap));
-}
-
-Command* DeclareSygusFunctionCommand::clone() const
-{
- return new DeclareSygusFunctionCommand(d_symbol, d_func, d_type);
-}
-
-std::string DeclareSygusFunctionCommand::getCommandName() const
-{
- return "declare-fun";
+ Printer::getPrinter(language)->toStreamCmdDeclareVar(
+ out, Node::fromExpr(d_var), TypeNode::fromType(d_type));
}
/* -------------------------------------------------------------------------- */
@@ -780,6 +841,16 @@ std::string SygusConstraintCommand::getCommandName() const
return "constraint";
}
+void SygusConstraintCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdConstraint(out,
+ Node::fromExpr(d_expr));
+}
+
/* -------------------------------------------------------------------------- */
/* class SygusInvConstraintCommand */
/* -------------------------------------------------------------------------- */
@@ -833,6 +904,20 @@ std::string SygusInvConstraintCommand::getCommandName() const
return "inv-constraint";
}
+void SygusInvConstraintCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdInvConstraint(
+ out,
+ Node::fromExpr(d_predicates[0]),
+ Node::fromExpr(d_predicates[1]),
+ Node::fromExpr(d_predicates[2]),
+ Node::fromExpr(d_predicates[3]));
+}
+
/* -------------------------------------------------------------------------- */
/* class CheckSynthCommand */
/* -------------------------------------------------------------------------- */
@@ -900,6 +985,15 @@ Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
+void CheckSynthCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class ResetCommand */
/* -------------------------------------------------------------------------- */
@@ -926,6 +1020,15 @@ Command* ResetCommand::exportTo(ExprManager* exprManager,
Command* ResetCommand::clone() const { return new ResetCommand(); }
std::string ResetCommand::getCommandName() const { return "reset"; }
+void ResetCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdReset(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class ResetAssertionsCommand */
/* -------------------------------------------------------------------------- */
@@ -959,6 +1062,15 @@ std::string ResetAssertionsCommand::getCommandName() const
return "reset-assertions";
}
+void ResetAssertionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class QuitCommand */
/* -------------------------------------------------------------------------- */
@@ -978,6 +1090,15 @@ Command* QuitCommand::exportTo(ExprManager* exprManager,
Command* QuitCommand::clone() const { return new QuitCommand(); }
std::string QuitCommand::getCommandName() const { return "exit"; }
+void QuitCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdQuit(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class CommentCommand */
/* -------------------------------------------------------------------------- */
@@ -999,6 +1120,15 @@ Command* CommentCommand::exportTo(ExprManager* exprManager,
Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
std::string CommentCommand::getCommandName() const { return "comment"; }
+void CommentCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
+}
+
/* -------------------------------------------------------------------------- */
/* class CommandSequence */
/* -------------------------------------------------------------------------- */
@@ -1102,6 +1232,30 @@ CommandSequence::iterator CommandSequence::end()
std::string CommandSequence::getCommandName() const { return "sequence"; }
+void CommandSequence::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
+ d_commandSequence);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclarationSequence */
+/* -------------------------------------------------------------------------- */
+
+void DeclarationSequence::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
+ out, d_commandSequence);
+}
+
/* -------------------------------------------------------------------------- */
/* class DeclarationDefinitionCommand */
/* -------------------------------------------------------------------------- */
@@ -1174,6 +1328,16 @@ std::string DeclareFunctionCommand::getCommandName() const
return "declare-fun";
}
+void DeclareFunctionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+ out, d_func.toString(), TypeNode::fromType(d_type));
+}
+
/* -------------------------------------------------------------------------- */
/* class DeclareTypeCommand */
/* -------------------------------------------------------------------------- */
@@ -1209,6 +1373,16 @@ std::string DeclareTypeCommand::getCommandName() const
return "declare-sort";
}
+void DeclareTypeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareType(
+ out, d_type.toString(), d_arity, TypeNode::fromType(d_type));
+}
+
/* -------------------------------------------------------------------------- */
/* class DefineTypeCommand */
/* -------------------------------------------------------------------------- */
@@ -1255,6 +1429,19 @@ Command* DefineTypeCommand::clone() const
std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
+void DefineTypeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineType(
+ out,
+ d_symbol,
+ typeVectorToTypeNodes(d_params),
+ TypeNode::fromType(d_type));
+}
+
/* -------------------------------------------------------------------------- */
/* class DefineFunctionCommand */
/* -------------------------------------------------------------------------- */
@@ -1333,6 +1520,20 @@ std::string DefineFunctionCommand::getCommandName() const
return "define-fun";
}
+void DefineFunctionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineFunction(
+ out,
+ d_func.toString(),
+ exprVectorToNodes(d_formals),
+ Node::fromExpr(d_func).getType().getRangeType(),
+ Node::fromExpr(d_formula));
+}
+
/* -------------------------------------------------------------------------- */
/* class DefineNamedFunctionCommand */
/* -------------------------------------------------------------------------- */
@@ -1377,6 +1578,20 @@ Command* DefineNamedFunctionCommand::clone() const
d_symbol, d_func, d_formals, d_formula, d_global);
}
+void DefineNamedFunctionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
+ out,
+ d_func.toString(),
+ exprVectorToNodes(d_formals),
+ Node::fromExpr(d_func).getType().getRangeType(),
+ Node::fromExpr(d_formula));
+}
+
/* -------------------------------------------------------------------------- */
/* class DefineFunctionRecCommand */
/* -------------------------------------------------------------------------- */
@@ -1454,6 +1669,26 @@ std::string DefineFunctionRecCommand::getCommandName() const
return "define-fun-rec";
}
+void DefineFunctionRecCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ std::vector<std::vector<Node>> formals;
+ formals.reserve(d_formals.size());
+ for (const std::vector<api::Term>& formal : d_formals)
+ {
+ formals.push_back(api::termVectorToNodes(formal));
+ }
+
+ Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
+ out,
+ api::termVectorToNodes(d_funcs),
+ formals,
+ api::termVectorToNodes(d_formulas));
+}
+
/* -------------------------------------------------------------------------- */
/* class SetUserAttribute */
/* -------------------------------------------------------------------------- */
@@ -1523,6 +1758,16 @@ std::string SetUserAttributeCommand::getCommandName() const
return "set-user-attribute";
}
+void SetUserAttributeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
+ out, d_attr, Node::fromExpr(d_expr));
+}
+
/* -------------------------------------------------------------------------- */
/* class SimplifyCommand */
/* -------------------------------------------------------------------------- */
@@ -1577,6 +1822,15 @@ Command* SimplifyCommand::clone() const
std::string SimplifyCommand::getCommandName() const { return "simplify"; }
+void SimplifyCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term);
+}
+
/* -------------------------------------------------------------------------- */
/* class ExpandDefinitionsCommand */
/* -------------------------------------------------------------------------- */
@@ -1625,6 +1879,16 @@ std::string ExpandDefinitionsCommand::getCommandName() const
return "expand-definitions";
}
+void ExpandDefinitionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdExpandDefinitions(
+ out, Node::fromExpr(d_term));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetValueCommand */
/* -------------------------------------------------------------------------- */
@@ -1724,6 +1988,16 @@ Command* GetValueCommand::clone() const
std::string GetValueCommand::getCommandName() const { return "get-value"; }
+void GetValueCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetValue(
+ out, exprVectorToNodes(d_terms));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetAssignmentCommand */
/* -------------------------------------------------------------------------- */
@@ -1793,6 +2067,15 @@ std::string GetAssignmentCommand::getCommandName() const
return "get-assignment";
}
+void GetAssignmentCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetModelCommand */
/* -------------------------------------------------------------------------- */
@@ -1857,6 +2140,15 @@ Command* GetModelCommand::clone() const
std::string GetModelCommand::getCommandName() const { return "get-model"; }
+void GetModelCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetModel(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class BlockModelCommand */
/* -------------------------------------------------------------------------- */
@@ -1898,6 +2190,15 @@ Command* BlockModelCommand::clone() const
std::string BlockModelCommand::getCommandName() const { return "block-model"; }
+void BlockModelCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdBlockModel(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class BlockModelValuesCommand */
/* -------------------------------------------------------------------------- */
@@ -1960,6 +2261,16 @@ std::string BlockModelValuesCommand::getCommandName() const
return "block-model-values";
}
+void BlockModelValuesCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdBlockModelValues(
+ out, exprVectorToNodes(d_terms));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetProofCommand */
/* -------------------------------------------------------------------------- */
@@ -2020,6 +2331,15 @@ Command* GetProofCommand::clone() const
std::string GetProofCommand::getCommandName() const { return "get-proof"; }
+void GetProofCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetProof(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetInstantiationsCommand */
/* -------------------------------------------------------------------------- */
@@ -2073,6 +2393,15 @@ std::string GetInstantiationsCommand::getCommandName() const
return "get-instantiations";
}
+void GetInstantiationsCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetSynthSolutionCommand */
/* -------------------------------------------------------------------------- */
@@ -2121,7 +2450,16 @@ Command* GetSynthSolutionCommand::clone() const
std::string GetSynthSolutionCommand::getCommandName() const
{
- return "get-instantiations";
+ return "get-synth-solution";
+}
+
+void GetSynthSolutionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
}
/* -------------------------------------------------------------------------- */
@@ -2218,6 +2556,19 @@ std::string GetInterpolCommand::getCommandName() const
return "get-interpol";
}
+void GetInterpolCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInterpol(
+ out,
+ d_name,
+ d_conj.getNode(),
+ TypeNode::fromType(d_sygus_grammar->resolve().getType()));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetAbductCommand */
/* -------------------------------------------------------------------------- */
@@ -2308,6 +2659,19 @@ Command* GetAbductCommand::clone() const
std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
+void GetAbductCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAbduct(
+ out,
+ d_name,
+ d_conj.getNode(),
+ TypeNode::fromType(d_sygus_grammar->resolve().getType()));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetQuantifierEliminationCommand */
/* -------------------------------------------------------------------------- */
@@ -2373,6 +2737,16 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
return d_doFull ? "get-qe" : "get-qe-disjunct";
}
+void GetQuantifierEliminationCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
+ out, Node::fromExpr(d_expr));
+}
+
/* -------------------------------------------------------------------------- */
/* class GetUnsatAssumptionsCommand */
/* -------------------------------------------------------------------------- */
@@ -2439,6 +2813,15 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const
return "get-unsat-assumptions";
}
+void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetUnsatCoreCommand */
/* -------------------------------------------------------------------------- */
@@ -2500,6 +2883,15 @@ std::string GetUnsatCoreCommand::getCommandName() const
return "get-unsat-core";
}
+void GetUnsatCoreCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetAssertionsCommand */
/* -------------------------------------------------------------------------- */
@@ -2557,6 +2949,15 @@ std::string GetAssertionsCommand::getCommandName() const
return "get-assertions";
}
+void GetAssertionsCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
+}
+
/* -------------------------------------------------------------------------- */
/* class SetBenchmarkStatusCommand */
/* -------------------------------------------------------------------------- */
@@ -2603,6 +3004,15 @@ std::string SetBenchmarkStatusCommand::getCommandName() const
return "set-info";
}
+void SetBenchmarkStatusCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, d_status);
+}
+
/* -------------------------------------------------------------------------- */
/* class SetBenchmarkLogicCommand */
/* -------------------------------------------------------------------------- */
@@ -2642,6 +3052,15 @@ std::string SetBenchmarkLogicCommand::getCommandName() const
return "set-logic";
}
+void SetBenchmarkLogicCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
+}
+
/* -------------------------------------------------------------------------- */
/* class SetInfoCommand */
/* -------------------------------------------------------------------------- */
@@ -2684,6 +3103,15 @@ Command* SetInfoCommand::clone() const
std::string SetInfoCommand::getCommandName() const { return "set-info"; }
+void SetInfoCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetInfoCommand */
/* -------------------------------------------------------------------------- */
@@ -2750,6 +3178,15 @@ Command* GetInfoCommand::clone() const
std::string GetInfoCommand::getCommandName() const { return "get-info"; }
+void GetInfoCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
+}
+
/* -------------------------------------------------------------------------- */
/* class SetOptionCommand */
/* -------------------------------------------------------------------------- */
@@ -2791,6 +3228,15 @@ Command* SetOptionCommand::clone() const
std::string SetOptionCommand::getCommandName() const { return "set-option"; }
+void SetOptionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
+}
+
/* -------------------------------------------------------------------------- */
/* class GetOptionCommand */
/* -------------------------------------------------------------------------- */
@@ -2845,6 +3291,15 @@ Command* GetOptionCommand::clone() const
std::string GetOptionCommand::getCommandName() const { return "get-option"; }
+void GetOptionCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
+}
+
/* -------------------------------------------------------------------------- */
/* class SetExpressionNameCommand */
/* -------------------------------------------------------------------------- */
@@ -2879,6 +3334,16 @@ std::string SetExpressionNameCommand::getCommandName() const
return "set-expr-name";
}
+void SetExpressionNameCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdSetExpressionName(
+ out, Node::fromExpr(d_expr), d_name);
+}
+
/* -------------------------------------------------------------------------- */
/* class DatatypeDeclarationCommand */
/* -------------------------------------------------------------------------- */
@@ -2922,4 +3387,14 @@ std::string DatatypeDeclarationCommand::getCommandName() const
return "declare-datatypes";
}
+void DatatypeDeclarationCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
+ out, typeVectorToTypeNodes(d_datatypes));
+}
+
} // namespace CVC4
diff --git a/src/smt/command.h b/src/smt/command.h
index fb7660b70..95274884f 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -210,7 +210,7 @@ class CVC4_PUBLIC Command
int toDepth = -1,
bool types = false,
size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const;
+ OutputLanguage language = language::output::LANG_AUTO) const = 0;
std::string toString() const;
@@ -308,6 +308,12 @@ class CVC4_PUBLIC EmptyCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
std::string d_name;
@@ -326,6 +332,12 @@ class CVC4_PUBLIC EchoCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
std::string d_output;
@@ -347,6 +359,12 @@ class CVC4_PUBLIC AssertCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class AssertCommand */
class CVC4_PUBLIC PushCommand : public Command
@@ -357,6 +375,12 @@ class CVC4_PUBLIC PushCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PushCommand */
class CVC4_PUBLIC PopCommand : public Command
@@ -367,6 +391,12 @@ class CVC4_PUBLIC PopCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class PopCommand */
class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
@@ -402,6 +432,12 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareFunctionCommand */
class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
@@ -421,6 +457,12 @@ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DeclareTypeCommand */
class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
@@ -443,6 +485,12 @@ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineTypeCommand */
class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
@@ -467,6 +515,12 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ 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 we are defining */
@@ -499,6 +553,12 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineNamedFunctionCommand */
/**
@@ -529,6 +589,12 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
/** functions we are defining */
@@ -564,6 +630,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
private:
SetUserAttributeCommand(const std::string& attr,
@@ -595,6 +667,12 @@ class CVC4_PUBLIC CheckSatCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
private:
Expr d_expr;
@@ -620,6 +698,12 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
private:
std::vector<Expr> d_terms;
@@ -644,6 +728,12 @@ class CVC4_PUBLIC QueryCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QueryCommand */
/* ------------------- sygus commands ------------------ */
@@ -670,6 +760,13 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
Command* clone() const override;
/** returns this command's name */
std::string getCommandName() const override;
+ /** prints this 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 declared variable */
@@ -678,37 +775,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
Type d_type;
};
-/** Declares a sygus universal function variable */
-class CVC4_PUBLIC DeclareSygusFunctionCommand
- : public DeclarationDefinitionCommand
-{
- public:
- DeclareSygusFunctionCommand(const std::string& id, Expr func, Type type);
- /** returns the declared function variable */
- Expr getFunction() const;
- /** returns the declared function variable's type */
- Type getType() const;
- /** invokes this command
- *
- * The declared sygus function variable is communicated to the SMT engine in
- * case a synthesis conjecture is built later on.
- */
- void invoke(SmtEngine* smtEngine) override;
- /** exports command to given expression manager */
- Command* exportTo(ExprManager* exprManager,
- ExprManagerMapCollection& variableMap) override;
- /** creates a copy of this command */
- Command* clone() const override;
- /** returns this command's name */
- std::string getCommandName() const override;
-
- protected:
- /** the declared function variable */
- Expr d_func;
- /** the declared function variable's type */
- Type d_type;
-};
-
/** Declares a sygus function-to-synthesize
*
* This command is also used for the special case in which we are declaring an
@@ -748,8 +814,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
Command* clone() const override;
/** returns this command's name */
std::string getCommandName() const override;
-
- /** prints the Synth-fun command */
+ /** prints this command */
void toStream(
std::ostream& out,
int toDepth = -1,
@@ -790,6 +855,13 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
Command* clone() const override;
/** returns this command's name */
std::string getCommandName() const override;
+ /** prints this 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 declared constraint */
@@ -830,6 +902,13 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command
Command* clone() const override;
/** returns this command's name */
std::string getCommandName() const override;
+ /** prints this 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 place holder predicates with which to build the actual constraint
@@ -863,6 +942,13 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
Command* clone() const override;
/** returns this command's name */
std::string getCommandName() const override;
+ /** prints this 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:
/** result of the check-synth call */
@@ -891,6 +977,12 @@ class CVC4_PUBLIC SimplifyCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SimplifyCommand */
class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
@@ -910,6 +1002,12 @@ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ExpandDefinitionsCommand */
class CVC4_PUBLIC GetValueCommand : public Command
@@ -930,6 +1028,12 @@ class CVC4_PUBLIC GetValueCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetValueCommand */
class CVC4_PUBLIC GetAssignmentCommand : public Command
@@ -947,6 +1051,12 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssignmentCommand */
class CVC4_PUBLIC GetModelCommand : public Command
@@ -962,6 +1072,12 @@ class CVC4_PUBLIC GetModelCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
Model* d_result;
@@ -979,6 +1095,12 @@ class CVC4_PUBLIC BlockModelCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class BlockModelCommand */
/** The command to block model values. */
@@ -993,6 +1115,12 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ 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 terms we are blocking */
@@ -1011,6 +1139,12 @@ class CVC4_PUBLIC GetProofCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
SmtEngine* d_smtEngine;
@@ -1029,6 +1163,12 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
SmtEngine* d_smtEngine;
@@ -1045,6 +1185,12 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
SmtEngine* d_smtEngine;
@@ -1085,6 +1231,12 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ 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 name of the interpolation predicate */
@@ -1138,6 +1290,12 @@ class CVC4_PUBLIC GetAbductCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ 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 name of the abduction predicate */
@@ -1173,6 +1331,12 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetQuantifierEliminationCommand */
class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
@@ -1186,6 +1350,12 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
std::vector<Expr> d_result;
@@ -1204,6 +1374,12 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ 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 result of the unsat core call
@@ -1225,6 +1401,12 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssertionsCommand */
class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
@@ -1242,6 +1424,12 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkStatusCommand */
class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
@@ -1258,6 +1446,12 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetBenchmarkLogicCommand */
class CVC4_PUBLIC SetInfoCommand : public Command
@@ -1277,6 +1471,12 @@ class CVC4_PUBLIC SetInfoCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetInfoCommand */
class CVC4_PUBLIC GetInfoCommand : public Command
@@ -1297,6 +1497,12 @@ class CVC4_PUBLIC GetInfoCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetInfoCommand */
class CVC4_PUBLIC SetOptionCommand : public Command
@@ -1316,6 +1522,12 @@ class CVC4_PUBLIC SetOptionCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetOptionCommand */
class CVC4_PUBLIC GetOptionCommand : public Command
@@ -1336,6 +1548,12 @@ class CVC4_PUBLIC GetOptionCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetOptionCommand */
// Set expression name command
@@ -1359,6 +1577,12 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SetExpressionNameCommand */
class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
@@ -1376,6 +1600,12 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DatatypeDeclarationCommand */
class CVC4_PUBLIC ResetCommand : public Command
@@ -1387,6 +1617,12 @@ class CVC4_PUBLIC ResetCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetCommand */
class CVC4_PUBLIC ResetAssertionsCommand : public Command
@@ -1398,6 +1634,12 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetAssertionsCommand */
class CVC4_PUBLIC QuitCommand : public Command
@@ -1409,6 +1651,12 @@ class CVC4_PUBLIC QuitCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class QuitCommand */
class CVC4_PUBLIC CommentCommand : public Command
@@ -1425,11 +1673,17 @@ class CVC4_PUBLIC CommentCommand : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommentCommand */
class CVC4_PUBLIC CommandSequence : public Command
{
- private:
+ protected:
/** All the commands to be executed (in sequence) */
std::vector<Command*> d_commandSequence;
/** Next command to be executed */
@@ -1458,10 +1712,22 @@ class CVC4_PUBLIC CommandSequence : public Command
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommandSequence */
class CVC4_PUBLIC DeclarationSequence : public CommandSequence
{
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
};
} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback