From f6fbd874ecfcf583a1b98000445421ae91c95a7e Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 3 Mar 2015 17:09:39 +0100 Subject: [PATCH] Fixed bug in sat example in readme --- README.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 0991d8b9..01111ef0 100644 --- a/README.md +++ b/README.md @@ -30,16 +30,18 @@ as shown in the following code : let b = Sat.make 1 (* Atoms can be created from integers *) (* Let's create some formulas *) - let p = F.make_and [a; b] - let q = F.make_or [F.make_not a; F.make_not b] + let p = F.make_atom a + let q = F.make_atom b + let r = F.make_and [p; q] + let s = F.make_or [F.make_not p; F.make_not q] (* We can try and check the satisfiability of the given formulas *) - Sat.assume (F.make_cnf p) + Sat.assume (F.make_cnf r) let _ = Sat.solve () (* Should return Sat.Sat *) (* The Sat solver has an incremental mutable state, so we still have - * the formula 'p' in our assumptions *) - Sat.assume (F.make_cnf q) + * the formula 'r' in our assumptions *) + Sat.assume (F.make_cnf s) let _ = Sat.solve () (* Should return Sat.Unsat *) ```