simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 13:14:09 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fixed bug in sat example in readme

Browse source
This commit is contained in:
Guillaume Bury 2015-03-03 17:09:39 +01:00
parent cdf8371394
commit f6fbd874ec
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
README.md
View file

@ -30,16 +30,18 @@ as shown in the following code :
let b = Sat.make 1 (* Atoms can be created from integers *) let b = Sat.make 1 (* Atoms can be created from integers *)
(* Let's create some formulas *) (* Let's create some formulas *)
let p = F.make_and [a; b] let p = F.make_atom a
let q = F.make_or [F.make_not a; F.make_not b] 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 *) (* 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 *) let _ = Sat.solve () (* Should return Sat.Sat *)
(* The Sat solver has an incremental mutable state, so we still have (* The Sat solver has an incremental mutable state, so we still have
* the formula 'p' in our assumptions *) * the formula 'r' in our assumptions *)
Sat.assume (F.make_cnf q) Sat.assume (F.make_cnf s)
let _ = Sat.solve () (* Should return Sat.Unsat *) let _ = Sat.solve () (* Should return Sat.Unsat *)
``` ```