mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-11 05:28:34 -05:00
Indent.
This commit is contained in:
Guillaume Bury
parent
aa5af3b0f2
commit
91cc15eec1
7 changed files with 203 additions and 203 deletions
266
sat/res.ml
266
sat/res.ml
|
|
@ -8,161 +8,161 @@ module type S = Res_intf.S
|
||||||
|
|
||||||
module Make(St : Solver_types.S)(Proof : sig type t end) = struct
|
module Make(St : Solver_types.S)(Proof : sig type t end) = struct
|
||||||
|
|
||||||
(* Type definitions *)
|
(* Type definitions *)
|
||||||
type lemma = Proof.t
|
type lemma = Proof.t
|
||||||
type clause = St.clause
|
type clause = St.clause
|
||||||
type atom = St.atom
|
type atom = St.atom
|
||||||
type int_cl = St.atom list
|
type int_cl = St.atom list
|
||||||
|
|
||||||
type node =
|
type node =
|
||||||
| Assumption
|
| Assumption
|
||||||
| Lemma of lemma
|
| Lemma of lemma
|
||||||
| Resolution of atom * int_cl * int_cl
|
| Resolution of atom * int_cl * int_cl
|
||||||
(* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
|
(* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
|
||||||
|
|
||||||
exception Tautology
|
exception Tautology
|
||||||
exception Resolution_error of string
|
exception Resolution_error of string
|
||||||
|
|
||||||
(* Proof graph *)
|
(* Proof graph *)
|
||||||
module H = Hashtbl.Make(struct
|
module H = Hashtbl.Make(struct
|
||||||
type t = St.atom list
|
type t = St.atom list
|
||||||
let hash= Hashtbl.hash
|
let hash= Hashtbl.hash
|
||||||
let equal = List.for_all2 (==)
|
let equal = List.for_all2 (==)
|
||||||
end)
|
end)
|
||||||
let proof : node H.t = H.create 1007;;
|
let proof : node H.t = H.create 1007;;
|
||||||
|
|
||||||
(* Misc functions *)
|
(* Misc functions *)
|
||||||
let compare_atoms a b =
|
let compare_atoms a b =
|
||||||
Pervasives.compare St.(a.aid) St.(b.aid)
|
Pervasives.compare St.(a.aid) St.(b.aid)
|
||||||
|
|
||||||
let equal_atoms a b = St.(a.aid) = St.(b.aid)
|
let equal_atoms a b = St.(a.aid) = St.(b.aid)
|
||||||
|
|
||||||
|
|
||||||
(* Compute resolution of 2 clauses *)
|
(* Compute resolution of 2 clauses *)
|
||||||
let resolve l =
|
let resolve l =
|
||||||
let rec aux resolved acc = function
|
let rec aux resolved acc = function
|
||||||
| [] -> resolved, acc
|
| [] -> resolved, acc
|
||||||
| [a] -> resolved, a :: acc
|
| [a] -> resolved, a :: acc
|
||||||
| a :: b :: r ->
|
| a :: b :: r ->
|
||||||
if equal_atoms a b then
|
if equal_atoms a b then
|
||||||
aux resolved (a :: acc) r
|
aux resolved (a :: acc) r
|
||||||
else if equal_atoms St.(a.neg) b then
|
else if equal_atoms St.(a.neg) b then
|
||||||
aux (St.(a.var.pa) :: resolved) acc r
|
aux (St.(a.var.pa) :: resolved) acc r
|
||||||
else
|
else
|
||||||
aux resolved (a :: acc) (b :: r)
|
aux resolved (a :: acc) (b :: r)
|
||||||
in
|
in
|
||||||
let resolved, new_clause = aux [] [] l in
|
let resolved, new_clause = aux [] [] l in
|
||||||
resolved, List.rev new_clause
|
resolved, List.rev new_clause
|
||||||
|
|
||||||
let to_list c =
|
let to_list c =
|
||||||
let v = St.(c.atoms) in
|
let v = St.(c.atoms) in
|
||||||
let l = ref [] in
|
let l = ref [] in
|
||||||
for i = 0 to Vec.size v - 1 do
|
for i = 0 to Vec.size v - 1 do
|
||||||
l := (Vec.get v i) :: !l
|
l := (Vec.get v i) :: !l
|
||||||
done;
|
done;
|
||||||
let l, res = resolve (List.sort_uniq compare_atoms !l) in
|
let l, res = resolve (List.sort_uniq compare_atoms !l) in
|
||||||
if l <> [] then
|
if l <> [] then
|
||||||
raise (Resolution_error "Input cause is a tautology");
|
raise (Resolution_error "Input cause is a tautology");
|
||||||
res
|
res
|
||||||
|
|
||||||
(* Adding new proven clauses *)
|
(* Adding new proven clauses *)
|
||||||
let is_proved c = H.mem proof c
|
let is_proved c = H.mem proof c
|
||||||
|
|
||||||
let rec add_res c d =
|
let rec add_res c d =
|
||||||
add_clause c;
|
add_clause c;
|
||||||
add_clause d;
|
add_clause d;
|
||||||
let cl_c = to_list c in
|
let cl_c = to_list c in
|
||||||
let cl_d = to_list d in
|
let cl_d = to_list d in
|
||||||
let l = List.merge compare_atoms cl_c cl_d in
|
let l = List.merge compare_atoms cl_c cl_d in
|
||||||
let resolved, new_clause = resolve l in
|
let resolved, new_clause = resolve l in
|
||||||
match resolved with
|
match resolved with
|
||||||
| [] -> raise (Resolution_error "No literal to resolve over")
|
| [] -> raise (Resolution_error "No literal to resolve over")
|
||||||
| [a] ->
|
| [a] ->
|
||||||
H.add proof new_clause (Resolution (a, cl_c, cl_d));
|
H.add proof new_clause (Resolution (a, cl_c, cl_d));
|
||||||
new_clause
|
new_clause
|
||||||
| _ -> raise (Resolution_error "Resolved to a tautology")
|
| _ -> raise (Resolution_error "Resolved to a tautology")
|
||||||
|
|
||||||
and add_clause c =
|
and add_clause c =
|
||||||
let cl = to_list c in
|
let cl = to_list c in
|
||||||
if is_proved cl then
|
if is_proved cl then
|
||||||
()
|
()
|
||||||
else if not St.(c.learnt) then
|
else if not St.(c.learnt) then
|
||||||
H.add proof cl Assumption
|
H.add proof cl Assumption
|
||||||
else begin
|
else begin
|
||||||
let history = St.(c.cpremise) in
|
let history = St.(c.cpremise) in
|
||||||
()
|
()
|
||||||
(* TODO
|
(* TODO
|
||||||
match history with
|
match history with
|
||||||
| a :: (_ :: _) as r ->
|
| a :: (_ :: _) as r ->
|
||||||
List.fold_left add_res a r
|
List.fold_left add_res a r
|
||||||
*)
|
*)
|
||||||
end
|
end
|
||||||
|
|
||||||
(* Print proof graph *)
|
(* Print proof graph *)
|
||||||
let _i = ref 0
|
let _i = ref 0
|
||||||
let new_id () = incr _i; "id_" ^ (string_of_int !_i)
|
let new_id () = incr _i; "id_" ^ (string_of_int !_i)
|
||||||
|
|
||||||
let ids : (bool * string) H.t = H.create 1007;;
|
let ids : (bool * string) H.t = H.create 1007;;
|
||||||
let cl_id c =
|
let cl_id c =
|
||||||
try
|
try
|
||||||
snd (H.find ids c)
|
snd (H.find ids c)
|
||||||
with Not_found ->
|
with Not_found ->
|
||||||
let id = new_id () in
|
let id = new_id () in
|
||||||
H.add ids c (false, id);
|
H.add ids c (false, id);
|
||||||
id
|
id
|
||||||
|
|
||||||
let is_drawn c =
|
let is_drawn c =
|
||||||
try
|
try
|
||||||
fst (H.find ids c)
|
fst (H.find ids c)
|
||||||
with Not_found ->
|
with Not_found ->
|
||||||
false
|
false
|
||||||
|
|
||||||
let has_drawn c =
|
let has_drawn c =
|
||||||
assert (H.mem ids c);
|
assert (H.mem ids c);
|
||||||
let b, id = H.find ids c in
|
let b, id = H.find ids c in
|
||||||
assert (not b);
|
assert (not b);
|
||||||
H.replace ids c (true, id)
|
H.replace ids c (true, id)
|
||||||
|
|
||||||
let print_atom fmt a =
|
let print_atom fmt a =
|
||||||
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
|
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
|
||||||
|
|
||||||
let rec print_clause fmt = function
|
let rec print_clause fmt = function
|
||||||
| [] -> Format.fprintf fmt "[]"
|
| [] -> Format.fprintf fmt "[]"
|
||||||
| [a] -> print_atom fmt a
|
| [a] -> print_atom fmt a
|
||||||
| a :: (_ :: _) as r -> Format.fprintf fmt "%a \\/ %a" print_atom a print_clause r
|
| a :: (_ :: _) as r -> Format.fprintf fmt "%a \\/ %a" print_atom a print_clause r
|
||||||
|
|
||||||
let print_dot_rule f arg fmt cl =
|
let print_dot_rule f arg fmt cl =
|
||||||
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
|
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
|
||||||
(cl_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\">" f arg
|
(cl_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\">" f arg
|
||||||
|
|
||||||
let print_dot_edge c fmt d =
|
let print_dot_edge c fmt d =
|
||||||
Format.fprintf fmt "%s -> %s;@\n" (cl_id c) (cl_id d)
|
Format.fprintf fmt "%s -> %s;@\n" (cl_id c) (cl_id d)
|
||||||
|
|
||||||
let print_dot_proof fmt cl =
|
let print_dot_proof fmt cl =
|
||||||
match H.find proof cl with
|
match H.find proof cl with
|
||||||
| Assumption ->
|
| Assumption ->
|
||||||
let aux fmt () =
|
let aux fmt () =
|
||||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>" print_clause cl
|
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>" print_clause cl
|
||||||
in
|
in
|
||||||
print_dot_rule aux () fmt cl
|
print_dot_rule aux () fmt cl
|
||||||
| Lemma _ ->
|
| Lemma _ ->
|
||||||
let aux fmt () =
|
let aux fmt () =
|
||||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>" print_clause cl
|
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>" print_clause cl
|
||||||
in
|
in
|
||||||
print_dot_rule aux () fmt cl
|
print_dot_rule aux () fmt cl
|
||||||
| Resolution (r, c, d) ->
|
| Resolution (r, c, d) ->
|
||||||
let aux fmt () =
|
let aux fmt () =
|
||||||
Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD</TR>"
|
Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD</TR>"
|
||||||
print_clause cl print_atom r
|
print_clause cl print_atom r
|
||||||
in
|
in
|
||||||
Format.fprintf fmt "%a%a%a"
|
Format.fprintf fmt "%a%a%a"
|
||||||
(print_dot_rule aux ()) cl
|
(print_dot_rule aux ()) cl
|
||||||
(print_dot_edge cl) c
|
(print_dot_edge cl) c
|
||||||
(print_dot_edge cl) d
|
(print_dot_edge cl) d
|
||||||
|
|
||||||
let print_dot fmt cl =
|
let print_dot fmt cl =
|
||||||
assert (is_proved cl);
|
assert (is_proved cl);
|
||||||
Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof cl
|
Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof cl
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -7,4 +7,4 @@ Copyright 2014 Simon Cruanes
|
||||||
module type S = Res_intf.S
|
module type S = Res_intf.S
|
||||||
|
|
||||||
module Make : functor (St : Solver_types.S)(Proof : sig type t end)
|
module Make : functor (St : Solver_types.S)(Proof : sig type t end)
|
||||||
-> S with type clause = St.clause and type lemma = Proof.t
|
-> S with type clause = St.clause and type lemma = Proof.t
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
(* Copyright 2014 Guillaume Bury *)
|
(* Copyright 2014 Guillaume Bury *)
|
||||||
|
|
||||||
module type S = sig
|
module type S = sig
|
||||||
type clause
|
type clause
|
||||||
type lemma
|
type lemma
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
||||||
|
|
@ -466,32 +466,32 @@ module Make (F : Formula_intf.S)
|
||||||
let locked c =
|
let locked c =
|
||||||
Vec.exists
|
Vec.exists
|
||||||
(fun v -> match v.reason with
|
(fun v -> match v.reason with
|
||||||
| Some c' -> c ==c'
|
| Some c' -> c ==c'
|
||||||
| _ -> false
|
| _ -> false
|
||||||
) env.vars
|
) env.vars
|
||||||
|
|
||||||
(* remove some learnt clauses *)
|
(* remove some learnt clauses *)
|
||||||
let reduce_db () =
|
let reduce_db () =
|
||||||
let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in
|
let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in
|
||||||
Vec.sort env.learnts f_sort_db;
|
Vec.sort env.learnts f_sort_db;
|
||||||
let lim2 = Vec.size env.learnts in
|
let lim2 = Vec.size env.learnts in
|
||||||
let lim1 = lim2 / 2 in
|
let lim1 = lim2 / 2 in
|
||||||
let j = ref 0 in
|
let j = ref 0 in
|
||||||
for i = 0 to lim1 - 1 do
|
for i = 0 to lim1 - 1 do
|
||||||
let c = Vec.get env.learnts i in
|
let c = Vec.get env.learnts i in
|
||||||
if Vec.size c.atoms > 2 && not (locked c) then
|
if Vec.size c.atoms > 2 && not (locked c) then
|
||||||
remove_clause c
|
remove_clause c
|
||||||
else
|
else
|
||||||
begin Vec.set env.learnts !j c; incr j end
|
begin Vec.set env.learnts !j c; incr j end
|
||||||
done;
|
done;
|
||||||
for i = lim1 to lim2 - 1 do
|
for i = lim1 to lim2 - 1 do
|
||||||
let c = Vec.get env.learnts i in
|
let c = Vec.get env.learnts i in
|
||||||
if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then
|
if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then
|
||||||
remove_clause c
|
remove_clause c
|
||||||
else
|
else
|
||||||
begin Vec.set env.learnts !j c; incr j end
|
begin Vec.set env.learnts !j c; incr j end
|
||||||
done;
|
done;
|
||||||
Vec.shrink env.learnts (lim2 - !j)
|
Vec.shrink env.learnts (lim2 - !j)
|
||||||
|
|
||||||
(* remove from [vec] the clauses that are satisfied in the current trail *)
|
(* remove from [vec] the clauses that are satisfied in the current trail *)
|
||||||
let remove_satisfied vec =
|
let remove_satisfied vec =
|
||||||
|
|
@ -792,7 +792,7 @@ module Make (F : Formula_intf.S)
|
||||||
check_vec env.learnts
|
check_vec env.learnts
|
||||||
|
|
||||||
(* fixpoint of propagation and decisions until a model is found, or a
|
(* fixpoint of propagation and decisions until a model is found, or a
|
||||||
conflict is reached *)
|
conflict is reached *)
|
||||||
let solve () =
|
let solve () =
|
||||||
if env.is_unsat then raise (Unsat env.unsat_core);
|
if env.is_unsat then raise (Unsat env.unsat_core);
|
||||||
let n_of_conflicts = ref (to_float env.restart_first) in
|
let n_of_conflicts = ref (to_float env.restart_first) in
|
||||||
|
|
@ -800,8 +800,8 @@ module Make (F : Formula_intf.S)
|
||||||
try
|
try
|
||||||
while true do
|
while true do
|
||||||
begin try
|
begin try
|
||||||
search (to_int !n_of_conflicts) (to_int !n_of_learnts);
|
search (to_int !n_of_conflicts) (to_int !n_of_learnts);
|
||||||
with Restart -> ()
|
with Restart -> ()
|
||||||
end;
|
end;
|
||||||
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
|
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
|
||||||
n_of_learnts := !n_of_learnts *. env.learntsize_inc;
|
n_of_learnts := !n_of_learnts *. env.learntsize_inc;
|
||||||
|
|
@ -924,7 +924,7 @@ module Make (F : Formula_intf.S)
|
||||||
|
|
||||||
let pop l =
|
let pop l =
|
||||||
if l > current_level()
|
if l > current_level()
|
||||||
then invalid_arg "cannot pop() to level, it is too high";
|
then invalid_arg "cannot pop() to level, it is too high";
|
||||||
let i = Vec.get env.levels l in
|
let i = Vec.get env.levels l in
|
||||||
(* see whether we can reset [env.is_unsat] *)
|
(* see whether we can reset [env.is_unsat] *)
|
||||||
if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
|
if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,7 @@ module Make (F : Formula_intf.S)
|
||||||
sig
|
sig
|
||||||
(** Functor to create a SMT Solver parametrised by the atomic
|
(** Functor to create a SMT Solver parametrised by the atomic
|
||||||
formulas and a theory. *)
|
formulas and a theory. *)
|
||||||
|
|
||||||
exception Unsat of St.clause list
|
exception Unsat of St.clause list
|
||||||
|
|
||||||
val solve : unit -> unit
|
val solve : unit -> unit
|
||||||
|
|
|
||||||
|
|
@ -64,8 +64,8 @@ module Make (F : Formula_intf.S) = struct
|
||||||
{ var = dummy_var;
|
{ var = dummy_var;
|
||||||
lit = dummy_lit;
|
lit = dummy_lit;
|
||||||
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 *)
|
||||||
neg = dummy_atom;
|
neg = dummy_atom;
|
||||||
is_true = false;
|
is_true = false;
|
||||||
aid = -102 }
|
aid = -102 }
|
||||||
|
|
|
||||||
|
|
@ -3,52 +3,52 @@
|
||||||
exception Syntax_error of int
|
exception Syntax_error of int
|
||||||
|
|
||||||
type line =
|
type line =
|
||||||
| Empty
|
| Empty
|
||||||
| Comment
|
| Comment
|
||||||
| Pcnf of int * int
|
| Pcnf of int * int
|
||||||
| Clause of int list
|
| Clause of int list
|
||||||
|
|
||||||
let ssplit = Str.split (Str.regexp "[ \t]+")
|
let ssplit = Str.split (Str.regexp "[ \t]+")
|
||||||
|
|
||||||
let of_input f =
|
let of_input f =
|
||||||
match ssplit (input_line f) with
|
match ssplit (input_line f) with
|
||||||
| [] -> Empty
|
| [] -> Empty
|
||||||
| "c" :: _ -> Comment
|
| "c" :: _ -> Comment
|
||||||
| "p" :: "cnf" :: i :: j :: [] ->
|
| "p" :: "cnf" :: i :: j :: [] ->
|
||||||
begin try
|
begin try
|
||||||
Pcnf (int_of_string i, int_of_string j)
|
Pcnf (int_of_string i, int_of_string j)
|
||||||
with Invalid_argument _ ->
|
with Invalid_argument _ ->
|
||||||
raise (Syntax_error (-1))
|
raise (Syntax_error (-1))
|
||||||
end
|
end
|
||||||
| l ->
|
| l ->
|
||||||
begin try
|
begin try
|
||||||
begin match List.rev_map int_of_string l with
|
begin match List.rev_map int_of_string l with
|
||||||
| 0 :: r -> Clause r
|
| 0 :: r -> Clause r
|
||||||
| _ -> raise (Syntax_error (-1))
|
| _ -> raise (Syntax_error (-1))
|
||||||
end
|
end
|
||||||
with Invalid_argument _ -> raise (Syntax_error (-1))
|
with Invalid_argument _ -> raise (Syntax_error (-1))
|
||||||
end
|
end
|
||||||
|
|
||||||
let parse_with todo file =
|
let parse_with todo file =
|
||||||
let f = open_in file in
|
let f = open_in file in
|
||||||
let line = ref 0 in
|
let line = ref 0 in
|
||||||
try
|
try
|
||||||
while true do
|
while true do
|
||||||
incr line;
|
incr line;
|
||||||
todo (of_input f)
|
todo (of_input f)
|
||||||
done
|
done
|
||||||
with
|
with
|
||||||
| Syntax_error _ ->
|
| Syntax_error _ ->
|
||||||
raise (Syntax_error !line)
|
raise (Syntax_error !line)
|
||||||
| End_of_file ->
|
| End_of_file ->
|
||||||
close_in f
|
close_in f
|
||||||
|
|
||||||
let cnf = ref []
|
let cnf = ref []
|
||||||
let parse_line = function
|
let parse_line = function
|
||||||
| Empty | Comment | Pcnf _ -> ()
|
| Empty | Comment | Pcnf _ -> ()
|
||||||
| Clause l -> cnf := l :: !cnf
|
| Clause l -> cnf := l :: !cnf
|
||||||
|
|
||||||
let parse f =
|
let parse f =
|
||||||
cnf := [];
|
cnf := [];
|
||||||
parse_with parse_line f;
|
parse_with parse_line f;
|
||||||
!cnf
|
!cnf
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue