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.
class DatatypeConstructor;
class DatatypeConstructorArg;
class ExprManager;
+class GetAbductCommand;
+class GetInterpolCommand;
class NodeManager;
class SmtEngine;
class SynthFunCommand;
*/
class CVC4_PUBLIC Grammar
{
- friend class Solver;
+ friend class CVC4::GetAbductCommand;
+ friend class CVC4::GetInterpolCommand;
friend class CVC4::SynthFunCommand;
+ friend class Solver;
public:
/**
template <class T>
static bool tryToStream(std::ostream& out, const Command* c);
-void AstPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if(tryToStream<EmptyCommand>(out, c) ||
- tryToStream<AssertCommand>(out, c) ||
- tryToStream<PushCommand>(out, c) ||
- tryToStream<PopCommand>(out, c) ||
- tryToStream<CheckSatCommand>(out, c) ||
- tryToStream<CheckSatAssumingCommand>(out, c) ||
- tryToStream<QueryCommand>(out, c) ||
- tryToStream<ResetCommand>(out, c) ||
- tryToStream<ResetAssertionsCommand>(out, c) ||
- tryToStream<QuitCommand>(out, c) ||
- tryToStream<DeclarationSequence>(out, c) ||
- tryToStream<CommandSequence>(out, c) ||
- tryToStream<DeclareFunctionCommand>(out, c) ||
- tryToStream<DeclareTypeCommand>(out, c) ||
- tryToStream<DefineTypeCommand>(out, c) ||
- tryToStream<DefineNamedFunctionCommand>(out, c) ||
- tryToStream<DefineFunctionCommand>(out, c) ||
- tryToStream<SimplifyCommand>(out, c) ||
- tryToStream<GetValueCommand>(out, c) ||
- tryToStream<GetModelCommand>(out, c) ||
- tryToStream<GetAssignmentCommand>(out, c) ||
- tryToStream<GetAssertionsCommand>(out, c) ||
- tryToStream<GetProofCommand>(out, c) ||
- tryToStream<SetBenchmarkStatusCommand>(out, c) ||
- tryToStream<SetBenchmarkLogicCommand>(out, c) ||
- tryToStream<SetInfoCommand>(out, c) ||
- tryToStream<GetInfoCommand>(out, c) ||
- tryToStream<SetOptionCommand>(out, c) ||
- tryToStream<GetOptionCommand>(out, c) ||
- tryToStream<DatatypeDeclarationCommand>(out, c) ||
- tryToStream<CommentCommand>(out, c)) {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* AstPrinter::toStream(Command*) */
-
template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s);
Unreachable();
}
-static void toStream(std::ostream& out, const EmptyCommand* c)
+void AstPrinter::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
{
- out << "EmptyCommand(" << c->getName() << ")";
+ out << "EmptyCommand(" << name << ')';
}
-static void toStream(std::ostream& out, const AssertCommand* c)
+void AstPrinter::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- out << "Assert(" << c->getExpr() << ")";
+ out << "EchoCommand(" << output << ')';
}
-static void toStream(std::ostream& out, const PushCommand* c)
+void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "Push()";
+ out << "Assert(" << n << ')';
}
-static void toStream(std::ostream& out, const PopCommand* c) { out << "Pop()"; }
+void AstPrinter::toStreamCmdPush(std::ostream& out) const { out << "Push()"; }
+
+void AstPrinter::toStreamCmdPop(std::ostream& out) const { out << "Pop()"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(e.isNull()) {
+ if (n.isNull())
+ {
out << "CheckSat()";
- } else {
- out << "CheckSat(" << e << ")";
+ }
+ else
+ {
+ out << "CheckSat(" << n << ')';
}
}
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void AstPrinter::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
- const vector<Expr>& terms = c->getTerms();
out << "CheckSatAssuming( << ";
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
out << ">> )";
}
-static void toStream(std::ostream& out, const QueryCommand* c)
+void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
- out << "Query(" << c->getExpr() << ')';
+ out << "Query(" << n << ')';
}
-static void toStream(std::ostream& out, const ResetCommand* c)
-{
- out << "Reset()";
-}
+void AstPrinter::toStreamCmdReset(std::ostream& out) const { out << "Reset()"; }
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "ResetAssertions()";
}
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
- out << "Quit()";
-}
+void AstPrinter::toStreamCmdQuit(std::ostream& out) const { out << "Quit()"; }
-static void toStream(std::ostream& out, const DeclarationSequence* c)
+void AstPrinter::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
out << "DeclarationSequence[" << endl;
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
out << "]";
}
-static void toStream(std::ostream& out, const CommandSequence* c)
+void AstPrinter::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
out << "CommandSequence[" << endl;
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
out << "]";
}
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- out << "Declare(" << c->getSymbol() << "," << c->getType() << ")";
+ out << "Declare(" << id << "," << type << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const std::vector<Expr>& formals = c->getFormals();
- Expr formula = c->getFormula();
- out << "DefineFunction( \"" << func << "\", [";
- if(formals.size() > 0) {
- copy( formals.begin(), formals.end() - 1,
- ostream_iterator<Expr>(out, ", ") );
+ out << "DefineFunction( \"" << id << "\", [";
+ if (formals.size() > 0)
+ {
+ copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
out << formals.back();
}
out << "], << " << formula << " >> )";
}
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << ","
- << c->getType() << ")";
+ out << "DeclareType(" << id << "," << arity << "," << type << ')';
}
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void AstPrinter::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- const vector<Type>& params = c->getParameters();
- out << "DefineType(" << c->getSymbol() << ",[";
- if(params.size() > 0) {
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(out, ", ") );
+ out << "DefineType(" << id << ",[";
+ if (params.size() > 0)
+ {
+ copy(params.begin(),
+ params.end() - 1,
+ ostream_iterator<TypeNode>(out, ", "));
out << params.back();
}
- out << "]," << c->getType() << ")";
+ out << "]," << t << ')';
}
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void AstPrinter::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
out << "DefineNamedFunction( ";
- toStream(out, static_cast<const DefineFunctionCommand*>(c));
- out << " )";
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
+ out << " )" << std::endl;
}
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "Simplify( << " << c->getTerm() << " >> )";
+ out << "Simplify( << " << n << " >> )";
}
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void AstPrinter::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
out << "GetValue( << ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
out << ">> )";
}
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
{
out << "GetModel()";
}
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "GetAssignment()";
}
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+
+void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "GetAssertions()";
}
-static void toStream(std::ostream& out, const GetProofCommand* c)
+
+void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
{
out << "GetProof()";
}
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c)
+
+void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
- out << "SetBenchmarkStatus(" << c->getStatus() << ")";
+ out << "GetUnsatCore()";
}
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "SetBenchmarkLogic(" << c->getLogic() << ")";
+ out << "SetBenchmarkStatus(" << status << ')';
}
-static void toStream(std::ostream& out, const SetInfoCommand* c)
+
+void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
+ out << "SetBenchmarkLogic(" << logic << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "GetInfo(" << c->getFlag() << ")";
+ out << "SetInfo(" << flag << ", " << sexpr << ')';
}
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+
+void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
+{
+ out << "GetInfo(" << flag << ')';
+}
+
+void AstPrinter::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
+ out << "SetOption(" << flag << ", " << sexpr << ')';
}
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void AstPrinter::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "GetOption(" << c->getFlag() << ")";
+ out << "GetOption(" << flag << ')';
}
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c)
+void AstPrinter::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const vector<Type>& datatypes = c->getDatatypes();
out << "DatatypeDeclarationCommand([";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
out << t << ";" << endl;
}
out << "])";
}
-static void toStream(std::ostream& out, const CommentCommand* c)
+void AstPrinter::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- out << "CommentCommand([" << c->getComment() << "])";
+ out << "CommentCommand([" << comment << "])";
}
template <class T>
namespace printer {
namespace ast {
-class AstPrinter : public CVC4::Printer {
+class AstPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
private:
void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
void toStream(std::ostream& out,
const Model& m,
const Command* c) const override;
-};/* class AstPrinter */
+}; /* class AstPrinter */
-}/* CVC4::printer::ast namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace ast
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__AST_PRINTER_H */
template <class T>
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
-void CvcPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
- tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
- tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) ||
- tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
- tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
- tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) ||
- tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
- tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
- tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetUnsatCoreCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
- tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
- tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
- tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
- tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
- tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* CvcPrinter::toStream(Command*) */
-
template <class T>
static bool tryToStream(std::ostream& out,
const CommandStatus* s,
}
}
-static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "ASSERT " << c->getExpr() << ";";
+ out << "ASSERT " << n << ';';
}
-static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode)
-{
- out << "PUSH;";
-}
+void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; }
-static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode)
-{
- out << "POP;";
-}
+void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << "PUSH; ";
}
- if(!e.isNull()) {
- out << "CHECKSAT " << e << ";";
- } else {
+ if (!n.isNull())
+ {
+ out << "CHECKSAT " << n << ';';
+ }
+ else
+ {
out << "CHECKSAT;";
}
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << " POP;";
}
}
-static void toStream(std::ostream& out,
- const CheckSatAssumingCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
- const vector<Expr>& exprs = c->getTerms();
- if (cvc3Mode)
+ if (d_cvc3Mode)
{
out << "PUSH; ";
}
out << "CHECKSAT";
- if (exprs.size() > 0)
+ if (nodes.size() > 0)
{
- out << " " << exprs[0];
- for (size_t i = 1, n = exprs.size(); i < n; ++i)
+ out << ' ' << nodes[0];
+ for (size_t i = 1, n = nodes.size(); i < n; ++i)
{
- out << " AND " << exprs[i];
+ out << " AND " << nodes[i];
}
}
- out << ";";
- if (cvc3Mode)
+ out << ';';
+ if (d_cvc3Mode)
{
out << " POP;";
}
}
-static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << "PUSH; ";
}
- if(!e.isNull()) {
- out << "QUERY " << e << ";";
- } else {
+ if (!n.isNull())
+ {
+ out << "QUERY " << n << ';';
+ }
+ else
+ {
out << "QUERY TRUE;";
}
- if(cvc3Mode) {
+ if (d_cvc3Mode)
+ {
out << " POP;";
}
}
-static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode)
-{
- out << "RESET;";
-}
+void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; }
-static void toStream(std::ostream& out,
- const ResetAssertionsCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "RESET ASSERTIONS;";
}
-static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
{
- //out << "EXIT;";
+ // out << "EXIT;";
}
-static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
+ for (CommandSequence::const_iterator i = sequence.cbegin();
+ i != sequence.cend();
+ ++i)
+ {
out << *i << endl;
}
}
-static void toStream(std::ostream& out,
- const DeclarationSequence* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- DeclarationSequence::const_iterator i = c->begin();
- for(;;) {
+ DeclarationSequence::const_iterator i = sequence.cbegin();
+ for (;;)
+ {
DeclarationDefinitionCommand* dd =
- static_cast<DeclarationDefinitionCommand*>(*i++);
- if(i != c->end()) {
+ static_cast<DeclarationDefinitionCommand*>(*i++);
+ if (i != sequence.cend())
+ {
out << dd->getSymbol() << ", ";
- } else {
+ }
+ else
+ {
out << *dd;
break;
}
}
}
-static void toStream(std::ostream& out,
- const DeclareFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- out << c->getSymbol() << " : " << c->getType() << ";";
+ out << id << " : " << type << ';';
}
-static void toStream(std::ostream& out,
- const DefineFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const vector<Expr>& formals = c->getFormals();
- Expr formula = c->getFormula();
- out << func << " : " << func.getType() << " = ";
- if(formals.size() > 0) {
+ std::vector<TypeNode> sorts;
+ sorts.reserve(formals.size() + 1);
+ for (const Node& n : formals)
+ {
+ sorts.push_back(n.getType());
+ }
+ sorts.push_back(range);
+
+ out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts)
+ << " = ";
+ if (formals.size() > 0)
+ {
out << "LAMBDA(";
- vector<Expr>::const_iterator i = formals.begin();
- while(i != formals.end()) {
+ vector<Node>::const_iterator i = formals.cbegin();
+ while (i != formals.end())
+ {
out << (*i) << ":" << (*i).getType();
- if(++i != formals.end()) {
+ if (++i != formals.end())
+ {
out << ", ";
}
}
out << "): ";
}
- out << formula << ";";
+ out << formula << ';';
}
-static void toStream(std::ostream& out,
- const DeclareTypeCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- if(c->getArity() > 0) {
- //TODO?
+ if (arity > 0)
+ {
+ // TODO?
out << "ERROR: Don't know how to print parameterized type declaration "
- "in CVC language." << endl;
- } else {
- out << c->getSymbol() << " : TYPE;";
+ "in CVC language."
+ << std::endl;
+ }
+ else
+ {
+ out << id << " : TYPE;";
}
}
-static void toStream(std::ostream& out,
- const DefineTypeCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- if(c->getParameters().size() > 0) {
+ if (params.size() > 0)
+ {
out << "ERROR: Don't know how to print parameterized type definition "
- "in CVC language:" << endl << c->toString() << endl;
- } else {
- out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
+ "in CVC language:"
+ << std::endl;
+ }
+ else
+ {
+ out << id << " : TYPE = " << t << ';';
}
}
-static void toStream(std::ostream& out,
- const DefineNamedFunctionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
}
-static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "TRANSFORM " << c->getTerm() << ";";
+ out << "TRANSFORM " << n << ';';
}
-static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
- const vector<Expr>& terms = c->getTerms();
- Assert(!terms.empty());
+ Assert(!nodes.empty());
out << "GET_VALUE ";
- copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
- out << terms.back() << ";";
+ copy(nodes.begin(),
+ nodes.end() - 1,
+ ostream_iterator<Node>(out, ";\nGET_VALUE "));
+ out << nodes.back() << ';';
}
-static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
{
out << "COUNTERMODEL;";
}
-static void toStream(std::ostream& out,
- const GetAssignmentCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "% (get-assignment)";
}
-static void toStream(std::ostream& out,
- const GetAssertionsCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "WHERE;";
}
-static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
{
out << "DUMP_PROOF;";
}
-static void toStream(std::ostream& out,
- const GetUnsatCoreCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
{
out << "DUMP_UNSAT_CORE;";
}
-static void toStream(std::ostream& out,
- const SetBenchmarkStatusCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "% (set-info :status " << c->getStatus() << ")";
+ out << "% (set-info :status " << status << ')';
}
-static void toStream(std::ostream& out,
- const SetBenchmarkLogicCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
+ out << "OPTION \"logic\" \"" << logic << "\";";
}
-static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "% (set-info " << c->getFlag() << " ";
+ out << "% (set-info " << flag << ' ';
OutputLanguage language =
- cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
- SExpr::toStream(out, c->getSExpr(), language);
- out << ")";
+ d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+ SExpr::toStream(out, sexpr, language);
+ out << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
{
- out << "% (get-info " << c->getFlag() << ")";
+ out << "% (get-info " << flag << ')';
}
-static void toStream(std::ostream& out,
- const SetOptionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "OPTION \"" << c->getFlag() << "\" ";
- SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
- out << ";";
+ out << "OPTION \"" << flag << "\" ";
+ SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
+ out << ';';
}
-static void toStream(std::ostream& out,
- const GetOptionCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "% (get-option " << c->getFlag() << ")";
+ out << "% (get-option " << flag << ')';
}
-static void toStream(std::ostream& out,
- const DatatypeDeclarationCommand* c,
- bool cvc3Mode)
+void CvcPrinter::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const vector<Type>& datatypes = c->getDatatypes();
Assert(!datatypes.empty() && datatypes[0].isDatatype());
- const DType& dt0 = TypeNode::fromType(datatypes[0]).getDType();
- //do not print tuple/datatype internal declarations
+ const DType& dt0 = datatypes[0].getDType();
+ // do not print tuple/datatype internal declarations
if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
{
out << "DATATYPE" << endl;
bool firstDatatype = true;
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
- if(! firstDatatype) {
+ if (!firstDatatype)
+ {
out << ',' << endl;
}
- const DType& dt = TypeNode::fromType(t).getDType();
+ const DType& dt = t.getDType();
out << " " << dt.getName();
- if(dt.isParametric()) {
+ if (dt.isParametric())
+ {
out << '[';
- for(size_t j = 0; j < dt.getNumParameters(); ++j) {
- if(j > 0) {
+ for (size_t j = 0; j < dt.getNumParameters(); ++j)
+ {
+ if (j > 0)
+ {
out << ',';
}
out << dt.getParameter(j);
}
}
-static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- out << "% " << c->getComment();
+ out << "% " << comment;
}
-static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) {}
+void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
+{
+}
-static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode)
+void CvcPrinter::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- out << "ECHO \"" << c->getOutput() << "\";";
+ out << "ECHO \"" << output << "\";";
}
template <class T>
namespace printer {
namespace cvc {
-class CvcPrinter : public CVC4::Printer {
+class CvcPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
- CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
+ CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {}
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
private:
void toStream(
std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
const Command* c) const override;
bool d_cvc3Mode;
-};/* class CvcPrinter */
+}; /* class CvcPrinter */
-}/* CVC4::printer::cvc namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace cvc
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__CVC_PRINTER_H */
void Printer::toStream(std::ostream& out, const UnsatCore& core) const
{
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
- AssertCommand cmd(*i);
- toStream(out, &cmd, -1, false, -1);
+ toStreamCmdAssert(out, Node::fromExpr(*i));
out << std::endl;
}
}/* Printer::toStream(UnsatCore) */
return d_printers[lang].get();
}
-/**
- * Write an error to `out` stating that command `name` is not supported by this
- * printer.
- */
-void printUnknownCommand(std::ostream& out, const std::string& name)
+void Printer::printUnknownCommand(std::ostream& out,
+ const std::string& name) const
{
out << "ERROR: don't know how to print " << name << " command" << std::endl;
}
+void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
+{
+ printUnknownCommand(out, "empty");
+}
+
+void Printer::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
+{
+ printUnknownCommand(out, "echo");
+}
+
+void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "assert");
+}
+
+void Printer::toStreamCmdPush(std::ostream& out) const
+{
+ printUnknownCommand(out, "push");
+}
+
+void Printer::toStreamCmdPop(std::ostream& out) const
+{
+ printUnknownCommand(out, "pop");
+}
+
+void Printer::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-fun");
+}
+
+void Printer::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-sort");
+}
+
+void Printer::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
+{
+ printUnknownCommand(out, "define-sort");
+}
+
+void Printer::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
+{
+ printUnknownCommand(out, "define-fun");
+}
+
+void Printer::toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
+{
+ printUnknownCommand(out, "define-named-function");
+}
+
+void Printer::toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const
+{
+ printUnknownCommand(out, "define-fun-rec");
+}
+
+void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
+ const std::string& attr,
+ Node n) const
+{
+ printUnknownCommand(out, "set-user-attribute");
+}
+
+void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "check-sat");
+}
+
+void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "check-sat-assuming");
+}
+
+void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "query");
+}
+
+void Printer::toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const
+{
+ printUnknownCommand(out, "declare-var");
+}
+
void Printer::toStreamCmdSynthFun(std::ostream& out,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType)
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun");
+}
+
+void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "constraint");
+}
+
+void Printer::toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const
+{
+ printUnknownCommand(out, "inv-constraint");
+}
+
+void Printer::toStreamCmdCheckSynth(std::ostream& out) const
+{
+ printUnknownCommand(out, "check-synth");
+}
+
+void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "simplify");
+}
+
+void Printer::toStreamCmdExpandDefinitions(std::ostream& out, Node n) const
+{
+ printUnknownCommand(out, "expand-definitions");
+}
+
+void Printer::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "get-value");
+}
+
+void Printer::toStreamCmdGetAssignment(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-assignment");
+}
+
+void Printer::toStreamCmdGetModel(std::ostream& out) const
+{
+ printUnknownCommand(out, "ge-model");
+}
+
+void Printer::toStreamCmdBlockModel(std::ostream& out) const
+{
+ printUnknownCommand(out, "block-model");
+}
+
+void Printer::toStreamCmdBlockModelValues(std::ostream& out,
+ const std::vector<Node>& nodes) const
+{
+ printUnknownCommand(out, "block-model-values");
+}
+
+void Printer::toStreamCmdGetProof(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-proof");
+}
+
+void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-instantiations");
+}
+
+void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-synth-solution");
+}
+
+void Printer::toStreamCmdGetInterpol(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, "get-interpol");
+}
+
+void Printer::toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
+{
+ printUnknownCommand(out, "get-abduct");
+}
+
+void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
+ Node n) const
+{
+ printUnknownCommand(out, "get-quantifier-elimination");
+}
+
+void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-unsat-assumption");
+}
+
+void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-unsat-core");
+}
+
+void Printer::toStreamCmdGetAssertions(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-assertions");
+}
+
+void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
+{
+ printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
+{
+ printUnknownCommand(out, "set-logic");
+}
+
+void Printer::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
+{
+ printUnknownCommand(out, "set-info");
+}
+
+void Printer::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
+{
+ printUnknownCommand(out, "get-info");
+}
+
+void Printer::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
+{
+ printUnknownCommand(out, "set-option");
+}
+
+void Printer::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
+{
+ printUnknownCommand(out, "get-option");
+}
+
+void Printer::toStreamCmdSetExpressionName(std::ostream& out,
+ Node n,
+ const std::string& name) const
+{
+ printUnknownCommand(out, "set-expression-name");
+}
+
+void Printer::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
+{
+ printUnknownCommand(
+ out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
+}
+
+void Printer::toStreamCmdReset(std::ostream& out) const
+{
+ printUnknownCommand(out, "reset");
+}
+
+void Printer::toStreamCmdResetAssertions(std::ostream& out) const
+{
+ printUnknownCommand(out, "reset-assertions");
+}
+
+void Printer::toStreamCmdQuit(std::ostream& out) const
+{
+ printUnknownCommand(out, "quit");
+}
+
+void Printer::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
+{
+ printUnknownCommand(out, "comment");
+}
+
+void Printer::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
+{
+ printUnknownCommand(out, "sequence");
+}
+
+void Printer::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- printUnknownCommand(out, "synth-fun");
+ printUnknownCommand(out, "sequence");
}
}/* CVC4 namespace */
bool types,
size_t dag) const = 0;
- /** Write a Command out to a stream with this Printer. */
- virtual void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const = 0;
-
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
/** Write an UnsatCore out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const UnsatCore& core) const;
+ /** Print empty command */
+ virtual void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const;
+
+ /** Print echo command */
+ virtual void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const;
+
+ /** Print assert command */
+ virtual void toStreamCmdAssert(std::ostream& out, Node n) const;
+
+ /** Print push command */
+ virtual void toStreamCmdPush(std::ostream& out) const;
+
+ /** Print pop command */
+ virtual void toStreamCmdPop(std::ostream& out) const;
+
+ /** Print declare-fun command */
+ virtual void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const;
+
+ /** Print declare-sort command */
+ virtual void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const;
+
+ /** Print define-sort command */
+ virtual void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const;
+
+ /** Print define-fun command */
+ virtual void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const;
+
+ /** Print define-named-fun command */
+ virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const;
+
+ /** Print define-fun-rec command */
+ virtual void toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const;
+
+ /** Print set-user-attribute command */
+ void toStreamCmdSetUserAttribute(std::ostream& out,
+ const std::string& attr,
+ Node n) const;
+
+ /** Print check-sat command */
+ virtual void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const;
+
+ /** Print check-sat-assuming command */
+ virtual void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const;
+
+ /** Print query command */
+ virtual void toStreamCmdQuery(std::ostream& out, Node n) const;
+
+ /** Print declare-var command */
+ virtual void toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const;
+
/** Print synth-fun command */
virtual void toStreamCmdSynthFun(std::ostream& out,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType);
+ TypeNode sygusType) const;
+
+ /** Print constraint command */
+ virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
+
+ /** Print inv-constraint command */
+ virtual void toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
+
+ /** Print check-synth command */
+ virtual void toStreamCmdCheckSynth(std::ostream& out) const;
+
+ /** Print simplify command */
+ virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
+
+ /** Print expand-definitions command */
+ void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const;
+
+ /** Print get-value command */
+ virtual void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const;
+
+ /** Print get-assignment command */
+ virtual void toStreamCmdGetAssignment(std::ostream& out) const;
+
+ /** Print get-model command */
+ virtual void toStreamCmdGetModel(std::ostream& out) const;
+
+ /** Print block-model command */
+ void toStreamCmdBlockModel(std::ostream& out) const;
+
+ /** Print block-model-values command */
+ void toStreamCmdBlockModelValues(std::ostream& out,
+ const std::vector<Node>& nodes) const;
+
+ /** Print get-proof command */
+ virtual void toStreamCmdGetProof(std::ostream& out) const;
+
+ /** Print get-instantiations command */
+ void toStreamCmdGetInstantiations(std::ostream& out) const;
+
+ /** Print get-synth-solution command */
+ void toStreamCmdGetSynthSolution(std::ostream& out) const;
+
+ /** Print get-interpol command */
+ void toStreamCmdGetInterpol(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const;
+
+ /** Print get-abduct command */
+ virtual void toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const;
+
+ /** Print get-quantifier-elimination command */
+ void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
+
+ /** Print get-unsat-assumptions command */
+ virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;
+
+ /** Print get-unsat-core command */
+ virtual void toStreamCmdGetUnsatCore(std::ostream& out) const;
+
+ /** Print get-assertions command */
+ virtual void toStreamCmdGetAssertions(std::ostream& out) const;
+
+ /** Print set-info :status command */
+ virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const;
+
+ /** Print set-logic command */
+ virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const;
+
+ /** Print set-info command */
+ virtual void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const;
+
+ /** Print get-info command */
+ virtual void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const;
+
+ /** Print set-option command */
+ virtual void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const;
+
+ /** Print get-option command */
+ virtual void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const;
+
+ /** Print set-expression-name command */
+ void toStreamCmdSetExpressionName(std::ostream& out,
+ Node n,
+ const std::string& name) const;
+
+ /** Print declare-datatype(s) command */
+ virtual void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const;
+
+ /** Print reset command */
+ virtual void toStreamCmdReset(std::ostream& out) const;
+
+ /** Print reset-assertions command */
+ virtual void toStreamCmdResetAssertions(std::ostream& out) const;
+
+ /** Print quit command */
+ virtual void toStreamCmdQuit(std::ostream& out) const;
+
+ /** Print comment command */
+ virtual void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const;
+
+ /** Print command sequence command */
+ virtual void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const;
+
+ /** Print declaration sequence command */
+ virtual void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const;
protected:
/** Derived classes can construct, but no one else. */
getPrinter(lang)->toStream(out, m, c);
}
+ /**
+ * Write an error to `out` stating that command `name` is not supported by
+ * this printer.
+ */
+ void printUnknownCommand(std::ostream& out, const std::string& name) const;
+
private:
/** Disallow copy, assignment */
Printer(const Printer&) = delete;
template <class T>
static bool tryToStream(std::ostream& out, const Command* c, Variant v);
-void Smt2Printer::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- expr::ExprSetDepth::Scope sdScope(out, toDepth);
- expr::ExprPrintTypes::Scope ptScope(out, types);
- expr::ExprDag::Scope dagScope(out, dag);
-
- if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
- || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c)
- || tryToStream<CheckSatAssumingCommand>(out, c)
- || tryToStream<QueryCommand>(out, c, d_variant)
- || tryToStream<ResetCommand>(out, c)
- || tryToStream<ResetAssertionsCommand>(out, c)
- || tryToStream<QuitCommand>(out, c)
- || tryToStream<DeclarationSequence>(out, c)
- || tryToStream<CommandSequence>(out, c)
- || tryToStream<DeclareFunctionCommand>(out, c)
- || tryToStream<DeclareTypeCommand>(out, c)
- || tryToStream<DefineTypeCommand>(out, c)
- || tryToStream<DefineNamedFunctionCommand>(out, c)
- || tryToStream<DefineFunctionCommand>(out, c)
- || tryToStream<DefineFunctionRecCommand>(out, c)
- || tryToStream<SimplifyCommand>(out, c)
- || tryToStream<GetValueCommand>(out, c)
- || tryToStream<GetModelCommand>(out, c)
- || tryToStream<GetAssignmentCommand>(out, c)
- || tryToStream<GetAssertionsCommand>(out, c)
- || tryToStream<GetProofCommand>(out, c)
- || tryToStream<GetUnsatAssumptionsCommand>(out, c)
- || tryToStream<GetUnsatCoreCommand>(out, c)
- || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
- || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
- || tryToStream<SetInfoCommand>(out, c, d_variant)
- || tryToStream<GetInfoCommand>(out, c)
- || tryToStream<SetOptionCommand>(out, c)
- || tryToStream<GetOptionCommand>(out, c)
- || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
- || tryToStream<CommentCommand>(out, c, d_variant)
- || tryToStream<EmptyCommand>(out, c)
- || tryToStream<EchoCommand>(out, c, d_variant)
- || tryToStream<DeclareSygusFunctionCommand>(out, c)
- || tryToStream<DeclareSygusVarCommand>(out, c)
- || tryToStream<SygusConstraintCommand>(out, c)
- || tryToStream<SygusInvConstraintCommand>(out, c)
- || tryToStream<CheckSynthCommand>(out, c)
- || tryToStream<GetAbductCommand>(out, c))
- {
- return;
- }
-
- out << "ERROR: don't know how to print a Command of class: "
- << typeid(*c).name() << endl;
-
-}/* Smt2Printer::toStream(Command*) */
-
-
static std::string quoteSymbol(TNode n) {
std::stringstream ss;
ss << n;
else if (const DatatypeDeclarationCommand* datatype_declaration_command =
dynamic_cast<const DatatypeDeclarationCommand*>(command))
{
- toStream(out, datatype_declaration_command, -1, false, 1);
+ out << datatype_declaration_command;
}
else
{
}
}
-static void toStream(std::ostream& out, const AssertCommand* c)
+void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
{
- out << "(assert " << c->getExpr() << ")";
+ out << "(assert " << n << ')';
}
-static void toStream(std::ostream& out, const PushCommand* c)
+void Smt2Printer::toStreamCmdPush(std::ostream& out) const
{
out << "(push 1)";
}
-static void toStream(std::ostream& out, const PopCommand* c)
-{
- out << "(pop 1)";
-}
+void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; }
-static void toStream(std::ostream& out, const CheckSatCommand* c)
+void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(!e.isNull() && !(e.getKind() == kind::CONST_BOOLEAN && e.getConst<bool>())) {
- out << PushCommand() << endl
- << AssertCommand(e) << endl
- << CheckSatCommand() << endl
- << PopCommand();
- } else {
+ if (!n.isNull())
+ {
+ toStreamCmdPush(out);
+ out << std::endl;
+ toStreamCmdAssert(out, n);
+ out << std::endl;
+ toStreamCmdCheckSat(out);
+ out << std::endl;
+ toStreamCmdPop(out);
+ }
+ else
+ {
out << "(check-sat)";
}
}
-static void toStream(std::ostream& out, const CheckSatAssumingCommand* c)
+void Smt2Printer::toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const
{
out << "(check-sat-assuming ( ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
out << "))";
}
-static void toStream(std::ostream& out, const QueryCommand* c, Variant v)
+void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
{
- Expr e = c->getExpr();
- if(!e.isNull()) {
- if (v == smt2_0_variant)
+ if (!n.isNull())
+ {
+ if (d_variant == smt2_0_variant)
{
- out << PushCommand() << endl
- << AssertCommand(BooleanSimplification::negate(e)) << endl
- << CheckSatCommand() << endl
- << PopCommand();
+ toStreamCmdCheckSat(out, BooleanSimplification::negate(n));
}
else
{
- out << CheckSatAssumingCommand(e.notExpr()) << endl;
+ toStreamCmdCheckSatAssuming(out, {n});
}
- } else {
- out << "(check-sat)";
+ }
+ else
+ {
+ toStreamCmdCheckSat(out);
}
}
-static void toStream(std::ostream& out, const ResetCommand* c)
+void Smt2Printer::toStreamCmdReset(std::ostream& out) const
{
out << "(reset)";
}
-static void toStream(std::ostream& out, const ResetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
{
out << "(reset-assertions)";
}
-static void toStream(std::ostream& out, const QuitCommand* c)
-{
- out << "(exit)";
-}
+void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
-static void toStream(std::ostream& out, const CommandSequence* c)
+void Smt2Printer::toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
{
- CommandSequence::const_iterator i = c->begin();
- if(i != c->end()) {
- for(;;) {
+ CommandSequence::const_iterator i = sequence.cbegin();
+ if (i != sequence.cend())
+ {
+ for (;;)
+ {
out << *i;
- if(++i != c->end()) {
+ if (++i != sequence.cend())
+ {
out << endl;
- } else {
+ }
+ else
+ {
break;
}
}
}
}
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c)
+void Smt2Printer::toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const
+{
+ toStreamCmdCommandSequence(out, sequence);
+}
+
+void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const
{
- Type type = c->getType();
- out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
- if(type.isFunction()) {
- FunctionType ft = type;
- const vector<Type> argTypes = ft.getArgTypes();
- if(argTypes.size() > 0) {
- copy( argTypes.begin(), argTypes.end() - 1,
- ostream_iterator<Type>(out, " ") );
+ out << "(declare-fun " << CVC4::quoteSymbol(id) << " (";
+ if (type.isFunction())
+ {
+ const vector<TypeNode> argTypes = type.getArgTypes();
+ if (argTypes.size() > 0)
+ {
+ copy(argTypes.begin(),
+ argTypes.end() - 1,
+ ostream_iterator<TypeNode>(out, " "));
out << argTypes.back();
}
- type = ft.getRangeType();
+ type = type.getRangeType();
}
- out << ") " << type << ")";
+ out << ") " << type << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
- Expr func = c->getFunction();
- const vector<Expr>* formals = &c->getFormals();
- out << "(define-fun " << func << " (";
- Type type = func.getType();
- Expr formula = c->getFormula();
- if(type.isFunction()) {
- vector<Expr> f;
- if(formals->empty()) {
- const vector<Type>& params = FunctionType(type).getArgTypes();
- for(vector<Type>::const_iterator j = params.begin(); j != params.end(); ++j) {
- f.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j), "",
- NodeManager::SKOLEM_NO_NOTIFY).toExpr());
- }
- formula = NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF, formula, f);
- formals = &f;
- }
- vector<Expr>::const_iterator i = formals->begin();
- for(;;) {
+ out << "(define-fun " << id << " (";
+ if (!formals.empty())
+ {
+ vector<Node>::const_iterator i = formals.cbegin();
+ for (;;)
+ {
out << "(" << (*i) << " " << (*i).getType() << ")";
++i;
- if(i != formals->end()) {
+ if (i != formals.cend())
+ {
out << " ";
- } else {
+ }
+ else
+ {
break;
}
}
- type = FunctionType(type).getRangeType();
}
- out << ") " << type << " " << formula << ")";
+ out << ") " << range << ' ' << formula << ')';
}
-static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
+void Smt2Printer::toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const
{
- const vector<api::Term>& funcs = c->getFunctions();
- const vector<vector<api::Term> >& formals = c->getFormals();
out << "(define-fun";
if (funcs.size() > 1)
{
}
out << funcs[i] << " (";
// print its type signature
- vector<api::Term>::const_iterator itf = formals[i].begin();
+ vector<Node>::const_iterator itf = formals[i].cbegin();
for (;;)
{
- out << "(" << (*itf) << " " << (*itf).getSort() << ")";
+ out << "(" << (*itf) << " " << (*itf).getType() << ")";
++itf;
if (itf != formals[i].end())
{
break;
}
}
- api::Sort type = funcs[i].getSort();
- type = type.getFunctionCodomainSort();
+ TypeNode type = funcs[i].getType();
+ type = type.getRangeType();
out << ") " << type;
if (funcs.size() > 1)
{
{
out << ") (";
}
- const vector<api::Term>& formulas = c->getFormulas();
for (unsigned i = 0, size = formulas.size(); i < size; i++)
{
if (i > 0)
}
}
-static void toStream(std::ostream& out, const DeclareTypeCommand* c)
+void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const
{
- out << "(declare-sort " << CVC4::quoteSymbol(c->getSymbol()) << " "
- << c->getArity() << ")";
+ out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")";
}
-static void toStream(std::ostream& out, const DefineTypeCommand* c)
+void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const
{
- const vector<Type>& params = c->getParameters();
- out << "(define-sort " << c->getSymbol() << " (";
- if(params.size() > 0) {
- copy( params.begin(), params.end() - 1,
- ostream_iterator<Type>(out, " ") );
+ out << "(define-sort " << CVC4::quoteSymbol(id) << " (";
+ if (params.size() > 0)
+ {
+ copy(
+ params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
out << params.back();
}
- out << ") " << c->getType() << ")";
+ out << ") " << t << ")";
}
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c)
+void Smt2Printer::toStreamCmdDefineNamedFunction(
+ std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const
{
out << "DefineNamedFunction( ";
- toStream(out, static_cast<const DefineFunctionCommand*>(c));
- out << " )";
+ toStreamCmdDefineFunction(out, id, formals, range, formula);
+ out << " )" << std::endl;
- out << "ERROR: don't know how to output define-named-function command" << endl;
+ printUnknownCommand(out, "define-named-function");
}
-static void toStream(std::ostream& out, const SimplifyCommand* c)
+void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
{
- out << "(simplify " << c->getTerm() << ")";
+ out << "(simplify " << n << ')';
}
-static void toStream(std::ostream& out, const GetValueCommand* c)
+void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& nodes) const
{
out << "(get-value ( ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+ copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
out << "))";
}
-static void toStream(std::ostream& out, const GetModelCommand* c)
+void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
{
out << "(get-model)";
}
-static void toStream(std::ostream& out, const GetAssignmentCommand* c)
+void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
{
out << "(get-assignment)";
}
-static void toStream(std::ostream& out, const GetAssertionsCommand* c)
+void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
{
out << "(get-assertions)";
}
-static void toStream(std::ostream& out, const GetProofCommand* c)
+void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
{
out << "(get-proof)";
}
-static void toStream(std::ostream& out, const GetUnsatAssumptionsCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
{
out << "(get-unsat-assumptions)";
}
-static void toStream(std::ostream& out, const GetUnsatCoreCommand* c)
+void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
{
out << "(get-unsat-core)";
}
-static void toStream(std::ostream& out,
- const SetBenchmarkStatusCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const
{
- out << "(set-info :status " << c->getStatus() << ")";
+ out << "(set-info :status " << status << ')';
}
-static void toStream(std::ostream& out,
- const SetBenchmarkLogicCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const
{
- out << "(set-logic " << c->getLogic() << ")";
+ out << "(set-logic " << logic << ')';
}
-static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "(set-info :" << c->getFlag() << " ";
- SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
- out << ")";
+ out << "(set-info :" << flag << ' ';
+ SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
+ out << ')';
}
-static void toStream(std::ostream& out, const GetInfoCommand* c)
+void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const
{
- out << "(get-info :" << c->getFlag() << ")";
+ out << "(get-info :" << flag << ')';
}
-static void toStream(std::ostream& out, const SetOptionCommand* c)
+void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const
{
- out << "(set-option :" << c->getFlag() << " ";
- SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
- out << ")";
+ out << "(set-option :" << flag << ' ';
+ SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
+ out << ')';
}
-static void toStream(std::ostream& out, const GetOptionCommand* c)
+void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const
{
- out << "(get-option :" << c->getFlag() << ")";
+ out << "(get-option :" << flag << ')';
}
-static void toStream(std::ostream& out, const DType& dt)
+void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
{
for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
}
}
-static void toStream(std::ostream& out,
- const DatatypeDeclarationCommand* c,
- Variant v)
+void Smt2Printer::toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const
{
- const std::vector<Type>& datatypes = c->getDatatypes();
Assert(!datatypes.empty());
Assert(datatypes[0].isDatatype());
- const DType& d0 = TypeNode::fromType(datatypes[0]).getDType();
+ const DType& d0 = datatypes[0].getDType();
if (d0.isTuple())
{
// not necessary to print tuples
out << "co";
}
out << "datatypes";
- if (isVariant_2_6(v))
+ if (isVariant_2_6(d_variant))
{
out << " (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& d = TypeNode::fromType(t).getDType();
+ const DType& d = t.getDType();
out << "(" << CVC4::quoteSymbol(d.getName());
out << " " << d.getNumParameters() << ")";
}
out << ") (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& d = TypeNode::fromType(t).getDType();
+ const DType& d = t.getDType();
if (d.isParametric())
{
out << "(par (";
for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
{
Assert(datatypes[j].isDatatype());
- const DType& dj = TypeNode::fromType(datatypes[j]).getDType();
+ const DType& dj = datatypes[j].getDType();
if (dj.getNumParameters() != nparam)
{
success = false;
out << std::endl;
}
out << ") (";
- for (const Type& t : datatypes)
+ for (const TypeNode& t : datatypes)
{
Assert(t.isDatatype());
- const DType& dt = TypeNode::fromType(t).getDType();
+ const DType& dt = t.getDType();
out << "(" << CVC4::quoteSymbol(dt.getName()) << " ";
toStream(out, dt);
out << ")";
out << ")" << endl;
}
-static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
+void Smt2Printer::toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const
{
- string s = c->getComment();
+ std::string s = comment;
size_t pos = 0;
- while((pos = s.find_first_of('"', pos)) != string::npos) {
- s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+ while ((pos = s.find_first_of('"', pos)) != string::npos)
+ {
+ s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(set-info :notes \"" << s << "\")";
}
-static void toStream(std::ostream& out, const EmptyCommand* c) {}
+void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const
+{
+}
-static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
+void Smt2Printer::toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const
{
- std::string s = c->getOutput();
+ std::string s = output;
// escape all double-quotes
size_t pos = 0;
- while((pos = s.find('"', pos)) != string::npos) {
- s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
+ while ((pos = s.find('"', pos)) != string::npos)
+ {
+ s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(echo \"" << s << "\")";
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType)
+ TypeNode sygusType) const
{
out << '(' << (isInv ? "synth-inv " : "synth-fun ") << CVC4::quoteSymbol(sym)
<< ' ';
out << ')';
}
-static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
-{
- out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol());
-
- FunctionType ft = c->getType();
- stringstream ss;
-
- for (const Type& i : ft.getArgTypes())
- {
- ss << i << ' ';
- }
-
- string argTypes = ss.str();
- argTypes.pop_back();
-
- out << " (" << argTypes << ") " << ft.getRangeType() << ')';
-}
-
-static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
+void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const
{
- out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
- << ')';
+ out << "(declare-var " << var << ' ' << type << ')';
}
-static void toStream(std::ostream& out, const SygusConstraintCommand* c)
+void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
{
- out << '(' << c->getCommandName() << ' ' << c->getExpr() << ')';
+ out << "(constraint " << n << ')';
}
-static void toStream(std::ostream& out, const SygusInvConstraintCommand* c)
+void Smt2Printer::toStreamCmdInvConstraint(
+ std::ostream& out, Node inv, Node pre, Node trans, Node post) const
{
- out << '(' << c->getCommandName() << ' ';
- copy(c->getPredicates().cbegin(),
- c->getPredicates().cend(),
- std::ostream_iterator<Expr>(out, " "));
- out << ')';
+ out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
+ << ')';
}
-static void toStream(std::ostream& out, const CheckSynthCommand* c)
+void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
{
- out << '(' << c->getCommandName() << ')';
+ out << "(check-synth)";
}
-static void toStream(std::ostream& out, const GetAbductCommand* c)
+void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const
{
- out << '(';
- out << c->getCommandName() << ' ';
- out << c->getAbductName() << ' ';
- out << c->getConjecture();
+ out << "(get-abduct ";
+ out << name << ' ';
+ out << conj << ' ';
// print grammar, if any
- if (c->getGrammar() != nullptr)
+ if (!sygusType.isNull())
{
- out << *c->getGrammar();
+ toStreamSygusGrammar(out, sygusType);
}
out << ')';
}
// support for the string standard
sygus_variant // variant for sygus
}; /* enum Variant */
-class Smt2Printer : public CVC4::Printer {
+
+class Smt2Printer : public CVC4::Printer
+{
public:
- Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
+ Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
/**
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
- /** Print synth fun command */
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-fun-rec command */
+ void toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print declare-var command */
+ void toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const override;
+
+ /** Print synth-fun command */
void toStreamCmdSynthFun(std::ostream& out,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType) override;
+ TypeNode sygusType) const override;
+
+ /** Print constraint command */
+ void toStreamCmdConstraint(std::ostream& out, Node n) const override;
+
+ /** Print inv-constraint command */
+ void toStreamCmdInvConstraint(std::ostream& out,
+ Node inv,
+ Node pre,
+ Node trans,
+ Node post) const override;
+
+ /** Print check-synth command */
+ void toStreamCmdCheckSynth(std::ostream& out) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-abduct command */
+ void toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const override;
+
+ /** Print get-unsat-assumptions command */
+ void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
void toStream(
const Model& m,
const Command* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
+ void toStream(std::ostream& out, const DType& dt) const;
Variant d_variant;
-};/* class Smt2Printer */
+}; /* class Smt2Printer */
-}/* CVC4::printer::smt2 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace smt2
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
}/* TptpPrinter::toStream() */
-void TptpPrinter::toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const
-{
- c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* TptpPrinter::toStream() */
-
void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
{
s->toStream(out, language::output::LANG_SMTLIB_V2_5);
namespace printer {
namespace tptp {
-class TptpPrinter : public CVC4::Printer {
+class TptpPrinter : public CVC4::Printer
+{
public:
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
/** print unsat core to stream
- * We use the expression names stored in the SMT engine associated with the unsat core
- * with UnsatCore::getSmtEngine.
- */
+ * We use the expression names stored in the SMT engine associated with the
+ * unsat core with UnsatCore::getSmtEngine.
+ */
void toStream(std::ostream& out, const UnsatCore& core) const override;
private:
void toStream(std::ostream& out,
const Model& m,
const Command* c) const override;
-};/* class TptpPrinter */
-}/* CVC4::printer::tptp namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+}; /* class TptpPrinter */
+
+} // namespace tptp
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__TPTP_PRINTER_H */
}
}
+// !!! 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 */
/* -------------------------------------------------------------------------- */
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);
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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));
}
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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);
}
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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 */
/* -------------------------------------------------------------------------- */
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
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;
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;
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;
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
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
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
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
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
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
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 */
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 */
/**
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 */
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,
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;
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
private:
std::vector<Expr> d_terms;
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 ------------------ */
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 */
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
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,
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 */
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
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 */
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
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
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
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
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;
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. */
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 */
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;
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;
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;
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 */
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 */
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
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
std::vector<Expr> d_result;
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
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
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
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
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
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
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
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
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
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
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
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
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
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class CommentCommand */
class CVC4_PUBLIC CommandSequence : public Command
{
- private:
+ protected:
/** All the commands to be executed (in sequence) */
std::vector<Command*> d_commandSequence;
/** Next command to be executed */
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
projects / cvc5.git / commitdiff