Verified Commit 301285e3 authored by Merlin Göttlinger's avatar Merlin Göttlinger 💧
Browse files

Doc update to reflect restructuring

parent 11c767ac
Pipeline #12380 passed with stages
in 3 minutes
......@@ -11,8 +11,8 @@ comments.
## Tests
There are two sets of tests: Integration tests in `src/testsuite` and unit tests
in `src/unit-tests`. The former can be used to test the whole reasoner on
There are two sets of tests: Integration tests in `lib/tests/testsuite` and unit tests
in `lib/tests/unit-tests`. The former can be used to test the whole reasoner on
example formulas with known satisfiability, the latter is for individual
functions.
......@@ -24,8 +24,8 @@ dependency `ounit`. The individual test suites can be run with
### Extending Formula Syntax
To add another functor, extend the algebraic type formula in CoAlgFormula.mli
**and** CoAlgFormula.ml in src/lib/ by adding another case. Note that normally,
To add another functor, extend the algebraic type formula in `CoAlgFormula.mli`
**and** `CoAlgFormula.ml` in `lib/` by adding another case. Note that normally,
you always need (at least) two constructors -- one for the negative and one for
the positive case. That is because in a later internal representation, the
assumption must hold that negations are only in front of atomic propositions
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment