simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 19:55:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: use submodules of Solver_types to clean up code

Browse source
This commit is contained in:
Simon Cruanes 2017-12-29 15:29:04 +01:00 • committed by Guillaume Bury
parent 8eef2deebd
commit eff3f8024f
10 changed files with 669 additions and 570 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/backend/Coq.ml
View file

@ -22,12 +22,11 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause) = struct and type assumption := S.clause) = struct
module M = Map.Make(struct module Atom = S.St.Atom
type t = S.St.atom module Clause = S.St.Clause
let compare a b = compare a.S.St.aid b.S.St.aid module M = Map.Make(S.St.Atom)
end)
let name c = c.S.St.name let name = S.St.Clause.name
let clause_map c = let clause_map c =
let rec aux acc a i = let rec aux acc a i =
@ -70,27 +69,26 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause
)) h1.S.St.atoms )) h1.S.St.atoms
let resolution fmt goal hyp1 hyp2 atom = let resolution fmt goal hyp1 hyp2 atom =
let a = S.St.(atom.var.pa) in let a = Atom.abs atom in
let h1, h2 = let h1, h2 =
if Array.exists ((==) a) hyp1.S.St.atoms then hyp1, hyp2 if Array.exists (Atom.equal a) hyp1.S.St.atoms then hyp1, hyp2
else (assert (Array.exists ((==) a) hyp2.S.St.atoms); hyp2, hyp1) else (assert (Array.exists (Atom.equal a) hyp2.S.St.atoms); hyp2, hyp1)
in in
(** Print some debug info *) (** Print some debug info *)
Format.fprintf fmt Format.fprintf fmt
"(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n" "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
(name goal) (name h1) (name h2); (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 goal.S.St.atoms = 0 then begin if Array.length goal.S.St.atoms = 0 then (
let m = M.empty in let m = M.empty in
Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) (); Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
false false
end else begin ) else (
let m = clause_map goal in let m = clause_map goal in
Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n" 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); (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
true true
end )
(* Count uses of hypotheses *) (* Count uses of hypotheses *)
let incr_use h c = let incr_use h c =

35
src/backend/Dimacs.ml
View file

@ -36,10 +36,10 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
(* Dimacs & iCNF export *) (* Dimacs & iCNF export *)
let export_vec name fmt vec = let export_vec name fmt vec =
Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.pp_dimacs) vec Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.Clause.pp_dimacs) vec
let export_assumption fmt vec = let export_assumption fmt vec =
Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec
let export_icnf_aux r name map_filter fmt vec = let export_icnf_aux r name map_filter fmt vec =
let aux fmt _ = let aux fmt _ =
@ -47,28 +47,28 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
let x = Vec.get vec i in let x = Vec.get vec i in
match map_filter x with match map_filter x with
| None -> () | None -> ()
| Some _ -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i) | Some _ -> Format.fprintf fmt "%a@," St.Clause.pp_dimacs (Vec.get vec i)
done; done;
r := Vec.size vec r := Vec.size vec
in in
Format.fprintf fmt "c %s@,%a" name aux vec Format.fprintf fmt "c %s@,%a" name aux vec
let map_filter_learnt c = let map_filter_learnt c =
match c.St.cpremise with match St.Clause.premise c with
| St.Hyp | St.Local -> assert false | St.Hyp | St.Local -> assert false
| St.Lemma _ -> Some c | St.Lemma _ -> Some c
| St.History l -> | St.History l ->
begin match l with begin match l with
| [] -> assert false | [] -> assert false
| d :: _ -> | d :: _ ->
begin match d.St.cpremise with begin match St.Clause.premise d with
| St.Lemma _ -> Some d | St.Lemma _ -> Some d
| St.Hyp | St.Local | St.History _ -> None | St.Hyp | St.Local | St.History _ -> None
end end
end end
let filter_vec learnt = let filter_vec learnt =
let lemmas = Vec.make (Vec.size learnt) St.dummy_clause in let lemmas = Vec.make (Vec.size learnt) St.Clause.dummy in
Vec.iter (fun c -> Vec.iter (fun c ->
match map_filter_learnt c with match map_filter_learnt c with
| None -> () | None -> ()
@ -77,17 +77,13 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
lemmas lemmas
let export fmt ~hyps ~history ~local = let export fmt ~hyps ~history ~local =
assert (Vec.for_all (function assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
| { St.cpremise = St.Hyp; _} -> true | _ -> false
) hyps);
(* Learnt clauses, then filtered to only keep only (* Learnt clauses, then filtered to only keep only
the theory lemmas; all other learnt clauses should be logical the theory lemmas; all other learnt clauses should be logical
consequences of the rest. *) consequences of the rest. *)
let lemmas = filter_vec history in let lemmas = filter_vec history in
(* Local assertions *) (* Local assertions *)
assert (Vec.for_all (function assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local);
| { St.cpremise = St.Local; _} -> true | _ -> false
) local);
(* Number of atoms and clauses *) (* Number of atoms and clauses *)
let n = St.nb_elt () in let n = St.nb_elt () in
let m = Vec.size local + Vec.size hyps + Vec.size lemmas in let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
@ -102,15 +98,16 @@ module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct
let icnf_lemmas = ref 0 let icnf_lemmas = ref 0
let export_icnf fmt ~hyps ~history ~local = let export_icnf fmt ~hyps ~history ~local =
assert (Vec.for_all (function assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
| { St.cpremise = St.Hyp; _} -> true | _ -> false
) hyps);
let lemmas = history in let lemmas = history in
(* Local assertions *) (* Local assertions *)
let l = List.map (function let l = List.map
| {St.cpremise = St.Local; atoms = [| a |];_ } -> a (fun c -> match St.Clause.premise c, St.Clause.atoms c with
| _ -> assert false) (Vec.to_list local) in | St.Local, [| a |] -> a
let local = St.make_clause "local (tmp)" l St.Local in | _ -> assert false)
(Vec.to_list local)
in
let local = St.Clause.make l St.Local in
(* Number of atoms and clauses *) (* Number of atoms and clauses *)
Format.fprintf fmt Format.fprintf fmt
"@[<v>%s@,%a%a%a@]@." "@[<v>%s@,%a%a%a@]@."

24
src/backend/Dot.ml
View file

@ -31,20 +31,22 @@ module type Arg = sig
end end
module Default(S : Res.S) = struct module Default(S : Res.S) = struct
module Atom = S.St.Atom
module Clause = S.St.Clause
let print_atom = S.St.print_atom let print_atom = Atom.pp
let hyp_info c = let hyp_info c =
"hypothesis", Some "LIGHTBLUE", "hypothesis", Some "LIGHTBLUE",
[ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
let lemma_info c = let lemma_info c =
"lemma", Some "BLUE", "lemma", Some "BLUE",
[ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
let assumption_info c = let assumption_info c =
"assumption", Some "PURPLE", "assumption", Some "PURPLE",
[ fun fmt () -> Format.fprintf fmt "%s" c.S.St.name] [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
end end
@ -53,15 +55,17 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
and type hyp := S.clause and type hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause) = struct and type assumption := S.clause) = struct
module Atom = S.St.Atom
module Clause = S.St.Clause
let node_id n = n.S.conclusion.S.St.name let node_id n = Clause.name n.S.conclusion
let res_node_id n = (node_id n) ^ "_res" let res_node_id n = (node_id n) ^ "_res"
let proof_id p = node_id (S.expand p) let proof_id p = node_id (S.expand p)
let print_clause fmt c = let print_clause fmt c =
let v = c.S.St.atoms in let v = Clause.atoms c in
if Array.length v = 0 then if Array.length v = 0 then
Format.fprintf fmt "⊥" Format.fprintf fmt "⊥"
else else
@ -149,9 +153,11 @@ module Simple(S : Res.S)
and type lemma := S.lemma and type lemma := S.lemma
and type assumption = S.St.formula) = and type assumption = S.St.formula) =
Make(S)(struct Make(S)(struct
module Atom = S.St.Atom
module Clause = S.St.Clause
(* Some helpers *) (* Some helpers *)
let lit a = a.S.St.lit let lit = Atom.lit
let get_assumption c = let get_assumption c =
match S.to_list c with match S.to_list c with
@ -159,13 +165,13 @@ module Simple(S : Res.S)
| _ -> assert false | _ -> assert false
let get_lemma c = let get_lemma c =
match c.S.St.cpremise with match Clause.premise c with
| S.St.Lemma p -> p | S.St.Lemma p -> p
| _ -> assert false | _ -> assert false
(* Actual functions *) (* Actual functions *)
let print_atom fmt a = let print_atom fmt a =
A.print_atom fmt a.S.St.lit A.print_atom fmt (Atom.lit a)
let hyp_info c = let hyp_info c =
A.hyp_info (List.map lit (S.to_list c)) A.hyp_info (List.map lit (S.to_list c))

430
src/core/Internal.ml
View file

File diff suppressed because it is too large Load diff

2
src/core/Internal.mli
View file

@ -92,7 +92,7 @@ module Make
These functions expose some internal data stored by the solver, as such These functions expose some internal data stored by the solver, as such
great care should be taken to ensure not to mess with the values returned. *) great care should be taken to ensure not to mess with the values returned. *)
val trail : unit -> St.t Vec.t val trail : unit -> St.trail_elt Vec.t
(** Returns the current trail. (** Returns the current trail.
*DO NOT MUTATE* *) *DO NOT MUTATE* *)

54
src/core/Res.ml
View file

@ -24,11 +24,10 @@ module Make(St : Solver_types.S) = struct
let info = 10 let info = 10
let debug = 80 let debug = 80
(* Misc functions *)
let equal_atoms a b = St.(a.aid) = St.(b.aid) let equal_atoms a b = St.(a.aid) = St.(b.aid)
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
let print_clause = St.pp_clause let print_clause = St.Clause.pp
let merge = List.merge compare_atoms let merge = List.merge compare_atoms
@ -52,19 +51,19 @@ module Make(St : Solver_types.S) = struct
resolved, List.rev new_clause resolved, List.rev new_clause
(* Compute the set of doublons of a clause *) (* Compute the set of doublons of a clause *)
let list c = List.sort compare_atoms (Array.to_list St.(c.atoms)) let list c = List.sort St.Atom.compare (Array.to_list St.(c.atoms))
let analyze cl = let analyze cl =
let rec aux duplicates free = function let rec aux duplicates free = function
| [] -> duplicates, free | [] -> duplicates, free
| [ x ] -> duplicates, x :: free | [ x ] -> duplicates, x :: free
| x :: ((y :: r) as l) -> | x :: ((y :: r) as l) ->
if equal_atoms x y then if x == y then
count duplicates (x :: free) x [y] r count duplicates (x :: free) x [y] r
else else
aux duplicates (x :: free) l aux duplicates (x :: free) l
and count duplicates free x acc = function and count duplicates free x acc = function
| (y :: r) when equal_atoms x y -> | (y :: r) when x == y ->
count duplicates free x (y :: acc) r count duplicates free x (y :: acc) r
| l -> | l ->
aux (acc :: duplicates) free l aux (acc :: duplicates) free l
@ -96,7 +95,8 @@ module Make(St : Solver_types.S) = struct
let cmp_cl c d = let cmp_cl c d =
let rec aux = function let rec aux = function
| [], [] -> 0 | [], [] -> 0
| a :: r, a' :: r' -> begin match compare_atoms a a' with | a :: r, a' :: r' ->
begin match compare_atoms a a' with
| 0 -> aux (r, r') | 0 -> aux (r, r')
| x -> x | x -> x
end end
@ -117,32 +117,32 @@ module Make(St : Solver_types.S) = struct
assert St.(a.var.v_level >= 0); assert St.(a.var.v_level >= 0);
match St.(a.var.reason) with match St.(a.var.reason) with
| Some St.Bcp c -> | Some St.Bcp c ->
Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.pp_atom a St.pp_clause 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 begin if Array.length c.St.atoms = 1 then (
Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.pp_atom a); Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.Atom.debug a);
c c
end else begin ) else (
assert (a.St.neg.St.is_true); assert (a.St.neg.St.is_true);
let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in let c' = St.Clause.make [a.St.neg] r in
a.St.var.St.reason <- Some St.(Bcp c'); a.St.var.St.reason <- Some St.(Bcp c');
Log.debugf debug Log.debugf debug
(fun k -> k "New reason: @[%a@ %a@]" St.pp_atom a St.pp_clause c'); (fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c');
c' c'
end )
| _ -> | _ ->
Log.debugf error (fun k -> k "Error while proving atom %a" St.pp_atom a); Log.debugf error (fun k -> k "Error while proving atom %a" St.Atom.debug a);
raise (Resolution_error "Cannot prove atom") raise (Resolution_error "Cannot prove atom")
let prove_unsat conflict = let prove_unsat conflict =
if Array.length conflict.St.atoms = 0 then conflict if Array.length conflict.St.atoms = 0 then conflict
else begin else (
Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.pp_clause conflict); 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 l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in let res = St.Clause.make [] (St.History (conflict :: l)) in
Log.debugf info (fun k -> k "Proof found: @[%a@]" St.pp_clause res); Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res);
res res
end )
let prove_atom a = let prove_atom a =
if St.(a.is_true && a.var.v_level = 0) then if St.(a.is_true && a.var.v_level = 0) then
@ -166,27 +166,26 @@ module Make(St : Solver_types.S) = struct
let rec chain_res (c, cl) = function let rec chain_res (c, cl) = function
| d :: r -> | d :: r ->
Log.debugf debug Log.debugf debug
(fun k -> k " Resolving clauses : @[%a@\n%a@]" St.pp_clause c St.pp_clause d); (fun k -> k " Resolving clauses : @[%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
let dl = to_list d in let dl = to_list d in
begin match resolve (merge cl dl) with begin match resolve (merge cl dl) with
| [ a ], l -> | [ a ], l ->
begin match r with begin match r with
| [] -> (l, c, d, a) | [] -> (l, c, d, a)
| _ -> | _ ->
let new_clause = St.make_clause (fresh_pcl_name ()) let new_clause = St.Clause.make l (St.History [c; d]) in
l (St.History [c; d]) in
chain_res (new_clause, l) r chain_res (new_clause, l) r
end end
| _ -> | _ ->
Log.debugf error Log.debugf error
(fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.pp_clause c St.pp_clause d); (fun k -> k "While resolving clauses:@[<hov>%a@\n%a@]" St.Clause.debug c St.Clause.debug d);
raise (Resolution_error "Clause mismatch") raise (Resolution_error "Clause mismatch")
end end
| _ -> | _ ->
raise (Resolution_error "Bad history") raise (Resolution_error "Bad history")
let expand conclusion = let expand conclusion =
Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.pp_clause conclusion); Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion);
match conclusion.St.cpremise with match conclusion.St.cpremise with
| St.Lemma l -> | St.Lemma l ->
{conclusion; step = Lemma l; } {conclusion; step = Lemma l; }
@ -195,7 +194,7 @@ module Make(St : Solver_types.S) = struct
| St.Local -> | St.Local ->
{ conclusion; step = Assumption; } { conclusion; step = Assumption; }
| St.History [] -> | St.History [] ->
Log.debugf error (fun k -> k "Empty history for clause: %a" St.pp_clause conclusion); Log.debugf error (fun k -> k "Empty history for clause: %a" St.Clause.debug conclusion);
raise (Resolution_error "Empty history") raise (Resolution_error "Empty history")
| St.History [ c ] -> | St.History [ c ] ->
let duplicates, res = analyze (list c) in let duplicates, res = analyze (list c) in
@ -240,7 +239,7 @@ module Make(St : Solver_types.S) = struct
let rec aux res acc = function let rec aux res acc = function
| [] -> res, acc | [] -> res, acc
| c :: r -> | c :: r ->
if not c.St.visited then begin if not c.St.visited then (
c.St.visited <- true; c.St.visited <- true;
match c.St.cpremise with match c.St.cpremise with
| St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r | St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r
@ -248,8 +247,9 @@ module Make(St : Solver_types.S) = struct
let l = List.fold_left (fun acc c -> let l = List.fold_left (fun acc c ->
if not c.St.visited then c :: acc else acc) r h in if not c.St.visited then c :: acc else acc) r h in
aux res (c :: acc) l aux res (c :: acc) l
end else ) else (
aux res acc r aux res acc r
)
in in
let res, tmp = aux [] [] [proof] in let res, tmp = aux [] [] [proof] in
List.iter (fun c -> c.St.visited <- false) res; List.iter (fun c -> c.St.visited <- false) res;

