about summary refs log tree commit diff homepage
path: root/test/Expr/print-smt-named.smt2.good
AgeCommit message (Collapse)Author
2014-12-02The printing of constraints and the QueryExpr have been merged into aDan Liew
single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()