Package org.smtlib.sexpr

Class Printer

java.lang.Object

org.smtlib.sexpr.Printer

All Implemented Interfaces:

IPrinter, IVisitor<Void>

Direct Known Subclasses:

Printer, Printer.WithLines, Solver_z3_4_3.Translator

public class Printer
extends Object
implements IPrinter, IVisitor<Void>

This class writes out SMT-LIB ASTs as concrete S-expression syntax; aside from white space between tokens it should simply reverse what the Parser class does.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
protected static interface	Printer.PrintArgs	Functional interface for the argument-printing lambda passed to printCommand(org.smtlib.ICommand, org.smtlib.sexpr.Printer.PrintArgs).
static class	Printer.WithLines

Nested classes/interfaces inherited from interface org.smtlib.IVisitor

IVisitor.TreeVisitor<T>, IVisitor.VisitorException

Field Summary

Fields

Modifier and Type	Field	Description
static final String	eol	The system-dependent line termination
protected final SMT.Configuration	smtConfig	The Configuration whose rules (e.g.
protected Writer	w	The writer to write text to

Constructor Summary

Constructors

Constructor	Description
Printer(SMT.Configuration smtConfig, Writer w)	Creates a printer object that follows the given Configuration's rules.

Method Summary

Modifier and Type	Method	Description
protected void	append(String s)	Appends a string to the writer, converting any IOException to VisitorException.
String	error(String message)	Utility function to print error messages in this printer's format
IVisitor.VisitorException	exc(Exception ex, Object possiblePos)	Utility function to create an exception using the message from the first argument and the position from the second, if it is IPosable.
protected void	flush()	Flushes the writer, converting any IOException to VisitorException.
Printer	newPrinter(Writer w)	Creates a new printer of the same type as the receiver, writing to the given Writer.
<T extends INode> void	print(T expr)	Prints the argument to the receiver
protected Void	printCommand(ICommand e)	Prints a no-argument command: (commandName()).
protected Void	printCommand(ICommand e, Printer.PrintArgs args)	Prints (commandName() args) — the space between name and args is emitted here, so the args lambda should not prepend one.
<T extends INode> String	toString(T expr)	Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.
Void	visit(ICommand e)	Fallback for extension command types not covered by a specific visit method; uses reflection to invoke write(Printer) on the command object.
Void	visit(ICommand.Iassert e)
Void	visit(ICommand.Icheck_sat e)
Void	visit(ICommand.Icheck_sat_assuming e)
Void	visit(ICommand.Icomment e)	A comment is never "(commandName args)" S-expression syntax to begin with, so this doesn't go through printCommand() like every other command here -- instead it's printed directly, now that Comment is a real, typed command rather than going through the generic visit(ICommand) fallback's reflection-based write() lookup (see issue #115; this logic used to live in a write() override on C_comment itself, invoked only via that reflection call -- moved here instead, so printing for every command, including this one, lives in exactly one place: Printer's own typed visit() methods).
Void	visit(ICommand.Ideclare_const e)
Void	visit(ICommand.Ideclare_datatype e)
Void	visit(ICommand.Ideclare_datatypes e)
Void	visit(ICommand.Ideclare_fun e)
Void	visit(ICommand.Ideclare_sort e)
Void	visit(ICommand.Ideclare_sort_parameter e)
Void	visit(ICommand.Idefine_const e)
Void	visit(ICommand.Idefine_fun e)
Void	visit(ICommand.Idefine_fun_rec e)
Void	visit(ICommand.Idefine_funs_rec e)
Void	visit(ICommand.Idefine_sort e)
Void	visit(ICommand.Iecho e)
Void	visit(ICommand.Iexit e)
Void	visit(ICommand.Iget_assertions e)
Void	visit(ICommand.Iget_assignment e)
Void	visit(ICommand.Iget_info e)
Void	visit(ICommand.Iget_model e)
Void	visit(ICommand.Iget_option e)
Void	visit(ICommand.Iget_proof e)
Void	visit(ICommand.Iget_unsat_assumptions e)
Void	visit(ICommand.Iget_unsat_core e)
Void	visit(ICommand.Iget_value e)
Void	visit(ICommand.Ipop e)
Void	visit(ICommand.Ipush e)
Void	visit(ICommand.Ireset e)
Void	visit(ICommand.Ireset_assertions e)
Void	visit(ICommand.IScript e)
Void	visit(ICommand.Iset_info e)
Void	visit(ICommand.Iset_logic e)
Void	visit(ICommand.Iset_option e)
Void	visit(IExpr.IAsIdentifier e)
Void	visit(IExpr.IAttribute<? extends IAttributeValue> e)
Void	visit(IExpr.IAttributedExpr e)
Void	visit(IExpr.IBinaryLiteral e)
Void	visit(IExpr.IBinding e)
Void	visit(IExpr.IConstructor e)
Void	visit(IExpr.IDecimal e)
Void	visit(IExpr.IDeclaration e)
Void	visit(IExpr.IError e)
Void	visit(IExpr.IExists e)
Void	visit(IExpr.IFcnExpr e)
Void	visit(IExpr.IForall e)
Void	visit(IExpr.IFunctionDeclaration e)
Void	visit(IExpr.IHexLiteral e)
Void	visit(IExpr.IKeyword e)
Void	visit(IExpr.ILambda e)
Void	visit(IExpr.ILet e)
Void	visit(IExpr.IMatch e)
Void	visit(IExpr.IMatchCase e)
Void	visit(IExpr.INumeral e)
Void	visit(IExpr.IParameterizedIdentifier e)
Void	visit(IExpr.IPattern e)
Void	visit(IExpr.IPatternTerms e)	Visits the value of a programmatically built :pattern attribute; by default does nothing.
Void	visit(IExpr.ISelector e)
Void	visit(IExpr.ISortDeclaration e)
Void	visit(IExpr.IStringLiteral e)
Void	visit(IExpr.ISymbol e)
Void	visit(ILogic s)
Void	visit(IResponse e)
Void	visit(IResponse.IAssertionsResponse e)
Void	visit(IResponse.IAssignmentResponse e)
Void	visit(IResponse.IAttributeList e)
Void	visit(IResponse.IError e)
Void	visit(IResponse.IProofResponse e)	Prints the proof s-expression compactly; a proof that is a list of lists (e.g.
Void	visit(IResponse.IUnsatAssumptionsResponse e)
Void	visit(IResponse.IUnsatCoreResponse e)
Void	visit(IResponse.IValueResponse e)
Void	visit(ISort.IAbbreviation s)
Void	visit(ISort.IApplication s)
Void	visit(ISort.IDatatype e)
Void	visit(ISort.IFamily s)
Void	visit(ISort.IFcnSort s)
Void	visit(ISort.IParameter s)
Void	visit(ITheory s)
Void	visit(ISexpr.ISeq e)
Void	visit(ISexpr.IToken<?> e)
static <T extends INode> void	write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> String	write(SMT.Configuration smtConfig, T e)	Writes the given expression and outputs as a String, following the given Configuration's rules (e.g.
Writer	writer()	The writer to write text to

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

smtConfig

protected final SMT.Configuration smtConfig

The Configuration whose rules (e.g. string-literal quoting -- see visit(IStringLiteral) -- which is version-dependent) this Printer instance follows. Issue #22: used to be a single static field shared by every Printer instance process-wide, so constructing a second Configuration anywhere in the process silently repointed every other Printer's quoting rules at the new instance's settings. Now set once per instance, at construction, like the writer itself.

w

protected Writer w

The writer to write text to

eol

public static final String eol

The system-dependent line termination

Constructor Details

Printer

public Printer(SMT.Configuration smtConfig,
 Writer w)

Creates a printer object that follows the given Configuration's rules.

Method Details

writer

public Writer writer()

The writer to write text to

append

protected void append(String s)
               throws IVisitor.VisitorException

Appends a string to the writer, converting any IOException to VisitorException.

Throws:

IVisitor.VisitorException

flush

protected void flush()
              throws IVisitor.VisitorException

Flushes the writer, converting any IOException to VisitorException.

Throws:

IVisitor.VisitorException

newPrinter

public Printer newPrinter(Writer w)

Description copied from interface: IPrinter

Creates a new printer of the same type as the receiver, writing to the given Writer.

Specified by:

newPrinter in interface IPrinter

print

public <T extends INode> void print(T expr)
                             throws IVisitor.VisitorException

Prints the argument to the receiver

Specified by:

print in interface IPrinter

Throws:

IVisitor.VisitorException

toString

public <T extends INode> String toString(T expr)

Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.

Specified by:

toString in interface IPrinter

write

public static <T extends INode> String write(SMT.Configuration smtConfig,
 T e)

Writes the given expression and outputs as a String, following the given Configuration's rules (e.g. string-literal quoting).

write

public static <T extends INode> void write(SMT.Configuration smtConfig,
 Writer w,
 T e)
                                    throws IVisitor.VisitorException

Writes the given expression to the given writer, following the given Configuration's rules.

Throws:

IVisitor.VisitorException

write

public static <T extends INode> void write(SMT.Configuration smtConfig,
 PrintStream w,
 T e)
                                    throws IVisitor.VisitorException

Writes the given expression to the given stream, following the given Configuration's rules.

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.INumeral e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.ISymbol e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IDecimal e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IBinaryLiteral e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IHexLiteral e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IStringLiteral e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IKeyword e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IError e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IParameterizedIdentifier e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IAsIdentifier e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IFcnExpr e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IForall e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IExists e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.ILambda e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.ILet e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IMatch e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IMatchCase e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IPattern e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IPatternTerms e)
           throws IVisitor.VisitorException

Description copied from interface: IVisitor

Visits the value of a programmatically built :pattern attribute; by default does nothing.

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IAttribute<? extends IAttributeValue> e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IAttributedExpr e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IDeclaration e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IFunctionDeclaration e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.ISortDeclaration e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.ISelector e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IConstructor e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IExpr.IBinding e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.IScript e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

printCommand

protected Void printCommand(ICommand e,
 Printer.PrintArgs args)
                     throws IVisitor.VisitorException

Prints (commandName() args) — the space between name and args is emitted here, so the args lambda should not prepend one. Subclasses may override to change the overall command format.

Throws:

IVisitor.VisitorException

printCommand

protected Void printCommand(ICommand e)
                     throws IVisitor.VisitorException

Prints a no-argument command: (commandName()). Subclasses may override to change format.

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand e)
           throws IVisitor.VisitorException

Fallback for extension command types not covered by a specific visit method; uses reflection to invoke write(Printer) on the command object.

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iassert e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Icheck_sat e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Icheck_sat_assuming e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_const e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_datatype e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_datatypes e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_fun e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_sort e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ideclare_sort_parameter e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Idefine_const e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Idefine_fun e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Idefine_fun_rec e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Idefine_funs_rec e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Idefine_sort e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iecho e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Icomment e)
           throws IVisitor.VisitorException

A comment is never "(commandName args)" S-expression syntax to begin with, so this doesn't go through printCommand() like every other command here -- instead it's printed directly, now that Comment is a real, typed command rather than going through the generic visit(ICommand) fallback's reflection-based write() lookup (see issue #115; this logic used to live in a write() override on C_comment itself, invoked only via that reflection call -- moved here instead, so printing for every command, including this one, lives in exactly one place: Printer's own typed visit() methods).

Text parsed from a real script is always already well-formed this way (every line, including a multi-line block's continuation lines, already carries its own leading ; in the source, so it prints back out verbatim, byte for byte) -- but text supplied directly via the public API might have an embedded newline with no ; on the continuation line, which would silently end the comment there and let the continuation be re-parsed as code. So each line is checked, and given its own ; if it doesn't already have one and isn't just blank. A comment parsed immediately before a real command always already ends with a newline in the captured source text (a ; comment can't share a line with whatever follows it, so there's necessarily at least one newline swept into the capture) -- but a trailing comment at true end-of-file, or text supplied directly via the public API, might not. Printing without a final newline would risk whatever gets printed right after landing on the same line and being silently swallowed by this comment (since ; consumes to end of line), so one is always guaranteed here regardless.

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iexit e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_assertions e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_assignment e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_info e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_model e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_option e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_proof e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_unsat_assumptions e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_unsat_core e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iget_value e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ipop e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ipush e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ireset e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Ireset_assertions e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iset_info e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iset_logic e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ICommand.Iset_option e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IFamily s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IAbbreviation s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IApplication s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IFcnSort s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IParameter s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ILogic s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ITheory s)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

exc

public IVisitor.VisitorException exc(Exception ex,
 Object possiblePos)

Utility function to create an exception using the message from the first argument and the position from the second, if it is IPosable.

error

public String error(String message)

Utility function to print error messages in this printer's format

visit

public Void visit(IResponse.IError e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IAssertionsResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IAssignmentResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IProofResponse e)
           throws IVisitor.VisitorException

Prints the proof s-expression compactly; a proof that is a list of lists (e.g. cvc5's steps, z3's (set-logic) and (proof)) gets one element per line, as get-assertions does.

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IValueResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IUnsatCoreResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IUnsatAssumptionsResponse e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(IResponse.IAttributeList e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISexpr.IToken<?> e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISexpr.ISeq e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException

visit

public Void visit(ISort.IDatatype e)
           throws IVisitor.VisitorException

Specified by:

visit in interface IVisitor<Void>

Throws:

IVisitor.VisitorException