summaryrefslogtreecommitdiff
path: root/src/printer/printer.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-12-22 10:56:51 -0600
committerGitHub <noreply@github.com>2021-12-22 10:56:51 -0600
commit5c3cc154d0896568099c18ee6929439d49954e8f (patch)
tree0385b1658e8f93122e0e395b145168860182bbfc /src/printer/printer.h
parent36f93a1431e93979744f2c2a1f3d06b2b9008a4f (diff)
Add support for incremental + interpolants (#7853)
Adds support for incrementality + get-interpol, including the get-interpol-next command.
Diffstat (limited to 'src/printer/printer.h')
-rw-r--r--src/printer/printer.h3
1 files changed, 3 insertions, 0 deletions
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback