summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/printer.cpp5
-rw-r--r--src/printer/printer.h3
-rw-r--r--src/printer/smt2/smt2_printer.cpp5
-rw-r--r--src/printer/smt2/smt2_printer.h3
4 files changed, 16 insertions, 0 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a4ff10014..12b52e284 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -405,6 +405,11 @@ void Printer::toStreamCmdGetInterpol(std::ostream& out,
printUnknownCommand(out, "get-interpol");
}
+void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+ printUnknownCommand(out, "get-interpol-next");
+}
+
void Printer::toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
Node conj,
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 74eb8970b..2a9283001 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -200,6 +200,9 @@ class Printer
Node conj,
TypeNode sygusType) const;
+ /** Print get-interpol-next command */
+ virtual void toStreamCmdGetInterpolNext(std::ostream& out) const;
+
/** Print get-abduct command */
virtual void toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e6c99c707..69da5d03d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1917,6 +1917,11 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
out << ')' << std::endl;
}
+void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
+{
+ out << "(get-interpol-next)" << std::endl;
+}
+
void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
Node conj,
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index aad3948fe..bf6c20d40 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -174,6 +174,9 @@ class Smt2Printer : public cvc5::Printer
Node conj,
TypeNode sygusType) const override;
+ /** Print get-interpol-next command */
+ void toStreamCmdGetInterpolNext(std::ostream& out) const override;
+
/** Print get-abduct command */
void toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback