From bcbef9dfa053a14ac48f176fe4bde9a1aa2b4931 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 18 Aug 2020 17:52:25 -0500 Subject: Refactor functions that print commands (Part 2) (#4905) This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code. --- src/smt/command.cpp | 583 +++++++++++++++++++++++++++++++++++++++++++++++----- src/smt/command.h | 336 ++++++++++++++++++++++++++---- 2 files changed, 830 insertions(+), 89 deletions(-) (limited to 'src/smt') 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 exprVectorToNodes(const std::vector& exprs) +{ + std::vector 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 typeVectorToTypeNodes(const std::vector& types) +{ + std::vector 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 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> formals; + formals.reserve(d_formals.size()); + for (const std::vector& 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 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 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 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 -- cgit v1.2.3