diff --git a/.github/workflows/fmt.yml b/.github/workflows/fmt.yml new file mode 100644 index 00000000..f24b67e2 --- /dev/null +++ b/.github/workflows/fmt.yml @@ -0,0 +1,29 @@ + +name: format + +on: + push: + branches: + - main + pull_request: + +jobs: + format: + name: format + strategy: + matrix: + ocaml-compiler: + - '5.3' + runs-on: 'ubuntu-latest' + steps: + - uses: actions/checkout@main + - name: Use OCaml ${{ matrix.ocaml-compiler }} + uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: ${{ matrix.ocaml-compiler }} + dune-cache: true + allow-prerelease-opam: true + + - run: opam install ocamlformat.0.27.0 + - run: opam exec -- make format-check + diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 00000000..f33f722c --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,15 @@ +version = 0.27.0 +profile=conventional +margin=80 +if-then-else=k-r +parens-ite=true +parens-tuple=multi-line-only +sequence-style=terminator +type-decl=sparse +break-cases=toplevel +cases-exp-indent=2 +field-space=tight-decl +leading-nested-match-parens=true +module-item-spacing=compact +quiet=true +ocaml-version=4.08.0 diff --git a/Makefile b/Makefile index c8f09a05..327cdbfb 100644 --- a/Makefile +++ b/Makefile @@ -31,15 +31,11 @@ doc: reinstall: | uninstall install -ocp-indent: - @which ocp-indent > /dev/null || { \ - echo 'ocp-indent not found; please run `opam install ocp-indent`'; \ - exit 1 ; \ - } - -reindent: ocp-indent - @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " - @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i +format: + @dune build $(DUNE_OPTS) @fmt --auto-promote + +format-check: + @dune build $(DUNE_OPTS) @fmt --display=quiet WATCH=all watch: diff --git a/README.md b/README.md index 8cf81dcc..5de36c65 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# MSAT [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT) +# MSAT [![Build and Test](https://github.com/Gbury/mSAT/actions/workflows/main.yml/badge.svg)](https://github.com/Gbury/mSAT/actions/workflows/main.yml) MSAT is an OCaml library that features a modular SAT-solver and some extensions (including SMT), derived from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero). diff --git a/dune b/dune index 24ee9b8e..b335d71f 100644 --- a/dune +++ b/dune @@ -1,27 +1,32 @@ - (rule (alias runtest) - (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src)) + (deps + README.md + src/core/msat.cma + src/sat/msat_sat.cma + (source_tree src)) (locks test) (package msat) - (action (progn - (run ocaml-mdx test README.md) - (diff? README.md README.md.corrected)))) + (action + (progn + (run ocaml-mdx test README.md) + (diff? README.md README.md.corrected)))) (env - (_ - (flags - :standard - -warn-error -a - -w +a-4-42-44-48-50-58-32-60-70@8 - -color always - -safe-string - ) - (ocamlopt_flags - :standard - -O3 - -bin-annot - -unbox-closures -unbox-closures-factor 20 - ) - ) -) + (_ + (flags + :standard + -warn-error + -a + -w + +a-4-42-44-48-50-58-32-60-70@8 + -color + always + -safe-string) + (ocamlopt_flags + :standard + -O3 + -bin-annot + -unbox-closures + -unbox-closures-factor + 20))) diff --git a/dune-project b/dune-project index 37f995d6..0a5fc997 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,39 @@ (lang dune 3.0) + +(generate_opam_files true) + +(package + (name msat) + (synopsis "Library containing a SAT solver that can be parametrized by a theory") + (version "0.9.1") + (license "Apache-2.0") + (authors "Simon Cruanes" "Guillaume Bury") + (maintainers "guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org") + (tags ("sat" "smt" "cdcl" "functor")) + (homepage "https://github.com/Gbury/mSAT") + (source (github Gbury/mSAT)) + (bug_reports "https://github.com/Gbury/mSAT/issues/") + (depends + (ocaml (>= 4.03)) + (dune (>= 3.0)) + (iter (>= 1.2)) + (containers (and :with-test (>= 2.8.1) (< 4.0))) + (mdx :with-test))) + +(package + (name msat-bin) + (synopsis "SAT solver binary based on the msat library") + (version "0.9.1") + (license "Apache-2.0") + (authors "Simon Cruanes" "Guillaume Bury") + (maintainers "guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org") + (tags ("sat")) + (homepage "https://github.com/Gbury/mSAT") + (source (github Gbury/mSAT)) + (bug_reports "https://github.com/Gbury/mSAT/issues/") + (depends + (ocaml (>= 4.03)) + (dune (>= 3.0)) + (msat (= :version)) + (containers (and (>= 2.8.1) (< 4.0))) + camlzip)) diff --git a/msat-bin.opam b/msat-bin.opam index f1e072c0..35af49ae 100644 --- a/msat-bin.opam +++ b/msat-bin.opam @@ -1,23 +1,33 @@ +# This file is generated by dune, edit dune-project instead opam-version: "2.0" -name: "msat-bin" -synopsis: "SAT solver binary based on the msat library" -license: "Apache-2.0" version: "0.9.1" -author: ["Simon Cruanes" "Guillaume Bury"] +synopsis: "SAT solver binary based on the msat library" maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - #["dune" "runtest" "-p" name "-j" jobs] {with-test} -] +authors: ["Simon Cruanes" "Guillaume Bury"] +license: "Apache-2.0" +tags: ["sat"] +homepage: "https://github.com/Gbury/mSAT" +bug-reports: "https://github.com/Gbury/mSAT/issues/" depends: [ - "ocaml" { >= "4.03" } - "dune" { >= "3.0" } - "msat" { = version } - "containers" { >= "2.8.1" & < "4.0" } + "ocaml" {>= "4.03"} + "dune" {>= "3.0" & >= "3.0"} + "msat" {= version} + "containers" {>= "2.8.1" & < "4.0"} "camlzip" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] ] -tags: [ "sat" ] -homepage: "https://github.com/Gbury/mSAT" dev-repo: "git+https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" - diff --git a/msat.opam b/msat.opam index 6c35acd4..adfcd094 100644 --- a/msat.opam +++ b/msat.opam @@ -1,24 +1,34 @@ +# This file is generated by dune, edit dune-project instead opam-version: "2.0" -name: "msat" -synopsis: "Library containing a SAT solver that can be parametrized by a theory" -license: "Apache-2.0" version: "0.9.1" -author: ["Simon Cruanes" "Guillaume Bury"] +synopsis: + "Library containing a SAT solver that can be parametrized by a theory" maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - ["dune" "build" "@doc" "-p" name] {with-doc} - ["dune" "runtest" "-p" name] {with-test} -] +authors: ["Simon Cruanes" "Guillaume Bury"] +license: "Apache-2.0" +tags: ["sat" "smt" "cdcl" "functor"] +homepage: "https://github.com/Gbury/mSAT" +bug-reports: "https://github.com/Gbury/mSAT/issues/" depends: [ - "ocaml" { >= "4.03" } - "dune" { >= "3.0" } - "iter" { >= "1.2" } - "containers" {with-test & >= "2.8.1" & < "4.0" } + "ocaml" {>= "4.03"} + "dune" {>= "3.0" & >= "3.0"} + "iter" {>= "1.2"} + "containers" {with-test & >= "2.8.1" & < "4.0"} "mdx" {with-test} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] ] -tags: [ "sat" "smt" "cdcl" "functor" ] -homepage: "https://github.com/Gbury/mSAT" dev-repo: "git+https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" - diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml index 29900a0c..2a616141 100644 --- a/src/backend/Backend_intf.ml +++ b/src/backend/Backend_intf.ml @@ -6,22 +6,18 @@ Copyright 2014 Simon Cruanes (** Backend interface - This modules defines the interface of the modules providing - export of proofs. -*) + This modules defines the interface of the modules providing export of + proofs. *) module type S = sig (** Proof exporting - Currently, exporting a proof means printing it into a file - according to the conventions of a given format. - *) + Currently, exporting a proof means printing it into a file according to + the conventions of a given format. *) type t (** The type of proofs. *) val pp : Format.formatter -> t -> unit (** A function for printing proofs in the desired format. *) - end - diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index ffb736fd..fb002d4f 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -6,7 +6,6 @@ Copyright 2015 Guillaume Bury module type S = Backend_intf.S module type Arg = sig - type hyp type lemma type assumption @@ -14,16 +13,19 @@ module type Arg = sig val prove_hyp : Format.formatter -> string -> hyp -> unit val prove_lemma : Format.formatter -> string -> lemma -> unit val prove_assumption : Format.formatter -> string -> assumption -> unit - end -module Make(S : Msat.S)(A : Arg with type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) = struct - +module Make + (S : Msat.S) + (A : + Arg + with type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) = +struct module Atom = S.Atom module Clause = S.Clause - module M = Map.Make(S.Atom) + module M = Map.Make (S.Atom) module C_tbl = S.Clause.Tbl module P = S.Proof @@ -31,11 +33,12 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause let clause_map c = let rec aux acc a i = - if i >= Array.length a then acc - else begin + if i >= Array.length a then + acc + else ( let name = Format.sprintf "A%d" i in aux (M.add a.(i) name acc) a (i + 1) - end + ) in aux M.empty (Clause.atoms c) 0 @@ -44,48 +47,50 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause Array.iter aux (Clause.atoms clause) let elim_duplicate fmt goal hyp _ = - (** Printing info comment in coq *) - Format.fprintf fmt - "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n" + (* Printing info comment in coq *) + Format.fprintf fmt "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n" (name goal) (name hyp); - (** Prove the goal: intro the atoms, then use them with the hyp *) + (* Prove the goal: intro the atoms, then use them with the hyp *) let m = clause_map goal in Format.fprintf fmt "pose proof @[(fun %a=>@ %s%a) as %s@].@\n" - (clause_iter m "%s@ ") goal (name hyp) - (clause_iter m "@ %s") hyp (name goal) + (clause_iter m "%s@ ") goal (name hyp) (clause_iter m "@ %s") hyp + (name goal) let resolution_aux m a h1 h2 fmt () = Format.fprintf fmt "%s%a" (name h1) - (fun fmt -> Array.iter (fun b -> - if b == a then begin - Format.fprintf fmt "@ (fun p =>@ %s%a)" - (name h2) (fun fmt -> (Array.iter (fun c -> - if Atom.equal c (Atom.neg a) then - Format.fprintf fmt "@ (fun np => np p)" - else - Format.fprintf fmt "@ %s" (M.find c m))) - ) (Clause.atoms h2) - end else - Format.fprintf fmt "@ %s" (M.find b m) - )) (Clause.atoms h1) + (fun fmt -> + Array.iter (fun b -> + if b == a then + Format.fprintf fmt "@ (fun p =>@ %s%a)" (name h2) + (fun fmt -> + Array.iter (fun c -> + if Atom.equal c (Atom.neg a) then + Format.fprintf fmt "@ (fun np => np p)" + else + Format.fprintf fmt "@ %s" (M.find c m))) + (Clause.atoms h2) + else + Format.fprintf fmt "@ %s" (M.find b m))) + (Clause.atoms h1) let resolution fmt goal hyp1 hyp2 atom = let a = Atom.abs atom in let h1, h2 = - if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2 + if Array.exists (Atom.equal a) (Clause.atoms hyp1) then + hyp1, hyp2 else ( assert (Array.exists (Atom.equal a) (Clause.atoms hyp2)); hyp2, hyp1 ) in - (** Print some debug info *) - Format.fprintf fmt - "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n" + (* Print some debug info *) + Format.fprintf fmt "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n" (name goal) (name h1) (name h2); - (** Prove the goal: intro the axioms, then perform resolution *) + (* Prove the goal: intro the axioms, then perform resolution *) if Array.length (Clause.atoms goal) = 0 then ( let m = M.empty in - Format.fprintf fmt "exact @[(%a)@].@\n" (resolution_aux m a h1 h2) (); + Format.fprintf fmt "exact @[(%a)@].@\n" (resolution_aux m a h1 h2) + (); false ) else ( let m = clause_map goal in @@ -105,40 +110,33 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause let () = C_tbl.add h c i in i <= 0 - let clear fmt c = - Format.fprintf fmt "clear %s." (name c) + let clear fmt c = Format.fprintf fmt "clear %s." (name c) let rec clean_aux fmt = function | [] -> () - | [x] -> - Format.fprintf fmt "%a@\n" clear x - | x :: ((_ :: _) as r) -> - Format.fprintf fmt "%a@ %a" clear x clean_aux r + | [ x ] -> Format.fprintf fmt "%a@\n" clear x + | x :: (_ :: _ as r) -> Format.fprintf fmt "%a@ %a" clear x clean_aux r let clean h fmt l = match List.filter (decr_use h) l with | [] -> () - | l' -> - Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l' + | l' -> Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l' let prove_node t fmt node = let clause = node.P.conclusion in match node.P.step with - | P.Hypothesis _ -> - A.prove_hyp fmt (name clause) clause - | P.Assumption -> - A.prove_assumption fmt (name clause) clause - | P.Lemma _ -> - A.prove_lemma fmt (name clause) clause + | P.Hypothesis _ -> A.prove_hyp fmt (name clause) clause + | P.Assumption -> A.prove_assumption fmt (name clause) clause + | P.Lemma _ -> A.prove_lemma fmt (name clause) clause | P.Duplicate (p, l) -> let c = P.conclusion p in let () = elim_duplicate fmt clause c l in - clean t fmt [c] + clean t fmt [ c ] | P.Hyper_res hr -> - let (p1, p2, a) = P.res_of_hyper_res hr in + let p1, p2, a = P.res_of_hyper_res hr in let c1 = P.conclusion p1 in let c2 = P.conclusion p2 in - if resolution fmt clause c1 c2 a then clean t fmt [c1; c2] + if resolution fmt clause c1 c2 a then clean t fmt [ c1; c2 ] let count_uses p = let h = C_tbl.create 128 in @@ -152,42 +150,41 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause one goal to prove, i.e False. So each *) let pp fmt p = let h = count_uses p in - let aux () node = - Format.fprintf fmt "%a" (prove_node h) node - in + let aux () node = Format.fprintf fmt "%a" (prove_node h) node in Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n"; P.fold aux () p end - -module Simple(S : Msat.S) - (A : Arg with type hyp = S.formula list - and type lemma := S.lemma - and type assumption := S.formula) = - Make(S)(struct - module P = S.Proof - - (* Some helpers *) - let lit = S.Atom.formula - - let get_assumption c = - match S.Clause.atoms_l c with - | [ x ] -> x - | _ -> assert false - - let get_lemma c = - match P.expand (P.prove c) with - | {P.step=P.Lemma p; _} -> p - | _ -> assert false - - let prove_hyp fmt name c = - A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c)) - - let prove_lemma fmt name c = - A.prove_lemma fmt name (get_lemma c) - - let prove_assumption fmt name c = - A.prove_assumption fmt name (lit (get_assumption c)) - - end) - +module Simple + (S : Msat.S) + (A : + Arg + with type hyp = S.formula list + and type lemma := S.lemma + and type assumption := S.formula) = + Make + (S) + (struct + module P = S.Proof + + (* Some helpers *) + let lit = S.Atom.formula + + let get_assumption c = + match S.Clause.atoms_l c with + | [ x ] -> x + | _ -> assert false + + let get_lemma c = + match P.expand (P.prove c) with + | { P.step = P.Lemma p; _ } -> p + | _ -> assert false + + let prove_hyp fmt name c = + A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c)) + + let prove_lemma fmt name c = A.prove_lemma fmt name (get_lemma c) + + let prove_assumption fmt name c = + A.prove_assumption fmt name (lit (get_assumption c)) + end) diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli index 8d7e982d..90a355b3 100644 --- a/src/backend/Coq.mli +++ b/src/backend/Coq.mli @@ -5,9 +5,8 @@ Copyright 2015 Guillaume Bury (** Coq Backend - This module provides an easy way to produce coq scripts - corresponding to the resolution proofs output by the - sat solver. *) + This module provides an easy way to produce coq scripts corresponding to the + resolution proofs output by the sat solver. *) module type S = Backend_intf.S (** Interface for exporting proofs. *) @@ -17,30 +16,37 @@ module type Arg = sig type hyp type lemma + type assumption (** The types of hypotheses, lemmas, and assumptions *) val prove_hyp : Format.formatter -> string -> hyp -> unit val prove_lemma : Format.formatter -> string -> lemma -> unit + val prove_assumption : Format.formatter -> string -> assumption -> unit (** Proving function for hypotheses, lemmas and assumptions. - [prove_x fmt name x] should prove [x], and be such that after - executing it, [x] is among the coq hypotheses under the name [name]. - The hypothesis should be the encoding of the given clause, i.e - for a clause [a \/ not b \/ c], the proved hypothesis should be: - [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the - one in the atoms array of the clause. *) - + [prove_x fmt name x] should prove [x], and be such that after executing + it, [x] is among the coq hypotheses under the name [name]. The hypothesis + should be the encoding of the given clause, i.e for a clause + [a \/ not b \/ c], the proved hypothesis should be: + [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the one in the + atoms array of the clause. *) end -module Make(S : Msat.S)(_ : Arg with type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) : S with type t := S.proof (** Base functor to output Coq proofs *) +module Make + (S : Msat.S) + (_ : + Arg + with type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) : S with type t := S.proof - -module Simple(S : Msat.S)(_ : Arg with type hyp = S.formula list - and type lemma := S.lemma - and type assumption := S.formula) : S with type t := S.proof (** Simple functor to output Coq proofs *) - +module Simple + (S : Msat.S) + (_ : + Arg + with type hyp = S.formula list + and type lemma := S.lemma + and type assumption := S.formula) : S with type t := S.proof diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index 7f8526eb..1d0db347 100644 --- a/src/backend/Dedukti.ml +++ b/src/backend/Dedukti.ml @@ -6,7 +6,6 @@ Copyright 2015 Guillaume Bury module type S = Backend_intf.S module type Arg = sig - type proof type lemma type formula @@ -16,14 +15,18 @@ module type Arg = sig val context : Format.formatter -> proof -> unit end -module Make(S : Msat.S)(A : Arg with type formula := S.formula - and type lemma := S.lemma - and type proof := S.proof) = struct +module Make + (S : Msat.S) + (A : + Arg + with type formula := S.formula + and type lemma := S.lemma + and type proof := S.proof) = +struct module P = S.Proof let pp_nl fmt = Format.fprintf fmt "@\n" let fprintf fmt format = Format.kfprintf pp_nl fmt format - let _clause_name = S.Clause.name let _pp_clause fmt c = @@ -37,7 +40,11 @@ module Make(S : Msat.S)(A : Arg with type formula := S.formula S.Atom.formula (S.Atom.neg a), false in fprintf fmt "%s _b %a ->@ %a" - (if pos then "_pos" else "_neg") A.pp f aux r + (if pos then + "_pos" + else + "_neg") + A.pp f aux r in fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c) @@ -57,6 +64,4 @@ module Make(S : Msat.S)(A : Arg with type formula := S.formula fprintf fmt "(; Dedukti file automatically generated by mSAT ;)"; context fmt p; () - end - diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli index c1563e5f..1f2c43c5 100644 --- a/src/backend/Dedukti.mli +++ b/src/backend/Dedukti.mli @@ -6,13 +6,11 @@ Copyright 2014 Simon Cruanes (** Deduki backend for proofs - Work in progress... -*) + Work in progress... *) module type S = Backend_intf.S module type Arg = sig - type lemma type proof type formula @@ -22,11 +20,12 @@ module type Arg = sig val context : Format.formatter -> proof -> unit end -module Make : - functor(S : Msat.S) -> - functor(_ : Arg - with type formula := S.formula - and type lemma := S.lemma - and type proof := S.proof) -> - S with type t := S.proof -(** Functor to generate a backend to output proofs for the dedukti type checker. *) +(** Functor to generate a backend to output proofs for the dedukti type checker. +*) +module Make : functor + (S : Msat.S) + (_ : Arg + with type formula := S.formula + and type lemma := S.lemma + and type proof := S.proof) + -> S with type t := S.proof diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 9097cc45..2501f266 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -4,55 +4,67 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -(** Output interface for the backend *) module type S = Backend_intf.S +(** Output interface for the backend *) (** Input module for the backend *) module type Arg = sig - type atom (* Type of atoms *) type hyp type lemma + type assumption (** Types for hypotheses, lemmas, and assumptions. *) val print_atom : Format.formatter -> atom -> unit (** Printing function for atoms *) - val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Functions to return information about hypotheses and lemmas *) + val hyp_info : + hyp -> string * string option * (Format.formatter -> unit -> unit) list + val lemma_info : + lemma -> string * string option * (Format.formatter -> unit -> unit) list + + val assumption_info : + assumption -> + string * string option * (Format.formatter -> unit -> unit) list + (** Functions to return information about hypotheses and lemmas *) end -module Default(S : Msat.S) = struct +module Default (S : Msat.S) = struct module Atom = S.Atom module Clause = S.Clause let print_atom = Atom.pp let hyp_info c = - "hypothesis", Some "LIGHTBLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] + ( "hypothesis", + Some "LIGHTBLUE", + [ (fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c) ] ) let lemma_info c = - "lemma", Some "BLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] + ( "lemma", + Some "BLUE", + [ (fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c) ] ) let assumption_info c = - "assumption", Some "PURPLE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] - + ( "assumption", + Some "PURPLE", + [ (fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c) ] ) end (** Functor to provide dot printing *) -module Make(S : Msat.S)(A : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) = struct +module Make + (S : Msat.S) + (A : + Arg + with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) = +struct module Atom = S.Atom module Clause = S.Clause module P = S.Proof @@ -66,38 +78,39 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom let v = Clause.atoms c in if Array.length v = 0 then Format.fprintf fmt "⊥" - else + else ( let n = Array.length v in for i = 0 to n - 1 do Format.fprintf fmt "%a" A.print_atom v.(i); - if i < n - 1 then - Format.fprintf fmt ", " + if i < n - 1 then Format.fprintf fmt ", " done + ) - let print_edge fmt i j = - Format.fprintf fmt "%s -> %s;@\n" j i + let print_edge fmt i j = Format.fprintf fmt "%s -> %s;@\n" j i let print_edges fmt n = match P.(n.step) with - | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *) - | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} -> + | P.Hyper_res { P.hr_steps = []; _ } -> + assert false (* NOTE: should never happen *) + | P.Hyper_res { P.hr_init; hr_steps = (_, p0) :: _ as l } -> print_edge fmt (res_np_id n p0) (proof_id hr_init); - List.iter - (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2)) - l; + List.iter (fun (_, p2) -> print_edge fmt (res_np_id n p2) (proof_id p2)) l | _ -> () let table_options fmt color = - Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color + Format.fprintf fmt + "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color let table fmt (c, rule, color, l) = Format.fprintf fmt "%a" print_clause c; match l with | [] -> - Format.fprintf fmt "%s" color rule + Format.fprintf fmt "%s" + color rule | f :: r -> - Format.fprintf fmt "%s%a" - color (List.length l) rule f (); + Format.fprintf fmt + "%s%a" color + (List.length l) rule f (); List.iter (fun f -> Format.fprintf fmt "%a" f ()) r let print_dot_node fmt id color c rule rule_color l = @@ -114,28 +127,43 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom (* Leafs of the proof tree *) | P.Hypothesis _ -> let rule, color, l = A.hyp_info P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in + let color = + match color with + | None -> "LIGHTBLUE" + | Some c -> c + in print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l | P.Assumption -> let rule, color, l = A.assumption_info P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in + let color = + match color with + | None -> "LIGHTBLUE" + | Some c -> c + in print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l | P.Lemma _ -> let rule, color, l = A.lemma_info P.(n.conclusion) in - let color = match color with None -> "YELLOW" | Some c -> c in + let color = + match color with + | None -> "YELLOW" + | Some c -> c + in print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l - (* Tree nodes *) | P.Duplicate (p, l) -> - print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY" - ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: - List.map (ttify A.print_atom) l); + print_dot_node fmt (node_id n) "GREY" + P.(n.conclusion) + "Duplicate" "GREY" + ((fun fmt () -> Format.fprintf fmt "%s" (node_id n)) + :: List.map (ttify A.print_atom) l); print_edge fmt (node_id n) (node_id (P.expand p)) - | P.Hyper_res {P.hr_steps=l; _} -> - print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" - [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; + | P.Hyper_res { P.hr_steps = l; _ } -> + print_dot_node fmt (node_id n) "GREY" + P.(n.conclusion) + "Resolution" "GREY" + [ (fun fmt () -> Format.fprintf fmt "%s" (node_id n)) ]; List.iter - (fun (a,p2) -> + (fun (a, p2) -> print_dot_res_node fmt (res_np_id n p2) a; print_edge fmt (node_id n) (res_np_id n p2)) l @@ -148,44 +176,39 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom Format.fprintf fmt "digraph proof {@\n"; P.fold (fun () -> print_node fmt) () p; Format.fprintf fmt "}@." - end -module Simple(S : Msat.S) - (A : Arg with type atom := S.formula - and type hyp = S.formula list - and type lemma := S.lemma - and type assumption = S.formula) = - Make(S)(struct - module Atom = S.Atom - module Clause = S.Clause - module P = S.Proof - - (* Some helpers *) - let lit = Atom.formula - - let get_assumption c = - match S.Clause.atoms_l c with - | [ x ] -> x - | _ -> assert false - - let get_lemma c = - match P.expand (P.prove c) with - | {P.step=P.Lemma p;_} -> p - | _ -> assert false - - (* Actual functions *) - let print_atom fmt a = - A.print_atom fmt (lit a) - - let hyp_info c = - A.hyp_info (List.map lit (S.Clause.atoms_l c)) - - let lemma_info c = - A.lemma_info (get_lemma c) - - let assumption_info c = - A.assumption_info (lit (get_assumption c)) - - end) - +module Simple + (S : Msat.S) + (A : + Arg + with type atom := S.formula + and type hyp = S.formula list + and type lemma := S.lemma + and type assumption = S.formula) = + Make + (S) + (struct + module Atom = S.Atom + module Clause = S.Clause + module P = S.Proof + + (* Some helpers *) + let lit = Atom.formula + + let get_assumption c = + match S.Clause.atoms_l c with + | [ x ] -> x + | _ -> assert false + + let get_lemma c = + match P.expand (P.prove c) with + | { P.step = P.Lemma p; _ } -> p + | _ -> assert false + + (* Actual functions *) + let print_atom fmt a = A.print_atom fmt (lit a) + let hyp_info c = A.hyp_info (List.map lit (S.Clause.atoms_l c)) + let lemma_info c = A.lemma_info (get_lemma c) + let assumption_info c = A.assumption_info (lit (get_assumption c)) + end) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index a16b7507..a4926932 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -7,8 +7,8 @@ Copyright 2014 Simon Cruanes (** Dot backend for proofs This module provides functions to export proofs into the dot graph format. - Graphs in dot format can be used to generates images using the graphviz tool. -*) + Graphs in dot format can be used to generates images using the graphviz + tool. *) module type S = Backend_intf.S (** Interface for exporting proofs. *) @@ -16,55 +16,70 @@ module type S = Backend_intf.S module type Arg = sig (** Term printing for DOT - This module defines what functions are required in order to export - a proof to the DOT format. - *) + This module defines what functions are required in order to export a proof + to the DOT format. *) type atom (** The type of atomic formuals *) type hyp type lemma + type assumption (** The type of theory-specifi proofs (also called lemmas). *) val print_atom : Format.formatter -> atom -> unit - (** Print the contents of the given atomic formulas. - WARNING: this function should take care to escape and/or not output special - reserved characters for the dot format (such as quotes and so on). *) + (** Print the contents of the given atomic formulas. WARNING: this function + should take care to escape and/or not output special reserved characters + for the dot format (such as quotes and so on). *) - val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Generate some information about the leafs of the proof tree. Currently this backend - print each lemma/assumption/hypothesis as a single leaf of the proof tree. - These function should return a triplet [(rule, color, l)], such that: - - [rule] is a name for the proof (arbitrary, does not need to be unique, but - should rather be descriptive) - - [color] is a color name (optional) understood by DOT - - [l] is a list of printers that will be called to print some additional information - *) + val hyp_info : + hyp -> string * string option * (Format.formatter -> unit -> unit) list + val lemma_info : + lemma -> string * string option * (Format.formatter -> unit -> unit) list + + val assumption_info : + assumption -> + string * string option * (Format.formatter -> unit -> unit) list + (** Generate some information about the leafs of the proof tree. Currently + this backend print each lemma/assumption/hypothesis as a single leaf of + the proof tree. These function should return a triplet [(rule, color, l)], + such that: + - [rule] is a name for the proof (arbitrary, does not need to be unique, + but should rather be descriptive) + - [color] is a color name (optional) understood by DOT + - [l] is a list of printers that will be called to print some additional + information *) end -module Default(S : Msat.S) : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause (** Provides a reasonnable default to instantiate the [Make] functor, assuming the original printing functions are compatible with DOT html labels. *) +module Default (S : Msat.S) : + Arg + with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause -module Make(S : Msat.S)(_ : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. *) +module Make + (S : Msat.S) + (_ : + Arg + with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) : S with type t := S.proof -module Simple(S : Msat.S)(_ : Arg with type atom := S.formula - and type hyp = S.formula list - and type lemma := S.lemma - and type assumption = S.formula) : S with type t := S.proof -(** Functor for making a module to export proofs to the DOT format. - The substitution of the hyp type is non-destructive due to a restriction - of destructive substitutions on earlier versions of ocaml. *) - +(** Functor for making a module to export proofs to the DOT format. The + substitution of the hyp type is non-destructive due to a restriction of + destructive substitutions on earlier versions of ocaml. *) +module Simple + (S : Msat.S) + (_ : + Arg + with type atom := S.formula + and type hyp = S.formula list + and type lemma := S.lemma + and type assumption = S.formula) : S with type t := S.proof diff --git a/src/backend/dune b/src/backend/dune index 2aa79aca..5b330892 100644 --- a/src/backend/dune +++ b/src/backend/dune @@ -1,7 +1,5 @@ (library - (name msat_backend) - (public_name msat.backend) - (synopsis "proof backends for msat") - (libraries msat) - ) - + (name msat_backend) + (public_name msat.backend) + (synopsis "proof backends for msat") + (libraries msat)) diff --git a/src/backtrack/Backtrackable_ref.ml b/src/backtrack/Backtrackable_ref.ml index bc91cfd5..467f25a4 100644 --- a/src/backtrack/Backtrackable_ref.ml +++ b/src/backtrack/Backtrackable_ref.ml @@ -1,28 +1,28 @@ - type 'a t = { mutable cur: 'a; stack: 'a Vec.t; copy: ('a -> 'a) option; } -let create ?copy x: _ t = - {cur=x; stack=Vec.create(); copy} - +let create ?copy x : _ t = { cur = x; stack = Vec.create (); copy } let[@inline] get self = self.cur let[@inline] set self x = self.cur <- x let[@inline] update self f = self.cur <- f self.cur - let[@inline] n_levels self = Vec.size self.stack let[@inline] push_level self : unit = let x = self.cur in - let x = match self.copy with None -> x | Some f -> f x in + let x = + match self.copy with + | None -> x + | Some f -> f x + in Vec.push self.stack x let pop_levels self n : unit = - assert (n>=0); + assert (n >= 0); if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels"; - let i = Vec.size self.stack-n in + let i = Vec.size self.stack - n in let x = Vec.get self.stack i in self.cur <- x; Vec.shrink self.stack i; diff --git a/src/backtrack/Backtrackable_ref.mli b/src/backtrack/Backtrackable_ref.mli index a1755115..d81e4cf2 100644 --- a/src/backtrack/Backtrackable_ref.mli +++ b/src/backtrack/Backtrackable_ref.mli @@ -1,12 +1,12 @@ - (** {1 Backtrackable ref} *) type 'a t val create : ?copy:('a -> 'a) -> 'a -> 'a t (** Create a backtrackable reference holding the given value initially. - @param copy if provided, will be used to copy the value when [push_level] - is called. *) + @param copy + if provided, will be used to copy the value when [push_level] is called. +*) val set : 'a t -> 'a -> unit (** Set the reference's current content *) @@ -16,10 +16,10 @@ val get : 'a t -> 'a val update : 'a t -> ('a -> 'a) -> unit (** Update the reference's current content *) - + val push_level : _ t -> unit -(** Push a backtracking level, copying the current value on top of some - stack. The [copy] function will be used if it was provided in {!create}. *) +(** Push a backtracking level, copying the current value on top of some stack. + The [copy] function will be used if it was provided in {!create}. *) val n_levels : _ t -> int (** Number of saved values *) diff --git a/src/backtrack/Msat_backtrack.ml b/src/backtrack/Msat_backtrack.ml index 14857855..9c986c83 100644 --- a/src/backtrack/Msat_backtrack.ml +++ b/src/backtrack/Msat_backtrack.ml @@ -1,2 +1 @@ - module Ref = Backtrackable_ref diff --git a/src/backtrack/dune b/src/backtrack/dune index b666ce9c..a54e6a16 100644 --- a/src/backtrack/dune +++ b/src/backtrack/dune @@ -1,8 +1,6 @@ - (library - (name msat_backtrack) - (public_name msat.backtrack) - (libraries msat) - (flags :standard -open Msat) - (synopsis "backtrackable data structures for msat") - ) + (name msat_backtrack) + (public_name msat.backtrack) + (libraries msat) + (flags :standard -open Msat) + (synopsis "backtrackable data structures for msat")) diff --git a/src/core/Heap.ml b/src/core/Heap.ml index ed9884bb..88698486 100644 --- a/src/core/Heap.ml +++ b/src/core/Heap.ml @@ -1,20 +1,12 @@ - module type RANKED = Heap_intf.RANKED - module type S = Heap_intf.S -module Make(Elt : RANKED) = struct +module Make (Elt : RANKED) = struct type elt = Elt.t - - type t = { - heap : elt Vec.t; - } [@@unboxed] + type t = { heap: elt Vec.t } [@@unboxed] let _absent_index = -1 - - let create () = - { heap = Vec.create(); } - + let create () = { heap = Vec.create () } let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *) let[@inline] parent i = (i - 1) asr 1 (* (i-1) / 2 *) @@ -30,46 +22,47 @@ module Make(Elt : RANKED) = struct (* [elt] is above or at its expected position. Move it up the heap (towards high indices) to restore the heap property *) - let percolate_up {heap} (elt:Elt.t) : unit = + let percolate_up { heap } (elt : Elt.t) : unit = let pi = ref (parent (Elt.idx elt)) in let i = ref (Elt.idx elt) in while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do Vec.set heap !i (Vec.get heap !pi); Elt.set_idx (Vec.get heap !i) !i; - i := !pi; + i := !pi; pi := parent !i done; Vec.set heap !i elt; Elt.set_idx elt !i - let percolate_down {heap} (elt:Elt.t): unit = + let percolate_down { heap } (elt : Elt.t) : unit = let sz = Vec.size heap in let li = ref (left (Elt.idx elt)) in let ri = ref (right (Elt.idx elt)) in let i = ref (Elt.idx elt) in - begin - try - while !li < sz do - let child = - if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li) - then !ri - else !li - in - if not (Elt.cmp (Vec.get heap child) elt) then raise Exit; - Vec.set heap !i (Vec.get heap child); - Elt.set_idx (Vec.get heap !i) !i; - i := child; - li := left !i; - ri := right !i - done; - with Exit -> () - end; + (try + while !li < sz do + let child = + if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li) then + !ri + else + !li + in + if not (Elt.cmp (Vec.get heap child) elt) then raise Exit; + Vec.set heap !i (Vec.get heap child); + Elt.set_idx (Vec.get heap !i) !i; + i := child; + li := left !i; + ri := right !i + done + with Exit -> ()); Vec.set heap !i elt; Elt.set_idx elt !i let[@inline] in_heap x = Elt.idx x >= 0 - let[@inline] decrease s x = assert (in_heap x); percolate_up s x + let[@inline] decrease s x = + assert (in_heap x); + percolate_up s x (* let increase cmp s n = @@ -83,10 +76,9 @@ module Make(Elt : RANKED) = struct if filt (Vec.get s.heap i) then ( Vec.set s.heap !j (Vec.get s.heap i); Elt.set_idx (Vec.get s.heap i) !j; - incr j; - ) else ( - Elt.set_idx (Vec.get s.heap i) _absent_index; - ); + incr j + ) else + Elt.set_idx (Vec.get s.heap i) _absent_index done; Vec.shrink s.heap (lim - !j); for i = (lim / 2) - 1 downto 0 do @@ -94,10 +86,9 @@ module Make(Elt : RANKED) = struct done let size s = Vec.size s.heap - let is_empty s = Vec.is_empty s.heap - let clear {heap} = + let clear { heap } = Vec.iter (fun e -> Elt.set_idx e _absent_index) heap; Vec.clear heap; () @@ -106,7 +97,7 @@ module Make(Elt : RANKED) = struct if not (in_heap elt) then ( Elt.set_idx elt (Vec.size s.heap); Vec.push s.heap elt; - percolate_up s elt; + percolate_up s elt ) (* @@ -123,7 +114,7 @@ module Make(Elt : RANKED) = struct assert (heap_property cmp s) *) - let remove_min ({heap} as s) = + let remove_min ({ heap } as s) = match Vec.size heap with | 0 -> raise Not_found | 1 -> @@ -132,14 +123,13 @@ module Make(Elt : RANKED) = struct x | _ -> let x = Vec.get heap 0 in - let new_hd = Vec.pop heap in (* heap.last() *) + let new_hd = Vec.pop heap in + (* heap.last() *) Vec.set heap 0 new_hd; Elt.set_idx x _absent_index; Elt.set_idx new_hd 0; (* enforce heap property again *) - if Vec.size heap > 1 then ( - percolate_down s new_hd; - ); + if Vec.size heap > 1 then percolate_down s new_hd; x - -end [@@inline] +end +[@@inline] diff --git a/src/core/Heap.mli b/src/core/Heap.mli index a621885c..61778ab5 100644 --- a/src/core/Heap.mli +++ b/src/core/Heap.mli @@ -1,5 +1,4 @@ module type RANKED = Heap_intf.RANKED - module type S = Heap_intf.S -module Make(X : RANKED) : S with type elt = X.t +module Make (X : RANKED) : S with type elt = X.t diff --git a/src/core/Heap_intf.ml b/src/core/Heap_intf.ml index bee623e6..897f3153 100644 --- a/src/core/Heap_intf.ml +++ b/src/core/Heap_intf.ml @@ -1,8 +1,12 @@ - module type RANKED = sig type t - val idx: t -> int (** Index in heap. return -1 if never set *) - val set_idx : t -> int -> unit (** Update index in heap *) + + val idx : t -> int + (** Index in heap. return -1 if never set *) + + val set_idx : t -> int -> unit + (** Update index in heap *) + val cmp : t -> t -> bool end @@ -11,8 +15,8 @@ module type S = sig (** Type of elements *) type t - (** Heap of {!elt}, whose priority is increased or decreased - incrementally (see {!decrease} for instance) *) + (** Heap of {!elt}, whose priority is increased or decreased incrementally + (see {!decrease} for instance) *) val create : unit -> t (** Create a heap *) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 4a292dea..a84994b0 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -9,8 +9,7 @@ module type PLUGIN = sig (** Is this a mcsat plugin? *) val has_theory : bool - (** Is this a CDCL(T) plugin or mcsat plugin? - i.e does it have theories *) + (** Is this a CDCL(T) plugin or mcsat plugin? i.e does it have theories *) include Solver_intf.PLUGIN_MCSAT end @@ -18,8 +17,7 @@ end let invalid_argf fmt = Format.kasprintf (fun msg -> invalid_arg ("msat: " ^ msg)) fmt -module Make(Plugin : PLUGIN) -= struct +module Make (Plugin : PLUGIN) = struct module Term = Plugin.Term module Formula = Plugin.Formula module Value = Plugin.Value @@ -32,40 +30,40 @@ module Make(Plugin : PLUGIN) (* MCSAT literal *) type lit = { - lid : int; - term : term; - mutable l_level : int; + lid: int; + term: term; + mutable l_level: int; mutable l_idx: int; - mutable l_weight : float; - mutable assigned : value option; + mutable l_weight: float; + mutable assigned: value option; } type var = { - vid : int; - pa : atom; - na : atom; - mutable v_fields : int; - mutable v_level : int; - mutable v_idx: int; (** position in heap *) - mutable v_weight : float; (** Weight (for the heap), tracking activity *) + vid: int; + pa: atom; + na: atom; + mutable v_fields: int; + mutable v_level: int; + mutable v_idx: int; (** position in heap *) + mutable v_weight: float; (** Weight (for the heap), tracking activity *) mutable v_assignable: lit list option; - mutable reason : reason option; + mutable reason: reason option; } and atom = { - aid : int; - var : var; - neg : atom; - lit : formula; - mutable is_true : bool; - watched : clause Vec.t; + aid: int; + var: var; + neg: atom; + lit: formula; + mutable is_true: bool; + watched: clause Vec.t; } and clause = { cid: int; - atoms : atom array; - mutable cpremise : premise; - mutable activity : float; + atoms: atom array; + mutable cpremise: premise; + mutable activity: float; mutable flags: int; (* bitfield *) } @@ -93,8 +91,8 @@ module Make(Plugin : PLUGIN) | Atom of atom (* Constructors *) - module MF = Hashtbl.Make(Formula) - module MT = Hashtbl.Make(Term) + module MF = Hashtbl.Make (Formula) + module MT = Hashtbl.Make (Term) type st = { t_map: lit MT.t; @@ -104,15 +102,17 @@ module Make(Plugin : PLUGIN) mutable cpt_mk_clause: int; } - let create_st ?(size=`Big) () : st = - let size_map = match size with + let create_st ?(size = `Big) () : st = + let size_map = + match size with | `Tiny -> 8 | `Small -> 16 | `Big -> 4096 in - { f_map = MF.create size_map; + { + f_map = MF.create size_map; t_map = MT.create size_map; - vars = Vec.create(); + vars = Vec.create (); cpt_mk_var = 0; cpt_mk_clause = 0; } @@ -121,7 +121,8 @@ module Make(Plugin : PLUGIN) let get_elt st i = Vec.get st.vars i let iter_elt st f = Vec.iter f st.vars - let name_of_clause c = match c.cpremise with + let name_of_clause c = + match c.cpremise with | Hyp _ -> "H" ^ string_of_int c.cid | Lemma _ -> "T" ^ string_of_int c.cid | Local -> "L" ^ string_of_int c.cid @@ -130,22 +131,25 @@ module Make(Plugin : PLUGIN) module Lit = struct type t = lit + let[@inline] term l = l.term let[@inline] level l = l.l_level let[@inline] assigned l = l.assigned let[@inline] weight l = l.l_weight - let make (st:st) (t:term) : t = + let make (st : st) (t : term) : t = try MT.find st.t_map t with Not_found -> - let res = { - lid = st.cpt_mk_var; - term = t; - l_weight = 1.; - l_idx= -1; - l_level = -1; - assigned = None; - } in + let res = + { + lid = st.cpt_mk_var; + term = t; + l_weight = 1.; + l_idx = -1; + l_level = -1; + assigned = None; + } + in st.cpt_mk_var <- st.cpt_mk_var + 1; MT.add st.t_map t res; Vec.push st.vars (E_lit res); @@ -153,15 +157,14 @@ module Make(Plugin : PLUGIN) let debug_assign fmt v = match v.assigned with - | None -> - Format.fprintf fmt "" - | Some t -> - Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level Value.pp t + | None -> Format.fprintf fmt "" + | Some t -> Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level Value.pp t let pp out v = Term.pp out v.term + let debug out v = - Format.fprintf out "%d[%a][lit:@[%a@]]" - (v.lid+1) debug_assign v Term.pp v.term + Format.fprintf out "%d[%a][lit:@[%a@]]" (v.lid + 1) debug_assign v + Term.pp v.term end (* some boolean flags for variables, used as masks *) @@ -172,6 +175,7 @@ module Make(Plugin : PLUGIN) module Var = struct type t = var + let[@inline] level v = v.v_level let[@inline] pos v = v.pa let[@inline] neg v = v.na @@ -179,43 +183,54 @@ module Make(Plugin : PLUGIN) let[@inline] assignable v = v.v_assignable let[@inline] weight v = v.v_weight let[@inline] mark v = v.v_fields <- v.v_fields lor seen_var - let[@inline] unmark v = v.v_fields <- v.v_fields land (lnot seen_var) - let[@inline] marked v = (v.v_fields land seen_var) <> 0 - let[@inline] set_default_pol_true v = v.v_fields <- v.v_fields lor default_pol_true - let[@inline] set_default_pol_false v = v.v_fields <- v.v_fields land (lnot default_pol_true) - let[@inline] default_pol v = (v.v_fields land default_pol_true) <> 0 + let[@inline] unmark v = v.v_fields <- v.v_fields land lnot seen_var + let[@inline] marked v = v.v_fields land seen_var <> 0 - let make ?(default_pol=true) (st:st) (t:formula) : var * Solver_intf.negated = + let[@inline] set_default_pol_true v = + v.v_fields <- v.v_fields lor default_pol_true + + let[@inline] set_default_pol_false v = + v.v_fields <- v.v_fields land lnot default_pol_true + + let[@inline] default_pol v = v.v_fields land default_pol_true <> 0 + + let make ?(default_pol = true) (st : st) (t : formula) : + var * Solver_intf.negated = let lit, negated = Formula.norm t in - try - MF.find st.f_map lit, negated + try MF.find st.f_map lit, negated with Not_found -> let cpt_double = st.cpt_mk_var lsl 1 in - let rec var = - { vid = st.cpt_mk_var; - pa = pa; - na = na; + let rec var = + { + vid = st.cpt_mk_var; + pa; + na; v_fields = 0; v_level = -1; - v_idx= -1; + v_idx = -1; v_weight = 0.; v_assignable = None; reason = None; } and pa = - { var = var; - lit = lit; - watched = Vec.create(); + { + var; + lit; + watched = Vec.create (); neg = na; is_true = false; - aid = cpt_double (* aid = vid*2 *) } + aid = cpt_double (* aid = vid*2 *); + } and na = - { var = var; + { + var; lit = Formula.neg lit; - watched = Vec.create(); + watched = Vec.create (); neg = pa; is_true = false; - aid = cpt_double + 1 (* aid = vid*2+1 *) } in + aid = cpt_double + 1 (* aid = vid*2+1 *); + } + in MF.add st.f_map lit var; st.cpt_mk_var <- st.cpt_mk_var + 1; if default_pol then set_default_pol_true var; @@ -225,15 +240,19 @@ module Make(Plugin : PLUGIN) (* Marking helpers *) let[@inline] clear v = let pol = default_pol v in - v.v_fields <- (if pol then default_pol_true else 0) + v.v_fields <- + (if pol then + default_pol_true + else + 0) let[@inline] seen_both v = - (seen_pos land v.v_fields <> 0) && - (seen_neg land v.v_fields <> 0) + seen_pos land v.v_fields <> 0 && seen_neg land v.v_fields <> 0 end module Atom = struct type t = atom + let[@inline] level a = a.var.v_level let[@inline] var a = a.var let[@inline] neg a = a.neg @@ -250,17 +269,17 @@ module Make(Plugin : PLUGIN) let has_value a = is_true a || is_false a let[@inline] seen a = - if sign a - then (seen_pos land a.var.v_fields <> 0) - else (seen_neg land a.var.v_fields <> 0) + if sign a then + seen_pos land a.var.v_fields <> 0 + else + seen_neg land a.var.v_fields <> 0 let[@inline] mark a = let pos = equal a (abs a) in - if pos then ( + if pos then a.var.v_fields <- seen_pos lor a.var.v_fields - ) else ( + else a.var.v_fields <- seen_neg lor a.var.v_fields - ) let[@inline] make ?default_pol st lit = let var, negated = Var.make ?default_pol st lit in @@ -271,36 +290,32 @@ module Make(Plugin : PLUGIN) let pp fmt a = Formula.pp fmt a.lit let pp_a fmt v = - if Array.length v = 0 then ( + if Array.length v = 0 then Format.fprintf fmt "∅" - ) else ( + else ( pp fmt v.(0); - if (Array.length v) > 1 then begin - for i = 1 to (Array.length v) - 1 do + if Array.length v > 1 then + for i = 1 to Array.length v - 1 do Format.fprintf fmt " ∨ %a" pp v.(i) done - end ) (* Complete debug printing *) - let pp_sign a = if a == a.var.pa then "+" else "-" + let pp_sign a = + if a == a.var.pa then + "+" + else + "-" let debug_reason fmt = function - | n, _ when n < 0 -> - Format.fprintf fmt "%%" - | n, None -> - Format.fprintf fmt "%d" n - | n, Some Decision -> - Format.fprintf fmt "@@%d" n - | n, Some Bcp c -> - Format.fprintf fmt "->%d/%s" n (name_of_clause c) - | n, Some (Bcp_lazy _) -> - Format.fprintf fmt "->%d/" n - | n, Some Semantic -> - Format.fprintf fmt "::%d" n + | n, _ when n < 0 -> Format.fprintf fmt "%%" + | n, None -> Format.fprintf fmt "%d" n + | n, Some Decision -> Format.fprintf fmt "@@%d" n + | n, Some (Bcp c) -> Format.fprintf fmt "->%d/%s" n (name_of_clause c) + | n, Some (Bcp_lazy _) -> Format.fprintf fmt "->%d/" n + | n, Some Semantic -> Format.fprintf fmt "::%d" n - let pp_level fmt a = - debug_reason fmt (a.var.v_level, a.var.reason) + let pp_level fmt a = debug_reason fmt (a.var.v_level, a.var.reason) let debug_value fmt a = if a.is_true then @@ -311,42 +326,63 @@ module Make(Plugin : PLUGIN) Format.fprintf fmt "" let debug out a = - Format.fprintf out "%s%d[%a][atom:@[%a@]]" - (pp_sign a) (a.var.vid+1) debug_value a Formula.pp a.lit + Format.fprintf out "%s%d[%a][atom:@[%a@]]" (pp_sign a) + (a.var.vid + 1) debug_value a Formula.pp a.lit let debug_a out vec = Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec - let debug_l out l = - List.iter (fun a -> Format.fprintf out "%a@ " debug a) l - module Set = Set.Make(struct type t=atom let compare=compare end) + let debug_l out l = List.iter (fun a -> Format.fprintf out "%a@ " debug a) l + + module Set = Set.Make (struct + type t = atom + + let compare = compare + end) end (* Elements *) module Elt = struct type t = elt + let[@inline] of_lit l = E_lit l let[@inline] of_var v = E_var v let[@inline] id = function - | E_lit l -> l.lid | E_var v -> v.vid + | E_lit l -> l.lid + | E_var v -> v.vid + let[@inline] level = function - | E_lit l -> l.l_level | E_var v -> v.v_level + | E_lit l -> l.l_level + | E_var v -> v.v_level + let[@inline] idx = function - | E_lit l -> l.l_idx | E_var v -> v.v_idx + | E_lit l -> l.l_idx + | E_var v -> v.v_idx + let[@inline] weight = function - | E_lit l -> l.l_weight | E_var v -> v.v_weight - - let[@inline] set_level e lvl = match e with - | E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl - let[@inline] set_idx e i = match e with - | E_lit l -> l.l_idx <- i | E_var v -> v.v_idx <- i - let[@inline] set_weight e w = match e with - | E_lit l -> l.l_weight <- w | E_var v -> v.v_weight <- w + | E_lit l -> l.l_weight + | E_var v -> v.v_weight + + let[@inline] set_level e lvl = + match e with + | E_lit l -> l.l_level <- lvl + | E_var v -> v.v_level <- lvl + + let[@inline] set_idx e i = + match e with + | E_lit l -> l.l_idx <- i + | E_var v -> v.v_idx <- i + + let[@inline] set_weight e w = + match e with + | E_lit l -> l.l_weight <- w + | E_var v -> v.v_weight <- w end module Trail_elt = struct type t = trail_elt + let[@inline] of_lit l = Lit l let[@inline] of_atom a = Atom a @@ -363,14 +399,9 @@ module Make(Plugin : PLUGIN) fun ~flags atoms premise -> let cid = !n in incr n; - { cid; - atoms = atoms; - flags; - activity = 0.; - cpremise = premise} + { cid; atoms; flags; activity = 0.; cpremise = premise } let make ~flags l premise = make_a ~flags (Array.of_list l) premise - let empty = make [] (History []) let name = name_of_clause let[@inline] equal c1 c2 = c1.cid = c2.cid @@ -378,45 +409,53 @@ module Make(Plugin : PLUGIN) let[@inline] atoms c = c.atoms let[@inline] atoms_seq c = Iter.of_array c.atoms let[@inline] atoms_l c = Array.to_list c.atoms - let flag_attached = 0b1 let flag_visited = 0b10 let flag_removable = 0b100 let flag_dead = 0b1000 - let[@inline] make_removable l premise = make ~flags:flag_removable l premise - let[@inline] make_removable_a l premise = make_a ~flags:flag_removable l premise + + let[@inline] make_removable_a l premise = + make_a ~flags:flag_removable l premise + let[@inline] make_permanent l premise = make ~flags:0 l premise + let[@inline] visited c = c.flags land flag_visited <> 0 - let[@inline] visited c = (c.flags land flag_visited) <> 0 let[@inline] set_visited c b = - if b then c.flags <- c.flags lor flag_visited - else c.flags <- c.flags land lnot flag_visited + if b then + c.flags <- c.flags lor flag_visited + else + c.flags <- c.flags land lnot flag_visited + + let[@inline] attached c = c.flags land flag_attached <> 0 - let[@inline] attached c = (c.flags land flag_attached) <> 0 let[@inline] set_attached c b = - if b then c.flags <- c.flags lor flag_attached - else c.flags <- c.flags land lnot flag_attached + if b then + c.flags <- c.flags lor flag_attached + else + c.flags <- c.flags land lnot flag_attached + + let[@inline] removable c = c.flags land flag_removable <> 0 - let[@inline] removable c = (c.flags land flag_removable) <> 0 let[@inline] set_removable c b = - if b then c.flags <- c.flags lor flag_removable - else c.flags <- c.flags land lnot flag_removable + if b then + c.flags <- c.flags lor flag_removable + else + c.flags <- c.flags land lnot flag_removable - let[@inline] dead c = (c.flags land flag_dead) <> 0 + let[@inline] dead c = c.flags land flag_dead <> 0 let[@inline] set_dead c = c.flags <- c.flags lor flag_dead - let[@inline] activity c = c.activity let[@inline] set_activity c w = c.activity <- w - module Tbl = Hashtbl.Make(struct - type t = clause - let hash = hash - let equal = equal - end) + module Tbl = Hashtbl.Make (struct + type t = clause + + let hash = hash + let equal = equal + end) - let pp fmt c = - Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms + let pp fmt c = Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms let debug_premise out = function | Hyp _ -> Format.fprintf out "hyp" @@ -426,12 +465,12 @@ module Make(Plugin : PLUGIN) List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v | Empty_premise -> Format.fprintf out "" - let debug out ({atoms=arr; cpremise=cp;_}as c) = + let debug out ({ atoms = arr; cpremise = cp; _ } as c) = Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" (name c) Atom.debug_a arr debug_premise cp end - module Proof = struct + module Proof = struct exception Resolution_error of string type atom = Atom.t @@ -439,13 +478,14 @@ module Make(Plugin : PLUGIN) type formula = Formula.t type lemma = Plugin.proof - let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg + let error_res_f msg = + Format.kasprintf (fun s -> raise (Resolution_error s)) msg - let[@inline] clear_var_of_ (a:atom) = Var.clear a.var + let[@inline] clear_var_of_ (a : atom) = Var.clear a.var (* Compute resolution of 2 clauses. returns [pivots, resulting_atoms] *) - let resolve (c1:clause) (c2:clause) : atom list * atom list = + let resolve (c1 : clause) (c2 : clause) : atom list * atom list = (* invariants: only atoms in [c2] are marked, and the pivot is cleared when traversing [c1] *) Array.iter Atom.mark c2.atoms; @@ -453,38 +493,46 @@ module Make(Plugin : PLUGIN) let l = Array.fold_left (fun l a -> - if Atom.seen a then l - else if Atom.seen a.neg then ( - pivots := a.var.pa :: !pivots; - clear_var_of_ a; - l - ) else a::l) + if Atom.seen a then + l + else if Atom.seen a.neg then ( + pivots := a.var.pa :: !pivots; + clear_var_of_ a; + l + ) else + a :: l) [] c1.atoms in let l = - Array.fold_left (fun l a -> if Atom.seen a then a::l else l) l c2.atoms + Array.fold_left + (fun l a -> + if Atom.seen a then + a :: l + else + l) + l c2.atoms in Array.iter clear_var_of_ c2.atoms; !pivots, l (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *) - let find_dups (c:clause) : atom list * atom list = + let find_dups (c : clause) : atom list * atom list = let res = Array.fold_left - (fun (dups,l) a -> - if Atom.seen a then ( - a::dups, l - ) else ( - Atom.mark a; - dups, a::l - )) + (fun (dups, l) a -> + if Atom.seen a then + a :: dups, l + else ( + Atom.mark a; + dups, a :: l + )) ([], []) c.atoms in Array.iter clear_var_of_ c.atoms; res (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *) - let same_lits (c1:atom Iter.t) (c2:atom Iter.t): bool = + let same_lits (c1 : atom Iter.t) (c2 : atom Iter.t) : bool = let subset a b = Iter.iter Atom.mark b; let res = Iter.for_all Atom.seen a in @@ -501,34 +549,44 @@ module Make(Plugin : PLUGIN) let rec set_atom_proof a = let aux acc b = - if Atom.equal a.neg b then acc - else set_atom_proof b :: acc + if Atom.equal a.neg b then + acc + else + set_atom_proof b :: acc in assert (a.var.v_level >= 0); - match (a.var.reason) with + match a.var.reason with | Some (Bcp c | Bcp_lazy (lazy c)) -> - Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c); + Log.debugf 5 (fun k -> + k "(@[proof.analyze.clause@ :atom %a@ :c %a@])" Atom.debug a + Clause.debug c); if Array.length c.atoms = 1 then ( - Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])" Atom.debug a); + Log.debugf 5 (fun k -> + k "(@[proof.analyze.old-reason@ %a@])" Atom.debug a); c ) else ( - assert (a.neg.is_true); - let r = History (c :: (Array.fold_left aux [] c.atoms)) in - let c' = Clause.make_permanent [a.neg] r in + assert a.neg.is_true; + let r = History (c :: Array.fold_left aux [] c.atoms) in + let c' = Clause.make_permanent [ a.neg ] r in a.var.reason <- Some (Bcp c'); - Log.debugf 5 - (fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c'); + Log.debugf 5 (fun k -> + k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])" Atom.debug a + Clause.debug c'); c' ) - | _ -> - error_res_f "cannot prove atom %a" Atom.debug a + | _ -> error_res_f "cannot prove atom %a" Atom.debug a let prove_unsat conflict = - if Array.length conflict.atoms = 0 then ( + if Array.length conflict.atoms = 0 then conflict - ) else ( - Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" Clause.debug conflict); - let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.atoms in + else ( + Log.debugf 1 (fun k -> + k "(@[sat.prove-unsat@ :from %a@])" Clause.debug conflict); + let l = + Array.fold_left + (fun acc a -> set_atom_proof a :: acc) + [] conflict.atoms + in let res = Clause.make_permanent [] (History (conflict :: l)) in Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" Clause.debug res); res @@ -541,10 +599,12 @@ module Make(Plugin : PLUGIN) None type t = clause + and proof_node = { - conclusion : clause; - step : step; + conclusion: clause; + step: step; } + and step = | Hypothesis of lemma | Assumption @@ -554,10 +614,11 @@ module Make(Plugin : PLUGIN) and hyper_res_step = { hr_init: t; - hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + hr_steps: (atom * t) list; + (* list of pivot+clause to resolve against [init] *) } - let[@inline] conclusion (p:t) : clause = p + let[@inline] conclusion (p : t) : clause = p type res_step = { rs_res: atom list; @@ -568,30 +629,33 @@ module Make(Plugin : PLUGIN) (* find pivots for resolving [l] with [init], and also return the atoms of the conclusion *) - let find_pivots (init:clause) (l:clause list) : _ * (atom * t) list = - Log.debugf 15 - (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])" - Clause.debug init (Format.pp_print_list Clause.debug) l); + let find_pivots (init : clause) (l : clause list) : _ * (atom * t) list = + Log.debugf 15 (fun k -> + k "(@[proof.find-pivots@ :init %a@ :l %a@])" Clause.debug init + (Format.pp_print_list Clause.debug) + l); Array.iter Atom.mark init.atoms; let steps = List.map (fun c -> - let pivot = - match - Iter.of_array c.atoms - |> Iter.filter (fun a -> Atom.seen (Atom.neg a)) - |> Iter.to_list - with - | [a] -> a - | [] -> - error_res_f "(@[proof.expand.pivot_missing@ %a@])" Clause.debug c - | pivots -> - error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])" - Clause.debug c Atom.debug_l pivots - in - Array.iter Atom.mark c.atoms; (* add atoms to result *) - clear_var_of_ pivot; - Atom.abs pivot, c) + let pivot = + match + Iter.of_array c.atoms + |> Iter.filter (fun a -> Atom.seen (Atom.neg a)) + |> Iter.to_list + with + | [ a ] -> a + | [] -> + error_res_f "(@[proof.expand.pivot_missing@ %a@])" Clause.debug + c + | pivots -> + error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])" + Clause.debug c Atom.debug_l pivots + in + Array.iter Atom.mark c.atoms; + (* add atoms to result *) + clear_var_of_ pivot; + Atom.abs pivot, c) l in (* cleanup *) @@ -607,52 +671,48 @@ module Make(Plugin : PLUGIN) !res, steps let expand conclusion = - Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" Clause.debug conclusion); + Log.debugf 5 (fun k -> + k "(@[sat.proof.expand@ @[%a@]@])" Clause.debug conclusion); match conclusion.cpremise with - | Lemma l -> - { conclusion; step = Lemma l; } - | Local -> - { conclusion; step = Assumption; } - | Hyp l -> - { conclusion; step = Hypothesis l; } + | Lemma l -> { conclusion; step = Lemma l } + | Local -> { conclusion; step = Assumption } + | Hyp l -> { conclusion; step = Hypothesis l } | History [] -> error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion - | History [c] -> + | History [ c ] -> let duplicates, res = find_dups c in assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); { conclusion; step = Duplicate (c, duplicates) } | History (c :: r) -> let res, steps = find_pivots c r in assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); - { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; } + { conclusion; step = Hyper_res { hr_init = c; hr_steps = steps } } | Empty_premise -> raise Solver_intf.No_proof - let rec res_of_hyper_res (hr: hyper_res_step) : _ * _ * atom = - let {hr_init=c1; hr_steps=l} = hr in + let rec res_of_hyper_res (hr : hyper_res_step) : _ * _ * atom = + let { hr_init = c1; hr_steps = l } = hr in match l with | [] -> assert false - | [a, c2] -> c1, c2, a (* done *) - | (a,c2) :: steps' -> + | [ (a, c2) ] -> c1, c2, a (* done *) + | (a, c2) :: steps' -> (* resolve [c1] with [c2], then resolve that against [steps] *) let pivots, l = resolve c1 c2 in - assert (match pivots with [a'] -> Atom.equal a a' | _ -> false); - let c_1_2 = Clause.make_removable l (History [c1; c2]) in - res_of_hyper_res {hr_init=c_1_2; hr_steps=steps'} + assert ( + match pivots with + | [ a' ] -> Atom.equal a a' + | _ -> false); + let c_1_2 = Clause.make_removable l (History [ c1; c2 ]) in + res_of_hyper_res { hr_init = c_1_2; hr_steps = steps' } (* Proof nodes manipulation *) let is_leaf = function - | Hypothesis _ - | Assumption - | Lemma _ -> true - | Duplicate _ - | Hyper_res _ -> false + | Hypothesis _ | Assumption | Lemma _ -> true + | Duplicate _ | Hyper_res _ -> false let parents = function - | Hypothesis _ - | Assumption - | Lemma _ -> [] - | Duplicate (p, _) -> [p] - | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps + | Hypothesis _ | Assumption | Lemma _ -> [] + | Duplicate (p, _) -> [ p ] + | Hyper_res { hr_init; hr_steps } -> hr_init :: List.map snd hr_steps let expl = function | Hypothesis _ -> "hypothesis" @@ -672,14 +732,20 @@ module Make(Plugin : PLUGIN) | Empty_premise -> raise Solver_intf.No_proof | Hyp _ | Lemma _ | Local -> aux (c :: res) acc r | History h -> - let l = List.fold_left (fun acc c -> - if not @@ Clause.visited c then c :: acc else acc) r h in + let l = + List.fold_left + (fun acc c -> + if not @@ Clause.visited c then + c :: acc + else + acc) + r h + in aux res (c :: acc) l - ) else ( + ) else aux res acc r - ) in - let res, tmp = aux [] [] [proof] in + let res, tmp = aux [] [] [ proof ] in List.iter (fun c -> Clause.set_visited c false) res; List.iter (fun c -> Clause.set_visited c false) tmp; res @@ -699,18 +765,16 @@ module Make(Plugin : PLUGIN) Tbl.add h c true; fold_aux s h f (f acc (expand c)) | Some (Enter c) -> - if not (Tbl.mem h c) then begin + if not (Tbl.mem h c) then ( Stack.push (Leaving c) s; let node = expand c in - begin match node.step with - | Duplicate (p1, _) -> - Stack.push (Enter p1) s - | Hyper_res {hr_init=p1; hr_steps=l} -> - List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l; - Stack.push (Enter p1) s; - | Hypothesis _ | Assumption | Lemma _ -> () - end - end; + match node.step with + | Duplicate (p1, _) -> Stack.push (Enter p1) s + | Hyper_res { hr_init = p1; hr_steps = l } -> + List.iter (fun (_, p2) -> Stack.push (Enter p2) s) l; + Stack.push (Enter p1) s + | Hypothesis _ | Assumption | Lemma _ -> () + ); fold_aux s h f acc let fold f acc p = @@ -719,18 +783,22 @@ module Make(Plugin : PLUGIN) Stack.push (Enter p) s; fold_aux s h f acc - let check_empty_conclusion (p:t) = - if Array.length p.atoms > 0 then ( - error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" Clause.debug p; - ) + let check_empty_conclusion (p : t) = + if Array.length p.atoms > 0 then + error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" + Clause.debug p - let check (p:t) = fold (fun () _ -> ()) () p + let check (p : t) = fold (fun () _ -> ()) () p end + type proof = Proof.t - module H = (Heap.Make [@specialise]) (struct + module H = Heap.Make [@specialise] (struct type t = Elt.t - let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *) + + let[@inline] cmp i j = + Elt.weight j < Elt.weight i (* comparison by weight *) + let idx = Elt.idx let set_idx = Elt.set_idx end) @@ -754,7 +822,6 @@ module Make(Plugin : PLUGIN) let warn = 3 let info = 5 let debug = 50 - let var_decay : float = 1. /. 0.95 (* inverse of the activity factor for variables. Default 1/0.95 *) @@ -769,48 +836,34 @@ module Make(Plugin : PLUGIN) (* Singleton type containing the current state *) type t = { - st : st; + st: st; th: theory; - store_proof: bool; (* do we store proofs? *) - (* Clauses are simplified for eficiency purposes. In the following vectors, the comments actually refer to the original non-simplified clause. *) - - clauses_hyps : clause Vec.t; + clauses_hyps: clause Vec.t; (* clauses added by the user *) - clauses_learnt : clause Vec.t; - (* learnt clauses (tautologies true at any time, whatever the user level) *) - - clauses_to_add : clause Vec.t; - (* Clauses either assumed or pushed by the theory, waiting to be added. *) - - mutable unsat_at_0: clause option; - (* conflict at level 0, if any *) - - mutable next_decisions : atom list; - (* When the last conflict was a semantic one (mcsat), + clauses_learnt: clause Vec.t; + (* learnt clauses (tautologies true at any time, whatever the user level) *) + clauses_to_add: clause Vec.t; + (* Clauses either assumed or pushed by the theory, waiting to be added. *) + mutable unsat_at_0: clause option; (* conflict at level 0, if any *) + mutable next_decisions: atom list; + (* When the last conflict was a semantic one (mcsat), this stores the next decision to make; if some theory wants atoms to be decided on (for theory combination), store them here. *) - - trail : trail_elt Vec.t; - (* decision stack + propagated elements (atoms or assignments). *) - - elt_levels : int Vec.t; - (* decision levels in [trail] *) - - mutable assumptions: atom Vec.t; - (* current assumptions *) - - mutable th_head : int; + trail: trail_elt Vec.t; + (* decision stack + propagated elements (atoms or assignments). *) + elt_levels: int Vec.t; (* decision levels in [trail] *) + mutable assumptions: atom Vec.t; (* current assumptions *) + mutable th_head: int; (* Start offset in the queue {!trail} of unit facts not yet seen by the theory. *) - mutable elt_head : int; + mutable elt_head: int; (* Start offset in the queue {!trail} of unit facts to propagate, within the trail *) - (* invariant: - during propagation, th_head <= elt_head - then, once elt_head reaches length trail, Th.assume is @@ -819,23 +872,15 @@ module Make(Plugin : PLUGIN) - before a decision (and after the fixpoint), th_head = elt_head = length trail *) - - order : H.t; - (* Heap ordered by variable activity *) - - to_clear: var Vec.t; - (* variables to unmark *) - - mutable var_incr : float; - (* increment for variables' activity *) - - mutable clause_incr : float; - (* increment for clauses' activity *) - - mutable on_conflict : (atom array -> unit) option; - mutable on_decision : (atom -> unit) option; + order: H.t; (* Heap ordered by variable activity *) + to_clear: var Vec.t; (* variables to unmark *) + mutable var_incr: float; (* increment for variables' activity *) + mutable clause_incr: float; (* increment for clauses' activity *) + mutable on_conflict: (atom array -> unit) option; + mutable on_decision: (atom -> unit) option; mutable on_new_atom: (atom -> unit) option; } + type solver = t (* intial restart limit *) @@ -844,41 +889,35 @@ module Make(Plugin : PLUGIN) (* initial limit for the number of learnt clauses, 1/3 of initial number of clauses by default *) let learntsize_factor = 1. /. 3. - - let _nop_on_conflict (_:atom array) = () + let _nop_on_conflict (_ : atom array) = () (* Starting environment. *) - let create_ ~st ~store_proof (th:theory) : t = { - st; th; - unsat_at_0=None; - next_decisions = []; - - clauses_hyps = Vec.create(); - clauses_learnt = Vec.create(); - - clauses_to_add = Vec.create (); - to_clear=Vec.create(); - - th_head = 0; - elt_head = 0; - - trail = Vec.create (); - elt_levels = Vec.create(); - assumptions= Vec.create(); - - order = H.create(); - - var_incr = 1.; - clause_incr = 1.; - store_proof; - on_conflict = None; - on_decision= None; - on_new_atom = None; - } + let create_ ~st ~store_proof (th : theory) : t = + { + st; + th; + unsat_at_0 = None; + next_decisions = []; + clauses_hyps = Vec.create (); + clauses_learnt = Vec.create (); + clauses_to_add = Vec.create (); + to_clear = Vec.create (); + th_head = 0; + elt_head = 0; + trail = Vec.create (); + elt_levels = Vec.create (); + assumptions = Vec.create (); + order = H.create (); + var_incr = 1.; + clause_incr = 1.; + store_proof; + on_conflict = None; + on_decision = None; + on_new_atom = None; + } - let create - ?on_conflict ?on_decision ?on_new_atom - ?(store_proof=true) ?(size=`Big) (th:theory) : t = + let create ?on_conflict ?on_decision ?on_new_atom ?(store_proof = true) + ?(size = `Big) (th : theory) : t = let st = create_st ~size () in let st = create_ ~st ~store_proof th in st.on_new_atom <- on_new_atom; @@ -923,11 +962,9 @@ module Make(Plugin : PLUGIN) (* When we have a new literal, we need to first create the list of its subterms. *) - let mk_atom ?default_pol st (f:formula) : atom = + let mk_atom ?default_pol st (f : formula) : atom = let res = Atom.make ?default_pol st.st f in - if Plugin.mcsat then ( - mk_atom_mcsat_ st res; - ); + if Plugin.mcsat then mk_atom_mcsat_ st res; res (* Variable and literal activity. @@ -937,7 +974,7 @@ module Make(Plugin : PLUGIN) When we add a variable (which wraps a formula), we also need to add all its subterms. *) - let rec insert_elt_order st (elt:elt) : unit = + let rec insert_elt_order st (elt : elt) : unit = H.insert st.order elt; if Plugin.mcsat then ( match elt with @@ -945,10 +982,9 @@ module Make(Plugin : PLUGIN) | E_var v -> insert_subterms_order st v ) - and insert_var_order st (v:var) : unit = - insert_elt_order st (E_var v) + and insert_var_order st (v : var) : unit = insert_elt_order st (E_var v) - and insert_subterms_order st (v:var) : unit = + and insert_subterms_order st (v : var) : unit = iter_sub (fun t -> insert_elt_order st (Elt.of_lit t)) v (* Add new litterals/atoms on which to decide on, even if there is no @@ -957,25 +993,23 @@ module Make(Plugin : PLUGIN) inserting them into the heap, if it appears that it helps performance. *) let make_term st t = let l = Lit.make st.st t in - if l.l_level < 0 then ( - insert_elt_order st (E_lit l); - ) + if l.l_level < 0 then insert_elt_order st (E_lit l) - let make_atom st (p:formula) : atom = + let make_atom st (p : formula) : atom = let a = mk_atom st p in if a.var.v_level < 0 then ( insert_elt_order st (E_var a.var); - (match st.on_new_atom with Some f -> f a | None -> ()); - ) else ( + match st.on_new_atom with + | Some f -> f a + | None -> () + ) else assert (a.is_true || a.neg.is_true); - ); a (* Rather than iterate over all the heap when we want to decrease all the variables/literals activity, we instead increase the value by which we increase the activity of 'interesting' var/lits. *) - let[@inline] var_decay_activity st = - st.var_incr <- st.var_incr *. var_decay + let[@inline] var_decay_activity st = st.var_incr <- st.var_incr *. var_decay let[@inline] clause_decay_activity st = st.clause_incr <- st.clause_incr *. clause_decay @@ -985,34 +1019,30 @@ module Make(Plugin : PLUGIN) v.v_weight <- v.v_weight +. st.var_incr; if v.v_weight > 1e100 then ( for i = 0 to nb_elt st.st - 1 do - Elt.set_weight (get_elt st.st i) ((Elt.weight (get_elt st.st i)) *. 1e-100) + Elt.set_weight (get_elt st.st i) (Elt.weight (get_elt st.st i) *. 1e-100) done; - st.var_incr <- st.var_incr *. 1e-100; + st.var_incr <- st.var_incr *. 1e-100 ); let elt = Elt.of_var v in - if H.in_heap elt then ( - H.decrease st.order elt - ) + if H.in_heap elt then H.decrease st.order elt (* increase activity of literal [l] *) - let lit_bump_activity_aux (st:t) (l:lit): unit = + let lit_bump_activity_aux (st : t) (l : lit) : unit = l.l_weight <- l.l_weight +. st.var_incr; if l.l_weight > 1e100 then ( iter_elt st.st (fun e -> Elt.set_weight e (Elt.weight e *. 1e-100)); - st.var_incr <- st.var_incr *. 1e-100; + st.var_incr <- st.var_incr *. 1e-100 ); let elt = Elt.of_lit l in - if H.in_heap elt then ( - H.decrease st.order elt - ) + if H.in_heap elt then H.decrease st.order elt (* increase activity of var [v] *) - let var_bump_activity st (v:var): unit = + let var_bump_activity st (v : var) : unit = var_bump_activity_aux st v; iter_sub (lit_bump_activity_aux st) v (* increase activity of clause [c] *) - let clause_bump_activity st (c:clause) : unit = + let clause_bump_activity st (c : clause) : unit = c.activity <- c.activity +. st.clause_incr; if c.activity > 1e20 then ( Vec.iter (fun c -> c.activity <- c.activity *. 1e-20) st.clauses_learnt; @@ -1034,16 +1064,20 @@ module Make(Plugin : PLUGIN) (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *) let arr_to_list arr i : _ list = - if i >= Array.length arr then [] - else Array.to_list (Array.sub arr i (Array.length arr - i)) + if i >= Array.length arr then + [] + else + Array.to_list (Array.sub arr i (Array.length arr - i)) (* Eliminates atom duplicates in clauses *) let eliminate_duplicates clause : clause = let trivial = ref false in let duplicates = ref [] in let res = ref [] in - Array.iter (fun a -> - if Atom.seen a then duplicates := a :: !duplicates + Array.iter + (fun a -> + if Atom.seen a then + duplicates := a :: !duplicates else ( Atom.mark a; res := a :: !res @@ -1051,16 +1085,15 @@ module Make(Plugin : PLUGIN) clause.atoms; List.iter (fun a -> - if Var.seen_both a.var then trivial := true; - Var.clear a.var) + if Var.seen_both a.var then trivial := true; + Var.clear a.var) !res; - if !trivial then ( + if !trivial then raise Trivial - ) else if !duplicates = [] then ( + else if !duplicates = [] then clause - ) else ( - Clause.make ~flags:clause.flags !res (History [clause]) - ) + else + Clause.make ~flags:clause.flags !res (History [ clause ]) (* Partition literals for new clauses, into: - true literals (maybe makes the clause trivial if the lit is proved true at level 0) @@ -1071,17 +1104,18 @@ module Make(Plugin : PLUGIN) *) let partition atoms : atom list * clause list = let rec partition_aux trues unassigned falses history i = - if i >= Array.length atoms then ( + if i >= Array.length atoms then trues @ unassigned @ falses, history - ) else ( + else ( let a = atoms.(i) in if a.is_true then ( let l = a.var.v_level in if l = 0 then - raise Trivial (* A var true at level 0 gives a trivially true clause *) + raise + Trivial (* A var true at level 0 gives a trivially true clause *) else - (a :: trues) @ unassigned @ falses @ - (arr_to_list atoms (i + 1)), history + ( (a :: trues) @ unassigned @ falses @ arr_to_list atoms (i + 1), + history ) ) else if a.neg.is_true then ( let l = a.var.v_level in if l = 0 then ( @@ -1096,20 +1130,18 @@ module Make(Plugin : PLUGIN) this shouldn't really happen actually (because semantic propagations at level 0 should come with a proof). *) (* TODO: get a proof of the propagation. *) - | None | Some Decision -> assert false - (* The var must have a reason, and it cannot be a decision/assumption, + | None | Some Decision -> + assert false + (* The var must have a reason, and it cannot be a decision/assumption, since its level is 0. *) - ) else ( - partition_aux trues unassigned (a::falses) history (i + 1) - ) - ) else ( - partition_aux trues (a::unassigned) falses history (i + 1) - ) + ) else + partition_aux trues unassigned (a :: falses) history (i + 1) + ) else + partition_aux trues (a :: unassigned) falses history (i + 1) ) in partition_aux [] [] [] [] 0 - (* Making a decision. Before actually creatig a new decision level, we check that all propagations have been done and propagated to the theory, @@ -1145,9 +1177,10 @@ module Make(Plugin : PLUGIN) let cancel_until st lvl = assert (lvl >= 0); (* Nothing to do if we try to backtrack to a non-existent level. *) - if decision_level st <= lvl then ( - Log.debugf debug (fun k -> k "(@[sat.cancel-until.nop@ :already-at-level <= %d@])" lvl) - ) else ( + if decision_level st <= lvl then + Log.debugf debug (fun k -> + k "(@[sat.cancel-until.nop@ :already-at-level <= %d@])" lvl) + else ( Log.debugf info (fun k -> k "(@[sat.cancel-until %d@])" lvl); (* We set the head of the solver and theory queue to what it was. *) let head = ref (Vec.get st.elt_levels lvl) in @@ -1156,7 +1189,7 @@ module Make(Plugin : PLUGIN) (* Now we need to cleanup the vars that are not valid anymore (i.e to the right of elt_head in the queue. *) for c = st.elt_head to Vec.size st.trail - 1 do - match (Vec.get st.trail c) with + match Vec.get st.trail c with (* A literal is unassigned, we nedd to add it back to the heap of potentially assignable literals, unless it has a level lower than [lvl], in which case we just move it back. *) @@ -1190,29 +1223,37 @@ module Make(Plugin : PLUGIN) done; (* Recover the right theory state. *) let n = decision_level st - lvl in - assert (n>0); + assert (n > 0); (* Resize the vectors according to their new size. *) Vec.shrink st.trail !head; Vec.shrink st.elt_levels lvl; Plugin.pop_levels st.th n; - st.next_decisions <- []; + st.next_decisions <- [] ); () let pp_unsat_cause out = function - | US_local {first=_; core} -> + | US_local { first = _; core } -> Format.fprintf out "(@[unsat-cause@ :false-assumptions %a@])" - (Format.pp_print_list Atom.pp) core + (Format.pp_print_list Atom.pp) + core | US_false c -> Format.fprintf out "(@[unsat-cause@ :false %a@])" Clause.debug c (* Unsatisfiability is signaled through an exception, since it can happen in multiple places (adding new clauses, or solving for instance). *) - let report_unsat st (us:unsat_cause) : _ = - Log.debugf info (fun k -> k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us); - let us = match us with + let report_unsat st (us : unsat_cause) : _ = + Log.debugf info (fun k -> + k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us); + let us = + match us with | US_false c -> - let c = if st.store_proof then Proof.prove_unsat c else c in + let c = + if st.store_proof then + Proof.prove_unsat c + else + c + in st.unsat_at_0 <- Some c; US_false c | _ -> us @@ -1228,134 +1269,151 @@ module Make(Plugin : PLUGIN) let simpl_reason : reason -> reason = function | (Bcp cl | Bcp_lazy (lazy cl)) as r -> let l, history = partition cl.atoms in - begin match l with - | [_] -> - if history = [] then ( - (* no simplification has been done, so [cl] is actually a clause with only + (match l with + | [ _ ] -> + if history = [] then + (* no simplification has been done, so [cl] is actually a clause with only [a], so it is a valid reason for propagating [a]. *) - r - ) else ( - (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl] + r + else ( + (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl] with only one formula (which is [a]). So we explicitly create that clause and set it as the cause for the propagation of [a], that way we can rebuild the whole resolution tree when we want to prove [a]. *) - let c' = Clause.make ~flags:cl.flags l (History (cl :: history)) in - Log.debugf debug - (fun k -> k "(@[sat.simplified-reason@ %a@ %a@])" Clause.debug cl Clause.debug c'); - Bcp c' - ) - | _ -> - Log.debugf error - (fun k -> - k "(@[sat.simplify-reason.failed@ :at %a@ %a@]" - (Vec.pp ~sep:"" Atom.debug) (Vec.of_list l) - Clause.debug cl); - assert false - end + let c' = Clause.make ~flags:cl.flags l (History (cl :: history)) in + Log.debugf debug (fun k -> + k "(@[sat.simplified-reason@ %a@ %a@])" Clause.debug cl + Clause.debug c'); + Bcp c' + ) + | _ -> + Log.debugf error (fun k -> + k "(@[sat.simplify-reason.failed@ :at %a@ %a@]" + (Vec.pp ~sep:"" Atom.debug) + (Vec.of_list l) Clause.debug cl); + assert false) | (Decision | Semantic) as r -> r (* Boolean propagation. Wrapper function for adding a new propagated formula. *) let enqueue_bool st a ~level:lvl reason : unit = if a.neg.is_true then ( - Log.debugf error - (fun k->k "(@[sat.error.trying to enqueue a false literal %a@])" Atom.debug a); + Log.debugf error (fun k -> + k "(@[sat.error.trying to enqueue a false literal %a@])" Atom.debug a); assert false ); - assert (not a.is_true && a.var.v_level < 0 && - a.var.reason = None && lvl >= 0); + assert ( + (not a.is_true) && a.var.v_level < 0 && a.var.reason = None && lvl >= 0); let reason = - if lvl > 0 then reason - else simpl_reason reason + if lvl > 0 then + reason + else + simpl_reason reason in a.is_true <- true; a.var.v_level <- lvl; a.var.reason <- Some reason; Vec.push st.trail (Trail_elt.of_atom a); - Log.debugf debug - (fun k->k "(@[sat.enqueue[%d]@ %a@])" (Vec.size st.trail) Atom.debug a); + Log.debugf debug (fun k -> + k "(@[sat.enqueue[%d]@ %a@])" (Vec.size st.trail) Atom.debug a); () let enqueue_semantic st a terms = if not a.is_true then ( let l = List.map (Lit.make st.st) terms in - let lvl = List.fold_left (fun acc {l_level; _} -> - assert (l_level > 0); max acc l_level) 0 l in + let lvl = + List.fold_left + (fun acc { l_level; _ } -> + assert (l_level > 0); + max acc l_level) + 0 l + in enqueue_bool st a ~level:lvl Semantic ) (* MCsat semantic assignment *) - let enqueue_assign st (l:lit) (value:value) lvl = + let enqueue_assign st (l : lit) (value : value) lvl = match l.assigned with | Some _ -> - Log.debugf error - (fun k -> k "(@[sat.error: Trying to assign an already assigned literal:@ %a@])" Lit.debug l); + Log.debugf error (fun k -> + k "(@[sat.error: Trying to assign an already assigned literal:@ %a@])" + Lit.debug l); assert false | None -> assert (l.l_level < 0); l.assigned <- Some value; l.l_level <- lvl; Vec.push st.trail (Trail_elt.of_lit l); - Log.debugf debug - (fun k -> k "(@[sat.enqueue-semantic[%d]@ %a@])" (Vec.size st.trail) Lit.debug l); + Log.debugf debug (fun k -> + k "(@[sat.enqueue-semantic[%d]@ %a@])" (Vec.size st.trail) Lit.debug l); () (* swap elements of array *) let[@inline] swap_arr a i j = - if i<>j then ( + if i <> j then ( let tmp = a.(i) in a.(i) <- a.(j); - a.(j) <- tmp; + a.(j) <- tmp ) (* move atoms assigned at high levels first *) - let put_high_level_atoms_first (arr:atom array) : unit = + let put_high_level_atoms_first (arr : atom array) : unit = Array.iteri (fun i a -> - if i>0 && Atom.level a > Atom.level arr.(0) then ( - (* move first to second, [i]-th to first, second to [i] *) - if i=1 then ( - swap_arr arr 0 1; - ) else ( - let tmp = arr.(1) in - arr.(1) <- arr.(0); - arr.(0) <- arr.(i); - arr.(i) <- tmp; - ); - ) else if i>1 && Atom.level a > Atom.level arr.(1) then ( - swap_arr arr 1 i; - )) + if i > 0 && Atom.level a > Atom.level arr.(0) then + if + (* move first to second, [i]-th to first, second to [i] *) + i = 1 + then + swap_arr arr 0 1 + else ( + let tmp = arr.(1) in + arr.(1) <- arr.(0); + arr.(0) <- arr.(i); + arr.(i) <- tmp + ) + else if i > 1 && Atom.level a > Atom.level arr.(1) then + swap_arr arr 1 i) arr (* evaluate an atom for MCsat, if it's not assigned by boolean propagation/decision *) let th_eval st a : bool option = - if a.is_true || a.neg.is_true then None - else match Plugin.eval st.th a.lit with + if a.is_true || a.neg.is_true then + None + else ( + match Plugin.eval st.th a.lit with | Solver_intf.Unknown -> None | Solver_intf.Valued (b, l) -> - if l = [] then ( - invalid_argf "semantic propagation at level 0 currently forbidden: %a" Atom.pp a; - ); - let atom = if b then a else a.neg in + if l = [] then + invalid_argf "semantic propagation at level 0 currently forbidden: %a" + Atom.pp a; + let atom = + if b then + a + else + a.neg + in enqueue_semantic st atom l; Some b + ) (* find which level to backtrack to, given a conflict clause and a boolean stating whether it is a UIP ("Unique Implication Point") precond: the atom list is sorted by decreasing decision level *) - let backtrack_lvl _st (arr: atom array) : int * bool = - if Array.length arr <= 1 then ( + let backtrack_lvl _st (arr : atom array) : int * bool = + if Array.length arr <= 1 then 0, true - ) else ( + else ( let a = arr.(0) in let b = arr.(1) in - assert(a.var.v_level > 0); - if a.var.v_level > b.var.v_level then ( - (* backtrack below [a], so we can propagate [not a] *) - b.var.v_level, true - ) else ( + assert (a.var.v_level > 0); + if a.var.v_level > b.var.v_level then + ( (* backtrack below [a], so we can propagate [not a] *) + b.var.v_level, + true ) + else ( assert (a.var.v_level = b.var.v_level); assert (a.var.v_level >= 0); max (a.var.v_level - 1) 0, false @@ -1369,7 +1427,7 @@ module Make(Plugin : PLUGIN) during pop operations to determine the origin of a clause/conflict (boolean conflict i.e hypothesis, or theory lemma) *) type conflict_res = { - cr_backtrack_lvl : int; (* level to backtrack to *) + cr_backtrack_lvl: int; (* level to backtrack to *) cr_learnt: atom array; (* lemma learnt from conflict *) cr_history: clause list; (* justification *) cr_is_uip: bool; (* conflict is UIP? *) @@ -1385,71 +1443,73 @@ module Make(Plugin : PLUGIN) except we look the the Last UIP (TODO: check ?), and do it in an imperative and efficient manner. *) let analyze st c_clause : conflict_res = - let pathC = ref 0 in + let pathC = ref 0 in let learnt = ref [] in - let cond = ref true in + let cond = ref true in let blevel = ref 0 in - let to_unmark = st.to_clear in (* for cleanup *) - let c = ref (Some c_clause) in + let to_unmark = st.to_clear in + (* for cleanup *) + let c = ref (Some c_clause) in let tr_ind = ref (Vec.size st.trail - 1) in let history = ref [] in assert (decision_level st > 0); Vec.clear to_unmark; let conflict_level = - if Plugin.mcsat || Plugin.has_theory - then Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms - else decision_level st + if Plugin.mcsat || Plugin.has_theory then + Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms + else + decision_level st in - Log.debugf debug - (fun k -> k "(@[sat.analyze-conflict@ :c-level %d@ :clause %a@])" conflict_level Clause.debug c_clause); + Log.debugf debug (fun k -> + k "(@[sat.analyze-conflict@ :c-level %d@ :clause %a@])" conflict_level + Clause.debug c_clause); while !cond do - begin match !c with - | None -> - Log.debug debug "(@[sat.analyze-conflict: skipping resolution for semantic propagation@])" - | Some clause -> - Log.debugf debug (fun k->k"(@[sat.analyze-conflict.resolve@ %a@])" Clause.debug clause); - if Clause.removable clause then ( - clause_bump_activity st clause; + (match !c with + | None -> + Log.debug debug + "(@[sat.analyze-conflict: skipping resolution for semantic \ + propagation@])" + | Some clause -> + Log.debugf debug (fun k -> + k "(@[sat.analyze-conflict.resolve@ %a@])" Clause.debug clause); + if Clause.removable clause then clause_bump_activity st clause; + history := clause :: !history; + (* visit the current predecessors *) + for j = 0 to Array.length clause.atoms - 1 do + let q = clause.atoms.(j) in + assert (q.is_true || (q.neg.is_true && q.var.v_level >= 0)); + (* unsure? *) + if q.var.v_level <= 0 then ( + assert q.neg.is_true; + match q.var.reason with + | Some (Bcp cl | Bcp_lazy (lazy cl)) -> history := cl :: !history + | Some (Decision | Semantic) | None -> assert false ); - history := clause :: !history; - (* visit the current predecessors *) - for j = 0 to Array.length clause.atoms - 1 do - let q = clause.atoms.(j) in - assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *) - if q.var.v_level <= 0 then ( - assert (q.neg.is_true); - match q.var.reason with - | Some (Bcp cl | Bcp_lazy (lazy cl)) -> history := cl :: !history - | Some (Decision | Semantic) | None -> assert false - ); - if not (Var.marked q.var) then ( - Var.mark q.var; - Vec.push to_unmark q.var; - if q.var.v_level > 0 then ( - var_bump_activity st q.var; - if q.var.v_level >= conflict_level then ( - incr pathC; - ) else ( - learnt := q :: !learnt; - blevel := max !blevel q.var.v_level - ) + if not (Var.marked q.var) then ( + Var.mark q.var; + Vec.push to_unmark q.var; + if q.var.v_level > 0 then ( + var_bump_activity st q.var; + if q.var.v_level >= conflict_level then + incr pathC + else ( + learnt := q :: !learnt; + blevel := max !blevel q.var.v_level ) ) - done - end; + ) + done); (* look for the next node to expand *) while let a = Vec.get st.trail !tr_ind in - Log.debugf debug - (fun k -> k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" Trail_elt.debug a); + Log.debugf debug (fun k -> + k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" Trail_elt.debug a); match a with - | Atom q -> - (not (Var.marked q.var)) || - (q.var.v_level < conflict_level) + | Atom q -> (not (Var.marked q.var)) || q.var.v_level < conflict_level | Lit _ -> true do - decr tr_ind; + decr tr_ind done; let p = get_atom st !tr_ind in decr pathC; @@ -1477,43 +1537,47 @@ module Make(Plugin : PLUGIN) Array.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) a; (* put_high_level_atoms_first a; *) let level, is_uip = backtrack_lvl st a in - { cr_backtrack_lvl = level; + { + cr_backtrack_lvl = level; cr_learnt = a; cr_history = List.rev !history; cr_is_uip = is_uip; } (* add the learnt clause to the clause database, propagate, etc. *) - let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = - let proof = if st.store_proof then History cr.cr_history else Empty_premise in - begin match cr.cr_learnt with - | [| |] -> assert false - | [|fuip|] -> - assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0); - if fuip.neg.is_true then ( - (* incompatible at level 0 *) - report_unsat st (US_false confl) - ) else ( - let uclause = Clause.make_removable_a cr.cr_learnt proof in - (* no need to attach [uclause], it is true at level 0 *) - enqueue_bool st fuip ~level:0 (Bcp uclause) - ) - | _ -> - let fuip = cr.cr_learnt.(0) in - let lclause = Clause.make_removable_a cr.cr_learnt proof in - if Array.length lclause.atoms > 2 then ( - Vec.push st.clauses_learnt lclause; (* potentially gc'able *) - ); - attach_clause lclause; - clause_bump_activity st lclause; - if cr.cr_is_uip then ( - enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) - ) else ( - assert Plugin.mcsat; - assert (st.next_decisions = []); - st.next_decisions <- [fuip.neg]; - ) - end; + let record_learnt_clause st (confl : clause) (cr : conflict_res) : unit = + let proof = + if st.store_proof then + History cr.cr_history + else + Empty_premise + in + (match cr.cr_learnt with + | [||] -> assert false + | [| fuip |] -> + assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0); + if fuip.neg.is_true then + (* incompatible at level 0 *) + report_unsat st (US_false confl) + else ( + let uclause = Clause.make_removable_a cr.cr_learnt proof in + (* no need to attach [uclause], it is true at level 0 *) + enqueue_bool st fuip ~level:0 (Bcp uclause) + ) + | _ -> + let fuip = cr.cr_learnt.(0) in + let lclause = Clause.make_removable_a cr.cr_learnt proof in + if Array.length lclause.atoms > 2 then + Vec.push st.clauses_learnt lclause (* potentially gc'able *); + attach_clause lclause; + clause_bump_activity st lclause; + if cr.cr_is_uip then + enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) + else ( + assert Plugin.mcsat; + assert (st.next_decisions = []); + st.next_decisions <- [ fuip.neg ] + )); var_decay_activity st; clause_decay_activity st @@ -1522,31 +1586,33 @@ module Make(Plugin : PLUGIN) - backtrack - report unsat if conflict at level 0 *) - let add_boolean_conflict st (confl:clause): unit = - Log.debugf info (fun k -> k "(@[sat.add-bool-conflict@ %a@])" Clause.debug confl); + let add_boolean_conflict st (confl : clause) : unit = + Log.debugf info (fun k -> + k "(@[sat.add-bool-conflict@ %a@])" Clause.debug confl); st.next_decisions <- []; assert (decision_level st >= 0); - if decision_level st = 0 || - Array.for_all (fun a -> a.var.v_level <= 0) confl.atoms then ( + if + decision_level st = 0 + || Array.for_all (fun a -> a.var.v_level <= 0) confl.atoms + then (* Top-level conflict *) report_unsat st (US_false confl); - ); let cr = analyze st confl in cancel_until st (max cr.cr_backtrack_lvl 0); record_learnt_clause st confl cr (* Get the correct vector to insert a clause in. *) let[@inline] add_clause_to_vec st c = - if Clause.removable c then ( + if Clause.removable c then Vec.push st.clauses_learnt c - ) else ( + else Vec.push st.clauses_hyps c - ) (* Add a new clause, simplifying, propagating, and backtracking if the clause is false in the current trail *) - let add_clause_ st (init:clause) : unit = - Log.debugf debug (fun k -> k "(@[sat.add-clause@ @[%a@]@])" Clause.debug init); + let add_clause_ st (init : clause) : unit = + Log.debugf debug (fun k -> + k "(@[sat.add-clause@ @[%a@]@])" Clause.debug init); (* Insertion of new lits is done before simplification. Indeed, else a lit in a trivial clause could end up being not decided on, which is a bug. *) Array.iter (fun x -> insert_elt_order st (Elt.of_var x.var)) init.atoms; @@ -1561,29 +1627,35 @@ module Make(Plugin : PLUGIN) List.iteri (fun i a -> c.atoms.(i) <- a) atoms; c ) else ( - let proof = if st.store_proof then History (c::history) else Empty_premise in + let proof = + if st.store_proof then + History (c :: history) + else + Empty_premise + in Clause.make ~flags:c.flags atoms proof ) in assert (clause.flags = init.flags); - Log.debugf info (fun k->k "(@[sat.new-clause@ @[%a@]@])" Clause.debug clause); + Log.debugf info (fun k -> + k "(@[sat.new-clause@ @[%a@]@])" Clause.debug clause); match atoms with - | [] -> - report_unsat st @@ US_false clause - | [a] -> + | [] -> report_unsat st @@ US_false clause + | [ a ] -> cancel_until st 0; - if a.neg.is_true then ( + if a.neg.is_true then (* cannot recover from this *) report_unsat st @@ US_false clause - ) else if a.is_true then ( - () (* atom is already true, nothing to do *) - ) else ( - Log.debugf debug - (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" Atom.debug a); + else if a.is_true then + () + (* atom is already true, nothing to do *) + else ( + Log.debugf debug (fun k -> + k "(@[sat.add-clause.unit-clause@ :propagating %a@])" Atom.debug a); add_clause_to_vec st clause; enqueue_bool st a ~level:0 (Bcp clause) ) - | a::b::_ -> + | a :: b :: _ -> add_clause_to_vec st clause; if a.neg.is_true then ( (* Atoms need to be sorted in decreasing order of decision level, @@ -1593,15 +1665,15 @@ module Make(Plugin : PLUGIN) add_boolean_conflict st clause ) else ( attach_clause clause; - if b.neg.is_true && not a.is_true && not a.neg.is_true then ( + if b.neg.is_true && (not a.is_true) && not a.neg.is_true then ( let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in cancel_until st lvl; enqueue_bool st a ~level:lvl (Bcp clause) ) ) with Trivial -> - Log.debugf info - (fun k->k "(@[sat.add-clause@ :ignore-trivial @[%a@]@])" Clause.debug init) + Log.debugf info (fun k -> + k "(@[sat.add-clause@ :ignore-trivial @[%a@]@])" Clause.debug init) let[@inline never] flush_clauses_ st = while not @@ Vec.is_empty st.clauses_to_add do @@ -1621,24 +1693,25 @@ module Make(Plugin : PLUGIN) [i] is the index of [c] in [a.watched] @return whether [c] was removed from [a.watched] *) - let propagate_in_clause st (a:atom) (c:clause) (i:int): watch_res = + let propagate_in_clause st (a : atom) (c : clause) (i : int) : watch_res = let atoms = c.atoms in let first = atoms.(0) in if first == a.neg then ( (* false lit must be at index 1 *) atoms.(0) <- atoms.(1); atoms.(1) <- first - ) else ( - assert (a.neg == atoms.(1)) - ); + ) else + assert (a.neg == atoms.(1)); let first = atoms.(0) in - if first.is_true - then Watch_kept (* true clause, keep it in watched *) + if first.is_true then + Watch_kept + (* true clause, keep it in watched *) else ( - try (* look for another watch lit *) + try + (* look for another watch lit *) for k = 2 to Array.length atoms - 1 do let ak = atoms.(k) in - if not (ak.neg.is_true) then ( + if not ak.neg.is_true then ( (* watch lit found: update and exit *) atoms.(1) <- ak; atoms.(k) <- a.neg; @@ -1656,7 +1729,8 @@ module Make(Plugin : PLUGIN) raise_notrace (Conflict c) ) else ( match th_eval st first with - | None -> (* clause is unit, keep the same watches, but propagate *) + | None -> + (* clause is unit, keep the same watches, but propagate *) enqueue_bool st first ~level:(decision_level st) (Bcp c) | Some true -> () | Some false -> @@ -1664,8 +1738,7 @@ module Make(Plugin : PLUGIN) raise_notrace (Conflict c) ); Watch_kept - with Exit -> - Watch_removed + with Exit -> Watch_removed ) (* propagate atom [a], which was just decided. This checks every @@ -1675,7 +1748,8 @@ module Make(Plugin : PLUGIN) let propagate_atom st a : unit = let watched = a.watched in let rec aux i = - if i >= Vec.size watched then () + if i >= Vec.size watched then + () else ( let c = Vec.get watched i in assert (Clause.attached c); @@ -1685,7 +1759,7 @@ module Make(Plugin : PLUGIN) i ) else ( match propagate_in_clause st a c i with - | Watch_kept -> i+1 + | Watch_kept -> i + 1 | Watch_removed -> i (* clause at this index changed *) ) in @@ -1704,91 +1778,113 @@ module Make(Plugin : PLUGIN) let slice_get st i = match Vec.get st.trail i with - | Atom a -> - Solver_intf.Lit a.lit - | Lit {term; assigned = Some v; _} -> - Solver_intf.Assign (term, v) + | Atom a -> Solver_intf.Lit a.lit + | Lit { term; assigned = Some v; _ } -> Solver_intf.Assign (term, v) | Lit _ -> assert false - let acts_add_clause st ?(keep=false) (l:formula list) (lemma:lemma): unit = + let acts_add_clause st ?(keep = false) (l : formula list) (lemma : lemma) : + unit = let atoms = List.rev_map (create_atom st) l in - let flags = if keep then 0 else Clause.flag_removable in + let flags = + if keep then + 0 + else + Clause.flag_removable + in let c = Clause.make ~flags atoms (Lemma lemma) in - Log.debugf info (fun k->k "(@[sat.th.add-clause@ %a@])" Clause.debug c); + Log.debugf info (fun k -> k "(@[sat.th.add-clause@ %a@])" Clause.debug c); Vec.push st.clauses_to_add c - let acts_add_decision_lit (st:t) (f:formula) (sign:bool) : unit = + let acts_add_decision_lit (st : t) (f : formula) (sign : bool) : unit = let a = create_atom st f in - let a = if sign then a else Atom.neg a in + let a = + if sign then + a + else + Atom.neg a + in if not (Atom.has_value a) then ( - Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); + Log.debugf 10 (fun k -> + k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); st.next_decisions <- a :: st.next_decisions ) - let acts_raise st (l:formula list) proof : 'a = + let acts_raise st (l : formula list) proof : 'a = let atoms = List.rev_map (create_atom st) l in (* conflicts can be removed *) let c = Clause.make_removable atoms (Lemma proof) in - Log.debugf 5 (fun k->k "(@[@{sat.th.raise-conflict@}@ %a@])" Clause.debug c); + Log.debugf 5 (fun k -> + k "(@[@{sat.th.raise-conflict@}@ %a@])" Clause.debug c); raise_notrace (Th_conflict c) let check_consequence_lits_false_ l : unit = match List.find Atom.is_true l with | a -> invalid_argf - "slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't" + "slice.acts_propagate:@ Consequence should contain only true literals, \ + but %a isn't" Atom.debug (Atom.neg a) | exception Not_found -> () - let acts_propagate (st:t) f = function + let acts_propagate (st : t) f = function | Solver_intf.Eval l -> let a = mk_atom st f in enqueue_semantic st a l | Solver_intf.Consequence mk_expl -> let p = mk_atom st f in - if Atom.is_true p then () + if Atom.is_true p then + () else if Atom.is_false p then ( - let lits, proof = mk_expl() in + let lits, proof = mk_expl () in let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in check_consequence_lits_false_ l; let c = Clause.make_removable (p :: l) (Lemma proof) in raise_notrace (Th_conflict c) ) else ( insert_var_order st p.var; - let c = lazy ( - let lits, proof = mk_expl () in - let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in - (* note: we can check that invariant here in the [lazy] block, + let c = + lazy + (let lits, proof = mk_expl () in + let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in + (* note: we can check that invariant here in the [lazy] block, as conflict analysis will run in an environment where the literals should be true anyway, since it's an extension of the current trail (otherwise the propagated lit would have been backtracked and discarded already.) *) - check_consequence_lits_false_ l; - Clause.make_removable (p :: l) (Lemma proof) - ) in + check_consequence_lits_false_ l; + Clause.make_removable (p :: l) (Lemma proof)) + in let level = decision_level st in enqueue_bool st p ~level (Bcp_lazy c) ) let[@specialise] acts_iter st ~full head f : unit = - for i = (if full then 0 else head) to Vec.size st.trail-1 do - let e = match Vec.get st.trail i with - | Atom a -> - Solver_intf.Lit a.lit - | Lit {term; assigned = Some v; _} -> - Solver_intf.Assign (term, v) + for + i = + if full then + 0 + else + head to Vec.size st.trail - 1 + do + let e = + match Vec.get st.trail i with + | Atom a -> Solver_intf.Lit a.lit + | Lit { term; assigned = Some v; _ } -> Solver_intf.Assign (term, v) | Lit _ -> assert false in f e done let eval_atom_ a = - if Atom.is_true a then Solver_intf.L_true - else if Atom.is_false a then Solver_intf.L_false - else Solver_intf.L_undefined - - let[@inline] acts_eval_lit st (f:formula) : Solver_intf.lbool = + if Atom.is_true a then + Solver_intf.L_true + else if Atom.is_false a then + Solver_intf.L_false + else + Solver_intf.L_undefined + + let[@inline] acts_eval_lit st (f : formula) : Solver_intf.lbool = let a = create_atom st f in eval_atom_ a @@ -1797,36 +1893,35 @@ module Make(Plugin : PLUGIN) let[@inline] acts_mk_term st t : unit = make_term st t - let[@inline] current_slice st : _ Solver_intf.acts = { - Solver_intf. - acts_iter_assumptions=acts_iter st ~full:false st.th_head; - acts_eval_lit= acts_eval_lit st; - acts_mk_lit=acts_mk_lit st; - acts_mk_term=acts_mk_term st; - acts_add_clause = acts_add_clause st; - acts_propagate = acts_propagate st; - acts_raise_conflict=acts_raise st; - acts_add_decision_lit=acts_add_decision_lit st; - } + let[@inline] current_slice st : _ Solver_intf.acts = + { + Solver_intf.acts_iter_assumptions = acts_iter st ~full:false st.th_head; + acts_eval_lit = acts_eval_lit st; + acts_mk_lit = acts_mk_lit st; + acts_mk_term = acts_mk_term st; + acts_add_clause = acts_add_clause st; + acts_propagate = acts_propagate st; + acts_raise_conflict = acts_raise st; + acts_add_decision_lit = acts_add_decision_lit st; + } (* full slice, for [if_sat] final check *) - let[@inline] full_slice st : _ Solver_intf.acts = { - Solver_intf. - acts_iter_assumptions=acts_iter st ~full:true st.th_head; - acts_eval_lit= acts_eval_lit st; - acts_mk_lit=acts_mk_lit st; - acts_mk_term=acts_mk_term st; - acts_add_clause = acts_add_clause st; - acts_propagate = acts_propagate st; - acts_raise_conflict=acts_raise st; - acts_add_decision_lit=acts_add_decision_lit st; - } + let[@inline] full_slice st : _ Solver_intf.acts = + { + Solver_intf.acts_iter_assumptions = acts_iter st ~full:true st.th_head; + acts_eval_lit = acts_eval_lit st; + acts_mk_lit = acts_mk_lit st; + acts_mk_term = acts_mk_term st; + acts_add_clause = acts_add_clause st; + acts_propagate = acts_propagate st; + acts_raise_conflict = acts_raise st; + acts_add_decision_lit = acts_add_decision_lit st; + } (* Assert that the conflict is indeeed a conflict *) - let check_is_conflict_ (c:Clause.t) : unit = - if not @@ Array.for_all (Atom.is_false) c.atoms then ( + let check_is_conflict_ (c : Clause.t) : unit = + if not @@ Array.for_all Atom.is_false c.atoms then invalid_argf "conflict should be false: %a" Clause.debug c - ) (* some boolean literals were decided/propagated within Msat. Now we need to inform the theory of those assumptions, so it can do its job. @@ -1834,11 +1929,13 @@ module Make(Plugin : PLUGIN) let rec theory_propagate st : clause option = assert (st.elt_head = Vec.size st.trail); assert (st.th_head <= st.elt_head); - if st.th_head = st.elt_head then ( - None (* fixpoint/no propagation *) - ) else ( + if st.th_head = st.elt_head then + None + (* fixpoint/no propagation *) + else ( let slice = current_slice st in - st.th_head <- st.elt_head; (* catch up *) + st.th_head <- st.elt_head; + (* catch up *) match Plugin.partial_check st.th slice with | () -> flush_clauses st; @@ -1851,65 +1948,67 @@ module Make(Plugin : PLUGIN) (* fixpoint between boolean propagation and theory propagation @return a conflict clause, if any *) - and propagate (st:t) : clause option = + and propagate (st : t) : clause option = (* First, treat the stack of lemmas added by the theory, if any *) flush_clauses st; (* Now, check that the situation is sane *) assert (st.elt_head <= Vec.size st.trail); - if st.elt_head = Vec.size st.trail then ( + if st.elt_head = Vec.size st.trail then theory_propagate st - ) else ( + else ( match while st.elt_head < Vec.size st.trail do - begin match Vec.get st.trail st.elt_head with - | Lit _ -> () - | Atom a -> propagate_atom st a - end; - st.elt_head <- st.elt_head + 1; - done; + (match Vec.get st.trail st.elt_head with + | Lit _ -> () + | Atom a -> propagate_atom st a); + st.elt_head <- st.elt_head + 1 + done with | () -> theory_propagate st | exception Conflict c -> Some c ) (* compute unsat core from assumption [a] *) - let analyze_final (self:t) (a:atom) : atom list = - Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a); + let analyze_final (self : t) (a : atom) : atom list = + Log.debugf 5 (fun k -> k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a); assert (Atom.is_false a); - let core = ref [a] in + let core = ref [ a ] in let idx = ref (Vec.size self.trail - 1) in Var.mark a.var; - let seen = ref [a.var] in + let seen = ref [ a.var ] in while !idx >= 0 do - begin match Vec.get self.trail !idx with - | Lit _ -> () (* semantic decision, ignore *) - | Atom a' -> - if Var.marked a'.var then ( - match Atom.reason a' with - | Some Semantic -> () - | Some Decision -> core := a' :: !core - | Some (Bcp c | Bcp_lazy (lazy c)) -> - Array.iter - (fun a -> - let v = a.var in - if not @@ Var.marked v then ( - seen := v :: !seen; - Var.mark v; - )) - c.atoms - | None -> () - ); - end; + (match Vec.get self.trail !idx with + | Lit _ -> () (* semantic decision, ignore *) + | Atom a' -> + if Var.marked a'.var then ( + match Atom.reason a' with + | Some Semantic -> () + | Some Decision -> core := a' :: !core + | Some (Bcp c | Bcp_lazy (lazy c)) -> + Array.iter + (fun a -> + let v = a.var in + if not @@ Var.marked v then ( + seen := v :: !seen; + Var.mark v + )) + c.atoms + | None -> () + )); decr idx done; List.iter Var.unmark !seen; - Log.debugf 5 (fun k->k "(@[sat.analyze-final.done@ :core %a@])" (Format.pp_print_list Atom.debug) !core); + Log.debugf 5 (fun k -> + k "(@[sat.analyze-final.done@ :core %a@])" + (Format.pp_print_list Atom.debug) + !core); !core (* remove some learnt clauses. *) - let reduce_db (st:t) (n_of_learnts: int) : unit = + let reduce_db (st : t) (n_of_learnts : int) : unit = let v = st.clauses_learnt in - Log.debugf 3 (fun k->k "(@[sat.gc.start :keep %d :out-of %d@])" n_of_learnts (Vec.size v)); + Log.debugf 3 (fun k -> + k "(@[sat.gc.start :keep %d :out-of %d@])" n_of_learnts (Vec.size v)); assert (Vec.size v > n_of_learnts); (* sort by decreasing activity *) Vec.sort v (fun c1 c2 -> compare c2.activity c1.activity); @@ -1919,9 +2018,9 @@ module Make(Plugin : PLUGIN) assert (Clause.removable c); Clause.set_dead c; assert (Clause.dead c); - incr n_collected; + incr n_collected done; - Log.debugf 3 (fun k->k "(@[sat.gc.done :collected %d@])" !n_collected); + Log.debugf 3 (fun k -> k "(@[sat.gc.done :collected %d@])" !n_collected); () (* Decide on a new literal, and enqueue it into the trail *) @@ -1936,15 +2035,24 @@ module Make(Plugin : PLUGIN) new_decision_level st; let current_level = decision_level st in enqueue_bool st atom ~level:current_level Decision; - (match st.on_decision with Some f -> f atom | None -> ()); + (match st.on_decision with + | Some f -> f atom + | None -> ()) | Solver_intf.Valued (b, l) -> - let a = if b then atom else atom.neg in + let a = + if b then + atom + else + atom.neg + in enqueue_semantic st a l ) else ( new_decision_level st; let current_level = decision_level st in enqueue_bool st atom ~level:current_level Decision; - (match st.on_decision with Some f -> f atom | None -> ()); + match st.on_decision with + | Some f -> f atom + | None -> () ) and pick_branch_lit st = @@ -1956,53 +2064,59 @@ module Make(Plugin : PLUGIN) (* use an assumption *) let a = Vec.get st.assumptions (decision_level st) in if Atom.is_true a then ( - new_decision_level st; (* pseudo decision level, [a] is already true *) + new_decision_level st; + (* pseudo decision level, [a] is already true *) pick_branch_lit st ) else if Atom.is_false a then ( (* root conflict, find unsat core *) let core = analyze_final st a in - raise (E_unsat (US_local {first=a; core})) - ) else ( + raise (E_unsat (US_local { first = a; core })) + ) else pick_branch_aux st a - ) | [] -> - begin match H.remove_min st.order with - | E_lit l -> - if Lit.level l >= 0 then ( - pick_branch_lit st - ) else ( - let value = Plugin.assign st.th l.term in - new_decision_level st; - let current_level = decision_level st in - enqueue_assign st l value current_level - ) - | E_var v -> - pick_branch_aux st (if Var.default_pol v then v.pa else v.na) - | exception Not_found -> raise_notrace E_sat - end + (match H.remove_min st.order with + | E_lit l -> + if Lit.level l >= 0 then + pick_branch_lit st + else ( + let value = Plugin.assign st.th l.term in + new_decision_level st; + let current_level = decision_level st in + enqueue_assign st l value current_level + ) + | E_var v -> + pick_branch_aux st + (if Var.default_pol v then + v.pa + else + v.na) + | exception Not_found -> raise_notrace E_sat) (* do some amount of search, until the number of conflicts or clause learnt reaches the given parameters *) - let search (st:t) n_of_conflicts n_of_learnts : unit = - Log.debugf 3 - (fun k->k "(@[sat.search@ :n-conflicts %d@ :n-learnt %d@])" n_of_conflicts n_of_learnts); + let search (st : t) n_of_conflicts n_of_learnts : unit = + Log.debugf 3 (fun k -> + k "(@[sat.search@ :n-conflicts %d@ :n-learnt %d@])" n_of_conflicts + n_of_learnts); let conflictC = ref 0 in while true do match propagate st with - | Some confl -> (* Conflict *) + | Some confl -> + (* Conflict *) incr conflictC; (* When the theory has raised Unsat, add_boolean_conflict might 'forget' the initial conflict clause, and only add the analyzed backtrack clause. So in those case, we use add_clause to make sure the initial conflict clause is also added. *) - if Clause.attached confl then ( + if Clause.attached confl then add_boolean_conflict st confl - ) else ( - add_clause_ st confl - ); - (match st.on_conflict with Some f -> f confl.atoms | None -> ()); - - | None -> (* No Conflict *) + else + add_clause_ st confl; + (match st.on_conflict with + | Some f -> f confl.atoms + | None -> ()) + | None -> + (* No Conflict *) assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = st.th_head); if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( @@ -2010,206 +2124,224 @@ module Make(Plugin : PLUGIN) cancel_until st 0; raise_notrace Restart ); - (* if decision_level() = 0 then simplify (); *) - if n_of_learnts > 0 && - Vec.size st.clauses_learnt - Vec.size st.trail > n_of_learnts then ( + (* if decision_level() = 0 then simplify (); *) + if + n_of_learnts > 0 + && Vec.size st.clauses_learnt - Vec.size st.trail > n_of_learnts + then reduce_db st n_of_learnts; - ); pick_branch_lit st done - let eval_level (_st:t) (a:atom) = + let eval_level (_st : t) (a : atom) = let lvl = a.var.v_level in if Atom.is_true a then ( assert (lvl >= 0); true, lvl - ) else if Atom.is_false a then ( + ) else if Atom.is_false a then false, lvl - ) else ( + else raise UndecidedLit - ) let[@inline] eval st lit = fst @@ eval_level st lit - let[@inline] unsat_conflict st = st.unsat_at_0 - let model (st:t) : (term * value) list = - let opt = function Some a -> a | None -> assert false in + let model (st : t) : (term * value) list = + let opt = function + | Some a -> a + | None -> assert false + in Vec.fold - (fun acc e -> match e with - | Lit v -> (v.term, opt v.assigned) :: acc - | Atom _ -> acc) + (fun acc e -> + match e with + | Lit v -> (v.term, opt v.assigned) :: acc + | Atom _ -> acc) [] st.trail (* fixpoint of propagation and decisions until a model is found, or a conflict is reached *) - let solve_ (st:t) : unit = - Log.debugf 5 (fun k->k "(@[sat.solve :assms %d@])" (Vec.size st.assumptions)); + let solve_ (st : t) : unit = + Log.debugf 5 (fun k -> + k "(@[sat.solve :assms %d@])" (Vec.size st.assumptions)); check_unsat_ st; try - flush_clauses st; (* add initial clauses *) + flush_clauses st; + (* add initial clauses *) let n_of_conflicts = ref (float_of_int restart_first) in - let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in + let n_of_learnts = + ref (float_of_int (nb_clauses st) *. learntsize_factor) + in while true do - begin try - search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) - with - | Restart -> - n_of_conflicts := !n_of_conflicts *. restart_inc; - n_of_learnts := !n_of_learnts *. learntsize_inc - | E_sat -> - assert (st.elt_head = Vec.size st.trail && - Vec.is_empty st.clauses_to_add && - st.next_decisions=[]); - begin match Plugin.final_check st.th (full_slice st) with - | () -> - if st.elt_head = Vec.size st.trail && - Vec.is_empty st.clauses_to_add && - st.next_decisions = [] - then ( - raise_notrace E_sat - ); - (* otherwise, keep on *) - flush_clauses st; - | exception Th_conflict c -> - check_is_conflict_ c; - Array.iter (fun a -> insert_elt_order st (Elt.of_var a.var)) c.atoms; - Log.debugf info (fun k -> k "(@[sat.theory-conflict-clause@ %a@])" Clause.debug c); - (match st.on_conflict with Some f -> f c.atoms | None -> ()); - Vec.push st.clauses_to_add c; - flush_clauses st; - end; - end + try + search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) + with + | Restart -> + n_of_conflicts := !n_of_conflicts *. restart_inc; + n_of_learnts := !n_of_learnts *. learntsize_inc + | E_sat -> + assert ( + st.elt_head = Vec.size st.trail + && Vec.is_empty st.clauses_to_add + && st.next_decisions = []); + (match Plugin.final_check st.th (full_slice st) with + | () -> + if + st.elt_head = Vec.size st.trail + && Vec.is_empty st.clauses_to_add + && st.next_decisions = [] + then + raise_notrace E_sat; + (* otherwise, keep on *) + flush_clauses st + | exception Th_conflict c -> + check_is_conflict_ c; + Array.iter (fun a -> insert_elt_order st (Elt.of_var a.var)) c.atoms; + Log.debugf info (fun k -> + k "(@[sat.theory-conflict-clause@ %a@])" Clause.debug c); + (match st.on_conflict with + | Some f -> f c.atoms + | None -> ()); + Vec.push st.clauses_to_add c; + flush_clauses st) done with E_sat -> () let assume st cnf lemma = List.iter (fun l -> - let atoms = List.rev_map (mk_atom st) l in - let c = Clause.make_permanent atoms (Hyp lemma) in - Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" Clause.debug c); - Vec.push st.clauses_to_add c) + let atoms = List.rev_map (mk_atom st) l in + let c = Clause.make_permanent atoms (Hyp lemma) in + Log.debugf debug (fun k -> + k "(@[sat.assume-clause@ @[%a@]@])" Clause.debug c); + Vec.push st.clauses_to_add c) cnf (* Check satisfiability *) let check_clause c = let res = Array.exists (fun a -> a.is_true) c.atoms in if not res then ( - Log.debugf debug - (fun k -> k "(@[sat.check-clause@ :not-satisfied @[%a@]@])" Clause.debug c); + Log.debugf debug (fun k -> + k "(@[sat.check-clause@ :not-satisfied @[%a@]@])" Clause.debug c); false ) else true let check_vec v = Vec.for_all check_clause v + let check st : bool = - Vec.is_empty st.clauses_to_add && - check_vec st.clauses_hyps && - check_vec st.clauses_learnt + Vec.is_empty st.clauses_to_add + && check_vec st.clauses_hyps + && check_vec st.clauses_learnt let[@inline] theory st = st.th (* Unsafe access to internal data *) let hyps env = env.clauses_hyps - let history env = env.clauses_learnt - let trail env = env.trail (* Result type *) type res = - | Sat of (term,Formula.t,value) Solver_intf.sat_state - | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state + | Sat of (term, Formula.t, value) Solver_intf.sat_state + | Unsat of (atom, clause, Proof.t) Solver_intf.unsat_state let pp_all st lvl status = - Log.debugf lvl - (fun k -> k - "(@[sat.full-state :res %s - Full summary:@,@[Trail:@\n%a@]@,\ - @[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." + Log.debugf lvl (fun k -> + k + "(@[sat.full-state :res %s - Full summary:@,\ + @[Trail:@\n\ + %a@]@,\ + @[Hyps:@\n\ + %a@]@,\ + @[Lemmas:@\n\ + %a@]@,\ + @]@." status - (Vec.pp ~sep:"" Trail_elt.debug) (trail st) - (Vec.pp ~sep:"" Clause.debug) (hyps st) - (Vec.pp ~sep:"" Clause.debug) (history st) - ) - - let mk_sat (st:t) : (Term.t, Formula.t, _) Solver_intf.sat_state = + (Vec.pp ~sep:"" Trail_elt.debug) + (trail st) + (Vec.pp ~sep:"" Clause.debug) + (hyps st) + (Vec.pp ~sep:"" Clause.debug) + (history st)) + + let mk_sat (st : t) : (Term.t, Formula.t, _) Solver_intf.sat_state = pp_all st 99 "SAT"; let t = trail st in let iter_trail f f' = - Vec.iter (function + Vec.iter + (function | Atom a -> f (Atom.formula a) | Lit l -> f' l.term) t in let[@inline] eval f = eval st (mk_atom st f) in let[@inline] eval_level f = eval_level st (mk_atom st f) in - { Solver_intf. - eval; eval_level; iter_trail; - model = (fun () -> model st); - } + { Solver_intf.eval; eval_level; iter_trail; model = (fun () -> model st) } - let mk_unsat (st:t) (us: unsat_cause) : _ Solver_intf.unsat_state = + let mk_unsat (st : t) (us : unsat_cause) : _ Solver_intf.unsat_state = pp_all st 99 "UNSAT"; - let unsat_assumptions () = match us with - | US_local {first=_; core} -> core + let unsat_assumptions () = + match us with + | US_local { first = _; core } -> core | _ -> [] in - let unsat_conflict = match us with - | US_false c -> fun() -> c - | US_local {core=[]; _} -> assert false - | US_local {first; core} -> - let c = lazy ( - let core = List.rev core in (* increasing trail order *) - assert (Atom.equal first @@ List.hd core); - let proof_of (a:atom) = match Atom.reason a with - | Some (Decision | Semantic) -> Clause.make_removable [a] Local - | Some (Bcp c | Bcp_lazy (lazy c)) -> c - | None -> assert false - in - let other_lits = List.filter (fun a -> not (Atom.equal a first)) core in - let hist = - Clause.make_permanent [first] Local :: - proof_of first :: - List.map proof_of other_lits in - Clause.make_permanent [] (History hist) - ) in + let unsat_conflict = + match us with + | US_false c -> fun () -> c + | US_local { core = []; _ } -> assert false + | US_local { first; core } -> + let c = + lazy + (let core = List.rev core in + (* increasing trail order *) + assert (Atom.equal first @@ List.hd core); + let proof_of (a : atom) = + match Atom.reason a with + | Some (Decision | Semantic) -> Clause.make_removable [ a ] Local + | Some (Bcp c | Bcp_lazy (lazy c)) -> c + | None -> assert false + in + let other_lits = + List.filter (fun a -> not (Atom.equal a first)) core + in + let hist = + Clause.make_permanent [ first ] Local + :: proof_of first + :: List.map proof_of other_lits + in + Clause.make_permanent [] (History hist)) + in fun () -> Lazy.force c in let get_proof () = let c = unsat_conflict () in Proof.prove c in - { Solver_intf.unsat_conflict; get_proof; unsat_assumptions; } + { Solver_intf.unsat_conflict; get_proof; unsat_assumptions } let add_clause_a st c lemma : unit = try let c = Clause.make_a ~flags:0 c (Hyp lemma) in add_clause_ st c - with - | E_unsat (US_false c) -> - st.unsat_at_0 <- Some c + with E_unsat (US_false c) -> st.unsat_at_0 <- Some c let add_clause st c lemma : unit = try let c = Clause.make_permanent c (Hyp lemma) in add_clause_ st c - with - | E_unsat (US_false c) -> - st.unsat_at_0 <- Some c + with E_unsat (US_false c) -> st.unsat_at_0 <- Some c - let solve ?(assumptions=[]) (st:t) : res = + let solve ?(assumptions = []) (st : t) : res = cancel_until st 0; Vec.clear st.assumptions; List.iter (Vec.push st.assumptions) assumptions; try solve_ st; Sat (mk_sat st) - with E_unsat us -> - Unsat (mk_unsat st us) + with E_unsat us -> Unsat (mk_unsat st us) let true_at_level0 st a = try @@ -2219,48 +2351,50 @@ module Make(Plugin : PLUGIN) let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a - let export (st:t) : clause Solver_intf.export = + let export (st : t) : clause Solver_intf.export = let hyps = hyps st in let history = history st in - {Solver_intf.hyps; history; } + { Solver_intf.hyps; history } end -[@@inline][@@specialise] +[@@inline] [@@specialise] - module Void_ = struct - type t = Solver_intf.void - let equal _ _ = assert false - let hash _ = assert false - let pp _ _ = assert false - end +module Void_ = struct + type t = Solver_intf.void -module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) = - Make(struct - include Plugin - module Term = Void_ - module Value = Void_ - let eval _ _ = Solver_intf.Unknown - let assign _ t = t - let mcsat = false - let has_theory = true - let iter_assignable _ _ _ = () - end) -[@@inline][@@specialise] + let equal _ _ = assert false + let hash _ = assert false + let pp _ _ = assert false +end -module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) = - Make(struct - include Plugin - let mcsat = true - let has_theory = false - end) -[@@inline][@@specialise] +module Make_cdcl_t (Plugin : Solver_intf.PLUGIN_CDCL_T) = Make (struct + include Plugin + module Term = Void_ + module Value = Void_ + + let eval _ _ = Solver_intf.Unknown + let assign _ t = t + let mcsat = false + let has_theory = true + let iter_assignable _ _ _ = () +end) +[@@inline] [@@specialise] + +module Make_mcsat (Plugin : Solver_intf.PLUGIN_MCSAT) = Make (struct + include Plugin -module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) = - Make(struct + let mcsat = true + let has_theory = false +end) +[@@inline] [@@specialise] + +module Make_pure_sat (Plugin : Solver_intf.PLUGIN_SAT) = Make (struct module Formula = Plugin.Formula module Term = Void_ module Value = Void_ + type t = unit type proof = Plugin.proof + let push_level () = () let pop_levels _ _ = () let partial_check () _ = () @@ -2272,5 +2406,4 @@ module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) = let iter_assignable () _ _ = () let mcsat = false end) -[@@inline][@@specialise] - +[@@inline] [@@specialise] diff --git a/src/core/Log.ml b/src/core/Log.ml index f60603ea..c0318e57 100644 --- a/src/core/Log.ml +++ b/src/core/Log.ml @@ -7,27 +7,17 @@ Copyright 2014 Simon Cruanes (** {1 Logging functions, real version} *) let enabled = true (* NOTE: change here for 0-overhead *) - let debug_level_ = ref 0 let set_debug l = debug_level_ := l let get_debug () = !debug_level_ - let debug_fmt_ = ref Format.err_formatter - let set_debug_out f = debug_fmt_ := f (* does the printing, inconditionally *) let debug_real_ l k = k (fun fmt -> - Format.fprintf !debug_fmt_ "@[<2>@{[%d|%.3f]@}@ " - l (Sys.time()); - Format.kfprintf - (fun fmt -> Format.fprintf fmt "@]@.") - !debug_fmt_ fmt) - -let[@inline] debugf l k = - if enabled && l <= !debug_level_ then ( - debug_real_ l k; - ) + Format.fprintf !debug_fmt_ "@[<2>@{[%d|%.3f]@}@ " l (Sys.time ()); + Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@.") !debug_fmt_ fmt) -let[@inline] debug l msg = debugf l (fun k->k "%s" msg) +let[@inline] debugf l k = if enabled && l <= !debug_level_ then debug_real_ l k +let[@inline] debug l msg = debugf l (fun k -> k "%s" msg) diff --git a/src/core/Log.mli b/src/core/Log.mli index 8923f8e3..a82a389f 100644 --- a/src/core/Log.mli +++ b/src/core/Log.mli @@ -8,19 +8,19 @@ Copyright 2014 Simon Cruanes val enabled : bool -val set_debug : int -> unit (** Set debug level *) -val get_debug : unit -> int (** Current debug level *) +val set_debug : int -> unit +(** Set debug level *) + +val get_debug : unit -> int +(** Current debug level *) val debugf : - int -> - ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) -> - unit -(** Emit a debug message at the given level. If the level is lower - than [get_debug ()], the message will indeed be emitted *) + int -> ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) -> unit +(** Emit a debug message at the given level. If the level is lower than + [get_debug ()], the message will indeed be emitted *) val debug : int -> string -> unit (** Simpler version of {!debug}, without formatting *) val set_debug_out : Format.formatter -> unit (** Change the output formatter. *) - diff --git a/src/core/Msat.ml b/src/core/Msat.ml index fb049615..cadf7d34 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -1,6 +1,5 @@ (** Main API *) - module Solver_intf = Solver_intf module type S = Solver_intf.S @@ -10,48 +9,59 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT module type PROOF = Solver_intf.PROOF +type void = (unit, bool) Solver_intf.gadt_eq (** Empty type *) -type void = (unit,bool) Solver_intf.gadt_eq - -type lbool = Solver_intf.lbool = L_true | L_false | L_undefined -type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = { - eval : 'form -> bool; - eval_level : 'form -> bool * int; - iter_trail : ('form -> unit) -> ('term -> unit) -> unit; - model : unit -> ('term * 'value) list; +type lbool = Solver_intf.lbool = + | L_true + | L_false + | L_undefined + +type ('term, 'form, 'value) sat_state = + ('term, 'form, 'value) Solver_intf.sat_state = { + eval: 'form -> bool; + eval_level: 'form -> bool * int; + iter_trail: ('form -> unit) -> ('term -> unit) -> unit; + model: unit -> ('term * 'value) list; } -type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = { - unsat_conflict : unit -> 'clause; - get_proof : unit -> 'proof; +type ('atom, 'clause, 'proof) unsat_state = + ('atom, 'clause, 'proof) Solver_intf.unsat_state = { + unsat_conflict: unit -> 'clause; + get_proof: unit -> 'proof; unsat_assumptions: unit -> 'atom list; } + type 'clause export = 'clause Solver_intf.export = { - hyps : 'clause Vec.t; - history : 'clause Vec.t; + hyps: 'clause Vec.t; + history: 'clause Vec.t; } -type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption = +type ('term, 'formula, 'value) assumption = + ('term, 'formula, 'value) Solver_intf.assumption = | Lit of 'formula (** The given formula is asserted true by the solver *) - | Assign of 'term * 'value (** The term is assigned to the value *) + | Assign of 'term * 'value (** The term is assigned to the value *) -type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason = +type ('term, 'formula, 'proof) reason = + ('term, 'formula, 'proof) Solver_intf.reason = | Eval of 'term list | Consequence of (unit -> 'formula list * 'proof) -type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = { - acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit; +type ('term, 'formula, 'value, 'proof) acts = + ('term, 'formula, 'value, 'proof) Solver_intf.acts = { + acts_iter_assumptions: (('term, 'formula, 'value) assumption -> unit) -> unit; acts_eval_lit: 'formula -> lbool; acts_mk_lit: ?default_pol:bool -> 'formula -> unit; acts_mk_term: 'term -> unit; - acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; + acts_add_clause: ?keep:bool -> 'formula list -> 'proof -> unit; acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; - acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; + acts_propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit; acts_add_decision_lit: 'formula -> bool -> unit; } -type negated = Solver_intf.negated = Negated | Same_sign +type negated = Solver_intf.negated = + | Negated + | Same_sign (** Print {!negated} values *) let pp_negated out = function @@ -71,6 +81,8 @@ module Make_cdcl_t = Solver.Make_cdcl_t module Make_pure_sat = Solver.Make_pure_sat (**/**) + module Vec = Vec module Log = Log + (**/**) diff --git a/src/core/Solver.ml b/src/core/Solver.ml index 5863de2a..69709874 100644 --- a/src/core/Solver.ml +++ b/src/core/Solver.ml @@ -9,4 +9,3 @@ module type S = Solver_intf.S module Make_cdcl_t = Internal.Make_cdcl_t module Make_mcsat = Internal.Make_mcsat module Make_pure_sat = Internal.Make_pure_sat - diff --git a/src/core/Solver.mli b/src/core/Solver.mli index b256a4a8..72a8e1d9 100644 --- a/src/core/Solver.mli +++ b/src/core/Solver.mli @@ -6,29 +6,29 @@ Copyright 2014 Simon Cruanes (** mSAT safe interface - This module defines a safe interface for the core solver. - It is the basis of the {!module:Solver} and {!module:Mcsolver} modules. -*) + This module defines a safe interface for the core solver. It is the basis of + the {!module:Solver} and {!module:Mcsolver} modules. *) module type S = Solver_intf.S (** Safe external interface of solvers. *) -module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T) - : S with type Term.t = Solver_intf.void - and module Formula = Th.Formula - and type lemma = Th.proof - and type theory = Th.t - -module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT) - : S with module Term = Th.Term - and module Formula = Th.Formula - and type lemma = Th.proof - and type theory = Th.t - -module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT) - : S with type Term.t = Solver_intf.void - and module Formula = Th.Formula - and type lemma = Th.proof - and type theory = unit - - +module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : + S + with type Term.t = Solver_intf.void + and module Formula = Th.Formula + and type lemma = Th.proof + and type theory = Th.t + +module Make_mcsat (Th : Solver_intf.PLUGIN_MCSAT) : + S + with module Term = Th.Term + and module Formula = Th.Formula + and type lemma = Th.proof + and type theory = Th.t + +module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : + S + with type Term.t = Solver_intf.void + and module Formula = Th.Formula + and type lemma = Th.proof + and type theory = unit diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index ab375a4d..c1841dda 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -6,39 +6,39 @@ Copyright 2016 Simon Cruanes (** Interface for Solvers - This modules defines the safe external interface for solvers. - Solvers that implements this interface can be obtained using the [Make] - functor in {!Solver} or {!Mcsolver}. -*) + This modules defines the safe external interface for solvers. Solvers that + implements this interface can be obtained using the [Make] functor in + {!Solver} or {!Mcsolver}. *) type 'a printer = Format.formatter -> 'a -> unit type ('term, 'form, 'value) sat_state = { eval: 'form -> bool; - (** Returns the valuation of a formula in the current state - of the sat solver. - @raise UndecidedLit if the literal is not decided *) + (** Returns the valuation of a formula in the current state of the sat + solver. + @raise UndecidedLit if the literal is not decided *) eval_level: 'form -> bool * int; - (** Return the current assignement of the literals, as well as its - decision level. If the level is 0, then it is necessary for - the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. - @raise UndecidedLit if the literal is not decided *) - iter_trail : ('form -> unit) -> ('term -> unit) -> unit; - (** Iter thorugh the formulas and terms in order of decision/propagation - (starting from the first propagation, to the last propagation). *) + (** Return the current assignement of the literals, as well as its + decision level. If the level is 0, then it is necessary for the atom + to have this value; otherwise it is due to choices that can + potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) + iter_trail: ('form -> unit) -> ('term -> unit) -> unit; + (** Iter thorugh the formulas and terms in order of decision/propagation + (starting from the first propagation, to the last propagation). *) model: unit -> ('term * 'value) list; - (** Returns the model found if the formula is satisfiable. *) + (** Returns the model found if the formula is satisfiable. *) } (** The type of values returned when the solver reaches a SAT state. *) type ('atom, 'clause, 'proof) unsat_state = { - unsat_conflict : unit -> 'clause; - (** Returns the unsat clause found at the toplevel *) - get_proof : unit -> 'proof; - (** returns a persistent proof of the empty clause from the Unsat result. *) + unsat_conflict: unit -> 'clause; + (** Returns the unsat clause found at the toplevel *) + get_proof: unit -> 'proof; + (** returns a persistent proof of the empty clause from the Unsat result. + *) unsat_assumptions: unit -> 'atom list; - (** Subset of assumptions responsible for "unsat" *) + (** Subset of assumptions responsible for "unsat" *) } (** The type of values returned when the solver reaches an UNSAT state. *) @@ -48,100 +48,95 @@ type 'clause export = { } (** Export internal state *) +(** This type is used during the normalisation of formulas. See + {!val:Expr_intf.S.norm} for more details. *) type negated = - | Negated (** changed sign *) - | Same_sign (** kept sign *) -(** This type is used during the normalisation of formulas. - See {!val:Expr_intf.S.norm} for more details. *) + | Negated (** changed sign *) + | Same_sign (** kept sign *) -type 'term eval_res = - | Unknown (** The given formula does not have an evaluation *) - | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. - The list of terms to give is the list of terms that - were effectively used for the evaluation. *) -(** The type of evaluation results for a given formula. - For instance, let's suppose we want to evaluate the formula [x * y = 0], the - following result are correct: +(** The type of evaluation results for a given formula. For instance, let's + suppose we want to evaluate the formula [x * y = 0], the following result + are correct: - [Unknown] if neither [x] nor [y] are assigned to a value - [Valued (true, [x])] if [x] is assigned to [0] - [Valued (true, [y])] if [y] is assigned to [0] - - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number) -*) + - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero + number) *) +type 'term eval_res = + | Unknown (** The given formula does not have an evaluation *) + | Valued of bool * 'term list + (** The given formula can be evaluated to the given bool. The list of + terms to give is the list of terms that were effectively used for the + evaluation. *) +(** Asusmptions made by the core SAT solver. *) type ('term, 'formula, 'value) assumption = | Lit of 'formula (** The given formula is asserted true by the solver *) - | Assign of 'term * 'value (** The term is assigned to the value *) -(** Asusmptions made by the core SAT solver. *) + | Assign of 'term * 'value (** The term is assigned to the value *) +(** The type of reasons for propagations of a formula [f]. *) type ('term, 'formula, 'proof) reason = | Eval of 'term list - (** The formula can be evalutaed using the terms in the list *) + (** The formula can be evalutaed using the terms in the list *) | Consequence of (unit -> 'formula list * 'proof) - (** [Consequence (l, p)] means that the formulas in [l] imply the propagated - formula [f]. The proof should be a proof of the clause "[l] implies [f]". - - invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in - the current trail. - - {b note} on lazyiness: the justification is suspended (using [unit -> …]) - to avoid potentially costly computations that might never be used - if this literal is backtracked without participating in a conflict. - Therefore the function that produces [(l,p)] needs only be safe in - trails (partial models) that are conservative extensions of the current - trail. - If the theory isn't robust w.r.t. extensions of the trail (e.g. if - its internal state undergoes significant changes), - it can be easier to produce the explanation eagerly when - propagating, and then use [Consequence (fun () -> expl, proof)] with - the already produced [(expl,proof)] tuple. - *) -(** The type of reasons for propagations of a formula [f]. *) - -type lbool = L_true | L_false | L_undefined -(** Valuation of an atom *) + (** [Consequence (l, p)] means that the formulas in [l] imply the + propagated formula [f]. The proof should be a proof of the clause "[l] + implies [f]". + + invariant: in [Consequence (fun () -> l,p)], all elements of [l] must + be true in the current trail. + + {b note} on lazyiness: the justification is suspended (using + [unit -> …]) to avoid potentially costly computations that might never + be used if this literal is backtracked without participating in a + conflict. Therefore the function that produces [(l,p)] needs only be + safe in trails (partial models) that are conservative extensions of + the current trail. If the theory isn't robust w.r.t. extensions of the + trail (e.g. if its internal state undergoes significant changes), it + can be easier to produce the explanation eagerly when propagating, and + then use [Consequence (fun () -> expl, proof)] with the already + produced [(expl,proof)] tuple. *) + +type lbool = + | L_true + | L_false + | L_undefined (** Valuation of an atom *) (* TODO: find a way to use atoms instead of formulas here *) type ('term, 'formula, 'value, 'proof) acts = { - acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit; - (** Traverse the new assumptions on the boolean trail. *) - + acts_iter_assumptions: (('term, 'formula, 'value) assumption -> unit) -> unit; + (** Traverse the new assumptions on the boolean trail. *) acts_eval_lit: 'formula -> lbool; - (** Obtain current value of the given literal *) - + (** Obtain current value of the given literal *) acts_mk_lit: ?default_pol:bool -> 'formula -> unit; - (** Map the given formula to a literal, which will be decided by the - SAT solver. *) - + (** Map the given formula to a literal, which will be decided by the SAT + solver. *) acts_mk_term: 'term -> unit; - (** Map the given term (and its subterms) to decision variables, - for the MCSAT solver to decide. *) - + (** Map the given term (and its subterms) to decision variables, for the + MCSAT solver to decide. *) acts_add_clause: ?keep:bool -> 'formula list -> 'proof -> unit; - (** Add a clause to the solver. - @param keep if true, the clause will be kept by the solver. - Otherwise the solver is allowed to GC the clause and propose this - partial model again. - *) - + (** Add a clause to the solver. + @param keep + if true, the clause will be kept by the solver. Otherwise the solver + is allowed to GC the clause and propose this partial model again. *) acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; - (** Raise a conflict, yielding control back to the solver. - The list of atoms must be a valid theory lemma that is false in the - current trail. *) - + (** Raise a conflict, yielding control back to the solver. The list of + atoms must be a valid theory lemma that is false in the current trail. + *) acts_propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit; - (** Propagate a formula, i.e. the theory can evaluate the formula to be true - (see the definition of {!type:eval_res} *) - + (** Propagate a formula, i.e. the theory can evaluate the formula to be + true (see the definition of {!type:eval_res} *) acts_add_decision_lit: 'formula -> bool -> unit; - (** Ask the SAT solver to decide on the given formula with given sign - before it can answer [SAT]. The order of decisions is still unspecified. - Useful for theory combination. This will be undone on backtracking. *) + (** Ask the SAT solver to decide on the given formula with given sign + before it can answer [SAT]. The order of decisions is still + unspecified. Useful for theory combination. This will be undone on + backtracking. *) } (** The type for a slice of assertions to assume/propagate in the theory. *) type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq -type void = (unit,bool) gadt_eq +type void = (unit, bool) gadt_eq (** A provably empty type *) exception No_proof @@ -156,20 +151,20 @@ module type FORMULA = sig (** Equality over formulas. *) val hash : t -> int - (** Hashing function for formulas. Should be such that two formulas equal according - to {!val:Expr_intf.S.equal} have the same hash. *) + (** Hashing function for formulas. Should be such that two formulas equal + according to {!val:Expr_intf.S.equal} have the same hash. *) val pp : t printer - (** Printing function used among other thing for debugging. *) + (** Printing function used among other thing for debugging. *) val neg : t -> t (** Formula negation *) val norm : t -> t * negated - (** Returns a 'normalized' form of the formula, possibly negated - (in which case return [Negated]). - [norm] must be so that [a] and [neg a] normalise to the same formula, - but one returns [Negated] and the other [Same_sign]. *) + (** Returns a 'normalized' form of the formula, possibly negated (in which + case return [Negated]). [norm] must be so that [a] and [neg a] normalise + to the same formula, but one returns [Negated] and the other [Same_sign]. + *) end (** Formulas and Terms required for mcSAT *) @@ -185,8 +180,8 @@ module type EXPR = sig (** Equality over terms. *) val hash : t -> int - (** Hashing function for terms. Should be such that two terms equal according - to {!equal} have the same hash. *) + (** Hashing function for terms. Should be such that two terms equal + according to {!equal} have the same hash. *) val pp : t printer (** Printing function used among other for debugging. *) @@ -219,15 +214,15 @@ module type PLUGIN_CDCL_T = sig (** Pop [n] levels of the theory *) val partial_check : t -> (void, Formula.t, void, proof) acts -> unit - (** Assume the formulas in the slice, possibly using the [slice] - to push new formulas to be propagated or to raising a conflict or to add - new lemmas. *) + (** Assume the formulas in the slice, possibly using the [slice] to push new + formulas to be propagated or to raising a conflict or to add new lemmas. + *) val final_check : t -> (void, Formula.t, void, proof) acts -> unit - (** Called at the end of the search in case a model has been found. - If no new clause is pushed, then proof search ends and "sat" is returned; - if lemmas are added, search is resumed; - if a conflict clause is added, search backtracks and then resumes. *) + (** Called at the end of the search in case a model has been found. If no new + clause is pushed, then proof search ends and "sat" is returned; if lemmas + are added, search is resumed; if a conflict clause is added, search + backtracks and then resumes. *) end (** Signature for theories to be given to the Model Constructing Solver. *) @@ -244,21 +239,22 @@ module type PLUGIN_MCSAT = sig (** Pop [n] levels of the theory *) val partial_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit - (** Assume the formulas in the slice, possibly using the [slice] - to push new formulas to be propagated or to raising a conflict or to add - new lemmas. *) + (** Assume the formulas in the slice, possibly using the [slice] to push new + formulas to be propagated or to raising a conflict or to add new lemmas. + *) val final_check : t -> (Term.t, Formula.t, Value.t, proof) acts -> unit - (** Called at the end of the search in case a model has been found. - If no new clause is pushed, then proof search ends and "sat" is returned; - if lemmas are added, search is resumed; - if a conflict clause is added, search backtracks and then resumes. *) + (** Called at the end of the search in case a model has been found. If no new + clause is pushed, then proof search ends and "sat" is returned; if lemmas + are added, search is resumed; if a conflict clause is added, search + backtracks and then resumes. *) val assign : t -> Term.t -> Value.t (** Returns an assignment value for the given term. *) val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit - (** An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts) *) + (** An iterator over the subTerm.ts of a Formula.t that should be assigned a + value (usually the poure subTerm.ts) *) val eval : t -> Formula.t -> Term.t eval_res (** Returns the evaluation of the Formula.t in the current assignment *) @@ -272,7 +268,8 @@ module type PLUGIN_SAT = sig end module type PROOF = sig - (** Signature for a module handling proof by resolution from sat solving traces *) + (** Signature for a module handling proof by resolution from sat solving + traces *) (** {3 Type declarations} *) @@ -282,6 +279,7 @@ module type PROOF = sig type formula type atom type lemma + type clause (** Abstract types for atoms, clauses and theory-specific lemmas *) @@ -290,27 +288,28 @@ module type PROOF = sig extended to proof nodes using functions defined later. *) and proof_node = { - conclusion : clause; (** The conclusion of the proof *) - step : step; (** The reasoning step used to prove the conclusion *) + conclusion: clause; (** The conclusion of the proof *) + step: step; (** The reasoning step used to prove the conclusion *) } - (** A proof can be expanded into a proof node, which show the first step of the proof. *) + (** A proof can be expanded into a proof node, which show the first step of + the proof. *) (** The type of reasoning steps allowed in a proof. *) and step = - | Hypothesis of lemma - (** The conclusion is a user-provided hypothesis *) - | Assumption - (** The conclusion has been locally assumed by the user *) + | Hypothesis of lemma (** The conclusion is a user-provided hypothesis *) + | Assumption (** The conclusion has been locally assumed by the user *) | Lemma of lemma - (** The conclusion is a tautology provided by the theory, with associated proof *) + (** The conclusion is a tautology provided by the theory, with + associated proof *) | Duplicate of t * atom list - (** The conclusion is obtained by eliminating multiple occurences of the atom in - the conclusion of the provided proof. *) + (** The conclusion is obtained by eliminating multiple occurences of the + atom in the conclusion of the provided proof. *) | Hyper_res of hyper_res_step and hyper_res_step = { hr_init: t; - hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + hr_steps: (atom * t) list; + (* list of pivot+clause to resolve against [init] *) } (** {3 Proof building functions} *) @@ -324,13 +323,14 @@ module type PROOF = sig @raise Resolution_error if it does not succeed. *) val prove_atom : atom -> t option - (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) + (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at + level 0 *) val res_of_hyper_res : hyper_res_step -> t * t * atom - (** Turn an hyper resolution step into a resolution step. - The conclusion can be deduced by performing a resolution between the conclusions - of the two given proofs. - The atom on which to perform the resolution is also given. *) + (** Turn an hyper resolution step into a resolution step. The conclusion can + be deduced by performing a resolution between the conclusions of the two + given proofs. The atom on which to perform the resolution is also given. + *) (** {3 Proof Nodes} *) @@ -338,15 +338,14 @@ module type PROOF = sig (** Returns the parents of a proof node. *) val is_leaf : step -> bool - (** Returns wether the the proof node is a leaf, i.e. an hypothesis, - an assumption, or a lemma. - [true] if and only if {!parents} returns the empty list. *) + (** Returns wether the the proof node is a leaf, i.e. an hypothesis, an + assumption, or a lemma. [true] if and only if {!parents} returns the empty + list. *) val expl : step -> string (** Returns a short string description for the proof step; for instance - ["hypothesis"] for a [Hypothesis] - (it currently returns the variant name in lowercase). *) - + ["hypothesis"] for a [Hypothesis] (it currently returns the variant name + in lowercase). *) (** {3 Proof Manipulation} *) @@ -357,15 +356,15 @@ module type PROOF = sig (** What is proved at the root of the clause *) val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a - (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that - [f] is executed exactly once on each proof node in the tree, and that the execution of - [f] on a proof node happens after the execution on the parents of the nodes. *) + (** [fold f acc p], fold [f] over the proof [p] and all its node. It is + guaranteed that [f] is executed exactly once on each proof node in the + tree, and that the execution of [f] on a proof node happens after the + execution on the parents of the nodes. *) val unsat_core : t -> clause list - (** Returns the unsat_core of the given proof, i.e the lists of conclusions - of all leafs of the proof. - More efficient than using the [fold] function since it has - access to the internal representation of proofs *) + (** Returns the unsat_core of the given proof, i.e the lists of conclusions of + all leafs of the proof. More efficient than using the [fold] function + since it has access to the internal representation of proofs *) (** {3 Misc} *) @@ -379,26 +378,26 @@ module type PROOF = sig module Tbl : Hashtbl.S with type key = t end -(** The external interface implemented by safe solvers, such as the one - created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) +(** The external interface implemented by safe solvers, such as the one created + by the {!Solver.Make} and {!Mcsolver.Make} functors. *) module type S = sig (** {2 Internal modules} - These are the internal modules used, you should probably not use them - if you're not familiar with the internals of mSAT. *) + These are the internal modules used, you should probably not use them if + you're not familiar with the internals of mSAT. *) include EXPR - type term = Term.t (** user terms *) + type term = Term.t + (** user terms *) - type formula = Formula.t (** user formulas *) + type formula = Formula.t + (** user formulas *) type atom - (** The type of atoms given by the module argument for formulas. - An atom is a user-defined atomic formula whose truth value is - picked by Msat. *) + (** The type of atoms given by the module argument for formulas. An atom is a + user-defined atomic formula whose truth value is picked by Msat. *) type clause - type theory type lemma @@ -426,19 +425,19 @@ module type S = sig val atoms_l : t -> atom list val equal : t -> t -> bool val name : t -> string - val pp : t printer module Tbl : Hashtbl.S with type key = t end - module Proof : PROOF - with type clause = clause - and type atom = atom - and type formula = formula - and type lemma = lemma - and type t = proof (** A module to manipulate proofs. *) + module Proof : + PROOF + with type clause = clause + and type atom = atom + and type formula = formula + and type lemma = lemma + and type t = proof type t = solver (** Main solver type, containing all state for solving. *) @@ -448,15 +447,17 @@ module type S = sig ?on_decision:(atom -> unit) -> ?on_new_atom:(atom -> unit) -> ?store_proof:bool -> - ?size:[`Tiny|`Small|`Big] -> + ?size:[ `Tiny | `Small | `Big ] -> theory -> t (** Create new solver @param theory the theory - @param store_proof if true, stores proof (default [true]). Otherwise - the functions that return proofs will fail with [No_proof] - @param size the initial size of internal data structures. The bigger, - the faster, but also the more RAM it uses. *) + @param store_proof + if true, stores proof (default [true]). Otherwise the functions that + return proofs will fail with [No_proof] + @param size + the initial size of internal data structures. The bigger, the faster, + but also the more RAM it uses. *) val theory : t -> theory (** Access the theory state *) @@ -465,18 +466,20 @@ module type S = sig (** Result type for the solver *) type res = - | Sat of (term,formula,Value.t) sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + | Sat of (term, formula, Value.t) sat_state + (** Returned when the solver reaches SAT, with a model *) + | Unsat of (atom, clause, Proof.t) unsat_state + (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit - (** Exception raised by the evaluating functions when a literal - has not yet been assigned a value. *) + (** Exception raised by the evaluating functions when a literal has not yet + been assigned a value. *) (** {2 Base operations} *) val assume : t -> formula list list -> lemma -> unit - (** Add the list of clauses to the current set of assumptions. - Modifies the sat solver state in place. *) + (** Add the list of clauses to the current set of assumptions. Modifies the + sat solver state in place. *) val add_clause : t -> atom list -> lemma -> unit (** Lower level addition of clauses *) @@ -484,31 +487,29 @@ module type S = sig val add_clause_a : t -> atom array -> lemma -> unit (** Lower level addition of clauses *) - val solve : - ?assumptions:atom list -> - t -> res + val solve : ?assumptions:atom list -> t -> res (** Try and solves the current set of clauses. - @param assumptions additional atomic assumptions to be temporarily added. - The assumptions are just used for this call to [solve], they are - not saved in the solver's state. *) + @param assumptions + additional atomic assumptions to be temporarily added. The assumptions + are just used for this call to [solve], they are not saved in the + solver's state. *) val make_term : t -> term -> unit - (** Add a new term (i.e. decision variable) to the solver. This term will - be decided on at some point during solving, wether it appears - in clauses or not. *) + (** Add a new term (i.e. decision variable) to the solver. This term will be + decided on at some point during solving, wether it appears in clauses or + not. *) val make_atom : t -> formula -> atom - (** Add a new atom (i.e propositional formula) to the solver. - This formula will be decided on at some point during solving, - wether it appears in clauses or not. *) + (** Add a new atom (i.e propositional formula) to the solver. This formula + will be decided on at some point during solving, wether it appears in + clauses or not. *) val true_at_level0 : t -> atom -> bool - (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. - it must hold in all models *) + (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. it + must hold in all models *) val eval_atom : t -> atom -> lbool (** Evaluate atom in current state *) val export : t -> clause export end - diff --git a/src/core/Vec.ml b/src/core/Vec.ml index 782a8b6a..7ebcdf73 100644 --- a/src/core/Vec.ml +++ b/src/core/Vec.ml @@ -1,18 +1,15 @@ - type 'a t = { - mutable data : 'a array; - mutable sz : int; + mutable data: 'a array; + mutable sz: int; } -let make n x = {data=Array.make n x; sz=0} - -let[@inline] create () = {data = [||]; sz = 0} - +let make n x = { data = Array.make n x; sz = 0 } +let[@inline] create () = { data = [||]; sz = 0 } let[@inline] clear s = s.sz <- 0 let[@inline] shrink t i = assert (i >= 0); - assert (i<=t.sz); + assert (i <= t.sz); t.sz <- i let[@inline] pop t = @@ -22,23 +19,18 @@ let[@inline] pop t = x let[@inline] size t = t.sz - let[@inline] is_empty t = t.sz = 0 - let[@inline] is_full t = Array.length t.data = t.sz let[@inline] copy t : _ t = let data = Array.copy t.data in - {t with data} + { t with data } (* grow the array *) let[@inline never] grow_to_double_size t x : unit = - if Array.length t.data = Sys.max_array_length then ( + if Array.length t.data = Sys.max_array_length then failwith "vec: cannot resize"; - ); - let size = - min Sys.max_array_length (max 4 (2 * Array.length t.data)) - in + let size = min Sys.max_array_length (max 4 (2 * Array.length t.data)) in let arr' = Array.make size x in Array.blit t.data 0 arr' 0 (Array.length t.data); t.data <- arr'; @@ -56,25 +48,32 @@ let[@inline] get t i = let[@inline] set t i v = if i < 0 || i > t.sz then invalid_arg "vec.set"; - if i = t.sz then ( + if i = t.sz then push t v - ) else ( + else Array.unsafe_set t.data i v - ) let[@inline] fast_remove t i = - assert (i>= 0 && i < t.sz); + assert (i >= 0 && i < t.sz); Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1); t.sz <- t.sz - 1 let filter_in_place f vec = let i = ref 0 in while !i < size vec do - if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i + if f (Array.unsafe_get vec.data !i) then + incr i + else + fast_remove vec !i done let sort t f : unit = - let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in + let sub_arr = + if is_full t then + t.data + else + Array.sub t.data 0 t.sz + in Array.fast_sort f sub_arr; t.data <- sub_arr @@ -89,7 +88,6 @@ let[@inline] iteri f t = done let[@inline] to_seq a k = iter k a - let exists p t = Iter.exists p @@ to_seq t let for_all p t = Iter.for_all p @@ to_seq t let fold f acc a = Iter.fold f acc @@ to_seq a @@ -98,16 +96,19 @@ let to_array a = Array.sub a.data 0 a.sz let of_list l : _ t = match l with - | [] -> create() + | [] -> create () | x :: tl -> - let v = make (List.length tl+1) x in + let v = make (List.length tl + 1) x in List.iter (push v) l; v -let pp ?(sep=", ") pp out v = +let pp ?(sep = ", ") pp out v = let first = ref true in iter (fun x -> - if !first then first := false else Format.fprintf out "%s@," sep; - pp out x) + if !first then + first := false + else + Format.fprintf out "%s@," sep; + pp out x) v diff --git a/src/core/Vec.mli b/src/core/Vec.mli index d51a2b69..adc61521 100644 --- a/src/core/Vec.mli +++ b/src/core/Vec.mli @@ -1,11 +1,10 @@ - type 'a t (** Abstract type of vectors of 'a *) val make : int -> 'a -> 'a t -(** [make cap dummy] creates a new vector filled with [dummy]. The vector - is initially empty but its underlying array has capacity [cap]. - [dummy] will stay alive as long as the vector *) +(** [make cap dummy] creates a new vector filled with [dummy]. The vector is + initially empty but its underlying array has capacity [cap]. [dummy] will + stay alive as long as the vector *) val create : unit -> 'a t @@ -13,24 +12,21 @@ val to_list : 'a t -> 'a list (** Returns the list of elements of the vector *) val to_array : 'a t -> 'a array - val of_list : 'a list -> 'a t - val to_seq : 'a t -> 'a Iter.t val clear : 'a t -> unit (** Set size to 0, doesn't free elements *) val shrink : 'a t -> int -> unit -(** [shrink vec sz] resets size of [vec] to [sz]. - Assumes [sz >=0 && sz <= size vec] *) +(** [shrink vec sz] resets size of [vec] to [sz]. Assumes + [sz >=0 && sz <= size vec] *) val pop : 'a t -> 'a (** Pop last element and return it. @raise Invalid_argument if the vector is empty *) val size : 'a t -> int - val is_empty : 'a t -> bool val is_full : 'a t -> bool @@ -44,20 +40,20 @@ val get : 'a t -> int -> 'a @raise Invalid_argument if the index is not valid *) val set : 'a t -> int -> 'a -> unit -(** set the element at the given index, either already set or the first - free slot if [not (is_full vec)], or +(** set the element at the given index, either already set or the first free + slot if [not (is_full vec)], or @raise Invalid_argument if the index is not valid *) val copy : 'a t -> 'a t (** Fresh copy *) val fast_remove : 'a t -> int -> unit -(** Remove element at index [i] without preserving order - (swap with last element) *) +(** Remove element at index [i] without preserving order (swap with last + element) *) val filter_in_place : ('a -> bool) -> 'a t -> unit -(** [filter_in_place f v] removes from [v] the elements that do - not satisfy [f] *) +(** [filter_in_place f v] removes from [v] the elements that do not satisfy [f] +*) val sort : 'a t -> ('a -> 'a -> int) -> unit (** Sort in place the array *) @@ -80,4 +76,6 @@ val for_all : ('a -> bool) -> 'a t -> bool val pp : ?sep:string -> (Format.formatter -> 'a -> unit) -> - Format.formatter -> 'a t -> unit + Format.formatter -> + 'a t -> + unit diff --git a/src/core/dune b/src/core/dune index f2f81950..0e201ba2 100644 --- a/src/core/dune +++ b/src/core/dune @@ -1,7 +1,5 @@ - (library - (name msat) - (public_name msat) - (libraries iter) - (synopsis "core data structures and algorithms for msat") - ) + (name msat) + (public_name msat) + (libraries iter) + (synopsis "core data structures and algorithms for msat")) diff --git a/src/dune b/src/dune index 05c64298..b70fd8b9 100644 --- a/src/dune +++ b/src/dune @@ -1,4 +1,3 @@ - (documentation - (package msat) - (mld_files :standard)) + (package msat) + (mld_files :standard)) diff --git a/src/main/dune b/src/main/dune index 1bb33c7c..e15ce2b5 100644 --- a/src/main/dune +++ b/src/main/dune @@ -1,12 +1,14 @@ - ; main binary + (executable - (name main) - (public_name msat) - (package msat-bin) - (libraries containers camlzip msat msat.sat msat.backend) - (flags :standard -open Msat) - ) + (name main) + (public_name msat) + (package msat-bin) + (libraries containers camlzip msat msat.sat msat.backend) + (flags :standard -open Msat)) + +(ocamlyacc + (modules Dimacs_parse)) -(ocamlyacc (modules Dimacs_parse)) -(ocamllex (modules Dimacs_lex)) +(ocamllex + (modules Dimacs_lex)) diff --git a/src/main/main.ml b/src/main/main.ml index ddc1d856..bc6f189e 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -19,19 +19,22 @@ let no_proof = ref false module S = Msat_sat -module Process() = struct - module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S)) +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 + 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 @@ -40,65 +43,64 @@ module Process() = struct 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 + 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' 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 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) + 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.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) + 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 + if l = 0 then + raise (Arg.Bad "bad numeric argument") + else ( try - match arg.[l-1] with + match arg.[l - 1] with | 'k' -> multiplier 1e3 | 'M' -> multiplier 1e6 | 'G' -> multiplier 1e9 @@ -107,37 +109,40 @@ let int_arg r arg = | 'm' -> multiplier 60. | 'h' -> multiplier 3600. | 'd' -> multiplier 86400. - | '0'..'9' -> r := float_of_string arg + | '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 setup_gc_stat () = at_exit (fun () -> Gc.print_stat stdout) let input_file = fun s -> file := s - let usage = "Usage : main [options] " -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), - "[kMGT] Sets the size limit for the sat solver"; - "-time", Arg.String (int_arg time_limit), - "[smhd] Sets the time limit for the sat solver"; - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - "-no-proof", Arg.Set no_proof, " disable proof logging"; - ] + +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), + "[kMGT] Sets the size limit for the sat solver" ); + ( "-time", + Arg.String (int_arg time_limit), + "[smhd] Sets the time limit for the sat solver" ); + ( "-v", + Arg.Int (fun i -> Log.set_debug i), + " Sets the debug verbose level" ); + "-no-proof", Arg.Set no_proof, " disable proof logging"; + ] (* Limits alarm *) let check () = @@ -158,8 +163,7 @@ let main () = ); let al = Gc.create_alarm check in - let module P = Process() in - + let module P = Process () in (* Interesting stuff happening *) let clauses = parse_file !file in P.add_clauses clauses; @@ -168,9 +172,7 @@ let main () = () let () = - try - main () - with + try main () with | Out_of_time -> Format.printf "Timeout@."; exit 2 @@ -180,7 +182,6 @@ let () = | Incorrect_model -> Format.printf "Internal error : incorrect *sat* model@."; exit 4 - | S.Proof.Resolution_error msg -> + | S.Proof.Resolution_error msg -> Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg; exit 5 - diff --git a/src/sat/Int_lit.ml b/src/sat/Int_lit.ml index 9f01aaeb..a1d30560 100644 --- a/src/sat/Int_lit.ml +++ b/src/sat/Int_lit.ml @@ -1,12 +1,10 @@ - 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. *) + 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 @@ -14,43 +12,49 @@ let max_lit = max_int let max_index = ref 0 let max_fresh = ref (-1) -(** Internal function for creating atoms. - Updates the internal counters *) +(** Internal function for creating atoms. Updates the internal counters *) let _make i = - if i <> 0 && (abs i) < max_lit then begin + if i <> 0 && abs i < max_lit then ( max_index := max !max_index (abs i); i - end else + ) else raise Bad_atom let to_int i = i (** *) -let neg a = - a +let neg a = -a let norm a = - abs a, if a < 0 then - Solver_intf.Negated - else - Solver_intf.Same_sign + ( 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 apply_sign b i = + if b then + i + else + neg 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 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) + _make ((2 * !max_fresh) + 1) (* let iter: (t -> unit) -> unit = fun f -> @@ -61,6 +65,12 @@ let iter: (t -> unit) -> unit = fun f -> 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) + (if a < 0 then + "~" + else + "") + (if a mod 2 = 0 then + "v" + else + "f") + (abs a / 2) diff --git a/src/sat/Int_lit.mli b/src/sat/Int_lit.mli index 6845d161..f6bd0025 100644 --- a/src/sat/Int_lit.mli +++ b/src/sat/Int_lit.mli @@ -1,12 +1,10 @@ - (** {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). -*) + 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. *) @@ -26,8 +24,8 @@ 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]. *) +(** [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. *) diff --git a/src/sat/Msat_sat.ml b/src/sat/Msat_sat.ml index 91cc70c6..9355522e 100644 --- a/src/sat/Msat_sat.ml +++ b/src/sat/Msat_sat.ml @@ -4,8 +4,9 @@ Copyright 2016 Guillaume Bury *) module Int_lit = Int_lit -include Msat.Make_pure_sat(struct - module Formula = Int_lit - type proof = unit - end) +include Msat.Make_pure_sat (struct + module Formula = Int_lit + + type proof = unit +end) diff --git a/src/sat/Msat_sat.mli b/src/sat/Msat_sat.mli index 0517e913..c4ccf8f6 100644 --- a/src/sat/Msat_sat.mli +++ b/src/sat/Msat_sat.mli @@ -6,14 +6,13 @@ Copyright 2016 Guillaume Bury (** Sat solver This modules instanciates a pure sat solver using integers to represent - atomic propositions. -*) + 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. *) - +include + Msat.S + with type Formula.t = Int_lit.t + and type theory = unit + and type lemma = unit diff --git a/src/sat/dune b/src/sat/dune index 60428a71..0fb97f93 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,9 +1,6 @@ - (library - (name msat_sat) - (public_name msat.sat) - (synopsis "purely boolean interface to Msat") - (libraries msat) - (flags :standard -open Msat) - ) - + (name msat_sat) + (public_name msat.sat) + (synopsis "purely boolean interface to Msat") + (libraries msat) + (flags :standard -open Msat)) diff --git a/src/sudoku/dune b/src/sudoku/dune index 8af1b6ed..cea8e324 100644 --- a/src/sudoku/dune +++ b/src/sudoku/dune @@ -1,6 +1,4 @@ - (executable - (name sudoku_solve) - (modes native) - (libraries msat msat.backtrack iter containers) -) + (name sudoku_solve) + (modes native) + (libraries msat msat.backtrack iter containers)) diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml index a75ace03..42015beb 100644 --- a/src/sudoku/sudoku_solve.ml +++ b/src/sudoku/sudoku_solve.ml @@ -1,4 +1,3 @@ - (** {1 simple sudoku solver} *) module Fmt = CCFormat @@ -9,6 +8,7 @@ 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 @@ -19,14 +19,24 @@ module Cell : sig 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] 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 + 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 @@ -35,15 +45,13 @@ module Grid : sig val get : t -> int -> int -> Cell.t val set : t -> int -> int -> Cell.t -> t + type set = (int * int * Cell.t) Iter.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 all_cells : t -> (int * int * Cell.t) Iter.t val parse : string -> t val is_full : t -> bool val is_valid : t -> bool @@ -52,73 +60,78 @@ module Grid : sig end = struct type t = Cell.t array - let[@inline] get (s:t) i j = s.(i*9 + j) + let[@inline] get (s : t) i j = s.((i * 9) + j) - let[@inline] set (s:t) i j n = + let[@inline] set (s : t) i j n = let s' = Array.copy s in - s'.(i*9 + j) <- n; + s'.((i * 9) + j) <- n; s' + type set = (int * int * Cell.t) Iter.t (** A set of related cells *) - type set = (int*int*Cell.t) Iter.t open Iter.Infix - let all_cells (g:t) = + let all_cells (g : t) = 0 -- 8 >>= fun i -> - 0 -- 8 >|= fun j -> (i,j,get g i j) + 0 -- 8 >|= fun j -> i, j, get g i j - let rows (g:t) = + let rows (g : t) = 0 -- 8 >|= fun i -> - ( 0 -- 8 >|= fun j -> (i,j,get g i j)) + 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)) + 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)) + 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) + let all_distinct (s : set) = + s + >|= (fun (_, _, c) -> c) |> Iter.diagonal - |> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2) + |> 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 + (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) + |> 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 "@["; Array.iteri (fun i n -> - Cell.pp out n; - if i mod 9 = 8 then Fmt.fprintf out "@,") + 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 ( + 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 + 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; @@ -129,6 +142,7 @@ module B_ref = Msat_backtrack.Ref module Solver : sig type t + val create : Grid.t -> t val solve : t -> Grid.t option end = struct @@ -136,133 +150,140 @@ end = struct (* 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) + 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} + 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) + 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 (); - )) + 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 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) + |> 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 () - )) + 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) = + let trail_ (acts : _ Msat.acts) = acts.acts_iter_assumptions - |> Iter.map - (function - | Assign _ -> assert false - | Lit f -> f) + |> 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)); + 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@])"); + 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) + module S = Msat.Make_cdcl_t (Theory) type t = { grid0: Grid.t; solver: S.t; } - let solve (self:t) : _ option = + 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.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); + 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)) @@ -272,60 +293,68 @@ end = struct r let create g : t = - { solver=S.create ~store_proof:false (Theory.create g); grid0=g } + { solver = S.create ~store_proof:false (Theory.create g); grid0 = g } end -let solve_grid (g:Grid.t) : Grid.t option = +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 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)) + |> 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); + Format.printf "parsed %d grids (in %.3fs)@." (List.length grids) + (Sys.time () -. start); List.iter (fun g -> - Format.printf "@[@,#########################@,@[<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 "@[@[<2>solution (in %.3fs):@ %a@]@,###################@]@." - (Sys.time()-.start) Grid.pp g') + Format.printf + "@[@,#########################@,@[<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 + "@[@[<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); + 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 + 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] "; Msat.Log.set_debug !debug; - try - List.iter (fun f -> solve_file f) !files; - with - | Failure msg | Invalid_argument msg -> + try List.iter (fun f -> solve_file f) !files + with Failure msg | Invalid_argument msg -> Format.printf "@{Error@}:@.%s@." msg; exit 1 diff --git a/src/tseitin/Msat_tseitin.ml b/src/tseitin/Msat_tseitin.ml index 79550e49..7cf62afc 100644 --- a/src/tseitin/Msat_tseitin.ml +++ b/src/tseitin/Msat_tseitin.ml @@ -11,14 +11,17 @@ (**************************************************************************) module type Arg = Tseitin_intf.Arg - module type S = Tseitin_intf.S module Make (F : Tseitin_intf.Arg) = struct - - type combinator = And | Or | Imp | Not + type combinator = + | And + | Or + | Imp + | Not type atom = F.t + type t = | True | Lit of atom @@ -28,38 +31,33 @@ module Make (F : Tseitin_intf.Arg) = struct 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 (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 + | 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 + | [ 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 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 + | 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 + | a :: r -> + (match f a with + | None -> opt_rev_map f acc r + | Some b -> opt_rev_map f (b :: acc) r) let remove_true l = let aux = function @@ -70,60 +68,68 @@ module Make (F : Tseitin_intf.Arg) = struct let remove_false l = let aux = function - | Comb(Not, [True]) -> None + | Comb (Not, [ True ]) -> None | f -> Some f in opt_rev_map aux [] l - - let make_not f = make Not [f] + 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 + 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 + if List.exists (( = ) f_true) l' then f_true - else match l' with + else ( + match l' with | [] -> f_false - | [a] -> a + | [ 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_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 ] ] + 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) + 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, [ 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 + + 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 + | 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) + 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 *) *) @@ -225,92 +231,89 @@ module Make (F : Tseitin_intf.Arg) = struct *) 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] - + 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 - + 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 + 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 + let acc = + match f with | True -> [] - | Comb(Not, [True]) -> [[]] - | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l - | _ -> [snd (cnf f)] + | 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;..]] + (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 + 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 + (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 + 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 diff --git a/src/tseitin/Msat_tseitin.mli b/src/tseitin/Msat_tseitin.mli index 498667c5..32ddc3f8 100644 --- a/src/tseitin/Msat_tseitin.mli +++ b/src/tseitin/Msat_tseitin.mli @@ -7,16 +7,15 @@ 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. -*) + 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. *) +(** 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. *) - +module Make : functor (F : Arg) -> S with type atom = F.t diff --git a/src/tseitin/Tseitin_intf.ml b/src/tseitin/Tseitin_intf.ml index 99805c35..7da4d41b 100644 --- a/src/tseitin/Tseitin_intf.ml +++ b/src/tseitin/Tseitin_intf.ml @@ -15,9 +15,8 @@ module type Arg = sig (** Formulas - This defines what is needed of formulas in order to implement - Tseitin's CNF conversion. - *) + This defines what is needed of formulas in order to implement Tseitin's + CNF conversion. *) type t (** Type of atomic formulas. *) @@ -30,22 +29,20 @@ module type Arg = sig 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. - *) + 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. *) + (** 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. *) @@ -54,16 +51,19 @@ module type S = sig (** 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]. *) + (** [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. *) + (** 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. *) + (** 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]". *) @@ -72,14 +72,14 @@ module type S = sig (** [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]". *) + (** [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. *) + 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 diff --git a/src/tseitin/dune b/src/tseitin/dune index 8ecca218..908bd91d 100644 --- a/src/tseitin/dune +++ b/src/tseitin/dune @@ -1,8 +1,5 @@ - (library - (name msat_tseitin) - (public_name msat.tseitin) - (synopsis "Tseitin transformation for msat") - (libraries msat) - ) - + (name msat_tseitin) + (public_name msat.tseitin) + (synopsis "Tseitin transformation for msat") + (libraries msat)) diff --git a/tests/dune b/tests/dune index f3197e8c..84b7b482 100644 --- a/tests/dune +++ b/tests/dune @@ -1,34 +1,45 @@ - (executable - (name test_api) - (libraries msat msat_sat) - (flags -open Msat) - ) + (name test_api) + (libraries msat msat_sat) + (flags -open Msat)) (rule - (alias runtest) - (package msat) - (deps test_api.exe) + (alias runtest) + (package msat) + (deps test_api.exe) (locks test) - (action (run %{deps}))) + (action + (run %{deps}))) (rule - (alias runtest) - (package msat) - (deps ./icnf-solve/icnf_solve.exe Makefile (source_tree regression)) + (alias runtest) + (package msat) + (deps + ./icnf-solve/icnf_solve.exe + Makefile + (source_tree regression)) (locks test) - (action (run make test-icnf))) + (action + (run make test-icnf))) (rule - (alias runtest) - (package msat) - (deps ./../src/sudoku/sudoku_solve.exe Makefile (source_tree sudoku)) + (alias runtest) + (package msat) + (deps + ./../src/sudoku/sudoku_solve.exe + Makefile + (source_tree sudoku)) (locks test) - (action (run make test-sudoku))) + (action + (run make test-sudoku))) (rule - (alias runtest) - (package msat-bin) - (deps ./../src/main/main.exe ./run (source_tree .)) - (locks test) - (action (run /usr/bin/time -f "%e" ./run sat))) + (alias runtest) + (package msat-bin) + (deps + ./../src/main/main.exe + ./run + (source_tree .)) + (locks test) + (action + (run /usr/bin/time -f "%e" ./run sat))) diff --git a/tests/icnf-solve/dune b/tests/icnf-solve/dune index e28262fc..930a6a00 100644 --- a/tests/icnf-solve/dune +++ b/tests/icnf-solve/dune @@ -1,6 +1,7 @@ (executable - (name icnf_solve) - (modes native) - (libraries containers msat msat_sat)) + (name icnf_solve) + (modes native) + (libraries containers msat msat_sat)) -(ocamllex (modules lexer)) +(ocamllex + (modules lexer)) diff --git a/tests/icnf-solve/icnf_solve.ml b/tests/icnf-solve/icnf_solve.ml index 567b58ad..21d0b9a8 100644 --- a/tests/icnf-solve/icnf_solve.ml +++ b/tests/icnf-solve/icnf_solve.ml @@ -1,4 +1,3 @@ - module Vec = Msat.Vec module Parse : sig @@ -10,7 +9,8 @@ module Parse : sig val make : file:string -> (int -> 'a) -> 'a t - val next : 'a t -> 'a event (** @raise End_of_file when done *) + val next : 'a t -> 'a event + (** @raise End_of_file when done *) end = struct module L = Lexer @@ -28,50 +28,64 @@ end = struct let ic = open_in file in let lex = Lexing.from_channel ic in at_exit (fun () -> close_in_noerr ic); - {lex; vec=Vec.create(); mk; } + { lex; vec = Vec.create (); mk } - let rec next (self:_ t) : _ event = + let rec next (self : _ t) : _ event = match L.token self.lex with | L.EOF -> raise End_of_file | L.A -> let c = read_ints self in Solve c - | L.I 0 -> - Add_clause [| |] + | L.I 0 -> Add_clause [||] | L.I x -> let c = read_ints ~first:(self.mk x) self in Add_clause c + and read_ints ?first self : _ array = - Vec.clear self.vec; (* reuse local vec *) + Vec.clear self.vec; + (* reuse local vec *) CCOpt.iter (Vec.push self.vec) first; - let rec aux() = + let rec aux () = match L.token self.lex with | L.I 0 -> Vec.to_array self.vec (* done *) | L.I n -> let x = self.mk n in Vec.push self.vec x; - aux() + aux () | L.A -> failwith "unexpected \"a\"" | L.EOF -> failwith "unexpected end of file" in - aux() + aux () end module Solver = struct module F = Msat_sat.Int_lit module S = Msat_sat + type t = S.t - let make () = S.create() - let mklit s i = S.make_atom s (let v = F.make (abs i) in if i>0 then v else F.neg v) - let add_clause s c = S.add_clause_a s c (); true + let make () = S.create () + + let mklit s i = + S.make_atom s + (let v = F.make (abs i) in + if i > 0 then + v + else + F.neg v) + + let add_clause s c = + S.add_clause_a s c (); + true + let to_int a : int = F.to_int @@ S.Atom.formula a + let solve s ass = let ass = Array.to_list ass in match S.solve ~assumptions:ass s with | S.Sat _ -> Ok () | S.Unsat { unsat_assumptions; _ } -> - let core = unsat_assumptions() in + let core = unsat_assumptions () in Error core end @@ -79,7 +93,7 @@ let solve_with_solver ~check ~debug file : unit = Printf.eprintf "c process %S\n%!" file; let s = Solver.make () in let pp_arr out a = - Array.iter (fun lit -> Printf.fprintf out "%d " (Solver.to_int lit)) a; + Array.iter (fun lit -> Printf.fprintf out "%d " (Solver.to_int lit)) a in let p = Parse.make ~file (Solver.mklit s) in let rec process_problem () = @@ -87,41 +101,36 @@ let solve_with_solver ~check ~debug file : unit = | Parse.Add_clause c -> if debug then ( Printf.printf "add_clause %a\n%!" pp_arr c; - Msat.Log.set_debug 5; + Msat.Log.set_debug 5 ); let r = Solver.add_clause s c in - if r then process_problem() + if r then + process_problem () else ( Printf.printf "UNSAT\n%!"; skip_problem () ) | Parse.Solve assumptions -> - if debug then ( - Printf.printf "c solve %a\n%!" pp_arr assumptions; - ); - begin match Solver.solve s assumptions with - | Ok () -> Printf.printf "SAT\n%!" - | Error (_::_ as core) when check -> - Printf.printf "UNSAT\n%!"; - let core = Array.of_list core in - if debug then Printf.printf "check unsat core %a\n" pp_arr core; - (* check unsat core *) - begin match Solver.solve s core with - | Ok () -> - Printf.printf "error: unsat core %a is SAT\n%!" pp_arr core; - exit 1 - | Error _ -> () - end; - | Error _ -> - Printf.printf "UNSAT\n%!"; - end; + if debug then Printf.printf "c solve %a\n%!" pp_arr assumptions; + (match Solver.solve s assumptions with + | Ok () -> Printf.printf "SAT\n%!" + | Error (_ :: _ as core) when check -> + Printf.printf "UNSAT\n%!"; + let core = Array.of_list core in + if debug then Printf.printf "check unsat core %a\n" pp_arr core; + (* check unsat core *) + (match Solver.solve s core with + | Ok () -> + Printf.printf "error: unsat core %a is SAT\n%!" pp_arr core; + exit 1 + | Error _ -> ()) + | Error _ -> Printf.printf "UNSAT\n%!"); (* next problem! *) - process_problem() - | exception End_of_file -> - done_ () - and skip_problem() = + process_problem () + | exception End_of_file -> done_ () + and skip_problem () = match Parse.next p with - | Parse.Add_clause _ -> skip_problem() + | Parse.Add_clause _ -> skip_problem () | Parse.Solve _ -> process_problem () | exception End_of_file -> done_ () and done_ () = @@ -133,18 +142,20 @@ let solve_with_solver ~check ~debug file : unit = let solve_with_file ~check ~debug file : unit = try solve_with_solver ~check ~debug file with e -> - Printf.printf "error while solving %S:\n%s" - file (Printexc.to_string e); + Printf.printf "error while solving %S:\n%s" file (Printexc.to_string e); exit 1 let () = let files = ref [] in let debug = ref false in let check = ref false in - let opts = [ - "-d", Arg.Set debug, " debug"; - "--check", Arg.Set check, " check unsat cores"; - ] |> Arg.align in + let opts = + [ + "-d", Arg.Set debug, " debug"; + "--check", Arg.Set check, " check unsat cores"; + ] + |> Arg.align + in Arg.parse opts (fun f -> files := f :: !files) "icnf_solve [options] "; List.iter (fun f -> solve_with_file ~check:!check ~debug:!debug f) !files; () diff --git a/tests/test_api.ml b/tests/test_api.ml index d4bb142b..d714700a 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -9,27 +9,30 @@ Copyright 2014 Simon Cruanes module F = Msat_sat.Int_lit module S = Msat_sat -let (|>) x f = f x - +let ( |> ) x f = f x let time_limit = ref 300. let size_limit = ref 1000_000_000. 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.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 () let set_flag opt arg flag l = - try - flag := List.assoc arg l - with Not_found -> - invalid_arg (error_msg opt arg l) + try flag := List.assoc arg l + with Not_found -> invalid_arg (error_msg opt arg l) let usage = "Usage : test_api [options]" -let argspec = Arg.align [ - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - ] + +let argspec = + Arg.align + [ + ( "-v", + Arg.Int (fun i -> Log.set_debug i), + " Sets the debug verbose level" ); + ] type solver_res = | R_sat @@ -47,17 +50,18 @@ let errorf msg = Format.ksprintf error msg module Test = struct type action = | A_assume of F.t list list - | A_solve of F.t list * [`Expect_sat | `Expect_unsat] + | A_solve of F.t list * [ `Expect_sat | `Expect_unsat ] type t = { name: string; actions: action list; } - let mk_test name l = {name; actions=l} + let mk_test name l = { name; actions = l } let assume l = A_assume (List.map (List.map F.make) l) - let assume1 c = assume [c] - let solve ?(assumptions=[]) e = + let assume1 c = assume [ c ] + + let solve ?(assumptions = []) e = let assumptions = List.map F.make assumptions in A_solve (assumptions, e) @@ -65,93 +69,87 @@ module Test = struct | Pass | Fail of string - let run (t:t): result = - (* Interesting stuff happening *) - let st = mk_solver() in + let run (t : t) : result = + (* Interesting stuff happening *) + let st = mk_solver () in try List.iter (function - | A_assume cs -> - S.assume st cs () + | A_assume cs -> S.assume st cs () | A_solve (assumptions, expect) -> let assumptions = List.map (S.make_atom st) assumptions in - match S.solve ~assumptions st, expect with - | S.Sat _, `Expect_sat -> () - | S.Unsat us, `Expect_unsat -> - let p = us.Msat.get_proof () in - S.Proof.check p; - | S.Unsat _, `Expect_sat -> - error "expect sat, got unsat" - | S.Sat _, `Expect_unsat -> - error "expect unsat, got sat" - ) + (match S.solve ~assumptions st, expect with + | S.Sat _, `Expect_sat -> () + | S.Unsat us, `Expect_unsat -> + let p = us.Msat.get_proof () in + S.Proof.check p + | S.Unsat _, `Expect_sat -> error "expect sat, got unsat" + | S.Sat _, `Expect_unsat -> error "expect unsat, got sat")) t.actions; Pass - with Error msg -> - Fail msg + with Error msg -> Fail msg (* basic test *) let test1 = - [ assume [[-1;2]; [-1;3]]; + [ + assume [ [ -1; 2 ]; [ -1; 3 ] ]; solve `Expect_sat; - assume [[-2;4]; [-3;-4]]; + assume [ [ -2; 4 ]; [ -3; -4 ] ]; solve `Expect_sat; - assume [[1]]; + assume [ [ 1 ] ]; solve `Expect_unsat; - ] |> mk_test "test1" + ] + |> mk_test "test1" (* same as test1 but with assumptions *) let test2 = - [ solve `Expect_sat; - assume [[-1;2]; [-1;3]]; + [ solve `Expect_sat; - assume [[-2;4]; [-3;-4]]; + assume [ [ -1; 2 ]; [ -1; 3 ] ]; solve `Expect_sat; - solve ~assumptions:[1] `Expect_unsat; + assume [ [ -2; 4 ]; [ -3; -4 ] ]; solve `Expect_sat; - ] |> mk_test "test2" + solve ~assumptions:[ 1 ] `Expect_unsat; + solve `Expect_sat; + ] + |> mk_test "test2" (* repeat assumptions *) let test3 = - [ assume [[-1;2]; [-1;3]]; + [ + assume [ [ -1; 2 ]; [ -1; 3 ] ]; solve `Expect_sat; - assume [[-2;4]; [-3;-4]]; + assume [ [ -2; 4 ]; [ -3; -4 ] ]; solve `Expect_sat; - solve ~assumptions:[1] `Expect_unsat; + solve ~assumptions:[ 1 ] `Expect_unsat; solve `Expect_sat; - solve ~assumptions:[1] `Expect_unsat; + solve ~assumptions:[ 1 ] `Expect_unsat; solve `Expect_sat; - solve ~assumptions:[1] `Expect_unsat; + solve ~assumptions:[ 1 ] `Expect_unsat; solve `Expect_sat; - solve ~assumptions:[2] `Expect_sat; - assume [[1]]; + solve ~assumptions:[ 2 ] `Expect_sat; + assume [ [ 1 ] ]; solve `Expect_unsat; - ] |> mk_test "test3" + ] + |> mk_test "test3" (* Conflict at level 0 *) let test4 = - [ assume [[-1; -2]]; + [ + assume [ [ -1; -2 ] ]; solve `Expect_sat; - assume [[1]]; + assume [ [ 1 ] ]; solve `Expect_sat; - assume [[2]]; - solve ~assumptions:[3] `Expect_unsat; + assume [ [ 2 ] ]; + solve ~assumptions:[ 3 ] `Expect_unsat; solve ~assumptions:[] `Expect_unsat; solve ~assumptions:[] `Expect_unsat; - ] |> mk_test "conflict0" + ] + |> mk_test "conflict0" (* just check that we do create new solvers *) - let test_clean = - [ solve `Expect_sat - ] |> mk_test "test_clean" - - let suite = - [ test1; - test2; - test3; - test4; - test_clean; (* after test3 *) - ] + let test_clean = [ solve `Expect_sat ] |> mk_test "test_clean" + let suite = [ test1; test2; test3; test4; test_clean (* after test3 *) ] end let main () = @@ -160,13 +158,13 @@ let main () = let failed = ref false in List.iter (fun test -> - Printf.printf "%-10s... %!" test.Test.name; - match Test.run test with - | Test.Pass -> Printf.printf "ok\n%!" - | Test.Fail msg -> - failed := true; - Printf.printf "fail (%s)\n%!" msg) + Printf.printf "%-10s... %!" test.Test.name; + match Test.run test with + | Test.Pass -> Printf.printf "ok\n%!" + | Test.Fail msg -> + failed := true; + Printf.printf "fail (%s)\n%!" msg) Test.suite; if !failed then exit 1 -let () = main() +let () = main ()