projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bb0e6dc) | patch
Add the print benchmark utility (#7196)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Oct 2021 13:58:14 +0000 (08:58 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Oct 2021 13:58:14 +0000 (13:58 +0000)
commit971ae785a4789776e6fe36121c80b69162c2fd27
treece487004cc4002056a656fc269079de7855af1ectree
parentbb0e6dcde2e7267e391a46b868b990d7cb7e42bdcommit | diff
Add the print benchmark utility (#7196)

This utility is capable of printing a vector of Node as a valid (SMT-LIB) benchmark with no prior bookkeeping. It also optionally allows for taking a vector Node corresponding to define-fun.

It will be used to replace the old internal benchmark dumping infrastructure which was error prone.
src/smt/print_benchmark.cpp [new file with mode: 0644] blob
src/smt/print_benchmark.h [new file with mode: 0644] blob