mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-22 17:36:41 -05:00
cleanup msat
This commit is contained in:
Simon Cruanes
parent
1a58ab0bfc
commit
4a337a85d3
45 changed files with 10 additions and 1323 deletions
|
|
@ -2,5 +2,5 @@
|
|||
(name Sidekick_msat_solver)
|
||||
(public_name sidekick.msat-solver)
|
||||
(libraries containers iter sidekick.core sidekick.util
|
||||
sidekick.cc msat msat.backend)
|
||||
sidekick.cc sidekick.sat)
|
||||
(flags :standard -open Sidekick_util))
|
||||
|
|
|
|||
18
src/sat/dune
18
src/sat/dune
|
|
@ -1,10 +1,10 @@
|
|||
|
||||
(alias
|
||||
(name runtest)
|
||||
(deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src))
|
||||
(locks test)
|
||||
(package msat)
|
||||
(action (progn
|
||||
(run mdx test README.md)
|
||||
(diff? README.md README.md.corrected))))
|
||||
|
||||
(library
|
||||
(name msat)
|
||||
(public_name msat)
|
||||
(libraries iter)
|
||||
(synopsis "core data structures and algorithms for msat")
|
||||
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -bin-annot
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,10 +0,0 @@
|
|||
|
||||
(library
|
||||
(name msat)
|
||||
(public_name msat)
|
||||
(libraries iter)
|
||||
(synopsis "core data structures and algorithms for msat")
|
||||
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -bin-annot
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
|
||||
(documentation
|
||||
(package msat)
|
||||
(mld_files :standard))
|
||||
|
|
@ -1,121 +0,0 @@
|
|||
|
||||
|
||||
{1 mSAT: a Modular SAT Solver}
|
||||
|
||||
(The entry point of this library is the module: {!module-Msat}.)
|
||||
|
||||
A modular implementation of the SMT algorithm can be found in the {!Msat.Solver} module,
|
||||
as a functor which takes two modules :
|
||||
|
||||
- A representation of formulas (which implements the `Formula_intf.S` signature)
|
||||
|
||||
- A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
|
||||
|
||||
- A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
|
||||
side effects to their internal state)
|
||||
|
||||
{3 Sat Solver}
|
||||
|
||||
A ready-to-use SAT solver is available in the {!Msat_sat} module
|
||||
using the [msat.sat] library (see {!module-Msat_sat}). It can be loaded
|
||||
as shown in the following code :
|
||||
|
||||
{[
|
||||
# #require "msat";;
|
||||
# #require "msat.sat";;
|
||||
# #print_depth 0;; (* do not print details *)
|
||||
]}
|
||||
|
||||
Then we can create a solver and create some boolean variables:
|
||||
|
||||
{[
|
||||
module Sat = Msat_sat
|
||||
module E = Sat.Int_lit (* expressions *)
|
||||
|
||||
let solver = Sat.create()
|
||||
|
||||
(* We create here two distinct atoms *)
|
||||
let a = E.fresh () (* A 'new_atom' is always distinct from any other atom *)
|
||||
let b = E.make 1 (* Atoms can be created from integers *)
|
||||
]}
|
||||
|
||||
We can try and check the satisfiability of some clauses — here, the clause [a or b].
|
||||
[Sat.assume] adds a list of clauses to the solver. Calling [Sat.solve]
|
||||
will check the satisfiability of the current set of clauses, here "Sat".
|
||||
|
||||
{[
|
||||
# a <> b;;
|
||||
- : bool = true
|
||||
# Sat.assume solver [[a; b]] ();;
|
||||
- : unit = ()
|
||||
# let res = Sat.solve solver;;
|
||||
val res : Sat.res = Sat.Sat ...
|
||||
]}
|
||||
|
||||
The Sat solver has an incremental mutable state, so we still have
|
||||
the clause `a or b` in our assumptions.
|
||||
We add `not a` and `not b` to the state, and get "Unsat".
|
||||
|
||||
{[
|
||||
# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
|
||||
- : unit = ()
|
||||
# let res = Sat.solve solver ;;
|
||||
val res : Sat.res = Sat.Unsat ...
|
||||
]}
|
||||
|
||||
{3 Formulas API}
|
||||
|
||||
Writing clauses by hand can be tedious and error-prone.
|
||||
The functor {!Msat_tseitin.Make} in the library [msat.tseitin] (see {!module-Msat_tseitin}).
|
||||
proposes a formula AST (parametrized by
|
||||
atoms) and a function to convert these formulas into clauses:
|
||||
|
||||
{[
|
||||
# #require "msat.tseitin";;
|
||||
]}
|
||||
|
||||
{[
|
||||
(* Module initialization *)
|
||||
module F = Msat_tseitin.Make(E)
|
||||
|
||||
let solver = Sat.create ()
|
||||
|
||||
(* We create here two distinct atoms *)
|
||||
let a = E.fresh () (* A fresh atom is always distinct from any other atom *)
|
||||
let b = E.make 1 (* Atoms can be created from integers *)
|
||||
|
||||
(* Let's create some formulas *)
|
||||
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, by turning
|
||||
it into clauses using `make_cnf`:
|
||||
|
||||
{[
|
||||
# Sat.assume solver (F.make_cnf r) ();;
|
||||
- : unit = ()
|
||||
# Sat.solve solver;;
|
||||
- : Sat.res = Sat.Sat ...
|
||||
]}
|
||||
|
||||
{[
|
||||
# Sat.assume solver (F.make_cnf s) ();;
|
||||
- : unit = ()
|
||||
# Sat.solve solver ;;
|
||||
- : Sat.res = Sat.Unsat ...
|
||||
]}
|
||||
|
||||
{3 Backtracking utils}
|
||||
|
||||
The library {!module-Msat_backtrack} contains some backtrackable
|
||||
data structures that are useful for implementing theories.
|
||||
|
||||
{3 Library msat.backend}
|
||||
|
||||
This is used for proof backends:
|
||||
|
||||
The entry point of this library is the module:
|
||||
{!module-Msat_backend}.
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
{
|
||||
open Dimacs_parse
|
||||
}
|
||||
|
||||
let number = ['1' - '9'] ['0' - '9']*
|
||||
|
||||
rule token = parse
|
||||
| eof { EOF }
|
||||
| "c" { comment lexbuf }
|
||||
| [' ' '\t' '\r'] { token lexbuf }
|
||||
| 'p' { P }
|
||||
| "cnf" { CNF }
|
||||
| '\n' { Lexing.new_line lexbuf; token lexbuf }
|
||||
| '0' { ZERO }
|
||||
| '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) }
|
||||
| _ { failwith @@ Printf.sprintf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
|
||||
|
||||
and comment = parse
|
||||
| '\n' { Lexing.new_line lexbuf; token lexbuf }
|
||||
| [^'\n'] { comment lexbuf }
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
/* Copyright 2005 INRIA */
|
||||
|
||||
%{
|
||||
let lnum pos = pos.Lexing.pos_lnum
|
||||
let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
|
||||
let pp_pos out (start,stop) =
|
||||
Format.fprintf out "(at %d:%d - %d:%d)"
|
||||
(lnum start) (cnum start) (lnum stop) (cnum stop)
|
||||
%}
|
||||
|
||||
%token <int> LIT
|
||||
%token ZERO
|
||||
%token P CNF EOF
|
||||
|
||||
%start file
|
||||
%type <int list list> file
|
||||
|
||||
%%
|
||||
|
||||
/* DIMACS syntax */
|
||||
|
||||
prelude:
|
||||
| P CNF LIT LIT { () }
|
||||
|
||||
clauses:
|
||||
| { [] }
|
||||
| clause clauses { $1 :: $2 }
|
||||
|
||||
file:
|
||||
| prelude clauses EOF { $2 }
|
||||
|
||||
clause:
|
||||
| ZERO { [] }
|
||||
| LIT clause { $1 :: $2 }
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
|
||||
; main binary
|
||||
(executable
|
||||
(name main)
|
||||
(public_name msat)
|
||||
(package msat-bin)
|
||||
(libraries containers camlzip msat msat.sat msat.backend)
|
||||
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
|
||||
(ocamlopt_flags :standard -O3 -color always
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
||||
(ocamlyacc (modules Dimacs_parse))
|
||||
(ocamllex (modules Dimacs_lex))
|
||||
|
|
@ -1,186 +0,0 @@
|
|||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
exception Incorrect_model
|
||||
exception Out_of_time
|
||||
exception Out_of_space
|
||||
|
||||
let file = ref ""
|
||||
let p_cnf = ref false
|
||||
let p_check = ref false
|
||||
let p_dot_proof = ref ""
|
||||
let p_proof_print = ref false
|
||||
let time_limit = ref 300.
|
||||
let size_limit = ref 1000_000_000.
|
||||
let no_proof = ref false
|
||||
|
||||
module S = Msat_sat
|
||||
|
||||
module Process() = struct
|
||||
module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S))
|
||||
|
||||
let hyps = ref []
|
||||
|
||||
let st = S.create ~store_proof:(not !no_proof) ~size:`Big ()
|
||||
|
||||
let check_model sat =
|
||||
let check_clause c =
|
||||
let l = List.map (function a ->
|
||||
Log.debugf 99
|
||||
(fun k -> k "Checking value of %a" S.Formula.pp a);
|
||||
sat.Msat.eval a) c in
|
||||
List.exists (fun x -> x) l
|
||||
in
|
||||
let l = List.map check_clause !hyps in
|
||||
List.for_all (fun x -> x) l
|
||||
|
||||
let prove ~assumptions () =
|
||||
let res = S.solve ~assumptions st in
|
||||
let t = Sys.time () in
|
||||
begin match res with
|
||||
| S.Sat state ->
|
||||
if !p_check then
|
||||
if not (check_model state) then
|
||||
raise Incorrect_model;
|
||||
let t' = Sys.time () -. t in
|
||||
Format.printf "Sat (%f/%f)@." t t'
|
||||
| S.Unsat state ->
|
||||
if !p_check then (
|
||||
let p = state.Msat.get_proof () in
|
||||
S.Proof.check_empty_conclusion p;
|
||||
S.Proof.check p;
|
||||
if !p_dot_proof <> "" then (
|
||||
let oc = open_out !p_dot_proof in
|
||||
let fmt = Format.formatter_of_out_channel oc in
|
||||
Format.fprintf fmt "%a@?" D.pp p;
|
||||
flush oc; close_out_noerr oc;
|
||||
)
|
||||
);
|
||||
let t' = Sys.time () -. t in
|
||||
Format.printf "Unsat (%f/%f)@." t t'
|
||||
end
|
||||
|
||||
let conv_c c = List.rev_map S.Int_lit.make c
|
||||
|
||||
let add_clauses cs =
|
||||
S.assume st (CCList.map conv_c cs) ()
|
||||
end[@@inline]
|
||||
|
||||
let parse_file f =
|
||||
let module L = Lexing in
|
||||
CCIO.with_in f
|
||||
(fun ic ->
|
||||
let buf =
|
||||
if CCString.suffix ~suf:".gz" f
|
||||
then (
|
||||
let gic = Gzip.open_in_chan ic in
|
||||
L.from_function (fun bytes len -> Gzip.input gic bytes 0 len)
|
||||
) else L.from_channel ic
|
||||
in
|
||||
buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;};
|
||||
Dimacs_parse.file Dimacs_lex.token buf)
|
||||
|
||||
let error_msg opt arg l =
|
||||
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
|
||||
arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
|
||||
Format.flush_str_formatter ()
|
||||
|
||||
(* Arguments parsing *)
|
||||
let int_arg r arg =
|
||||
let l = String.length arg in
|
||||
let multiplier m =
|
||||
let arg1 = String.sub arg 0 (l-1) in
|
||||
r := m *. (float_of_string arg1)
|
||||
in
|
||||
if l = 0 then raise (Arg.Bad "bad numeric argument")
|
||||
else
|
||||
try
|
||||
match arg.[l-1] with
|
||||
| 'k' -> multiplier 1e3
|
||||
| 'M' -> multiplier 1e6
|
||||
| 'G' -> multiplier 1e9
|
||||
| 'T' -> multiplier 1e12
|
||||
| 's' -> multiplier 1.
|
||||
| 'm' -> multiplier 60.
|
||||
| 'h' -> multiplier 3600.
|
||||
| 'd' -> multiplier 86400.
|
||||
| '0'..'9' -> r := float_of_string arg
|
||||
| _ -> raise (Arg.Bad "bad numeric argument")
|
||||
with Failure _ -> raise (Arg.Bad "bad numeric argument")
|
||||
|
||||
let setup_gc_stat () =
|
||||
at_exit (fun () ->
|
||||
Gc.print_stat stdout;
|
||||
)
|
||||
|
||||
let input_file = fun s -> file := s
|
||||
|
||||
let usage = "Usage : main [options] <file>"
|
||||
let argspec = Arg.align [
|
||||
"-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
|
||||
" Enable stack traces";
|
||||
"-cnf", Arg.Set p_cnf,
|
||||
" Prints the cnf used.";
|
||||
"-check", Arg.Set p_check,
|
||||
" Build, check and print the proof (if output is set), if unsat";
|
||||
"-dot", Arg.Set_string p_dot_proof,
|
||||
" If provided, print the dot proof in the given file";
|
||||
"-gc", Arg.Unit setup_gc_stat,
|
||||
" Outputs statistics about the GC";
|
||||
"-size", Arg.String (int_arg size_limit),
|
||||
"<s>[kMGT] Sets the size limit for the sat solver";
|
||||
"-time", Arg.String (int_arg time_limit),
|
||||
"<t>[smhd] Sets the time limit for the sat solver";
|
||||
"-v", Arg.Int (fun i -> Log.set_debug i),
|
||||
"<lvl> Sets the debug verbose level";
|
||||
"-no-proof", Arg.Set no_proof, " disable proof logging";
|
||||
]
|
||||
|
||||
(* Limits alarm *)
|
||||
let check () =
|
||||
let t = Sys.time () in
|
||||
let heap_size = (Gc.quick_stat ()).Gc.heap_words in
|
||||
let s = float heap_size *. float Sys.word_size /. 8. in
|
||||
if t > !time_limit then
|
||||
raise Out_of_time
|
||||
else if s > !size_limit then
|
||||
raise Out_of_space
|
||||
|
||||
let main () =
|
||||
(* Administrative duties *)
|
||||
Arg.parse argspec input_file usage;
|
||||
if !file = "" then (
|
||||
Arg.usage argspec usage;
|
||||
exit 2
|
||||
);
|
||||
let al = Gc.create_alarm check in
|
||||
|
||||
let module P = Process() in
|
||||
|
||||
(* Interesting stuff happening *)
|
||||
let clauses = parse_file !file in
|
||||
P.add_clauses clauses;
|
||||
P.prove ~assumptions:[] ();
|
||||
Gc.delete_alarm al;
|
||||
()
|
||||
|
||||
let () =
|
||||
try
|
||||
main ()
|
||||
with
|
||||
| Out_of_time ->
|
||||
Format.printf "Timeout@.";
|
||||
exit 2
|
||||
| Out_of_space ->
|
||||
Format.printf "Spaceout@.";
|
||||
exit 3
|
||||
| Incorrect_model ->
|
||||
Format.printf "Internal error : incorrect *sat* model@.";
|
||||
exit 4
|
||||
| S.Proof.Resolution_error msg ->
|
||||
Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg;
|
||||
exit 5
|
||||
|
||||
|
|
@ -1,66 +0,0 @@
|
|||
|
||||
exception Bad_atom
|
||||
(** Exception raised if an atom cannot be created *)
|
||||
|
||||
type t = int
|
||||
(** Atoms are represented as integers. [-i] begin the negation of [i].
|
||||
Additionally, since we nee dot be able to create fresh atoms, we
|
||||
use even integers for user-created atoms, and odd integers for the
|
||||
fresh atoms. *)
|
||||
|
||||
let max_lit = max_int
|
||||
|
||||
(* Counters *)
|
||||
let max_index = ref 0
|
||||
let max_fresh = ref (-1)
|
||||
|
||||
(** Internal function for creating atoms.
|
||||
Updates the internal counters *)
|
||||
let _make i =
|
||||
if i <> 0 && (abs i) < max_lit then begin
|
||||
max_index := max !max_index (abs i);
|
||||
i
|
||||
end else
|
||||
raise Bad_atom
|
||||
|
||||
let to_int i = i
|
||||
|
||||
(** *)
|
||||
let neg a = - a
|
||||
|
||||
let norm a =
|
||||
abs a, if a < 0 then
|
||||
Solver_intf.Negated
|
||||
else
|
||||
Solver_intf.Same_sign
|
||||
|
||||
let abs = abs
|
||||
|
||||
let sign i = i > 0
|
||||
|
||||
let apply_sign b i = if b then i else neg i
|
||||
|
||||
let set_sign b i = if b then abs i else neg (abs i)
|
||||
|
||||
let hash (a:int) = a land max_int
|
||||
let equal (a:int) b = a=b
|
||||
let compare (a:int) b = compare a b
|
||||
|
||||
let make i = _make (2 * i)
|
||||
|
||||
let fresh () =
|
||||
incr max_fresh;
|
||||
_make (2 * !max_fresh + 1)
|
||||
|
||||
(*
|
||||
let iter: (t -> unit) -> unit = fun f ->
|
||||
for j = 1 to !max_index do
|
||||
f j
|
||||
done
|
||||
*)
|
||||
|
||||
let pp fmt a =
|
||||
Format.fprintf fmt "%s%s%d"
|
||||
(if a < 0 then "~" else "")
|
||||
(if a mod 2 = 0 then "v" else "f")
|
||||
((abs a) / 2)
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
|
||||
(** {1 The module defining formulas} *)
|
||||
|
||||
(** SAT Formulas
|
||||
|
||||
This modules implements formuals adequate for use in a pure SAT Solver.
|
||||
Atomic formuals are represented using integers, that should allow
|
||||
near optimal efficiency (both in terms of space and time).
|
||||
*)
|
||||
|
||||
include Solver_intf.FORMULA
|
||||
(** This modules implements the requirements for implementing an SAT Solver. *)
|
||||
|
||||
val make : int -> t
|
||||
(** Make a proposition from an integer. *)
|
||||
|
||||
val to_int : t -> int
|
||||
|
||||
val fresh : unit -> t
|
||||
(** Make a fresh atom *)
|
||||
|
||||
val compare : t -> t -> int
|
||||
(** Compare atoms *)
|
||||
|
||||
val sign : t -> bool
|
||||
(** Is the given atom positive ? *)
|
||||
|
||||
val apply_sign : bool -> t -> t
|
||||
(** [apply_sign b] is the identity if [b] is [true], and the negation
|
||||
function if [b] is [false]. *)
|
||||
|
||||
val set_sign : bool -> t -> t
|
||||
(** Return the atom with the sign set. *)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2016 Guillaume Bury
|
||||
*)
|
||||
|
||||
module Int_lit = Int_lit
|
||||
include Msat.Make_pure_sat(struct
|
||||
module Formula = Int_lit
|
||||
type proof = unit
|
||||
end)
|
||||
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2016 Guillaume Bury
|
||||
*)
|
||||
|
||||
(** Sat solver
|
||||
|
||||
This modules instanciates a pure sat solver using integers to represent
|
||||
atomic propositions.
|
||||
*)
|
||||
|
||||
module Int_lit = Int_lit
|
||||
|
||||
include Msat.S
|
||||
with type Formula.t = Int_lit.t
|
||||
and type theory = unit
|
||||
and type lemma = unit
|
||||
(** A functor that can generate as many solvers as needed. *)
|
||||
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
|
||||
(library
|
||||
(name msat_sat)
|
||||
(public_name msat.sat)
|
||||
(synopsis "purely boolean interface to Msat")
|
||||
(libraries msat)
|
||||
(flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
|
||||
(ocamlopt_flags :standard -O3 -color always
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
|
||||
(executable
|
||||
(name sudoku_solve)
|
||||
(modes native)
|
||||
(libraries msat msat.backtrack iter containers)
|
||||
(flags :standard -warn-error -a -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -bin-annot
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
|
@ -1,331 +0,0 @@
|
|||
|
||||
(** {1 simple sudoku solver} *)
|
||||
|
||||
module Fmt = CCFormat
|
||||
module Log = Msat.Log
|
||||
module Vec = Msat.Vec
|
||||
|
||||
let errorf msg = CCFormat.kasprintf failwith msg
|
||||
|
||||
module Cell : sig
|
||||
type t = private int
|
||||
val equal : t -> t -> bool
|
||||
val neq : t -> t -> bool
|
||||
val hash : t -> int
|
||||
val empty : t
|
||||
val is_empty : t -> bool
|
||||
val is_full : t -> bool
|
||||
val make : int -> t
|
||||
val pp : t Fmt.printer
|
||||
end = struct
|
||||
type t = int
|
||||
let empty = 0
|
||||
let[@inline] make i = assert (i >= 0 && i <= 9); i
|
||||
let[@inline] is_empty x = x = 0
|
||||
let[@inline] is_full x = x > 0
|
||||
let hash = CCHash.int
|
||||
let[@inline] equal (a:t) b = a=b
|
||||
let[@inline] neq (a:t) b = a<>b
|
||||
let pp out i = if i=0 then Fmt.char out '.' else Fmt.int out i
|
||||
end
|
||||
|
||||
module Grid : sig
|
||||
type t
|
||||
|
||||
val get : t -> int -> int -> Cell.t
|
||||
val set : t -> int -> int -> Cell.t -> t
|
||||
|
||||
(** A set of related cells *)
|
||||
type set = (int*int*Cell.t) Iter.t
|
||||
|
||||
val rows : t -> set Iter.t
|
||||
val cols : t -> set Iter.t
|
||||
val squares : t -> set Iter.t
|
||||
|
||||
val all_cells : t -> (int*int*Cell.t) Iter.t
|
||||
|
||||
val parse : string -> t
|
||||
val is_full : t -> bool
|
||||
val is_valid : t -> bool
|
||||
val matches : pat:t -> t -> bool
|
||||
val pp : t Fmt.printer
|
||||
end = struct
|
||||
type t = Cell.t array
|
||||
|
||||
let[@inline] get (s:t) i j = s.(i*9 + j)
|
||||
|
||||
let[@inline] set (s:t) i j n =
|
||||
let s' = Array.copy s in
|
||||
s'.(i*9 + j) <- n;
|
||||
s'
|
||||
|
||||
(** A set of related cells *)
|
||||
type set = (int*int*Cell.t) Iter.t
|
||||
|
||||
open Iter.Infix
|
||||
|
||||
let all_cells (g:t) =
|
||||
0 -- 8 >>= fun i ->
|
||||
0 -- 8 >|= fun j -> (i,j,get g i j)
|
||||
|
||||
let rows (g:t) =
|
||||
0 -- 8 >|= fun i ->
|
||||
( 0 -- 8 >|= fun j -> (i,j,get g i j))
|
||||
|
||||
let cols g =
|
||||
0 -- 8 >|= fun j ->
|
||||
( 0 -- 8 >|= fun i -> (i,j,get g i j))
|
||||
|
||||
let squares g =
|
||||
0 -- 2 >>= fun sq_i ->
|
||||
0 -- 2 >|= fun sq_j ->
|
||||
( 0 -- 2 >>= fun off_i ->
|
||||
0 -- 2 >|= fun off_j ->
|
||||
let i = 3*sq_i + off_i in
|
||||
let j = 3*sq_j + off_j in
|
||||
(i,j,get g i j))
|
||||
|
||||
let is_full g = Array.for_all Cell.is_full g
|
||||
|
||||
let is_valid g =
|
||||
let all_distinct (s:set) =
|
||||
(s >|= fun (_,_,c) -> c)
|
||||
|> Iter.diagonal
|
||||
|> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2)
|
||||
in
|
||||
Iter.for_all all_distinct @@ rows g &&
|
||||
Iter.for_all all_distinct @@ cols g &&
|
||||
Iter.for_all all_distinct @@ squares g
|
||||
|
||||
let matches ~pat:g1 g2 : bool =
|
||||
all_cells g1
|
||||
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||
|> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y)
|
||||
|
||||
let pp out g =
|
||||
Fmt.fprintf out "@[<v>";
|
||||
Array.iteri
|
||||
(fun i n ->
|
||||
Cell.pp out n;
|
||||
if i mod 9 = 8 then Fmt.fprintf out "@,")
|
||||
g;
|
||||
Fmt.fprintf out "@]"
|
||||
|
||||
let parse (s:string) : t =
|
||||
if String.length s < 81 then (
|
||||
errorf "line is too short, expected 81 chars, not %d" (String.length s);
|
||||
);
|
||||
let a = Array.make 81 Cell.empty in
|
||||
for i = 0 to 80 do
|
||||
let c = String.get s i in
|
||||
let n = if c = '.' then 0 else Char.code c - Char.code '0' in
|
||||
if n < 0 || n > 9 then errorf "invalid char %c" c;
|
||||
a.(i) <- Cell.make n
|
||||
done;
|
||||
a
|
||||
end
|
||||
|
||||
module B_ref = Msat_backtrack.Ref
|
||||
|
||||
module Solver : sig
|
||||
type t
|
||||
val create : Grid.t -> t
|
||||
val solve : t -> Grid.t option
|
||||
end = struct
|
||||
open Msat.Solver_intf
|
||||
|
||||
(* formulas *)
|
||||
module F = struct
|
||||
type t = bool*int*int*Cell.t
|
||||
let equal (sign1,x1,y1,c1)(sign2,x2,y2,c2) =
|
||||
sign1=sign2 && x1=x2 && y1=y2 && Cell.equal c1 c2
|
||||
let hash (sign,x,y,c) = CCHash.(combine4 (bool sign)(int x)(int y)(Cell.hash c))
|
||||
let pp out (sign,x,y,c) =
|
||||
Fmt.fprintf out "[@[(%d,%d) %s %a@]]" x y (if sign then "=" else "!=") Cell.pp c
|
||||
let neg (sign,x,y,c) = (not sign,x,y,c)
|
||||
let norm ((sign,_,_,_) as f) =
|
||||
if sign then f, Same_sign else neg f, Negated
|
||||
|
||||
let make sign x y (c:Cell.t) : t = (sign,x,y,c)
|
||||
end
|
||||
|
||||
module Theory = struct
|
||||
type proof = unit
|
||||
module Formula = F
|
||||
type t = {
|
||||
grid: Grid.t B_ref.t;
|
||||
}
|
||||
|
||||
let create g : t = {grid=B_ref.create g}
|
||||
let[@inline] grid self : Grid.t = B_ref.get self.grid
|
||||
let[@inline] set_grid self g : unit = B_ref.set self.grid g
|
||||
|
||||
let push_level self = B_ref.push_level self.grid
|
||||
let pop_levels self n = B_ref.pop_levels self.grid n
|
||||
|
||||
let pp_c_ = Fmt.(list ~sep:(return "@ ∨ ")) F.pp
|
||||
let[@inline] logs_conflict kind c : unit =
|
||||
Log.debugf 4 (fun k->k "(@[conflict.%s@ %a@])" kind pp_c_ c)
|
||||
|
||||
(* check that all cells are full *)
|
||||
let check_full_ (self:t) acts : unit =
|
||||
Grid.all_cells (grid self)
|
||||
(fun (x,y,c) ->
|
||||
if Cell.is_empty c then (
|
||||
let c =
|
||||
CCList.init 9
|
||||
(fun c -> F.make true x y (Cell.make (c+1)))
|
||||
in
|
||||
Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c);
|
||||
acts.acts_add_clause ~keep:true c ();
|
||||
))
|
||||
|
||||
(* check constraints *)
|
||||
let check_ (self:t) acts : unit =
|
||||
Log.debugf 4 (fun k->k "(@[sudoku.check@ @[:g %a@]@])" Grid.pp (B_ref.get self.grid));
|
||||
let[@inline] all_diff kind f =
|
||||
let pairs =
|
||||
f (grid self)
|
||||
|> Iter.flat_map
|
||||
(fun set ->
|
||||
set
|
||||
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||
|> Iter.diagonal)
|
||||
in
|
||||
pairs
|
||||
(fun ((x1,y1,c1),(x2,y2,c2)) ->
|
||||
if Cell.equal c1 c2 then (
|
||||
assert (x1<>x2 || y1<>y2);
|
||||
let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in
|
||||
logs_conflict ("all-diff." ^ kind) c;
|
||||
acts.acts_raise_conflict c ()
|
||||
))
|
||||
in
|
||||
all_diff "rows" Grid.rows;
|
||||
all_diff "cols" Grid.cols;
|
||||
all_diff "squares" Grid.squares;
|
||||
()
|
||||
|
||||
let trail_ (acts:_ Msat.acts) =
|
||||
acts.acts_iter_assumptions
|
||||
|> Iter.map
|
||||
(function
|
||||
| Assign _ -> assert false
|
||||
| Lit f -> f)
|
||||
|
||||
(* update current grid with the given slice *)
|
||||
let add_slice (self:t) acts : unit =
|
||||
trail_ acts
|
||||
(function
|
||||
| false,_,_,_ -> ()
|
||||
| true,x,y,c ->
|
||||
assert (Cell.is_full c);
|
||||
let grid = grid self in
|
||||
let c' = Grid.get grid x y in
|
||||
if Cell.is_empty c' then (
|
||||
set_grid self (Grid.set grid x y c);
|
||||
) else if Cell.neq c c' then (
|
||||
(* conflict: at most one value *)
|
||||
let c = [F.make false x y c; F.make false x y c'] in
|
||||
logs_conflict "at-most-one" c;
|
||||
acts.acts_raise_conflict c ()
|
||||
)
|
||||
)
|
||||
|
||||
let partial_check (self:t) acts : unit =
|
||||
Log.debugf 4
|
||||
(fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])"
|
||||
(Fmt.list F.pp) (trail_ acts |> Iter.to_list));
|
||||
add_slice self acts;
|
||||
check_ self acts
|
||||
|
||||
let final_check (self:t) acts : unit =
|
||||
Log.debugf 4 (fun k->k "(@[sudoku.final-check@])");
|
||||
check_full_ self acts;
|
||||
check_ self acts
|
||||
|
||||
end
|
||||
|
||||
module S = Msat.Make_cdcl_t(Theory)
|
||||
|
||||
type t = {
|
||||
grid0: Grid.t;
|
||||
solver: S.t;
|
||||
}
|
||||
|
||||
let solve (self:t) : _ option =
|
||||
let assumptions =
|
||||
Grid.all_cells self.grid0
|
||||
|> Iter.filter (fun (_,_,c) -> Cell.is_full c)
|
||||
|> Iter.map (fun (x,y,c) -> F.make true x y c)
|
||||
|> Iter.map (S.make_atom self.solver)
|
||||
|> Iter.to_rev_list
|
||||
in
|
||||
Log.debugf 2
|
||||
(fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
|
||||
let r =
|
||||
match S.solve self.solver ~assumptions with
|
||||
| S.Sat _ -> Some (Theory.grid (S.theory self.solver))
|
||||
| S.Unsat _ -> None
|
||||
in
|
||||
(* TODO: print some stats *)
|
||||
r
|
||||
|
||||
let create g : t =
|
||||
{ solver=S.create ~store_proof:false (Theory.create g); grid0=g }
|
||||
end
|
||||
|
||||
let solve_grid (g:Grid.t) : Grid.t option =
|
||||
let s = Solver.create g in
|
||||
Solver.solve s
|
||||
|
||||
let solve_file file =
|
||||
Format.printf "solve grids in file %S@." file;
|
||||
let start = Sys.time() in
|
||||
let grids =
|
||||
CCIO.with_in file CCIO.read_lines_l
|
||||
|> CCList.filter_map
|
||||
(fun s ->
|
||||
let s = String.trim s in
|
||||
if s="" then None
|
||||
else match Grid.parse s with
|
||||
| g -> Some g
|
||||
| exception e ->
|
||||
errorf "cannot parse sudoku %S: %s@." s (Printexc.to_string e))
|
||||
in
|
||||
Format.printf "parsed %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
|
||||
List.iter
|
||||
(fun g ->
|
||||
Format.printf "@[<v>@,#########################@,@[<2>solve grid:@ %a@]@]@." Grid.pp g;
|
||||
let start=Sys.time() in
|
||||
match solve_grid g with
|
||||
| None -> Format.printf "no solution (in %.3fs)@." (Sys.time()-.start)
|
||||
| Some g' when not @@ Grid.is_full g' ->
|
||||
errorf "grid %a@ is not full" Grid.pp g'
|
||||
| Some g' when not @@ Grid.is_valid g' ->
|
||||
errorf "grid %a@ is not valid" Grid.pp g'
|
||||
| Some g' when not @@ Grid.matches ~pat:g g' ->
|
||||
errorf "grid %a@ @[<2>does not match original@ %a@]" Grid.pp g' Grid.pp g
|
||||
| Some g' ->
|
||||
Format.printf "@[<v>@[<2>solution (in %.3fs):@ %a@]@,###################@]@."
|
||||
(Sys.time()-.start) Grid.pp g')
|
||||
grids;
|
||||
Format.printf "@.solved %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
|
||||
()
|
||||
|
||||
let () =
|
||||
Fmt.set_color_default true;
|
||||
let files = ref [] in
|
||||
let debug = ref 0 in
|
||||
let opts = [
|
||||
"--debug", Arg.Set_int debug, " debug";
|
||||
"-d", Arg.Set_int debug, " debug";
|
||||
] |> Arg.align in
|
||||
Arg.parse opts (fun f -> files := f :: !files) "sudoku_solve [options] <file>";
|
||||
Msat.Log.set_debug !debug;
|
||||
try
|
||||
List.iter (fun f -> solve_file f) !files;
|
||||
with
|
||||
| Failure msg | Invalid_argument msg ->
|
||||
Format.printf "@{<Red>Error@}:@.%s@." msg;
|
||||
exit 1
|
||||
|
|
@ -1,326 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Alt-Ergo Zero *)
|
||||
(* *)
|
||||
(* Sylvain Conchon and Alain Mebsout *)
|
||||
(* Universite Paris-Sud 11 *)
|
||||
(* *)
|
||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
||||
(* Apache Software License version 2.0 *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
module type Arg = Tseitin_intf.Arg
|
||||
|
||||
module type S = Tseitin_intf.S
|
||||
|
||||
module Make (F : Tseitin_intf.Arg) = struct
|
||||
|
||||
exception Empty_Or
|
||||
type combinator = And | Or | Imp | Not
|
||||
|
||||
type atom = F.t
|
||||
type t =
|
||||
| True
|
||||
| Lit of atom
|
||||
| Comb of combinator * t list
|
||||
|
||||
let rec pp fmt phi =
|
||||
match phi with
|
||||
| True -> Format.fprintf fmt "true"
|
||||
| Lit a -> F.pp fmt a
|
||||
| Comb (Not, [f]) ->
|
||||
Format.fprintf fmt "not (%a)" pp f
|
||||
| Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l
|
||||
| Comb (Or, l) -> Format.fprintf fmt "(%a)" (pp_list "or") l
|
||||
| Comb (Imp, [f1; f2]) ->
|
||||
Format.fprintf fmt "(%a => %a)" pp f1 pp f2
|
||||
| _ -> assert false
|
||||
and pp_list sep fmt = function
|
||||
| [] -> ()
|
||||
| [f] -> pp fmt f
|
||||
| f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l
|
||||
|
||||
let make comb l = Comb (comb, l)
|
||||
|
||||
let make_atom p = Lit p
|
||||
|
||||
let f_true = True
|
||||
let f_false = Comb(Not, [True])
|
||||
|
||||
let rec flatten comb acc = function
|
||||
| [] -> acc
|
||||
| (Comb (c, l)) :: r when c = comb ->
|
||||
flatten comb (List.rev_append l acc) r
|
||||
| a :: r ->
|
||||
flatten comb (a :: acc) r
|
||||
|
||||
let rec opt_rev_map f acc = function
|
||||
| [] -> acc
|
||||
| a :: r -> begin match f a with
|
||||
| None -> opt_rev_map f acc r
|
||||
| Some b -> opt_rev_map f (b :: acc) r
|
||||
end
|
||||
|
||||
let remove_true l =
|
||||
let aux = function
|
||||
| True -> None
|
||||
| f -> Some f
|
||||
in
|
||||
opt_rev_map aux [] l
|
||||
|
||||
let remove_false l =
|
||||
let aux = function
|
||||
| Comb(Not, [True]) -> None
|
||||
| f -> Some f
|
||||
in
|
||||
opt_rev_map aux [] l
|
||||
|
||||
|
||||
let make_not f = make Not [f]
|
||||
|
||||
let make_and l =
|
||||
let l' = remove_true (flatten And [] l) in
|
||||
if List.exists ((=) f_false) l' then
|
||||
f_false
|
||||
else
|
||||
make And l'
|
||||
|
||||
let make_or l =
|
||||
let l' = remove_false (flatten Or [] l) in
|
||||
if List.exists ((=) f_true) l' then
|
||||
f_true
|
||||
else match l' with
|
||||
| [] -> raise Empty_Or
|
||||
| [a] -> a
|
||||
| _ -> Comb (Or, l')
|
||||
|
||||
let make_imply f1 f2 = make Imp [f1; f2]
|
||||
let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1]
|
||||
let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ];
|
||||
make_and [ f1; make_not f2 ] ]
|
||||
|
||||
(* simplify formula *)
|
||||
let (%%) f g x = f (g x)
|
||||
|
||||
let rec sform f k = match f with
|
||||
| True | Comb (Not, [True]) -> k f
|
||||
| Comb (Not, [Lit a]) -> k (Lit (F.neg a))
|
||||
| Comb (Not, [Comb (Not, [f])]) -> sform f k
|
||||
| Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and)
|
||||
| Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or)
|
||||
| Comb (And, l) -> sform_list [] l (k %% make_and)
|
||||
| Comb (Or, l) -> sform_list [] l (k %% make_or)
|
||||
| Comb (Imp, [f1; f2]) ->
|
||||
sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2'])))
|
||||
| Comb (Not, [Comb (Imp, [f1; f2])]) ->
|
||||
sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2'])))
|
||||
| Comb ((Imp | Not), _) -> assert false
|
||||
| Lit _ -> k f
|
||||
and sform_list acc l k = match l with
|
||||
| [] -> k acc
|
||||
| f :: tail ->
|
||||
sform f (fun f' -> sform_list (f'::acc) tail k)
|
||||
and sform_list_not acc l k = match l with
|
||||
| [] -> k acc
|
||||
| f :: tail ->
|
||||
sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
|
||||
|
||||
let ( @@ ) l1 l2 = List.rev_append l1 l2
|
||||
(* let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) *)
|
||||
|
||||
(*
|
||||
let distrib l_and l_or =
|
||||
let l =
|
||||
if l_or = [] then l_and
|
||||
else
|
||||
List.rev_map
|
||||
(fun x ->
|
||||
match x with
|
||||
| Lit _ -> Comb (Or, x::l_or)
|
||||
| Comb (Or, l) -> Comb (Or, l @@ l_or)
|
||||
| _ -> assert false
|
||||
) l_and
|
||||
in
|
||||
Comb (And, l)
|
||||
|
||||
let rec flatten_or = function
|
||||
| [] -> []
|
||||
| Comb (Or, l)::r -> l @@ (flatten_or r)
|
||||
| Lit a :: r -> (Lit a)::(flatten_or r)
|
||||
| _ -> assert false
|
||||
|
||||
let rec flatten_and = function
|
||||
| [] -> []
|
||||
| Comb (And, l)::r -> l @@ (flatten_and r)
|
||||
| a :: r -> a::(flatten_and r)
|
||||
|
||||
|
||||
let rec cnf f =
|
||||
match f with
|
||||
| Comb (Or, l) ->
|
||||
begin
|
||||
let l = List.rev_map cnf l in
|
||||
let l_and, l_or =
|
||||
List.partition (function Comb(And,_) -> true | _ -> false) l in
|
||||
match l_and with
|
||||
| [ Comb(And, l_conj) ] ->
|
||||
let u = flatten_or l_or in
|
||||
distrib l_conj u
|
||||
|
||||
| Comb(And, l_conj) :: r ->
|
||||
let u = flatten_or l_or in
|
||||
cnf (Comb(Or, (distrib l_conj u)::r))
|
||||
|
||||
| _ ->
|
||||
begin
|
||||
match flatten_or l_or with
|
||||
| [] -> assert false
|
||||
| [r] -> r
|
||||
| v -> Comb (Or, v)
|
||||
end
|
||||
end
|
||||
| Comb (And, l) ->
|
||||
Comb (And, List.rev_map cnf l)
|
||||
| f -> f
|
||||
|
||||
let rec mk_cnf = function
|
||||
| Comb (And, l) ->
|
||||
List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l
|
||||
|
||||
| Comb (Or, [f1;f2]) ->
|
||||
let ll1 = mk_cnf f1 in
|
||||
let ll2 = mk_cnf f2 in
|
||||
List.fold_left
|
||||
(fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
|
||||
|
||||
| Comb (Or, f1 :: l) ->
|
||||
let ll1 = mk_cnf f1 in
|
||||
let ll2 = mk_cnf (Comb (Or, l)) in
|
||||
List.fold_left
|
||||
(fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
|
||||
|
||||
| Lit a -> [[a]]
|
||||
| Comb (Not, [Lit a]) -> [[F.neg a]]
|
||||
| _ -> assert false
|
||||
|
||||
|
||||
let rec unfold mono f =
|
||||
match f with
|
||||
| Lit a -> a::mono
|
||||
| Comb (Not, [Lit a]) ->
|
||||
(F.neg a)::mono
|
||||
| Comb (Or, l) ->
|
||||
List.fold_left unfold mono l
|
||||
| _ -> assert false
|
||||
|
||||
let rec init monos f =
|
||||
match f with
|
||||
| Comb (And, l) ->
|
||||
List.fold_left init monos l
|
||||
| f -> (unfold [] f)::monos
|
||||
|
||||
let make_cnf f =
|
||||
let sfnc = cnf (sform f) in
|
||||
init [] sfnc
|
||||
*)
|
||||
|
||||
let mk_proxy = F.fresh
|
||||
|
||||
let acc_or = ref []
|
||||
let acc_and = ref []
|
||||
|
||||
(* build a clause by flattening (if sub-formulas have the
|
||||
same combinator) and proxy-ing sub-formulas that have the
|
||||
opposite operator. *)
|
||||
let rec cnf f = match f with
|
||||
| Lit a -> None, [a]
|
||||
| Comb (Not, [Lit a]) -> None, [F.neg a]
|
||||
|
||||
| Comb (And, l) ->
|
||||
List.fold_left
|
||||
(fun (_, acc) f ->
|
||||
match cnf f with
|
||||
| _, [] -> assert false
|
||||
| _cmb, [a] -> Some And, a :: acc
|
||||
| Some And, l ->
|
||||
Some And, l @@ acc
|
||||
(* let proxy = mk_proxy () in *)
|
||||
(* acc_and := (proxy, l) :: !acc_and; *)
|
||||
(* proxy :: acc *)
|
||||
| Some Or, l ->
|
||||
let proxy = mk_proxy () in
|
||||
acc_or := (proxy, l) :: !acc_or;
|
||||
Some And, proxy :: acc
|
||||
| None, l -> Some And, l @@ acc
|
||||
| _ -> assert false
|
||||
) (None, []) l
|
||||
|
||||
| Comb (Or, l) ->
|
||||
List.fold_left
|
||||
(fun (_, acc) f ->
|
||||
match cnf f with
|
||||
| _, [] -> assert false
|
||||
| _cmb, [a] -> Some Or, a :: acc
|
||||
| Some Or, l ->
|
||||
Some Or, l @@ acc
|
||||
(* let proxy = mk_proxy () in *)
|
||||
(* acc_or := (proxy, l) :: !acc_or; *)
|
||||
(* proxy :: acc *)
|
||||
| Some And, l ->
|
||||
let proxy = mk_proxy () in
|
||||
acc_and := (proxy, l) :: !acc_and;
|
||||
Some Or, proxy :: acc
|
||||
| None, l -> Some Or, l @@ acc
|
||||
| _ -> assert false
|
||||
) (None, []) l
|
||||
| _ -> assert false
|
||||
|
||||
let cnf f =
|
||||
let acc = match f with
|
||||
| True -> []
|
||||
| Comb(Not, [True]) -> [[]]
|
||||
| Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l
|
||||
| _ -> [snd (cnf f)]
|
||||
in
|
||||
let proxies = ref [] in
|
||||
(* encore clauses that make proxies in !acc_and equivalent to
|
||||
their clause *)
|
||||
let acc =
|
||||
List.fold_left
|
||||
(fun acc (p,l) ->
|
||||
proxies := p :: !proxies;
|
||||
let np = F.neg p in
|
||||
(* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
|
||||
also add clauses [p => l1], [p => l2], etc. *)
|
||||
let cl, acc =
|
||||
List.fold_left
|
||||
(fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc)
|
||||
([p],acc) l in
|
||||
cl :: acc
|
||||
) acc !acc_and
|
||||
in
|
||||
(* encore clauses that make proxies in !acc_or equivalent to
|
||||
their clause *)
|
||||
let acc =
|
||||
List.fold_left
|
||||
(fun acc (p,l) ->
|
||||
proxies := p :: !proxies;
|
||||
(* add clause [p => l1 | l2 | ... | ln], and add clauses
|
||||
[l1 => p], [l2 => p], etc. *)
|
||||
let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc)
|
||||
acc l in
|
||||
(F.neg p :: l) :: acc
|
||||
) acc !acc_or
|
||||
in
|
||||
acc
|
||||
|
||||
let make_cnf f =
|
||||
acc_or := [];
|
||||
acc_and := [];
|
||||
cnf (sform f (fun f' -> f'))
|
||||
|
||||
(* Naive CNF XXX remove???
|
||||
let make_cnf f = mk_cnf (sform f)
|
||||
*)
|
||||
end
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
(*
|
||||
MSAT is free software, using the Apache license, see file LICENSE
|
||||
Copyright 2014 Guillaume Bury
|
||||
Copyright 2014 Simon Cruanes
|
||||
*)
|
||||
|
||||
(** Tseitin CNF conversion
|
||||
|
||||
This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
|
||||
the ability to transform an arbitrary boolean formula into an equi-satisfiable
|
||||
CNF, that can then be fed to a SAT/SMT/McSat solver.
|
||||
*)
|
||||
|
||||
module type Arg = Tseitin_intf.Arg
|
||||
(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
|
||||
|
||||
module type S = Tseitin_intf.S
|
||||
(** The exposed interface of Tseitin's CNF conversion. *)
|
||||
|
||||
module Make : functor (F : Arg) -> S with type atom = F.t
|
||||
(** This functor provides an implementation of Tseitin's CNF conversion. *)
|
||||
|
||||
|
|
@ -1,85 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Alt-Ergo Zero *)
|
||||
(* *)
|
||||
(* Sylvain Conchon and Alain Mebsout *)
|
||||
(* Universite Paris-Sud 11 *)
|
||||
(* *)
|
||||
(* Copyright 2011. This file is distributed under the terms of the *)
|
||||
(* Apache Software License version 2.0 *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
(** Interfaces for Tseitin's CNF conversion *)
|
||||
|
||||
module type Arg = sig
|
||||
(** Formulas
|
||||
|
||||
This defines what is needed of formulas in order to implement
|
||||
Tseitin's CNF conversion.
|
||||
*)
|
||||
|
||||
type t
|
||||
(** Type of atomic formulas. *)
|
||||
|
||||
val neg : t -> t
|
||||
(** Negation of atomic formulas. *)
|
||||
|
||||
val fresh : unit -> t
|
||||
(** Generate fresh formulas (that are different from any other). *)
|
||||
|
||||
val pp : Format.formatter -> t -> unit
|
||||
(** Print the given formula. *)
|
||||
|
||||
end
|
||||
|
||||
module type S = sig
|
||||
(** CNF conversion
|
||||
|
||||
This modules converts arbitrary boolean formulas into CNF.
|
||||
*)
|
||||
|
||||
type atom
|
||||
(** The type of atomic formulas. *)
|
||||
|
||||
type t
|
||||
(** The type of arbitrary boolean formulas. Arbitrary boolean formulas
|
||||
can be built using functions in this module, and then converted
|
||||
to a CNF, which is a list of clauses that only use atomic formulas. *)
|
||||
|
||||
val f_true : t
|
||||
(** The [true] formula, i.e a formula that is always satisfied. *)
|
||||
|
||||
val f_false : t
|
||||
(** The [false] formula, i.e a formula that cannot be satisfied. *)
|
||||
|
||||
val make_atom : atom -> t
|
||||
(** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
|
||||
|
||||
val make_not : t -> t
|
||||
(** Creates the negation of a boolean formula. *)
|
||||
|
||||
val make_and : t list -> t
|
||||
(** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
|
||||
|
||||
val make_or : t list -> t
|
||||
(** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
|
||||
|
||||
val make_xor : t -> t -> t
|
||||
(** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
|
||||
|
||||
val make_imply : t -> t -> t
|
||||
(** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
|
||||
|
||||
val make_equiv : t -> t -> t
|
||||
(** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
|
||||
|
||||
val make_cnf : t -> atom list list
|
||||
(** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
|
||||
list (which is a conjunction) of lists (which are disjunctions) of
|
||||
atomic formulas. *)
|
||||
|
||||
val pp : Format.formatter -> t -> unit
|
||||
(** [print fmt f] prints the formula on the formatter [fmt].*)
|
||||
|
||||
end
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
|
||||
(library
|
||||
(name msat_tseitin)
|
||||
(public_name msat.tseitin)
|
||||
(synopsis "Tseitin transformation for msat")
|
||||
(libraries msat)
|
||||
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
|
||||
(ocamlopt_flags :standard -O3 -bin-annot
|
||||
-unbox-closures -unbox-closures-factor 20)
|
||||
)
|
||||
|
||||
Loading…
Add table
Reference in a new issue