From 817742c04203819d3cfb1dd4a4453fee3147e02b Mon Sep 17 00:00:00 2001 From: Connor Olding Date: Wed, 8 Jun 2022 04:54:47 +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 31a9454..03e0360 100644 --- a/logic/README.md +++ b/logic/README.md @@ -1 +1,12 @@ satisfy them booleans, solve them integers. + +`cnf.py` is a small library for creating formulas in conjunctive normal form, +and also for dealing with the eponymous CNF file format. +the types used internally and exposed externally are very simple: +booleans, integers, and lists of each. + +`z0.py` is a slightly larger library that builds upon `cnf.py`, +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)