Skip to content

Latest commit

 

History

History
35 lines (23 loc) · 927 Bytes

README.md

File metadata and controls

35 lines (23 loc) · 927 Bytes
Raw

Proof Signatures

This repository contains the proof signatures for CVC4.

Testing

Testing LFSC Signatures

Running Tests

make test runs all LFSC tests. make <test name> runs a single test, for example make drat_test.

Adding a New Signature Test

To add a new signature test file, create a new file in test/lfsc and add it to git, for example:

git add test/lfsc/new_signature_test.plf

Also add it to the LFSC_TESTS variable in Makefile in the root directory and declare the dependencies of the test as explained below.

Tests can declare the signature files that they depend on using the ; Deps: directive followed by a space-separated list of files. For example:

; Deps: sat.plf smt.plf

indicates that the test depends on sat.plf and smt.plf. The run script automatically searches for the listed files in lfsc as well as the directory of the test input.