Add testing infrastructure for LFSC signatures (#4678)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 1 Jul 2020 15:44:21 +0000 (08:44 -0700)
committerGitHub <noreply@github.com>
Wed, 1 Jul 2020 15:44:21 +0000 (10:44 -0500)
commit9ce4c3153d42bc079470b7bd73bf131499b3fcbe
tree40a384f74915e2c009bb2a66bd0295e62edcfc2e
parent04154c08c1af81bb751376ae9379c071a95c5a3f
Add testing infrastructure for LFSC signatures (#4678)

This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.

Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
31 files changed:
cmake/FindLFSC.cmake
proofs/signatures/drat.plf
proofs/signatures/drat_test.plf [deleted file]
proofs/signatures/er.plf
proofs/signatures/er_test.plf [deleted file]
proofs/signatures/ex-mem.plf [deleted file]
proofs/signatures/ex_bv.plf [deleted file]
proofs/signatures/example-arrays.plf [deleted file]
proofs/signatures/example-quant.plf [deleted file]
proofs/signatures/example.plf [deleted file]
proofs/signatures/lrat.plf
proofs/signatures/lrat_test.plf [deleted file]
proofs/signatures/smt.plf
proofs/signatures/th_arrays.plf
proofs/signatures/th_base.plf
proofs/signatures/th_lira.plf
proofs/signatures/th_lira_test.plf [deleted file]
proofs/signatures/th_real.plf
test/CMakeLists.txt
test/signatures/CMakeLists.txt [new file with mode: 0644]
test/signatures/README.md [new file with mode: 0644]
test/signatures/drat_test.plf [new file with mode: 0644]
test/signatures/er_test.plf [new file with mode: 0644]
test/signatures/ex-mem.plf [new file with mode: 0644]
test/signatures/ex_bv.plf [new file with mode: 0644]
test/signatures/example-arrays.plf [new file with mode: 0644]
test/signatures/example-quant.plf [new file with mode: 0644]
test/signatures/example.plf [new file with mode: 0644]
test/signatures/lrat_test.plf [new file with mode: 0644]
test/signatures/run_test.py [new file with mode: 0755]
test/signatures/th_lira_test.plf [new file with mode: 0644]