git.unchartedbackwaters.co.uk Git - francis/stp.git/commit

* 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

author	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Wed, 10 Mar 2010 05:09:20 +0000 (05:09 +0000)
committer	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Wed, 10 Mar 2010 05:09:20 +0000 (05:09 +0000)
commit	eaab1611e5dc8209ae24fbeecfd361109be42bfd
tree	effa1093b9ebbcdd1cbfc5b02cb51d90e8830613	tree \| snapshot
parent	aec81b61712d48d96c0f702d53c317d4612c8619	commit \| diff

src/main/main.cpp		diff \| blob \| history
src/printer/AssortedPrinters.cpp		diff \| blob \| history
src/printer/AssortedPrinters.h		diff \| blob \| history
src/printer/PLPrinter.cpp		diff \| blob \| history
src/printer/SMTLIBPrinter.cpp		diff \| blob \| history