summaryrefslogtreecommitdiff
path: root/src/smt/command.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r--src/smt/command.cpp583
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback