simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-24 02:16:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

large refactor of SAT solver, all internal code in Internal now

Browse source
This commit is contained in:
Simon Cruanes 2018-05-09 22:47:21 -05:00
parent 36df2d952b
commit 3968688a35
23 changed files with 861 additions and 1543 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

191
src/backend/Coq.ml
View file

@ -1,191 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)
module type S = Backend_intf.S
module type Arg = sig
type hyp
type lemma
type assumption
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 : Res.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 C_tbl = S.Clause.Tbl
let name = Clause.name
let clause_map c =
let rec aux acc a i =
if i >= Array.length a then acc
else begin
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
let clause_iter m format fmt clause =
let aux atom = Format.fprintf fmt format (M.find atom m) in
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"
(name goal) (name hyp);
(** Prove the goal: intro the atoms, then use them with the hyp *)
let m = clause_map goal in
Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
(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)
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
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"
(name goal) (name h1) (name h2);
(** 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 @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
false
) else (
let m = clause_map goal in
Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
(clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
true
)
(* Count uses of hypotheses *)
let incr_use h c =
let i = try C_tbl.find h c with Not_found -> 0 in
C_tbl.add h c (i + 1)
let decr_use h c =
let i = C_tbl.find h c - 1 in
assert (i >= 0);
let () = C_tbl.add h c i in
i <= 0
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
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'
let prove_node t fmt node =
let clause = node.S.conclusion in
match node.S.step with
| S.Hypothesis ->
A.prove_hyp fmt (name clause) clause
| S.Assumption ->
A.prove_assumption fmt (name clause) clause
| S.Lemma _ ->
A.prove_lemma fmt (name clause) clause
| S.Duplicate (p, l) ->
let c = S.conclusion p in
let () = elim_duplicate fmt clause c l in
clean t fmt [c]
| S.Resolution (p1, p2, a) ->
let c1 = S.conclusion p1 in
let c2 = S.conclusion p2 in
if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
let count_uses p =
let h = C_tbl.create 128 in
let aux () node =
List.iter (fun p' -> incr_use h S.(conclusion p')) (S.parents node.S.step)
in
let () = S.fold aux () p in
h
(* Here the main idea is to always try and have exactly
one goal to prove, i.e False. So each *)
let print fmt p =
let h = count_uses p in
let aux () node =
Format.fprintf fmt "%a" (prove_node h) node
in
Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
S.fold aux () p
end
module Simple(S : Res.S)
(A : Arg with type hyp = S.formula list
and type lemma := S.lemma
and type assumption := S.formula) =
Make(S)(struct
(* Some helpers *)
let lit = S.Atom.lit
let get_assumption c =
match S.Clause.atoms_l c with
| [ x ] -> x
| _ -> assert false
let get_lemma c =
match S.expand (S.prove c) with
| {S.step=S.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)

46
src/backend/Coq.mli
View file

@ -1,46 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
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. *)
module type S = Backend_intf.S
(** Interface for exporting proofs. *)
module type Arg = sig
(** Term printing for Coq *)
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. *)
end
module Make(S : Res.S)(A : 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 Simple(S : Res.S)(A : Arg with type hyp = S.formula list
and type lemma := S.lemma
and type assumption := S.formula) : S with type t := S.proof
(** Simple functo to output Coq proofs *)

61
src/backend/Dedukti.ml
View file

@ -1,61 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)
module type S = Backend_intf.S
module type Arg = sig
type proof
type lemma
type formula
val print : Format.formatter -> formula -> unit
val prove : Format.formatter -> lemma -> unit
val context : Format.formatter -> proof -> unit
end
module Make(S : Res.S)(A : Arg with type formula := S.formula
and type lemma := S.lemma
and type proof := S.proof) = struct
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 =
let rec aux fmt = function
| [] -> ()
| a :: r ->
let f, pos =
if S.Atom.is_pos a then
S.Atom.lit a, true
else
S.Atom.lit (S.Atom.neg a), false
in
fprintf fmt "%s _b %a ->@ %a"
(if pos then "_pos" else "_neg") A.print f aux r
in
fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
let context fmt p =
fprintf fmt "(; Embedding ;)";
fprintf fmt "Prop : Type.";
fprintf fmt "_proof : Prop -> Type.";
fprintf fmt "(; Notations for clauses ;)";
fprintf fmt "_pos : Prop -> Prop -> Type.";
fprintf fmt "_neg : Prop -> Prop -> Type.";
fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
A.context fmt p
let print fmt p =
fprintf fmt "#NAME Proof.";
fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
context fmt p;
()
end

32
src/backend/Dedukti.mli
View file

@ -1,32 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Deduki backend for proofs
Work in progress...
*)
module type S = Backend_intf.S
module type Arg = sig
type lemma
type proof
type formula
val print : Format.formatter -> formula -> unit
val prove : Format.formatter -> lemma -> unit
val context : Format.formatter -> proof -> unit
end
module Make :
functor(S : Res.S) ->
functor(A : 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. *)

28
src/backend/Dimacs.ml
View file

@ -15,19 +15,17 @@ module type S = sig
Format.formatter ->
hyps:clause Vec.t ->
history:clause Vec.t ->
local:clause Vec.t ->
unit
val export_icnf :
Format.formatter ->
hyps:clause Vec.t ->
history:clause Vec.t ->
local:clause Vec.t ->
unit
end
module Make(St : Solver_types_intf.S) = struct
module Make(St : Sidekick_sat.S) = struct
type st = St.t
(* Dimacs & iCNF export *)
@ -72,20 +70,17 @@ module Make(St : Solver_types_intf.S) = struct
) learnt;
lemmas
let export st fmt ~hyps ~history ~local =
let export st fmt ~hyps ~history : unit =
assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
(* Learnt clauses, then filtered to only keep only
the theory lemmas; all other learnt clauses should be logical
consequences of the rest. *)
let lemmas = filter_vec history in
(* Local assertions *)
assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local);
(* Number of atoms and clauses *)
let n = St.nb_elt st in
let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
let n = St.n_vars st in
let m = Vec.size hyps + Vec.size lemmas in
Format.fprintf fmt
"@[<v>p cnf %d %d@,%a%a%a@]@." n m
(export_vec "Local assumptions") local
"@[<v>p cnf %d %d@,%a%a@]@." n m
(export_vec "Hypotheses") hyps
(export_vec "Lemmas") lemmas
@ -93,24 +88,15 @@ module Make(St : Solver_types_intf.S) = struct
let icnf_hyp = ref 0
let icnf_lemmas = ref 0
let export_icnf fmt ~hyps ~history ~local =
let export_icnf fmt ~hyps ~history =
assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
let lemmas = history in
(* Local assertions *)
let l = List.map
(fun c -> match St.Clause.premise c, St.Clause.atoms c with
| St.Local, [| a |] -> a
| _ -> assert false)
(Vec.to_list local)
in
let local = St.Clause.make_l l St.Local in
(* Number of atoms and clauses *)
Format.fprintf fmt
"@[<v>%s@,%a%a%a@]@."
"@[<v>%s@,%a%a@]@."
(if !icnf_hyp = 0 && !icnf_lemmas = 0 then "p inccnf" else "")
(export_icnf_aux icnf_hyp "Hypotheses" (fun x -> Some x)) hyps
(export_icnf_aux icnf_lemmas "Lemmas" map_filter_learnt) lemmas
export_assumption local
end

4
src/backend/Dimacs.mli
View file

@ -21,7 +21,6 @@ module type S = sig
Format.formatter ->
hyps:clause Vec.t ->
history:clause Vec.t ->
local:clause Vec.t ->
unit
(** Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
@ -31,7 +30,6 @@ module type S = sig
Format.formatter ->
hyps:clause Vec.t ->
history:clause Vec.t ->
local:clause Vec.t ->
unit
(** Export the given clause vectors to the dimacs format.
The arguments should be transmitted directly from the corresponding
@ -42,6 +40,6 @@ module type S = sig
end
module Make(St: Solver_types_intf.S) : S with type clause := St.clause and type st = St.t
module Make(St: Sidekick_sat.S) : S with type clause := St.clause and type st = St.t
(** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *)

75
src/backend/Dot.ml
View file

@ -11,7 +11,6 @@ module type S = Backend_intf.S
module type Arg = sig
type atom
(* Type of atoms *)
type hyp
type lemma
@ -28,9 +27,10 @@ module type Arg = sig
end
module Default(S : Res.S) = struct
module Default(S : Sidekick_sat.S) = struct
module Atom = S.Atom
module Clause = S.Clause
module P = S.Proof
let print_atom = Atom.pp
@ -49,37 +49,39 @@ module Default(S : Res.S) = struct
end
(** Functor to provide dot printing *)
module Make(S : Res.S)(A : Arg with type atom := S.atom
module Make(S : Sidekick_sat.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
let node_id n = Clause.name n.S.conclusion
let node_id n = Clause.name n.P.conclusion
let res_node_id n = (node_id n) ^ "_res"
let proof_id p = node_id (S.expand p)
let proof_id p = node_id (P.expand p)
let print_clause fmt c =
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);
Format.fprintf fmt "%a" A.print_atom (Array.get v i);
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_edges fmt n =
match S.(n.step) with
| S.Resolution (p1, p2, _) ->
match n.P.step with
| P.Resolution (p1, p2, _) ->
print_edge fmt (res_node_id n) (proof_id p1);
print_edge fmt (res_node_id n) (proof_id p2)
| _ -> ()
@ -107,29 +109,29 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let ttify f c = fun fmt () -> f fmt c
let print_contents fmt n =
match S.(n.step) with
match n.P.step with
(* Leafs of the proof tree *)
| S.Hypothesis ->
let rule, color, l = A.hyp_info S.(n.conclusion) in
| P.Hypothesis ->
let rule, color, l = A.hyp_info P.(n.conclusion) in
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
| S.Assumption ->
let rule, color, l = A.assumption_info S.(n.conclusion) 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
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
| S.Lemma _ ->
let rule, color, l = A.lemma_info S.(n.conclusion) 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
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
(* Tree nodes *)
| S.Duplicate (p, l) ->
print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY"
| 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_edge fmt (node_id n) (node_id (S.expand p))
| S.Resolution (_, _, a) ->
print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
print_edge fmt (node_id n) (node_id (P.expand p))
| P.Resolution (_, _, a) ->
print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY"
[(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
print_dot_res_node fmt (res_node_id n) a;
print_edge fmt (node_id n) (res_node_id n)
@ -140,45 +142,46 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let print fmt p =
Format.fprintf fmt "digraph proof {@\n";
S.fold (fun () -> print_node fmt) () p;
P.fold (fun () -> print_node fmt) () p;
Format.fprintf fmt "}@."
end
module Simple(S : Res.S)
(A : Arg with type atom := S.formula
and type hyp = S.formula list
module Simple(S : Sidekick_sat.S)
(A : Arg with type atom := S.atom
and type hyp = S.atom list
and type lemma := S.lemma
and type assumption = S.formula) =
and type assumption = S.atom) =
Make(S)(struct
module Atom = S.Atom
module Clause = S.Clause
module P = S.Proof
(* Some helpers *)
let lit = Atom.lit
let get_form = Atom.get_formula
let get_assumption c =
match S.Clause.atoms_l c with
match Clause.atoms_l c with
| [ x ] -> x
| _ -> assert false
let get_lemma c =
match S.expand (S.prove c) with
| {S.step=S.Lemma p;_} -> p
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 (Atom.lit a)
A.print_atom fmt a
let hyp_info c =
A.hyp_info (List.map lit (S.Clause.atoms_l c))
A.hyp_info (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))
A.assumption_info (get_assumption c)
end)

10
src/backend/Dot.mli
View file

@ -47,23 +47,23 @@ module type Arg = sig
end
module Default(S : Res.S) : Arg with type atom := S.atom
module Default(S : Sidekick_sat.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 Make(S : Res.S)(A : Arg with type atom := S.atom
module Make(S : Sidekick_sat.S)(A : 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 Simple(S : Res.S)(A : Arg with type atom := S.formula
and type hyp = S.formula list
module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
and type hyp = S.atom list
and type lemma := S.lemma
and type assumption = S.formula) : S with type t := S.proof
and type assumption = S.atom) : 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. *)

3
src/backend/jbuild
View file

@ -6,7 +6,8 @@
(public_name sidekick.backend)
(synopsis "proof backends for Sidekick")
(libraries (sidekick.sat))
(flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat))
(flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string
-open Sidekick_sat -open Sidekick_util))
(ocamlopt_flags (:standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20))
))

2
src/main/main.ml
View file

@ -34,7 +34,7 @@ let p_progress = ref false
let hyps : Ast.term list ref = ref []
module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver.Proof)(Sidekick_backend.Dot.Default(Solver.Sat_solver.Proof))
module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver)
let check_model _state =
let check_clause _c =

668
src/sat/Internal.ml
View file

@ -4,21 +4,109 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make
(St : Solver_types.S)
(Th : Theory_intf.S with type formula = St.formula
and type proof = St.proof)
= struct
module Proof = Res.Make(St)
open St
module Var_fields = Solver_intf.Var_fields
let v_field_seen_neg = Var_fields.mk_field()
let v_field_seen_pos = Var_fields.mk_field()
let () = Var_fields.freeze()
module C_fields = Solver_intf.C_fields
let c_field_attached = C_fields.mk_field () (* watching literals? *)
let c_field_visited = C_fields.mk_field () (* used during propagation and proof generation. *)
module Make (Th : Theory_intf.S) = struct
type formula = Th.Form.t
type lemma = Th.proof
type var = {
vid : int;
pa : atom;
na : atom;
mutable v_fields : Var_fields.t;
mutable v_level : int;
mutable v_idx: int; (** position in heap *)
mutable v_weight : float; (** Weight (for the heap), tracking activity *)
mutable reason : reason option;
}
and atom = {
aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
mutable watched : clause Vec.t;
}
and clause = {
name : int;
tag : int option;
atoms : atom array;
mutable cpremise : premise;
mutable activity : float;
mutable c_flags : C_fields.t
}
and reason =
| Decision
| Bcp of clause
and premise =
| Hyp
| Local
| Lemma of lemma
| History of clause list
type proof = clause
let rec dummy_var =
{ vid = -101;
pa = dummy_atom;
na = dummy_atom;
v_fields = Var_fields.empty;
v_level = -1;
v_weight = -1.;
v_idx= -1;
reason = None;
}
and dummy_atom =
{ var = dummy_var;
lit = Th.Form.dummy;
watched = Obj.magic 0;
(* should be [Vec.make_empty dummy_clause]
but we have to break the cycle *)
neg = dummy_atom;
is_true = false;
aid = -102;
}
let dummy_clause =
{ name = -1;
tag = None;
atoms = [| |];
activity = -1.;
c_flags = C_fields.empty;
cpremise = History [];
}
let () = dummy_atom.watched <- Vec.make_empty dummy_clause
(* Constructors *)
module MF = Hashtbl.Make(Th.Form)
let name_of_clause c = match c.cpremise with
| Hyp -> "H" ^ string_of_int c.name
| Local -> "L" ^ string_of_int c.name
| Lemma _ -> "T" ^ string_of_int c.name
| History _ -> "C" ^ string_of_int c.name
module H = Heap.Make(struct
type t = St.var
let[@inline] cmp i j = Var.weight j < Var.weight i (* comparison by weight *)
let dummy = St.Var.dummy
let idx = St.Var.idx
let set_idx = St.Var.set_idx
type t = var
let[@inline] cmp i j = j.v_weight < i.v_weight (* comparison by weight *)
let dummy = dummy_var
let[@inline] idx v = v.v_idx
let[@inline] set_idx v i = v.v_idx <- i
end)
exception Sat
@ -48,7 +136,10 @@ module Make
(* Singleton type containing the current state *)
type t = {
st : St.t;
f_map: var MF.t;
vars: var Vec.t;
mutable cpt_mk_var: int;
mutable cpt_mk_clause: int;
th: Th.t lazy_t;
@ -123,20 +214,23 @@ module Make
}
(* Starting environment. *)
let create_ ~st ~size_trail ~size_lvl th : t = {
st;
let create_ ~size_map ~size_vars ~size_trail ~size_lvl th : t = {
f_map = MF.create size_map;
vars = Vec.make size_vars dummy_var;
cpt_mk_var = 0;
cpt_mk_clause = 0;
th;
unsat_conflict = None;
next_decision = None;
clauses_hyps = Vec.make 0 Clause.dummy;
clauses_learnt = Vec.make 0 Clause.dummy;
clauses_temp = Vec.make 0 Clause.dummy;
clauses_hyps = Vec.make 0 dummy_clause;
clauses_learnt = Vec.make 0 dummy_clause;
clauses_temp = Vec.make 0 dummy_clause;
th_head = 0;
elt_head = 0;
trail = Vec.make size_trail Atom.dummy;
trail = Vec.make size_trail dummy_atom;
elt_levels = Vec.make size_lvl (-1);
backtrack_levels = Vec.make size_lvl (-1);
backtrack = Vec.make size_lvl (fun () -> ());
@ -151,6 +245,497 @@ module Make
dirty=false;
}
type state = t
let[@inline] n_vars st = Vec.size st.vars
let[@inline] get_var st i = Vec.get st.vars i
module Var = struct
type t = var
let dummy = dummy_var
let[@inline] level v = v.v_level
let[@inline] pos v = v.pa
let[@inline] neg v = v.na
let[@inline] reason v = v.reason
let[@inline] weight v = v.v_weight
let[@inline] id v = v.vid
let[@inline] level v = v.v_level
let[@inline] idx v = v.v_idx
let[@inline] set_level v lvl = v.v_level <- lvl
let[@inline] set_idx v i = v.v_idx <- i
let[@inline] set_weight v w = v.v_weight <- w
let[@inline] in_heap v = v.v_idx >= 0
let make (st:state) (t:formula) : var * Theory_intf.negated =
let lit, negated = Th.Form.norm t in
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;
v_fields = Var_fields.empty;
v_level = -1;
v_idx= -1;
v_weight = 0.;
reason = None;
}
and pa =
{ var = var;
lit = lit;
watched = Vec.make 10 dummy_clause;
neg = na;
is_true = false;
aid = cpt_double (* aid = vid*2 *) }
and na =
{ var = var;
lit = Th.Form.neg lit;
watched = Vec.make 10 dummy_clause;
neg = pa;
is_true = false;
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;
Vec.push st.vars var;
var, negated
(* Marking helpers *)
let[@inline] clear v =
v.v_fields <- Var_fields.empty
let[@inline] seen_both v =
Var_fields.get v_field_seen_pos v.v_fields &&
Var_fields.get v_field_seen_neg v.v_fields
end
module Atom = struct
type t = atom
let dummy = dummy_atom
let[@inline] level a = a.var.v_level
let[@inline] var a = a.var
let[@inline] neg a = a.neg
let[@inline] abs a = a.var.pa
let[@inline] get_formula a = a.lit
let[@inline] equal a b = a == b
let[@inline] is_pos a = a == abs a
let[@inline] compare a b = Pervasives.compare a.aid b.aid
let[@inline] reason a = Var.reason a.var
let[@inline] id a = a.aid
let[@inline] is_true a = a.is_true
let[@inline] is_false a = a.neg.is_true
let[@inline] seen a =
let pos = equal a (abs a) in
if pos
then Var_fields.get v_field_seen_pos a.var.v_fields
else Var_fields.get v_field_seen_neg a.var.v_fields
let[@inline] mark a =
let pos = equal a (abs a) in
if pos
then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields
else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields
let[@inline] make st lit =
let var, negated = Var.make st lit in
match negated with
| Theory_intf.Negated -> var.na
| Theory_intf.Same_sign -> var.pa
let pp fmt a = Th.Form.print fmt a.lit
let pp_a fmt v =
if Array.length v = 0 then (
Format.fprintf fmt "∅"
) else (
pp fmt v.(0);
if (Array.length v) > 1 then begin
for i = 1 to (Array.length v) - 1 do
Format.fprintf fmt " ∨ %a" pp v.(i)
done
end
)
(* Complete debug printing *)
let 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)
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
Format.fprintf fmt "T%a" pp_level a
else if a.neg.is_true then
Format.fprintf fmt "F%a" pp_level a
else
Format.fprintf fmt ""
let debug out a =
Format.fprintf out "%s%d[%a][@[%a@]]"
(sign a) (a.var.vid+1) debug_value a Th.Form.print a.lit
let debug_a out vec =
Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec
end
module Clause = struct
type t = clause
let dummy = dummy_clause
let make =
let n = ref 0 in
fun ?tag atoms premise ->
let name = !n in
incr n;
{ name;
tag = tag;
atoms = atoms;
c_flags = C_fields.empty;
activity = 0.;
cpremise = premise;
}
let make_l ?tag l pr = make ?tag (Array.of_list l) pr
let empty = make [| |] (History [])
let name = name_of_clause
let[@inline] equal c1 c2 = c1==c2
let[@inline] atoms c = c.atoms
let[@inline] atoms_l c = Array.to_list c.atoms
let[@inline] tag c = c.tag
let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms
let[@inline] premise c = c.cpremise
let[@inline] set_premise c p = c.cpremise <- p
let[@inline] visited c = C_fields.get c_field_visited c.c_flags
let[@inline] set_visited c b = c.c_flags <- C_fields.set c_field_visited b c.c_flags
let[@inline] attached c = C_fields.get c_field_attached c.c_flags
let[@inline] set_attached c b = c.c_flags <- C_fields.set c_field_attached b c.c_flags
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)
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"
| Local -> Format.fprintf out "local"
| Lemma _ -> Format.fprintf out "th_lemma"
| History v -> Util.pp_list (CCFormat.of_to_string name_of_clause) out v
let debug out ({atoms=arr; cpremise=cp;_}as c) =
Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
(name c) Atom.debug_a arr debug_premise cp
let pp_dimacs fmt {atoms;_} =
let aux fmt a =
Array.iter (fun p ->
Format.fprintf fmt "%s%d "
(if p == p.var.pa then "-" else "")
(p.var.vid+1)
) a
in
Format.fprintf fmt "%a0" aux atoms
end
module Formula = struct
include Th.Form
let pp = print
end
module Proof = struct
type t = proof
exception Resolution_error of string
exception Insufficient_hyps
(** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
let equal_atoms = Atom.equal
let compare_atoms = Atom.compare
let merge = List.merge compare_atoms
let _c = ref 0
let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
(* Compute resolution of 2 clauses *)
let resolve l =
let rec aux resolved acc = function
| [] -> resolved, acc
| [a] -> resolved, a :: acc
| a :: b :: r ->
if equal_atoms a b then
aux resolved (a :: acc) r
else if equal_atoms (a.neg) b then
aux ((a.var.pa) :: resolved) acc r
else
aux resolved (a :: acc) (b :: r)
in
let resolved, new_clause = aux [] [] l in
resolved, List.rev new_clause
(* Compute the set of doublons of a clause *)
let list c = List.sort Atom.compare (Array.to_list (c.atoms))
let analyze cl =
let rec aux duplicates free = function
| [] -> duplicates, free
| [ x ] -> duplicates, x :: free
| x :: ((y :: r) as l) ->
if x == y then
count duplicates (x :: free) x [y] r
else
aux duplicates (x :: free) l
and count duplicates free x acc = function
| (y :: r) when x == y ->
count duplicates free x (y :: acc) r
| l ->
aux (acc :: duplicates) free l
in
let doublons, acc = aux [] [] cl in
doublons, List.rev acc
let to_list c =
let cl = list c in
let doublons, l = analyze cl in
let conflicts, _ = resolve l in
if doublons <> [] then
Log.debug 5 "Input clause has redundancies";
if conflicts <> [] then
Log.debug 5 "Input clause is a tautology";
cl
(* Comparison of clauses *)
let cmp_cl c d =
let rec aux = function
| [], [] -> 0
| a :: r, a' :: r' ->
begin match compare_atoms a a' with
| 0 -> aux (r, r')
| x -> x
end
| _ :: _ , [] -> -1
| [], _ :: _ -> 1
in
aux (c, d)
let[@inline] prove conclusion =
assert (conclusion.cpremise <> History []);
conclusion
let rec set_atom_proof a =
let aux acc b =
if equal_atoms a.neg b then acc
else set_atom_proof b :: acc
in
assert (a.var.v_level >= 0);
match (a.var.reason) with
| Some Bcp c ->
Log.debugf 5 (fun k->k "Analysing: @[%a@ %a@]" Atom.debug a Clause.debug c);
if Array.length c.atoms = 1 then (
Log.debugf 5 (fun k -> k "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 [| a.neg |] r in
a.var.reason <- Some (Bcp c');
Log.debugf 5
(fun k -> k "New reason: @[%a@ %a@]" Atom.debug a Clause.debug c');
c'
)
| _ ->
Log.debugf 1 (fun k -> k "Error while proving atom %a" Atom.debug a);
raise (Resolution_error "Cannot prove atom")
let prove_unsat conflict =
if Array.length conflict.atoms = 0 then conflict
else (
Log.debugf 2 (fun k -> k "Proving 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 [| |] (History (conflict :: l)) in
Log.debugf 2 (fun k -> k "Proof found: @[%a@]" Clause.debug res);
res
)
let prove_atom a =
if (a.is_true && a.var.v_level = 0) then
Some (set_atom_proof a)
else
None
(* Interface exposed *)
type node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis
| Assumption
| Lemma of lemma
| Duplicate of proof * atom list
| Resolution of proof * proof * atom
let rec chain_res (c, cl) = function
| d :: r ->
Log.debugf 5
(fun k -> k " Resolving clauses : @[%a@\n%a@]" Clause.debug c Clause.debug d);
let dl = to_list d in
begin match resolve (merge cl dl) with
| [ a ], l ->
begin match r with
| [] -> (l, c, d, a)
| _ ->
let new_clause = Clause.make_l l (History [c; d]) in
chain_res (new_clause, l) r
end
| _ ->
Log.debugf 1
(fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]"
Clause.debug c Clause.debug d);
raise (Resolution_error "Clause mismatch")
end
| _ ->
raise (Resolution_error "Bad history")
let[@inline] conclusion (p:proof) : clause = p
let expand conclusion =
Log.debugf 5 (fun k -> k "Expanding : @[%a@]" Clause.debug conclusion);
match conclusion.cpremise with
| Lemma l ->
{conclusion; step = Lemma l; }
| Hyp ->
{ conclusion; step = Hypothesis; }
| Local ->
{ conclusion; step = Assumption; }
| History [] ->
Log.debugf 1 (fun k -> k "Empty history for clause: %a" Clause.debug conclusion);
raise (Resolution_error "Empty history")
| History [ c ] ->
let duplicates, res = analyze (list c) in
assert (cmp_cl res (list conclusion) = 0);
{ conclusion; step = Duplicate (c, List.concat duplicates) }
| History ( c :: ([_] as r)) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
| History ( c :: r ) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
conclusion.cpremise <- History [c'; d'];
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
let[@inline] step p = (expand p).step
(* Proof nodes manipulation *)
let is_leaf = function
| Hypothesis
| Assumption
| Lemma _ -> true
| Duplicate _
| Resolution _ -> false
let parents = function
| Hypothesis
| Assumption
| Lemma _ -> []
| Duplicate (p, _) -> [p]
| Resolution (p, p', _) -> [p; p']
let expl = function
| Hypothesis -> "hypothesis"
| Assumption -> "assumption"
| Lemma _ -> "lemma"
| Duplicate _ -> "duplicate"
| Resolution _ -> "resolution"
(* Compute unsat-core
TODO: replace visited bool by a int unique to each call
of unsat_core, so that the cleanup can be removed ? *)
let unsat_core proof =
let rec aux res acc = function
| [] -> res, acc
| c :: r ->
if not (Clause.visited c) then (
Clause.set_visited c true;
match c.cpremise with
| Hyp | Local | Lemma _ -> 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
aux res (c :: acc) l
) else (
aux res acc r
)
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
module Tbl = Clause.Tbl
type task =
| Enter of proof
| Leaving of proof
let spop s = try Some (Stack.pop s) with Stack.Empty -> None
let rec fold_aux s h f acc =
match spop s with
| None -> acc
| Some (Leaving c) ->
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
Stack.push (Leaving c) s;
let node = expand c in
begin match node.step with
| Duplicate (p1, _) ->
Stack.push (Enter p1) s
| Resolution (p1, p2, _) ->
Stack.push (Enter p2) s;
Stack.push (Enter p1) s
| Hypothesis | Assumption | Lemma _ -> ()
end
end;
fold_aux s h f acc
let fold f acc p =
let h = Tbl.create 42 in
let s = Stack.create () in
Stack.push (Enter p) s;
fold_aux s h f acc
let check p = fold (fun () _ -> ()) () p
end
let[@inline] theory st = Lazy.force st.th
let[@inline] at_level_0 st : bool = Vec.is_empty st.backtrack_levels
let[@inline] on_backtrack st f : unit =
@ -158,7 +743,6 @@ module Make
Vec.push st.backtrack f
)
let[@inline] st t = t.st
let[@inline] nb_clauses st = Vec.size st.clauses_hyps
let[@inline] decision_level st = Vec.size st.elt_levels
let[@inline] base_level st = Vec.size st.user_levels
@ -202,8 +786,8 @@ module Make
H.insert st.order v;
)
let new_atom ~permanent st (p:formula) : St.atom =
let a = Atom.make st.st p in
let new_atom ~permanent st (p:formula) : atom =
let a = Atom.make st p in
if permanent then (
redo_down_to_level_0 st
(fun () -> insert_var_order st a.var)
@ -225,8 +809,8 @@ module Make
let var_bump_activity st v =
v.v_weight <- v.v_weight +. st.var_incr;
if v.v_weight > 1e100 then (
for i = 0 to St.nb_elt st.st - 1 do
Var.set_weight (St.get_elt st.st i) ((Var.weight (St.get_elt st.st i)) *. 1e-100)
for i = 0 to n_vars st - 1 do
Var.set_weight (get_var st i) ((Var.weight (get_var st i)) *. 1e-100)
done;
st.var_incr <- st.var_incr *. 1e-100;
);
@ -474,7 +1058,7 @@ module Make
Wrapper function for adding a new propagated formula. *)
let enqueue_bool st a reason : unit =
if a.neg.is_true then (
Util.errorf "(@[sat.enqueue_bool.error@ :false-literal %a@])" Atom.debug a
Util.errorf "(@[sat.enqueue_bool.1@ :false-literal %a@])" Atom.debug a
);
let level = decision_level st in
Log.debugf 5
@ -539,7 +1123,7 @@ module Make
)
(* result of conflict analysis, containing the learnt clause and some
additional info.
additional 2.
invariant: cr_history's order matters, as its head is later used
during pop operations to determine the origin of a clause/conflict
@ -609,7 +1193,7 @@ module Make
(* look for the next node to expand *)
while
let a = Vec.get st.trail !tr_ind in
Log.debugf 5 (fun k -> k "(@[sat.conflict.looking-at@ %a@])" St.Atom.debug a);
Log.debugf 5 (fun k -> k "(@[sat.conflict.looking-at@ %a@])" Atom.debug a);
(not (Var.seen_both a.var)) || (a.var.v_level < conflict_level)
do
decr tr_ind;
@ -906,7 +1490,7 @@ module Make
f a.lit
done
let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit =
let act_push_ ~permanent st (l:formula IArray.t) (lemma:lemma): unit =
let atoms = IArray.to_array_map (new_atom ~permanent st) l in
let c = Clause.make atoms (Lemma lemma) in
Log.debugf 3
@ -933,7 +1517,7 @@ module Make
)
) else (
Util.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \
:error all lits are not true@])"
:1 all lits are not true@])"
(Util.pp_list Atom.debug) l
)
@ -955,15 +1539,14 @@ module Make
propagate = act_propagate st;
}
let create ?(size=`Big) ?st () : t =
let st = match st with Some s -> s | None -> St.create ~size () in
let size_trail, size_lvl = match size with
| `Tiny -> 0, 0
| `Small -> 32, 16
| `Big -> 600, 50
let create ?(size=`Big) () : t =
let size_map, size_vars, size_trail, size_lvl = match size with
| `Tiny -> 8, 0, 0, 0
| `Small -> 16, 0, 32, 16
| `Big -> 4096, 128, 600, 50
in
let rec solver = lazy (
create_ ~st ~size_trail ~size_lvl th
create_ ~size_map ~size_vars ~size_trail ~size_lvl th
) and th = lazy (
Th.create (actions (Lazy.force solver))
) in
@ -991,7 +1574,7 @@ module Make
(* conflict *)
let l = List.rev_map (new_atom ~permanent:false st) l in
List.iter (fun a -> insert_var_order st a.var) l;
let c = St.Clause.make_l l (Lemma p) in
let c = Clause.make_l l (Lemma p) in
Some c
)
@ -1057,8 +1640,7 @@ module Make
| None -> (* No Conflict *)
assert (st.elt_head = Vec.size st.trail);
assert (st.elt_head = st.th_head);
if Vec.size st.trail = St.nb_elt st.st
then raise Sat;
if Vec.size st.trail = n_vars st then raise Sat;
if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
Log.debug 3 "(sat.restarting)";
cancel_until st (base_level st);
@ -1074,7 +1656,7 @@ module Make
done
let eval_level (st:t) lit =
let var, negated = Var.make st.st lit in
let var, negated = Var.make st lit in
if not var.pa.is_true && not var.na.is_true
then raise UndecidedLit
else assert (var.v_level >= 0);
@ -1172,7 +1754,7 @@ module Make
(* pop the last factice decision level *)
let pop st : unit =
if base_level st = 0 then (
Log.debug 2 "(sat.error: cannot pop (already at level 0))"
Log.debug 2 "(sat.1: cannot pop (already at level 0))"
) else (
Log.debug 3 "(sat.pop-user-level)";
assert (base_level st > 0);
@ -1212,7 +1794,7 @@ module Make
cancel_until st (base_level st);
List.iter add_lit assumptions
| Some _ ->
Log.debug 2 "(sat.local_assumptions.error: already unsat)"
Log.debug 2 "(sat.local_assumptions.1: already unsat)"
(* Check satisfiability *)
let check_clause c =
@ -1223,7 +1805,7 @@ module Make
let res = Array.exists (fun x -> x) tmp in
if not res then (
Log.debugf 5
(fun k -> k "(@[sat.check-clause.error@ :not-satisfied %a@])" Clause.debug c);
(fun k -> k "(@[sat.check-clause.1@ :not-satisfied %a@])" Clause.debug c);
false
) else
true

302
src/sat/Res.ml
View file

@ -1,302 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type S = Res_intf.S
module type FULL = Res_intf.FULL
module Make(St : Solver_types.S) = struct
module St = St
type formula = St.formula
type lemma = St.proof
type clause = St.clause
type atom = St.atom
exception Insufficient_hyps
exception Resolution_error of string
(* Log levels *)
let error = 1
let warn = 3
let info = 10
let debug = 80
let equal_atoms a b = St.(a.aid) = St.(b.aid)
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
module Clause = St.Clause
module Atom = St.Atom
let merge = List.merge compare_atoms
let _c = ref 0
let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
(* Compute resolution of 2 clauses *)
let resolve l =
let rec aux resolved acc = function
| [] -> resolved, acc
| [a] -> resolved, a :: acc
| a :: b :: r ->
if equal_atoms a b then
aux resolved (a :: acc) r
else if equal_atoms St.(a.neg) b then
aux (St.(a.var.pa) :: resolved) acc r
else
aux resolved (a :: acc) (b :: r)
in
let resolved, new_clause = aux [] [] l in
resolved, List.rev new_clause
(* Compute the set of doublons of a clause *)
let list c = List.sort St.Atom.compare (Array.to_list St.(c.atoms))
let analyze cl =
let rec aux duplicates free = function
| [] -> duplicates, free
| [ x ] -> duplicates, x :: free
| x :: ((y :: r) as l) ->
if x == y then
count duplicates (x :: free) x [y] r
else
aux duplicates (x :: free) l
and count duplicates free x acc = function
| (y :: r) when x == y ->
count duplicates free x (y :: acc) r
| l ->
aux (acc :: duplicates) free l
in
let doublons, acc = aux [] [] cl in
doublons, List.rev acc
let to_list c =
let cl = list c in
let doublons, l = analyze cl in
let conflicts, _ = resolve l in
if doublons <> [] then
Log.debug warn "Input clause has redundancies";
if conflicts <> [] then
Log.debug warn "Input clause is a tautology";
cl
(*
let pp_cl fmt l =
let rec aux fmt = function
| [] -> ()
| a :: r ->
Format.fprintf fmt "%a@,%a" St.pp_atom a aux r
in
Format.fprintf fmt "@[<v>%a@]" aux l
*)
(* Comparison of clauses *)
let cmp_cl c d =
let rec aux = function
| [], [] -> 0
| a :: r, a' :: r' ->
begin match compare_atoms a a' with
| 0 -> aux (r, r')
| x -> x
end
| _ :: _ , [] -> -1
| [], _ :: _ -> 1
in
aux (c, d)
let[@inline] prove conclusion =
assert St.(conclusion.cpremise <> History []);
conclusion
let rec set_atom_proof a =
let aux acc b =
if equal_atoms a.St.neg b then acc
else set_atom_proof b :: acc
in
assert St.(a.var.v_level >= 0);
match St.(a.var.reason) with
| Some St.Bcp c ->
Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c);
if Array.length c.St.atoms = 1 then (
Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.Atom.debug a);
c
) else (
assert (a.St.neg.St.is_true);
let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
let c' = St.Clause.make [| a.St.neg |] r in
a.St.var.St.reason <- Some St.(Bcp c');
Log.debugf debug
(fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c');
c'
)
| _ ->
Log.debugf error (fun k -> k "Error while proving atom %a" St.Atom.debug a);
raise (Resolution_error "Cannot prove atom")
let prove_unsat conflict =
if Array.length conflict.St.atoms = 0 then conflict
else (
Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict);
let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
let res = St.Clause.make [| |] (St.History (conflict :: l)) in
Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res);
res
)
let prove_atom a =
if St.(a.is_true && a.var.v_level = 0) then
Some (set_atom_proof a)
else
None
(* Interface exposed *)
type proof = clause
and proof_node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis
| Assumption
| Lemma of lemma
| Duplicate of proof * atom list
| Resolution of proof * proof * atom
let rec chain_res (c, cl) = function
| d :: r ->
Log.debugf debug
(fun k -> k " Resolving clauses : @[%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
let dl = to_list d in
begin match resolve (merge cl dl) with
| [ a ], l ->
begin match r with
| [] -> (l, c, d, a)
| _ ->
let new_clause = St.Clause.make_l l (St.History [c; d]) in
chain_res (new_clause, l) r
end
| _ ->
Log.debugf error
(fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]"
St.Clause.debug c St.Clause.debug d);
raise (Resolution_error "Clause mismatch")
end
| _ ->
raise (Resolution_error "Bad history")
let[@inline] conclusion (p:proof) : clause = p
let expand conclusion =
Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion);
match conclusion.St.cpremise with
| St.Lemma l ->
{conclusion; step = Lemma l; }
| St.Hyp ->
{ conclusion; step = Hypothesis; }
| St.Local ->
{ conclusion; step = Assumption; }
| St.History [] ->
Log.debugf error (fun k -> k "Empty history for clause: %a" St.Clause.debug conclusion);
raise (Resolution_error "Empty history")
| St.History [ c ] ->
let duplicates, res = analyze (list c) in
assert (cmp_cl res (list conclusion) = 0);
{ conclusion; step = Duplicate (c, List.concat duplicates) }
| St.History ( c :: ([_] as r)) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
| St.History ( c :: r ) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
conclusion.St.cpremise <- St.History [c'; d'];
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
(* Proof nodes manipulation *)
let is_leaf = function
| Hypothesis
| Assumption
| Lemma _ -> true
| Duplicate _
| Resolution _ -> false
let parents = function
| Hypothesis
| Assumption
| Lemma _ -> []
| Duplicate (p, _) -> [p]
| Resolution (p, p', _) -> [p; p']
let expl = function
| Hypothesis -> "hypothesis"
| Assumption -> "assumption"
| Lemma _ -> "lemma"
| Duplicate _ -> "duplicate"
| Resolution _ -> "resolution"
(* Compute unsat-core
TODO: replace visited bool by a int unique to each call
of unsat_core, so that the cleanup can be removed ? *)
let unsat_core proof =
let rec aux res acc = function
| [] -> res, acc
| c :: r ->
if not (Clause.visited c) then (
Clause.set_visited c true;
match c.St.cpremise with
| St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r
| St.History h ->
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 (
aux res acc r
)
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
module Tbl = Clause.Tbl
type task =
| Enter of proof
| Leaving of proof
let spop s = try Some (Stack.pop s) with Stack.Empty -> None
let rec fold_aux s h f acc =
match spop s with
| None -> acc
| Some (Leaving c) ->
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
Stack.push (Leaving c) s;
let node = expand c in
begin match node.step with
| Duplicate (p1, _) ->
Stack.push (Enter p1) s
| Resolution (p1, p2, _) ->
Stack.push (Enter p2) s;
Stack.push (Enter p1) s
| Hypothesis | Assumption | Lemma _ -> ()
end
end;
fold_aux s h f acc
let fold f acc p =
let h = Tbl.create 42 in
let s = Stack.create () in
Stack.push (Enter p) s;
fold_aux s h f acc
let check p = fold (fun () _ -> ()) () p
end

19
src/sat/Res.mli
View file

@ -1,19 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Resolution proofs
This modules defines functions to create and manipulate resolution proofs.
*)
module type S = Res_intf.S
(** Interface for a module manipulating resolution proofs. *)
module type FULL = Res_intf.FULL
module Make : functor (St : Solver_types.S) -> FULL with module St = St
(** Functor to create a module building proofs from a sat-solver unsat trace. *)

136
src/sat/Res_intf.ml
View file

@ -1,136 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Interface for proofs *)
type 'a printer = Format.formatter -> 'a -> unit
module type S = sig
(** Signature for a module handling proof by resolution from sat solving traces *)
(** {3 Type declarations} *)
exception Insufficient_hyps
(** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
type formula
type atom
type lemma
type clause
(** Abstract types for atoms, clauses and theory-specific lemmas *)
type proof
(** Lazy type for proof trees. Proofs are persistent objects, and can be
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 *)
}
(** 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
(** 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 *)
| Duplicate of proof * atom list
(** The conclusion is obtained by eliminating multiple occurences of the atom in
the conclusion of the provided proof. *)
| Resolution of proof * proof * atom
(** 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 building functions} *)
val prove : clause -> proof
(** Given a clause, return a proof of that clause.
@raise Insuficient_hyps if it does not succeed. *)
val prove_unsat : clause -> proof
(** Given a conflict clause [c], returns a proof of the empty clause.
@raise Insuficient_hyps if it does not succeed. *)
val prove_atom : atom -> proof option
(** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
(** {3 Proof Nodes} *)
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. *)
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). *)
val parents : step -> proof list
(** Returns the parents of a proof node. *)
(** {3 Proof Manipulation} *)
val expand : proof -> proof_node
(** Return the proof step at the root of a given proof. *)
val conclusion : proof -> clause
(** What is proved at the root of the clause *)
val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> '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. *)
val unsat_core : proof -> 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 *)
(** {3 Misc} *)
val check : proof -> unit
(** Check the contents of a proof. Mainly for internal use *)
module Clause : sig
type t = clause
val name : t -> string
val atoms : t -> atom array
val atoms_l : t -> atom list
val pp : t printer
(** A nice looking printer for clauses, which sort the atoms before printing. *)
module Tbl : Hashtbl.S with type key = t
end
module Atom : sig
type t = atom
val is_pos : t -> bool
val neg : t -> t
val abs : t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val lit : t -> formula
val pp : t printer
end
module Tbl : Hashtbl.S with type key = proof
end
module type FULL = sig
module St : Solver_types.S
(** Module defining atom and clauses *)
include S with type atom = St.atom
and type lemma = St.proof
and type clause = St.clause
and type formula = St.formula
end

5
src/sat/Sidekick_sat.ml
View file

@ -2,9 +2,6 @@
(** Main API *)
module Theory_intf = Theory_intf
module Solver_types_intf = Solver_types_intf
module Res = Res
module type S = Solver_intf.S
@ -50,7 +47,7 @@ type ('form, 'proof) slice_actions = ('form, 'proof) Theory_intf.slice_actions =
slice_iter : ('form -> unit) -> unit;
}
module Make(E : Theory_intf.S) = Solver.Make(Solver_types.Make(E))(E)
module Make = Solver.Make
(**/**)
module Vec = Vec

64
src/sat/Solver.ml
View file

@ -8,25 +8,24 @@ module type S = Solver_intf.S
open Solver_intf
module Make
(St : Solver_types.S)
(Th : Theory_intf.S with type formula = St.formula
and type proof = St.proof)
= struct
module St = St
module S = Internal.Make(St)(Th)
module Make (Th : Theory_intf.S) = struct
module S = Internal.Make(Th)
module Proof = S.Proof
exception UndecidedLit = S.UndecidedLit
type formula = St.formula
type atom = St.formula
type lit = St.atom
type clause = St.clause
type formula = S.formula
type atom = S.atom
type clause = S.clause
type theory = Th.t
type proof = S.proof
type lemma = S.lemma
type premise = S.premise =
| Hyp
| Local
| Lemma of lemma
| History of clause list
type t = S.t
type solver = t
@ -35,8 +34,8 @@ module Make
(* Result type *)
type res =
| Sat of St.formula sat_state
| Unsat of (St.clause,Proof.proof) unsat_state
| Sat of formula sat_state
| Unsat of (clause,proof) unsat_state
let pp_all st lvl status =
Log.debugf lvl
@ -44,15 +43,15 @@ module Make
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
status
(Vec.print ~sep:"" St.Atom.debug) (S.trail st)
(Vec.print ~sep:"" St.Clause.debug) (S.temp st)
(Vec.print ~sep:"" St.Clause.debug) (S.hyps st)
(Vec.print ~sep:"" St.Clause.debug) (S.history st)
(Vec.print ~sep:"" S.Atom.debug) (S.trail st)
(Vec.print ~sep:"" S.Clause.debug) (S.temp st)
(Vec.print ~sep:"" S.Clause.debug) (S.hyps st)
(Vec.print ~sep:"" S.Clause.debug) (S.history st)
)
let mk_sat (st:S.t) : _ sat_state =
pp_all st 99 "SAT";
let iter f : unit = Vec.iter (fun a -> f a.St.lit) (S.trail st) in
let iter f : unit = Vec.iter (fun a -> f a.S.lit) (S.trail st) in
Sat_state {
eval = S.eval st;
eval_level = S.eval_level st;
@ -109,6 +108,7 @@ module Make
cleanup_ st;
S.pop st
let n_vars = S.n_vars
let unsat_core = S.Proof.unsat_core
let true_at_level0 st a =
@ -117,7 +117,7 @@ module Make
b && lev = 0
with S.UndecidedLit -> false
let get_tag cl = St.(cl.tag)
let[@inline] get_tag cl = S.(cl.tag)
let[@inline] new_atom ~permanent st a =
cleanup_ st;
@ -125,32 +125,30 @@ module Make
let actions = S.actions
let export (st:t) : St.clause export =
let export (st:t) : S.clause export =
let hyps = S.hyps st in
let history = S.history st in
let local = S.temp st in
{hyps; history; local}
module Lit = struct
type t = lit
let pp = St.Atom.pp
module Atom = struct
include S.Atom
let make = S.new_atom ~permanent:false
end
module Clause = struct
include St.Clause
include S.Clause
let atoms c = St.Clause.atoms c |> IArray.of_array_map (fun a -> a.St.lit)
let atoms_l c = St.Clause.atoms_l c |> List.map (fun a -> a.St.lit)
let forms c = atoms c |> IArray.of_array_map Atom.get_formula
let forms_l c = atoms_l c |> List.map Atom.get_formula
let[@inline] make ?tag (a:lit array) : t = St.Clause.make ?tag a St.Hyp
let[@inline] make_l ?tag l : t = St.Clause.make_l ?tag l St.Hyp
let[@inline] make ?tag (a:atom array) : t = S.Clause.make ?tag a S.Hyp
let[@inline] make_l ?tag l : t = S.Clause.make_l ?tag l S.Hyp
let of_atoms st ?tag l =
let of_formulas st ?tag l =
let l = List.map (S.new_atom ~permanent:false st) l in
make_l ?tag l
end
module Formula = St.Formula
module Formula = S.Formula
end

10
src/sat/Solver.mli
View file

@ -13,14 +13,10 @@ Copyright 2014 Simon Cruanes
module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Make
(St : Solver_types.S)
(Th : Theory_intf.S with type formula = St.formula
and type proof = St.proof)
: S with type formula = St.formula
and type clause = St.clause
and type Proof.lemma = St.proof
module Make(Th : Theory_intf.S)
: S with type formula = Th.formula
and type theory = Th.t
and type lemma = Th.proof
(** Functor to make a safe external interface. *)

167
src/sat/Solver_intf.ml
View file

@ -5,6 +5,11 @@
functor in {!Solver} or {!Mcsolver}.
*)
module Var_fields = BitField.Make()
module C_fields = BitField.Make()
type 'a printer = Format.formatter -> 'a -> unit
type 'form sat_state = Sat_state of {
eval: 'form -> bool;
(** Returns the valuation of a formula in the current state
@ -37,8 +42,6 @@ type 'clause export = {
}
(** Export internal state *)
type 'a printer = Format.formatter -> 'a -> unit
(** The external interface implemented by safe solvers, such as the one
created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
module type S = sig
@ -46,16 +49,29 @@ module type S = sig
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
type formula (** user formulas *)
type formula
(** 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 lit (** SAT solver literals *)
type atom (** SAT solver literals *)
type clause (** SAT solver clauses *)
type theory (** user theory *)
module Proof : Res.S with type clause = clause
(** A module to manipulate proofs. *)
type proof
(** Lazy type for proof trees. Proofs are persistent objects, and can be
extended to proof nodes using functions defined later. *)
type lemma (** A theory lemma, used to justify a theory conflict clause *)
type premise =
| Hyp
| Local
| Lemma of lemma
| History of clause list
type t
(** Main solver type, containing all state for solving. *)
@ -67,15 +83,10 @@ module type S = sig
(** {2 Types} *)
type atom = formula
(** 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. *)
(** Result type for the solver *)
type res =
| Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
| Unsat of (clause,proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
@ -83,9 +94,11 @@ module type S = sig
(** {2 Base operations} *)
val n_vars : t -> int
val theory : t -> theory
val assume : ?permanent:bool -> t -> ?tag:int -> atom list list -> unit
val assume : ?permanent:bool -> t -> ?tag:int -> formula list list -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place.
@param permanent if true, kept after backtracking (default true) *)
@ -94,23 +107,23 @@ module type S = sig
(** Lower level addition of clauses. See {!Clause} to create clauses.
@param permanent if true, kept after backtracking *)
val solve : t -> ?assumptions:atom list -> unit -> res
val solve : t -> ?assumptions:formula list -> unit -> 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. *)
val new_atom : permanent:bool -> t -> atom -> unit
val new_atom : permanent:bool -> t -> formula -> unit
(** Add a new atom (i.e propositional formula) to the solver.
This formula will be decided on at some point during solving,
whether it appears in clauses or not.
@param permanent if true, kept after backtracking *)
val unsat_core : Proof.proof -> clause list
val unsat_core : proof -> clause list
(** Returns the unsat core of a given proof, ie a subset of all the added
clauses that is sufficient to establish unsatisfiability. *)
val true_at_level0 : t -> atom -> bool
val true_at_level0 : t -> formula -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *)
@ -126,7 +139,7 @@ module type S = sig
(** Return to last save point, discarding clauses added since last
call to [push] *)
val actions : t -> (formula,Proof.lemma) Theory_intf.actions
val actions : t -> (formula,lemma) Theory_intf.actions
(** Obtain actions *)
val export : t -> clause export
@ -135,30 +148,132 @@ module type S = sig
type solver = t
module Lit : sig
type t = lit
module Atom : sig
type t = atom
val is_pos : t -> bool
val neg : t -> t
val abs : t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val get_formula : t -> formula
val make : solver -> atom -> t
val pp : t CCFormat.printer
val make : solver -> formula -> t
val pp : t printer
end
(** A module to manipulate proofs. *)
module Proof : sig
type t = proof
type node = {
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. *)
(** The type of reasoning steps allowed in a proof. *)
and step =
| Hypothesis
(** 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 *)
| Duplicate of proof * atom list
(** The conclusion is obtained by eliminating multiple occurences of the atom in
the conclusion of the provided proof. *)
| Resolution of proof * proof * atom
(** 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. *)
exception Insufficient_hyps
(** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
(** {3 Proof building functions} *)
val prove : clause -> t
(** Given a clause, return a proof of that clause.
@raise Insuficient_hyps if it does not succeed. *)
val prove_unsat : clause -> t
(** Given a conflict clause [c], returns a proof of the empty clause.
@raise Insuficient_hyps 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 *)
(** {3 Proof Nodes} *)
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. *)
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). *)
val parents : step -> t list
(** Returns the parents of a proof node. *)
(** {3 Proof Manipulation} *)
val expand : proof -> node
(** Return the proof step at the root of a given proof. *)
val step : proof -> step
val conclusion : proof -> clause
(** What is proved at the root of the clause *)
val fold : ('a -> 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. *)
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 *)
(** {3 Misc} *)
val check : t -> unit
(** Check the contents of a proof. Mainly for internal use *)
module Tbl : Hashtbl.S with type key = t
end
module Clause : sig
type t = clause
val atoms : t -> atom IArray.t
val atoms : t -> atom array (** do not modify *)
val atoms_l : t -> atom list
val forms : t -> formula IArray.t
val forms_l : t -> formula list
val tag : t -> int option
val equal : t -> t -> bool
val make : ?tag:int -> lit array -> t
val make : ?tag:int -> atom array -> t
(** Make a clause from this array of SAT literals.
The array's ownership is transferred to the clause, do not mutate it *)
val make_l : ?tag:int -> lit list -> t
val make_l : ?tag:int -> atom list -> t
val of_atoms : solver -> ?tag:int -> atom list -> t
val of_formulas : solver -> ?tag:int -> formula list -> t
val premise : t -> premise
val name : t -> string
val pp : t printer
val pp_dimacs : t printer
val dummy : t
module Tbl : Hashtbl.S with type key = t
end
module Formula : sig

345
src/sat/Solver_types.ml
View file

@ -1,345 +0,0 @@
module type S = Solver_types_intf.S
module Var_fields = Solver_types_intf.Var_fields
let v_field_seen_neg = Var_fields.mk_field()
let v_field_seen_pos = Var_fields.mk_field()
let () = Var_fields.freeze()
module C_fields = Solver_types_intf.C_fields
let c_field_attached = C_fields.mk_field () (* watching literals? *)
let c_field_visited = C_fields.mk_field () (* used during propagation and proof generation. *)
(* Solver types for McSat Solving *)
(* ************************************************************************ *)
module Make (E : Theory_intf.S) = struct
type formula = E.Form.t
type proof = E.proof
type var = {
vid : int;
pa : atom;
na : atom;
mutable v_fields : Var_fields.t;
mutable v_level : int;
mutable v_idx: int; (** position in heap *)
mutable v_weight : float; (** Weight (for the heap), tracking activity *)
mutable reason : reason option;
}
and atom = {
aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
mutable watched : clause Vec.t;
}
and clause = {
name : int;
tag : int option;
atoms : atom array;
mutable cpremise : premise;
mutable activity : float;
mutable c_flags : C_fields.t
}
and reason =
| Decision
| Bcp of clause
and premise =
| Hyp
| Local
| Lemma of proof
| History of clause list
let rec dummy_var =
{ vid = -101;
pa = dummy_atom;
na = dummy_atom;
v_fields = Var_fields.empty;
v_level = -1;
v_weight = -1.;
v_idx= -1;
reason = None;
}
and dummy_atom =
{ var = dummy_var;
lit = E.Form.dummy;
watched = Obj.magic 0;
(* should be [Vec.make_empty dummy_clause]
but we have to break the cycle *)
neg = dummy_atom;
is_true = false;
aid = -102;
}
let dummy_clause =
{ name = -1;
tag = None;
atoms = [| |];
activity = -1.;
c_flags = C_fields.empty;
cpremise = History [];
}
let () = dummy_atom.watched <- Vec.make_empty dummy_clause
(* Constructors *)
module MF = Hashtbl.Make(E.Form)
type t = {
f_map: var MF.t;
vars: var Vec.t;
mutable cpt_mk_var: int;
mutable cpt_mk_clause: int;
}
type state = t
let create_ size_map size_vars () : t = {
f_map = MF.create size_map;
vars = Vec.make size_vars dummy_var;
cpt_mk_var = 0;
cpt_mk_clause = 0;
}
let create ?(size=`Big) () : t =
let size_map, size_vars = match size with
| `Tiny -> 8, 0
| `Small -> 16, 10
| `Big -> 4096, 128
in
create_ size_map size_vars ()
let nb_elt st = Vec.size st.vars
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
| Hyp -> "H" ^ string_of_int c.name
| Local -> "L" ^ string_of_int c.name
| Lemma _ -> "T" ^ string_of_int c.name
| History _ -> "C" ^ string_of_int c.name
module Var = struct
type t = var
let dummy = dummy_var
let[@inline] level v = v.v_level
let[@inline] pos v = v.pa
let[@inline] neg v = v.na
let[@inline] reason v = v.reason
let[@inline] weight v = v.v_weight
let[@inline] id v = v.vid
let[@inline] level v = v.v_level
let[@inline] idx v = v.v_idx
let[@inline] set_level v lvl = v.v_level <- lvl
let[@inline] set_idx v i = v.v_idx <- i
let[@inline] set_weight v w = v.v_weight <- w
let[@inline] in_heap v = v.v_idx >= 0
let make (st:state) (t:formula) : var * Theory_intf.negated =
let lit, negated = E.Form.norm t in
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;
v_fields = Var_fields.empty;
v_level = -1;
v_idx= -1;
v_weight = 0.;
reason = None;
}
and pa =
{ var = var;
lit = lit;
watched = Vec.make 10 dummy_clause;
neg = na;
is_true = false;
aid = cpt_double (* aid = vid*2 *) }
and na =
{ var = var;
lit = E.Form.neg lit;
watched = Vec.make 10 dummy_clause;
neg = pa;
is_true = false;
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;
Vec.push st.vars var;
var, negated
(* Marking helpers *)
let[@inline] clear v =
v.v_fields <- Var_fields.empty
let[@inline] seen_both v =
Var_fields.get v_field_seen_pos v.v_fields &&
Var_fields.get v_field_seen_neg v.v_fields
end
module Atom = struct
type t = atom
let dummy = dummy_atom
let[@inline] level a = a.var.v_level
let[@inline] var a = a.var
let[@inline] neg a = a.neg
let[@inline] abs a = a.var.pa
let[@inline] lit a = a.lit
let[@inline] equal a b = a == b
let[@inline] is_pos a = a == abs a
let[@inline] compare a b = Pervasives.compare a.aid b.aid
let[@inline] reason a = Var.reason a.var
let[@inline] id a = a.aid
let[@inline] is_true a = a.is_true
let[@inline] is_false a = a.neg.is_true
let[@inline] seen a =
let pos = equal a (abs a) in
if pos
then Var_fields.get v_field_seen_pos a.var.v_fields
else Var_fields.get v_field_seen_neg a.var.v_fields
let[@inline] mark a =
let pos = equal a (abs a) in
if pos
then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields
else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields
let[@inline] make st lit =
let var, negated = Var.make st lit in
match negated with
| Theory_intf.Negated -> var.na
| Theory_intf.Same_sign -> var.pa
let pp fmt a = E.Form.print fmt a.lit
let pp_a fmt v =
if Array.length v = 0 then (
Format.fprintf fmt "∅"
) else (
pp fmt v.(0);
if (Array.length v) > 1 then begin
for i = 1 to (Array.length v) - 1 do
Format.fprintf fmt " ∨ %a" pp v.(i)
done
end
)
(* Complete debug printing *)
let 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)
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
Format.fprintf fmt "T%a" pp_level a
else if a.neg.is_true then
Format.fprintf fmt "F%a" pp_level a
else
Format.fprintf fmt ""
let debug out a =
Format.fprintf out "%s%d[%a][@[%a@]]"
(sign a) (a.var.vid+1) debug_value a E.Form.print a.lit
let debug_a out vec =
Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec
end
module Clause = struct
type t = clause
let dummy = dummy_clause
let make =
let n = ref 0 in
fun ?tag atoms premise ->
let name = !n in
incr n;
{ name;
tag = tag;
atoms = atoms;
c_flags = C_fields.empty;
activity = 0.;
cpremise = premise;
}
let make_l ?tag l pr = make ?tag (Array.of_list l) pr
let empty = make [| |] (History [])
let name = name_of_clause
let[@inline] equal c1 c2 = c1==c2
let[@inline] atoms c = c.atoms
let[@inline] atoms_l c = Array.to_list c.atoms
let[@inline] tag c = c.tag
let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms
let[@inline] premise c = c.cpremise
let[@inline] set_premise c p = c.cpremise <- p
let[@inline] visited c = C_fields.get c_field_visited c.c_flags
let[@inline] set_visited c b = c.c_flags <- C_fields.set c_field_visited b c.c_flags
let[@inline] attached c = C_fields.get c_field_attached c.c_flags
let[@inline] set_attached c b = c.c_flags <- C_fields.set c_field_attached b c.c_flags
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)
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"
| Local -> Format.fprintf out "local"
| Lemma _ -> Format.fprintf out "th_lemma"
| History v -> Util.pp_list (CCFormat.of_to_string name_of_clause) out v
let debug out ({atoms=arr; cpremise=cp;_}as c) =
Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
(name c) Atom.debug_a arr debug_premise cp
let pp_dimacs fmt {atoms;_} =
let aux fmt a =
Array.iter (fun p ->
Format.fprintf fmt "%s%d "
(if p == p.var.pa then "-" else "")
(p.var.vid+1)
) a
in
Format.fprintf fmt "%a0" aux atoms
end
module Formula = struct
include E.Form
let pp = print
end
end[@@inline]

18
src/sat/Solver_types.mli
View file

@ -1,18 +0,0 @@
(** Internal types (implementation)
This modules actually implements the internal types used by the solver.
Since mutation is heavily used in the solver, it is really, really, *really*
discouraged to direclty use the functions in this module if you don't know the
inner working of mSAT perfectly as even the simplest
change can have dramatic effects on the solver.
*)
module type S = Solver_types_intf.S
(** Interface for the internal types. *)
module Make (E : Theory_intf.S):
S with type formula = E.formula
and type proof = E.proof
(** Functor to instantiate the types of clauses for a solver. *)

208
src/sat/Solver_types_intf.ml
View file

@ -1,208 +0,0 @@
(** Internal types (interface)
This modules defines the interface of most of the internal types
used in the core solver.
*)
module Var_fields = BitField.Make()
module C_fields = BitField.Make()
type 'a printer = Format.formatter -> 'a -> unit
module type S = sig
(** The signatures of clauses used in the Solver. *)
type t
(** State for creating new terms, literals, clauses *)
val create: ?size:[`Tiny|`Small|`Big] -> unit -> t
(** {2 Type definitions} *)
type formula
type proof
(** The types of formulas and proofs. All of these are user-provided. *)
(* TODO: hide these types (from the outside of [Msat]);
instead, provide well defined modules [module Lit : sig type t val …]
that define their API in Msat itself (not here) *)
type var = {
vid : int; (** Unique identifier *)
pa : atom; (** Link for the positive atom *)
na : atom; (** Link for the negative atom *)
mutable v_fields : Var_fields.t; (** bool fields *)
mutable v_level : int; (** Level of decision/propagation *)
mutable v_idx: int; (** rank in variable heap *)
mutable v_weight : float; (** Variable weight (for the heap) *)
mutable reason : reason option;
(** The reason for propagation/decision of the literal *)
}
and atom = {
aid : int; (** Unique identifier *)
var : var; (** Link for the parent variable *)
neg : atom; (** Link for the negation of the atom *)
lit : formula; (** Wrapped formula *)
mutable is_true : bool; (** Is the atom true ? Conversely, the atom
is false iff a.neg.is_true *)
mutable watched : clause Vec.t; (** The vector of clauses that watch this atom *)
}
(** Atoms and variables wrap theory formulas. They exist in the form of
triplet: a variable and two atoms. For a formula [f] in normal form,
the variable v points to the positive atom [a] which wraps [f], while
[a.neg] wraps the theory negation of [f]. *)
and clause = {
name : int; (** Clause name, mainly for printing, unique. *)
tag : int option; (** User-provided tag for clauses. *)
atoms : atom array; (** The atoms that constitute the clause.*)
mutable cpremise : premise; (** The premise of the clause, i.e. the justification
of why the clause must be satisfied. *)
mutable activity : float; (** Clause activity, used for the heap heuristics. *)
mutable c_flags: C_fields.t; (** Boolean flags for the clause *)
}
(** The type of clauses. Each clause generated should be true, i.e. enforced
by the current problem (for more information, see the cpremise field). *)
and reason =
| Decision (** The atom has been decided by the sat solver *)
| Bcp of clause (** The atom has been propagated by the given clause *)
(** Reasons of propagation/decision of atoms. *)
and premise =
| Hyp (** The clause is a hypothesis, provided by the user. *)
| Local (** The clause is a 1-atom clause,
where the atom is a local assumption*)
| Lemma of proof (** The clause is a theory-provided tautology, with
the given proof. *)
| History of clause list (** The clause can be obtained by resolution of the clauses
in the list. If the list has a single element [c] , then
the clause can be obtained by simplifying [c] (i.e
eliminating doublons in its atom list).
For a premise [History [a_1 :: ... :: a_n]] ([n > 0])
the clause is obtained by performing resolution of
[a_1] with [a_2], and then performing a resolution step between
the result and [a_3], etc...
Of course, each of the clause [a_i] also has its own premise. *)
(** Premises for clauses. Indeed each clause generated during a run of the solver
should be satisfied, the premise is the justification of why it should be
satisfied by the solver. *)
(** {2 Decisions and propagations} *)
(** {2 Elements} *)
val nb_elt : t -> int
val get_elt : t -> int -> var
val iter_elt : t -> (var -> unit) -> unit
(** Read access to the vector of variables created *)
(** {2 Variables, Literals & Clauses } *)
type state = t
module Var : sig
type t = var
val dummy : t
val pos : t -> atom
val neg : t -> atom
val level : t -> int
val idx : t -> int
val reason : t -> reason option
val weight : t -> float
val set_level : t -> int -> unit
val set_idx : t -> int -> unit
val set_weight : t -> float -> unit
val in_heap : t -> bool
val make : state -> formula -> t * Theory_intf.negated
(** Returns the variable linked with the given formula,
and whether the atom associated with the formula
is [var.pa] or [var.na] *)
val seen_both : t -> bool
(** both atoms have been seen? *)
val clear : t -> unit
(** Clear the 'seen' field of the variable. *)
end
module Atom : sig
type t = atom
val dummy : t
val level : t -> int
val reason : t -> reason option
val lit : t -> formula
val equal : t -> t -> bool
val compare : t -> t -> int
val var : t -> Var.t
val abs : t -> t (** positive atom *)
val neg : t -> t
val id : t -> int
val is_pos : t -> bool (* positive atom? *)
val is_true : t -> bool
val is_false : t -> bool
val make : state -> formula -> t
(** Returns the atom associated with the given formula *)
val mark : t -> unit
(** Mark the atom as seen, using the 'seen' field in the variable. *)
val seen : t -> bool
(** Returns wether the atom has been marked as seen. *)
val pp : t printer
val pp_a : t array printer
val debug : t printer
val debug_a : t array printer
end
module Clause : sig
type t = clause
val dummy : t
val name : t -> string
val equal : t -> t -> bool
val hash : t -> int
val atoms : t -> Atom.t array
val atoms_l : t -> Atom.t list
val tag : t -> int option
val premise : t -> premise
val attached : t -> bool
val set_attached : t -> bool -> unit
val visited : t -> bool
val set_visited : t -> bool -> unit
val empty : t
(** The empty clause *)
val make : ?tag:int -> Atom.t array -> premise -> t
(** [make_clause name atoms size premise] creates a clause with
the given attributes.
The array's ownership is transferred to the clause, do not
mutate it after that. *)
val make_l : ?tag:int -> Atom.t list -> premise -> t
val pp : t printer
val pp_dimacs : t printer
val debug : t printer
module Tbl : Hashtbl.S with type key = t
end
module Formula : sig
type t = formula
val equal : t -> t -> bool
val hash : t -> int
val pp : t printer
end
end

6
src/smt/Solver.ml
View file

@ -14,10 +14,10 @@ type level = int
module Sat_solver = Sidekick_sat.Make(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c
Sat_solver.Clause.forms c
module Proof = struct
type t = Sat_solver.Proof.proof
type t = Sat_solver.Proof.t
let pp out (p:t) : unit =
let pp_step_res out p =
@ -389,7 +389,7 @@ let do_on_exit ~on_exit =
let assume (self:t) (c:Lit.t IArray.t) : unit =
let sat = solver self in
let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Lit.make sat) c) in
let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Atom.make sat) c) in
Sat_solver.add_clause ~permanent:false sat c
let[@inline] assume_eq self t u expl : unit =

4
src/smt/Solver.mli
View file

@ -8,14 +8,14 @@
module Sat_solver : Sidekick_sat.S
with type formula = Lit.t
and type theory = Theory_combine.t
and type Proof.lemma = Theory_combine.proof
and type lemma = Theory_combine.proof
(** {2 Result} *)
type model = Model.t
module Proof : sig
type t = Sat_solver.Proof.proof
type t = Sat_solver.Proof.t
val pp : t CCFormat.printer
end