From 3d7f0b44604f1ff5777af45f827c1c02ecde817f Mon Sep 17 00:00:00 2001 From: Connor Olding Date: Wed, 8 Jun 2022 05:28:51 +0200 Subject: [PATCH] logic: update readme --- logic/README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/logic/README.md b/logic/README.md index 03e0360..8af30be 100644 --- a/logic/README.md +++ b/logic/README.md @@ -10,3 +10,14 @@ mimicing a tiny subset of the [z3](https://github.com/Z3Prover/z3) library's interface. it exposes classes for high-level bitvectors and [unary-encoded integers.](https://en.wikipedia.org/wiki/Unary_numeral_system) (unary is sometimes more efficient to solve) + +`sugarcane4unary2.py` utilizes z0 to solve a (pretty arbitrary) problem +relating to farming sugarcane in Minecraft. you will need to set +the environment variable `SOLVER` to (the path of) an external SAT solver. +[kissat](https://github.com/arminbiere/kissat) works well. + +`hex_problem.py` creates a hexagon grid with some colored numbers in it. +it doesn't really a serve a purpose. + +`yices_solution.py` parses a solution from a SAT solver, +given the original yices-generated CNF.