summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.h')
-rw-r--r--src/printer/smt2/smt2_printer.h190
1 files changed, 177 insertions, 13 deletions
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index cb1ffe9bd..6b57823a4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -35,20 +35,17 @@ enum Variant
// support for the string standard
sygus_variant // variant for sygus
}; /* enum Variant */
-class Smt2Printer : public CVC4::Printer {
+
+class Smt2Printer : public CVC4::Printer
+{
public:
- Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
+ Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
- void toStream(std::ostream& out,
- const Command* c,
- int toDepth,
- bool types,
- size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const Model& m) const override;
/**
@@ -58,13 +55,179 @@ class Smt2Printer : public CVC4::Printer {
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
- /** Print synth fun command */
+ /** Print empty command */
+ void toStreamCmdEmpty(std::ostream& out,
+ const std::string& name) const override;
+
+ /** Print echo command */
+ void toStreamCmdEcho(std::ostream& out,
+ const std::string& output) const override;
+
+ /** Print assert command */
+ void toStreamCmdAssert(std::ostream& out, Node n) const override;
+
+ /** Print push command */
+ void toStreamCmdPush(std::ostream& out) const override;
+
+ /** Print pop command */
+ void toStreamCmdPop(std::ostream& out) const override;
+
+ /** Print declare-fun command */
+ void toStreamCmdDeclareFunction(std::ostream& out,
+ const std::string& id,
+ TypeNode type) const override;
+
+ /** Print declare-sort command */
+ void toStreamCmdDeclareType(std::ostream& out,
+ const std::string& id,
+ size_t arity,
+ TypeNode type) const override;
+
+ /** Print define-sort command */
+ void toStreamCmdDefineType(std::ostream& out,
+ const std::string& id,
+ const std::vector<TypeNode>& params,
+ TypeNode t) const override;
+
+ /** Print define-fun command */
+ void toStreamCmdDefineFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-named-fun command */
+ void toStreamCmdDefineNamedFunction(std::ostream& out,
+ const std::string& id,
+ const std::vector<Node>& formals,
+ TypeNode range,
+ Node formula) const override;
+
+ /** Print define-fun-rec command */
+ void toStreamCmdDefineFunctionRec(
+ std::ostream& out,
+ const std::vector<Node>& funcs,
+ const std::vector<std::vector<Node>>& formals,
+ const std::vector<Node>& formulas) const override;
+
+ /** Print check-sat command */
+ void toStreamCmdCheckSat(std::ostream& out,
+ Node n = Node::null()) const override;
+
+ /** Print check-sat-assuming command */
+ void toStreamCmdCheckSatAssuming(
+ std::ostream& out, const std::vector<Node>& nodes) const override;
+
+ /** Print query command */
+ void toStreamCmdQuery(std::ostream& out, Node n) const override;
+
+ /** Print declare-var command */
+ void toStreamCmdDeclareVar(std::ostream& out,
+ Node var,
+ TypeNode type) const override;
+
+ /** Print synth-fun command */
void toStreamCmdSynthFun(std::ostream& out,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType) override;
+ TypeNode sygusType) const override;
+
+ /** Print constraint command */
+ void toStreamCmdConstraint(std::ostream& out, Node n) const override;
+
+ /** Print inv-constraint command */
+ void toStreamCmdInvConstraint(std::ostream& out,
+ Node inv,
+ Node pre,
+ Node trans,
+ Node post) const override;
+
+ /** Print check-synth command */
+ void toStreamCmdCheckSynth(std::ostream& out) const override;
+
+ /** Print simplify command */
+ void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
+
+ /** Print get-value command */
+ void toStreamCmdGetValue(std::ostream& out,
+ const std::vector<Node>& n) const override;
+
+ /** Print get-assignment command */
+ void toStreamCmdGetAssignment(std::ostream& out) const override;
+
+ /** Print get-model command */
+ void toStreamCmdGetModel(std::ostream& out) const override;
+
+ /** Print get-proof command */
+ void toStreamCmdGetProof(std::ostream& out) const override;
+
+ /** Print get-abduct command */
+ void toStreamCmdGetAbduct(std::ostream& out,
+ const std::string& name,
+ Node conj,
+ TypeNode sygusType) const override;
+
+ /** Print get-unsat-assumptions command */
+ void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
+
+ /** Print get-unsat-core command */
+ void toStreamCmdGetUnsatCore(std::ostream& out) const override;
+
+ /** Print get-assertions command */
+ void toStreamCmdGetAssertions(std::ostream& out) const override;
+
+ /** Print set-info :status command */
+ void toStreamCmdSetBenchmarkStatus(std::ostream& out,
+ BenchmarkStatus status) const override;
+
+ /** Print set-logic command */
+ void toStreamCmdSetBenchmarkLogic(std::ostream& out,
+ const std::string& logic) const override;
+
+ /** Print set-info command */
+ void toStreamCmdSetInfo(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-info command */
+ void toStreamCmdGetInfo(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print set-option command */
+ void toStreamCmdSetOption(std::ostream& out,
+ const std::string& flag,
+ SExpr sexpr) const override;
+
+ /** Print get-option command */
+ void toStreamCmdGetOption(std::ostream& out,
+ const std::string& flag) const override;
+
+ /** Print declare-datatype(s) command */
+ void toStreamCmdDatatypeDeclaration(
+ std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
+
+ /** Print reset command */
+ void toStreamCmdReset(std::ostream& out) const override;
+
+ /** Print reset-assertions command */
+ void toStreamCmdResetAssertions(std::ostream& out) const override;
+
+ /** Print quit command */
+ void toStreamCmdQuit(std::ostream& out) const override;
+
+ /** Print comment command */
+ void toStreamCmdComment(std::ostream& out,
+ const std::string& comment) const override;
+
+ /** Print command sequence command */
+ void toStreamCmdCommandSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
+
+ /** Print declaration sequence command */
+ void toStreamCmdDeclarationSequence(
+ std::ostream& out, const std::vector<Command*>& sequence) const override;
private:
void toStream(
@@ -73,12 +236,13 @@ class Smt2Printer : public CVC4::Printer {
const Model& m,
const Command* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
+ void toStream(std::ostream& out, const DType& dt) const;
Variant d_variant;
-};/* class Smt2Printer */
+}; /* class Smt2Printer */
-}/* CVC4::printer::smt2 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+} // namespace smt2
+} // namespace printer
+} // namespace CVC4
#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback