]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
* Fix the SMT-LIB format printer so that it produces correct output. STP can now...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 10 Mar 2010 05:09:20 +0000 (05:09 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 10 Mar 2010 05:09:20 +0000 (05:09 +0000)
commiteaab1611e5dc8209ae24fbeecfd361109be42bfd
treeeffa1093b9ebbcdd1cbfc5b02cb51d90e8830613
parentaec81b61712d48d96c0f702d53c317d4612c8619
* Fix the SMT-LIB format printer so that it produces correct output. STP can now function as a CVC to SMT-LIB translator.
* Cleanup the CVC format printer.
* Bugfix in the CVC format printer. Add brackets to some unary operations to enforce the correct precedence.
* Remove a un-unsed parameter from the CVC print-back.

To isolate the bug in the CVC format printer I used Robert Brummayer's excellent delta-debugger.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@635 e59a4935-1847-0410-ae03-e826735625c1
src/main/main.cpp
src/printer/AssortedPrinters.cpp
src/printer/AssortedPrinters.h
src/printer/PLPrinter.cpp
src/printer/SMTLIBPrinter.cpp