diff options
Diffstat (limited to 'content/zettel/2d5.md')
| -rw-r--r-- | content/zettel/2d5.md | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/content/zettel/2d5.md b/content/zettel/2d5.md new file mode 100644 index 0000000..87f79c2 --- /dev/null +++ b/content/zettel/2d5.md @@ -0,0 +1,21 @@ ++++ +title = "Using a realistic SAT solver" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["2d4"] +forwardlinks = [] +zettelid = "2d5" ++++ + +I have now implemented usage of a real SMT solver (Z3) using OCaml. It +is surprisingly easy to use this SMT solver from the OCaml code, much +easier than using the external Z3 executable. Expressions can easily be +added as various assertions, and expressions themselves can also be +built quite easily and recursively from given predicates. This makes it +simple to add a custom solver to custom predicates. + +It should therefore be possible to also use the SAT solver to simplify +arbitrary predicates as well, however, there are still various problems +with extracting the expressions from the SAT solver again, as they are +in the internal expression format of the solver. |