Document SAT API. #4096
Document SAT API. #4096
Conversation
NlightNFotis
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
src/solvers/README.md
Outdated
| The interface supports the following operations by default: | ||
| 1. Boolean operations on literals (like `and`, `or`, `xor`), etc. | ||
| These take as input two [literal](\ref literalt) and return as | ||
| output another [literal](\ref literalt). |
There was a problem hiding this comment.
This should likely reference https://en.wikipedia.org/wiki/Tseytin_transformation or some more original description of it.
src/solvers/README.md
Outdated
| as variables to the formula and returning the number of variables | ||
| or clauses the solver is operating with (with `no_variables`). | ||
| 3. Simulate gate operations on literals, applying Tseitin's | ||
| transformation on them. Tseitin's transformation converts a |
There was a problem hiding this comment.
Ah, I thought 1. was describing the same?
There was a problem hiding this comment.
It's weird if I'm honest, I don't know how to describe it better. At least from the preexisting function documentation, the gate_x functions seem to be implementing tseitin's transformation, and the literal_x functions are just setup functions that end up calling equivalent the gate_x ones. Both are part of the interface of cnft, and I don't know which ones are to be favoured (they seem to be doing the same thing, but with a different interface).
I'm open to suggestions on how to rephrase it in a way that makes more sense.
There was a problem hiding this comment.
I believe the gate_* simply should not be part of the public interface, AFAIK they aren't actually used outside the class! They are concrete implementations of the lx functions, which the propt interface prescribes. Would you mind adding a commit to this PR that shifts the protected up to line 45 of cnf.h?
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: aee8fa3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99823799
NlightNFotis
force-pushed
the
sat_solver_api_doc
branch
from
aee8fa3 to
46acaa1
Compare
|
@hannes-steffenhagen-diffblue @tautschnig Outstanding comments have been addressed. Can I get another review on this please? |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 46acaa1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99915855
NlightNFotis
force-pushed
the
sat_solver_api_doc
branch
from
46acaa1 to
33572ba
Compare
|
@tautschnig This is ready for another review now. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 33572ba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100087744
|
@NlightNFotis This needs a rebase to pick up the Windows CI fix. |
Add some basic explanation of how the SAT api we are working with is implemented.
NlightNFotis
force-pushed
the
sat_solver_api_doc
branch
from
33572ba to
1d3aa5c
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 1d3aa5c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100119505
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
Add some basic explanation of how the SAT api we are working with is implemented.