diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 583 |
1 files changed, 529 insertions, 54 deletions
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 |