43
src/core/Solver.ml
View file

@ -6,36 +6,7 @@ Copyright 2016 Simon Cruanes
module type S = Solver_intf.S module type S = Solver_intf.S
type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { open Solver_intf
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 *)
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). *)
model: unit -> ('term * 'term) list;
(** Returns the model found if the formula is satisfiable. *)
}
type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.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. *)
}
type 'clause export = 'clause Solver_intf.export = {
hyps: 'clause Vec.t;
history: 'clause Vec.t;
local: 'clause Vec.t;
}
module Make module Make
(St : Solver_types.S) (St : Solver_types.S)
@ -65,10 +36,10 @@ module Make
(fun k -> k (fun k -> k
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@." "@[<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 status
(Vec.print ~sep:"" St.pp) (S.trail ()) (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail ())
(Vec.print ~sep:"" St.pp_clause) (S.temp ()) (Vec.print ~sep:"" St.Clause.debug) (S.temp ())
(Vec.print ~sep:"" St.pp_clause) (S.hyps ()) (Vec.print ~sep:"" St.Clause.debug) (S.hyps ())
(Vec.print ~sep:"" St.pp_clause) (S.history ()) (Vec.print ~sep:"" St.Clause.debug) (S.history ())
) )
let mk_sat () : (_,_) sat_state = let mk_sat () : (_,_) sat_state =
@ -77,8 +48,8 @@ module Make
let iter f f' = let iter f f' =
Vec.iter (function Vec.iter (function
| St.Atom a -> f a.St.lit | St.Atom a -> f a.St.lit
| St.Lit l -> f' l.St.term | St.Lit l -> f' l.St.term)
) t t
in in
{ {
eval = S.eval; eval = S.eval;

450
src/core/Solver_types.ml
View file

@ -73,7 +73,7 @@ module McMake (E : Expr_intf.S)() = struct
} }
and clause = { and clause = {
name : string; name : int;
tag : int option; tag : int option;
atoms : atom array; atoms : atom array;
mutable cpremise : premise; mutable cpremise : premise;
@ -97,8 +97,9 @@ module McMake (E : Expr_intf.S)() = struct
| E_lit of lit | E_lit of lit
| E_var of var | E_var of var
(* Dummy values *) type trail_elt =
let dummy_lit = E.Formula.dummy | Lit of lit
| Atom of atom
let rec dummy_var = let rec dummy_var =
{ vid = -101; { vid = -101;
@ -113,7 +114,7 @@ module McMake (E : Expr_intf.S)() = struct
} }
and dummy_atom = and dummy_atom =
{ var = dummy_var; { var = dummy_var;
lit = dummy_lit; lit = E.Formula.dummy;
watched = Obj.magic 0; watched = Obj.magic 0;
(* should be [Vec.make_empty dummy_clause] (* should be [Vec.make_empty dummy_clause]
but we have to break the cycle *) but we have to break the cycle *)
@ -121,7 +122,7 @@ module McMake (E : Expr_intf.S)() = struct
is_true = false; is_true = false;
aid = -102 } aid = -102 }
let dummy_clause = let dummy_clause =
{ name = ""; { name = -1;
tag = None; tag = None;
atoms = [| |]; atoms = [| |];
activity = -1.; activity = -1.;
@ -129,13 +130,13 @@ module McMake (E : Expr_intf.S)() = struct
visited = false; visited = false;
cpremise = History [] } cpremise = History [] }
let () = let () = dummy_atom.watched <- Vec.make_empty dummy_clause
dummy_atom.watched <- Vec.make_empty dummy_clause
(* Constructors *) (* Constructors *)
module MF = Hashtbl.Make(E.Formula) module MF = Hashtbl.Make(E.Formula)
module MT = Hashtbl.Make(E.Term) module MT = Hashtbl.Make(E.Term)
(* TODO: embed a state `t` with these inside *)
let f_map = MF.create 4096 let f_map = MF.create 4096
let t_map = MT.create 4096 let t_map = MT.create 4096
@ -146,229 +147,286 @@ module McMake (E : Expr_intf.S)() = struct
let cpt_mk_var = ref 0 let cpt_mk_var = ref 0
let make_semantic_var t = let name_of_clause c = match c.cpremise with
try MT.find t_map t | Hyp -> "H" ^ string_of_int c.name
with Not_found -> | Local -> "L" ^ string_of_int c.name
let res = { | Lemma _ -> "T" ^ string_of_int c.name
lid = !cpt_mk_var; | History _ -> "C" ^ string_of_int c.name
term = t;
l_weight = 1.;
l_idx= -1;
l_level = -1;
assigned = None;
} in
incr cpt_mk_var;
MT.add t_map t res;
Vec.push vars (E_lit res);
res
let make_boolean_var : formula -> var * Expr_intf.negated = module Lit = struct
fun t -> type t = lit
let lit, negated = E.Formula.norm t in let[@inline] term l = l.term
try let[@inline] level l = l.l_level
MF.find f_map lit, negated let[@inline] set_level l lvl = l.l_level <- lvl
let[@inline] assigned l = l.assigned
let[@inline] set_assigned l t = l.assigned <- t
let[@inline] weight l = l.l_weight
let[@inline] set_weight l w = l.l_weight <- w
let make t =
try MT.find t_map t
with Not_found -> with Not_found ->
let cpt_fois_2 = !cpt_mk_var lsl 1 in let res = {
let rec var = lid = !cpt_mk_var;
{ vid = !cpt_mk_var; term = t;
pa = pa; l_weight = 1.;
na = na; l_idx= -1;
v_fields = Var_fields.empty; l_level = -1;
v_level = -1; assigned = None;
v_idx= -1; } in
v_weight = 0.;
v_assignable = None;
reason = None;
}
and pa =
{ var = var;
lit = lit;
watched = Vec.make 10 dummy_clause;
neg = na;
is_true = false;
aid = cpt_fois_2 (* aid = vid*2 *) }
and na =
{ var = var;
lit = E.Formula.neg lit;
watched = Vec.make 10 dummy_clause;
neg = pa;
is_true = false;
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
MF.add f_map lit var;
incr cpt_mk_var; incr cpt_mk_var;
Vec.push vars (E_var var); MT.add t_map t res;
var, negated Vec.push vars (E_lit res);
res
let add_term t = make_semantic_var t let debug_assign fmt v =
match v.assigned with
| None ->
Format.fprintf fmt ""
| Some t ->
Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
let add_atom lit = let pp out v = E.Term.print out v.term
let var, negated = make_boolean_var lit in let debug out v =
match negated with Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
| Formula_intf.Negated -> var.na (v.lid+1) debug_assign v E.Term.print v.term
| Formula_intf.Same_sign -> var.pa end
let make_clause ?tag name ali premise = module Var = struct
let atoms = Array.of_list ali in type t = var
{ name = name; let dummy = dummy_var
tag = tag; let[@inline] level v = v.v_level
atoms = atoms; let[@inline] set_level v lvl = v.v_level <- lvl
attached = false; let[@inline] pos v = v.pa
visited = false; let[@inline] neg v = v.na
activity = 0.; let[@inline] reason v = v.reason
cpremise = premise} let[@inline] set_reason v r = v.reason <- r
let[@inline] assignable v = v.v_assignable
let[@inline] set_assignable v x = v.v_assignable <- x
let[@inline] weight v = v.v_weight
let[@inline] set_weight v w = v.v_weight <- w
let empty_clause = make_clause "Empty" [] (History []) let make : formula -> var * Expr_intf.negated =
fun t ->
let lit, negated = E.Formula.norm t in
try
MF.find f_map lit, negated
with Not_found ->
let cpt_fois_2 = !cpt_mk_var lsl 1 in
let rec var =
{ vid = !cpt_mk_var;
pa = pa;
na = na;
v_fields = Var_fields.empty;
v_level = -1;
v_idx= -1;
v_weight = 0.;
v_assignable = None;
reason = None;
}
and pa =
{ var = var;
lit = lit;
watched = Vec.make 10 dummy_clause;
neg = na;
is_true = false;
aid = cpt_fois_2 (* aid = vid*2 *) }
and na =
{ var = var;
lit = E.Formula.neg lit;
watched = Vec.make 10 dummy_clause;
neg = pa;
is_true = false;
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
MF.add f_map lit var;
incr cpt_mk_var;
Vec.push vars (E_var var);
var, negated
(* Marking helpers *) (* Marking helpers *)
let clear v = v.v_fields <- Var_fields.empty let[@inline] clear v =
v.v_fields <- Var_fields.empty
let seen a = let[@inline] seen_both v =
let pos = (a == a.var.pa) in Var_fields.get v_field_seen_pos v.v_fields &&
let field = if pos then v_field_seen_pos else v_field_seen_neg in Var_fields.get v_field_seen_neg v.v_fields
Var_fields.get field a.var.v_fields end
let seen_both v = module Atom = struct
Var_fields.get v_field_seen_pos v.v_fields && type t = atom
Var_fields.get v_field_seen_neg v.v_fields 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] 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 mark a = let[@inline] seen a =
let pos = (a == a.var.pa) in let pos = equal a (abs a) in
let field = if pos then v_field_seen_pos else v_field_seen_neg in if pos
a.var.v_fields <- Var_fields.set field true a.var.v_fields then Var_fields.get v_field_seen_pos a.var.v_fields
else Var_fields.get v_field_seen_neg a.var.v_fields
(* Decisions & propagations *) let[@inline] mark a =
type t = let pos = equal a (abs a) in
| Lit of lit if pos
| Atom of atom 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 of_lit l = Lit l let[@inline] make lit =
let of_atom a = Atom a let var, negated = Var.make lit in
match negated with
| Formula_intf.Negated -> var.na
| Formula_intf.Same_sign -> var.pa
let pp fmt a = E.Formula.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)
| n, Some Semantic ->
Format.fprintf fmt "::%d" n
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][atom:@[<hov>%a@]]"
(sign a) (a.var.vid+1) debug_value a E.Formula.print a.lit
let debug_a out vec =
Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec
end
(* Elements *) (* Elements *)
let[@inline] elt_of_lit l = E_lit l module Elt = struct
let[@inline] elt_of_var v = E_var v type t = elt
let[@inline] of_lit l = E_lit l
let[@inline] of_var v = E_var v
let get_elt_id = function 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 get_elt_level = function 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 get_elt_idx = function 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 get_elt_weight = function let[@inline] weight = function
| E_lit l -> l.l_weight | E_var v -> v.v_weight | E_lit l -> l.l_weight | E_var v -> v.v_weight
let set_elt_level e lvl = match e with let[@inline] set_level e lvl = match e with
| E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl | E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl
let set_elt_idx e i = match e with let[@inline] set_idx e i = match e with
| E_lit l -> l.l_idx <- i | E_var v -> v.v_idx <- i | E_lit l -> l.l_idx <- i | E_var v -> v.v_idx <- i
let set_elt_weight e w = match e with 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 <- w | E_var v -> v.v_weight <- w
end
(* Name generation *) module Trail_elt = struct
let fresh_lname = type t = trail_elt
let cpt = ref 0 in let[@inline] of_lit l = Lit l
fun () -> incr cpt; "L" ^ (string_of_int !cpt) let[@inline] of_atom a = Atom a
let fresh_hname = let debug fmt = function
let cpt = ref 0 in | Lit l -> Lit.debug fmt l
fun () -> incr cpt; "H" ^ (string_of_int !cpt) | Atom a -> Atom.debug fmt a
end
let fresh_tname = module Clause = struct
let cpt = ref 0 in type t = clause
fun () -> incr cpt; "T" ^ (string_of_int !cpt) let dummy = dummy_clause
let fresh_name = let make =
let cpt = ref 0 in let n = ref 0 in
fun () -> incr cpt; "C" ^ (string_of_int !cpt) fun ?tag ali premise ->
let atoms = Array.of_list ali in
let name = !n in
incr n;
{ name;
tag = tag;
atoms = atoms;
visited = false;
attached = false;
activity = 0.;
cpremise = premise}
(* Pretty printing for atoms and clauses *) let empty = make [] (History [])
let print_lit fmt v = E.Term.print fmt v.term let name = name_of_clause
let[@inline] atoms c = c.atoms
let[@inline] tag c = c.tag
let print_atom fmt a = E.Formula.print fmt a.lit let[@inline] premise c = c.cpremise
let[@inline] set_premise c p = c.cpremise <- p
let print_atoms fmt v = let[@inline] visited c = c.visited
if Array.length v = 0 then let[@inline] set_visited c b = c.visited <- b
Format.fprintf fmt "∅"
else begin
print_atom fmt v.(0);
if (Array.length v) > 1 then begin
for i = 1 to (Array.length v) - 1 do
Format.fprintf fmt " ∨ %a" print_atom v.(i)
done
end
end
let print_clause fmt c = let[@inline] attached c = c.attached
Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms let[@inline] set_attached c b = c.attached <- b
(* Complete debug printing *) let[@inline] activity c = c.activity
let sign a = if a == a.var.pa then "+" else "-" let[@inline] set_activity c w = c.activity <- w
let pp_reason fmt = function let pp fmt c =
| n, _ when n < 0 -> Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
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 c.name
| n, Some Semantic ->
Format.fprintf fmt "::%d" n
let pp_level fmt a = let debug_premise out = function
pp_reason fmt (a.var.v_level, a.var.reason) | Hyp -> Format.fprintf out "hyp"
| Local -> Format.fprintf out "local"
| Lemma _ -> Format.fprintf out "th_lemma"
| History v ->
List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v
let pp_value fmt a = let debug out ({atoms=arr; cpremise=cp;_}as c) =
if a.is_true then Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
Format.fprintf fmt "T%a" pp_level a (name c) Atom.debug_a arr debug_premise cp
else if a.neg.is_true then
Format.fprintf fmt "F%a" pp_level a
else
Format.fprintf fmt ""
let pp_premise out = function let pp_dimacs fmt {atoms;_} =
| Hyp -> Format.fprintf out "hyp" let aux fmt a =
| Local -> Format.fprintf out "local" Array.iter (fun p ->
| Lemma _ -> Format.fprintf out "th_lemma"
| History v -> List.iter (fun { name; _ } -> Format.fprintf out "%s,@ " name) v
let pp_assign fmt v =
match v.assigned with
| None ->
Format.fprintf fmt ""
| Some t ->
Format.fprintf fmt "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
let pp_lit out v =
Format.fprintf out "%d[%a][lit:@[<hov>%a@]]"
(v.lid+1) pp_assign v E.Term.print v.term
let pp_atom out a =
Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
(sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit
let pp_atoms_vec out vec =
Array.iter (fun a -> Format.fprintf out "%a@ " pp_atom a) vec
let pp_clause out {name=name; atoms=arr; cpremise=cp;_} =
Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
name pp_atoms_vec arr pp_premise cp
let pp_dimacs fmt {atoms;_} =
let aux fmt a =
Array.iter (fun p ->
Format.fprintf fmt "%s%d " Format.fprintf fmt "%s%d "
(if p == p.var.pa then "-" else "") (if p == p.var.pa then "-" else "")
(p.var.vid+1) (p.var.vid+1)
) a ) a
in in
Format.fprintf fmt "%a0" aux atoms Format.fprintf fmt "%a0" aux atoms
end
let pp fmt = function
| Lit l -> pp_lit fmt l
| Atom a -> pp_atom fmt a
end end

177
src/core/Solver_types_intf.ml
View file

@ -24,6 +24,8 @@ Copyright 2016 Simon Cruanes
module Var_fields = BitField.Make() module Var_fields = BitField.Make()
type 'a printer = Format.formatter -> 'a -> unit
module type S = sig module type S = sig
(** The signatures of clauses used in the Solver. *) (** The signatures of clauses used in the Solver. *)
@ -86,7 +88,7 @@ module type S = sig
[a.neg] wraps the theory negation of [f]. *) [a.neg] wraps the theory negation of [f]. *)
and clause = { and clause = {
name : string; (** Clause name, mainly for printing, unique. *) name : int; (** Clause name, mainly for printing, unique. *)
tag : int option; (** User-provided tag for clauses. *) tag : int option; (** User-provided tag for clauses. *)
atoms : atom array; (** The atoms that constitute the clause.*) atoms : atom array; (** The atoms that constitute the clause.*)
mutable cpremise : premise; (** The premise of the clause, i.e. the justification mutable cpremise : premise; (** The premise of the clause, i.e. the justification
@ -124,15 +126,11 @@ module type S = sig
satisfied by the solver. *) satisfied by the solver. *)
(** {2 Decisions and propagations} *) (** {2 Decisions and propagations} *)
type t = type trail_elt =
| Lit of lit | Lit of lit
| Atom of atom (**) | Atom of atom (**)
(** Either a lit of an atom *) (** Either a lit of an atom *)
val of_lit : lit -> t
val of_atom : atom -> t
(** Constructors and destructors *)
(** {2 Elements} *) (** {2 Elements} *)
type elt = type elt =
@ -145,77 +143,136 @@ module type S = sig
val iter_elt : (elt -> unit) -> unit val iter_elt : (elt -> unit) -> unit
(** Read access to the vector of variables created *) (** Read access to the vector of variables created *)
val elt_of_lit : lit -> elt (** {2 Variables, Literals & Clauses } *)
val elt_of_var : var -> elt
(** Constructors & destructor for elements *)
val get_elt_id : elt -> int module Lit : sig
val get_elt_level : elt -> int type t = lit
val get_elt_idx : elt -> int val term : t -> term
val get_elt_weight : elt -> float val make : term -> t
val set_elt_level : elt -> int -> unit (** Returns the variable associated with the term *)
val set_elt_idx : elt -> int -> unit
val set_elt_weight : elt -> float -> unit
(** Accessors for elements *)
(** {2 Variables, Litterals & Clauses } *) val level : t -> int
val set_level : t -> int -> unit
val dummy_var : var val assigned : t -> term option
val dummy_atom : atom val set_assigned : t -> term option -> unit
val dummy_clause : clause val weight : t -> float
(** Dummy values for use in vector dummys *) val set_weight : t -> float -> unit
val add_term : term -> lit val pp : t printer
(** Returns the variable associated with the term *) val debug : t printer
val add_atom : formula -> atom end
(** Returns the atom associated with the given formula *)
val make_boolean_var : formula -> var * Formula_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 empty_clause : clause module Var : sig
(** The empty clause *) type t = var
val make_clause : ?tag:int -> string -> atom list -> premise -> clause val dummy : t
(** [make_clause name atoms size premise] creates a clause with the given attributes. *)
(** {2 Helpers} *) val pos : t -> atom
val neg : t -> atom
val mark : atom -> unit val level : t -> int
(** Mark the atom as seen, using the 'seen' field in the variable. *) val set_level : t -> int -> unit
val reason : t -> reason option
val set_reason : t -> reason option -> unit
val assignable : t -> lit list option
val set_assignable : t -> lit list option -> unit
val weight : t -> float
val set_weight : t -> float -> unit
val seen : atom -> bool val make : formula -> t * Formula_intf.negated
(** Returns wether the atom has been marked as seen. *) (** 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 : var -> bool val seen_both : t -> bool
(** both atoms have been seen? *) (** both atoms have been seen? *)
val clear : var -> unit val clear : t -> unit
(** Clear the 'seen' field of the variable. *) (** 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_true : t -> bool
val is_false : t -> bool
(** {2 Clause names} *) val make : formula -> t
(** Returns the atom associated with the given formula *)
val fresh_name : unit -> string val mark : t -> unit
val fresh_lname : unit -> string (** Mark the atom as seen, using the 'seen' field in the variable. *)
val fresh_tname : unit -> string
val fresh_hname : unit -> string
(** Fresh names for clauses *)
(** {2 Printing} *) val seen : t -> bool
(** Returns wether the atom has been marked as seen. *)
val print_lit : Format.formatter -> lit -> unit val pp : t printer
val print_atom : Format.formatter -> atom -> unit val pp_a : t array printer
val print_clause : Format.formatter -> clause -> unit val debug : t printer
(** Pretty printing functions for atoms and clauses *) val debug_a : t array printer
end
val pp : Format.formatter -> t -> unit module Elt : sig
val pp_lit : Format.formatter -> lit -> unit type t = elt
val pp_atom : Format.formatter -> atom -> unit
val pp_clause : Format.formatter -> clause -> unit
val pp_dimacs : Format.formatter -> clause -> unit
val pp_reason : Format.formatter -> (int * reason option) -> unit
(** Debug function for atoms and clauses (very verbose) *)
val of_lit : Lit.t -> t
val of_var : Var.t -> t
val id : t -> int
val level : t -> int
val idx : t -> int
val weight : t -> float
val set_level : t -> int -> unit
val set_idx : t -> int -> unit
val set_weight : t -> float -> unit
end
module Clause : sig
type t = clause
val dummy : t
val name : t -> string
val atoms : t -> Atom.t array
val tag : t -> int option
val premise : t -> premise
val set_premise : t -> premise -> unit
val visited : t -> bool
val set_visited : t -> bool -> unit
val attached : t -> bool
val set_attached : t -> bool -> unit
val activity : t -> float
val set_activity : t -> float -> unit
val empty : t
(** The empty clause *)
val make : ?tag:int -> Atom.t list -> premise -> clause
(** [make_clause name atoms size premise] creates a clause with the given attributes. *)
val pp : t printer
val pp_dimacs : t printer
val debug : t printer
end
module Trail_elt : sig
type t = trail_elt
val of_lit : Lit.t -> t
val of_atom : Atom.t -> t
(** Constructors and destructors *)
val debug : t printer
end
end end

2
src/main/main.ml
View file

@ -41,7 +41,7 @@ module Make
let check_clause c = let check_clause c =
let l = List.map (function a -> let l = List.map (function a ->
Log.debugf 99 Log.debugf 99
(fun k -> k "Checking value of %a" S.St.pp_atom (S.St.add_atom a)); (fun k -> k "Checking value of %a" S.St.Atom.debug (S.St.Atom.make a));
state.Msat.eval a) c in state.Msat.eval a) c in
List.exists (fun x -> x) l List.exists (fun x -> x) l
in in