diff options
-rw-r--r-- | src/api/cvc4cpp.h | 6 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 253 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 148 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 380 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 150 | ||||
-rw-r--r-- | src/printer/printer.cpp | 310 | ||||
-rw-r--r-- | src/printer/printer.h | 213 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 451 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 190 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 9 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.h | 23 | ||||
-rw-r--r-- | src/smt/command.cpp | 583 | ||||
-rw-r--r-- | src/smt/command.h | 336 |
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 |