projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 54fc9c8) | patch
Fix missing/redundant spaces in proofs
authorAndres Notzli <andres.noetzli@gmail.com>
Tue, 9 Aug 2016 03:33:24 +0000 (20:33 -0700)
committerAndres Notzli <andres.noetzli@gmail.com>
Tue, 9 Aug 2016 08:05:30 +0000 (01:05 -0700)
commitd0610224d0eeab12fd4f779e01b5fdd36c57b304
tree03ab85e9d8a9b55e3d259aae53c45c1e3b496eabtree
parent54fc9c88ac754c96fc0a9c88d6c80c72e9050d34commit | diff
Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.
src/proof/arith_proof.cpp diff | blob | history
src/proof/array_proof.cpp diff | blob | history
src/proof/bitvector_proof.cpp diff | blob | history
src/proof/sat_proof_implementation.h diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/proof/uf_proof.cpp diff | blob | history