From d6fac5f28f99464dc04d8fb604ce16e56342300e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 24 Jan 2021 12:12:10 -0600 Subject: (proof-new) Instantiation list utility (#5768) This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new. --- src/printer/printer.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/printer/printer.h') diff --git a/src/printer/printer.h b/src/printer/printer.h index 3c53e34e6..835dbe798 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -32,8 +32,9 @@ namespace CVC4 { class Command; class CommandStatus; -class NodeCommand; class UnsatCore; +class InstantiationList; +class SkolemList; class Printer { @@ -62,6 +63,12 @@ class Printer /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const; + /** Write an instantiation list out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const InstantiationList& is) const; + + /** Write a skolem list out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const SkolemList& sks) const; + /** Print empty command */ virtual void toStreamCmdEmpty(std::ostream& out, const std::string& name) const; -- cgit v1.2.3