mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-08 04:05:43 -05:00
Indentation + some debug output in res.ml
This commit is contained in:
Guillaume Bury
parent
a13029f96c
commit
62835b35d0
9 changed files with 263 additions and 257 deletions
440
sat/res.ml
440
sat/res.ml
|
|
@ -8,255 +8,261 @@ module type S = Res_intf.S
|
|||
|
||||
module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
|
||||
|
||||
(* Type definitions *)
|
||||
type lemma = Proof.proof
|
||||
type clause = St.clause
|
||||
type atom = St.atom
|
||||
type int_cl = clause * St.atom list
|
||||
(* Type definitions *)
|
||||
type lemma = Proof.proof
|
||||
type clause = St.clause
|
||||
type atom = St.atom
|
||||
type int_cl = clause * St.atom list
|
||||
|
||||
type node =
|
||||
| Assumption
|
||||
| Lemma of lemma
|
||||
| Resolution of atom * int_cl * int_cl
|
||||
(* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
|
||||
type node =
|
||||
| Assumption
|
||||
| Lemma of lemma
|
||||
| Resolution of atom * int_cl * int_cl
|
||||
(* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
|
||||
|
||||
exception Resolution_error of string
|
||||
exception Resolution_error of string
|
||||
|
||||
(* Proof graph *)
|
||||
let hash_cl cl =
|
||||
Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
|
||||
(* Proof graph *)
|
||||
let hash_cl cl =
|
||||
Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
|
||||
|
||||
let equal_cl cl_c cl_d =
|
||||
try
|
||||
List.for_all2 (==) cl_c cl_d
|
||||
with Invalid_argument _ ->
|
||||
false
|
||||
let equal_cl cl_c cl_d =
|
||||
try
|
||||
List.for_all2 (==) cl_c cl_d
|
||||
with Invalid_argument _ ->
|
||||
false
|
||||
|
||||
module H = Hashtbl.Make(struct
|
||||
type t = St.atom list
|
||||
let hash = hash_cl
|
||||
let equal = equal_cl
|
||||
module H = Hashtbl.Make(struct
|
||||
type t = St.atom list
|
||||
let hash = hash_cl
|
||||
let equal = equal_cl
|
||||
end)
|
||||
let proof : node H.t = H.create 1007;;
|
||||
let proof : node H.t = H.create 1007;;
|
||||
|
||||
(* Misc functions *)
|
||||
let equal_atoms a b = St.(a.aid) = St.(b.aid)
|
||||
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
|
||||
(* Misc functions *)
|
||||
let equal_atoms a b = St.(a.aid) = St.(b.aid)
|
||||
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
|
||||
|
||||
(* 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
|
||||
(* Printing functions *)
|
||||
let print_atom fmt a =
|
||||
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
|
||||
|
||||
let to_list c =
|
||||
let v = St.(c.atoms) in
|
||||
let l = ref [] in
|
||||
for i = 0 to Vec.size v - 1 do
|
||||
l := (Vec.get v i) :: !l
|
||||
done;
|
||||
let l, res = resolve (List.sort_uniq compare_atoms !l) in
|
||||
if l <> [] then
|
||||
raise (Resolution_error "Input cause is a tautology");
|
||||
res
|
||||
let rec print_cl fmt = function
|
||||
| [] -> Format.fprintf fmt "[]"
|
||||
| [a] -> print_atom fmt a
|
||||
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r
|
||||
|
||||
(* Adding new proven clauses *)
|
||||
let is_proved c = H.mem proof c
|
||||
let is_proven c = is_proved (to_list 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
|
||||
|
||||
let add_res (c, cl_c) (d, cl_d) =
|
||||
Log.debug 7 "Resolving clauses :";
|
||||
Log.debug 7 " %a" St.pp_clause c;
|
||||
Log.debug 7 " %a" St.pp_clause d;
|
||||
let l = List.merge compare_atoms cl_c cl_d in
|
||||
let resolved, new_clause = resolve l in
|
||||
match resolved with
|
||||
| [] -> raise (Resolution_error "No literal to resolve over")
|
||||
| [a] ->
|
||||
H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
|
||||
let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in
|
||||
Log.debug 5 "New clause : %a" St.pp_clause new_c;
|
||||
new_c, new_clause
|
||||
| _ -> raise (Resolution_error "Resolved to a tautology")
|
||||
let to_list c =
|
||||
let v = St.(c.atoms) in
|
||||
let l = ref [] in
|
||||
for i = 0 to Vec.size v - 1 do
|
||||
l := (Vec.get v i) :: !l
|
||||
done;
|
||||
let l, res = resolve (List.sort_uniq compare_atoms !l) in
|
||||
if l <> [] then
|
||||
raise (Resolution_error "Input cause is a tautology");
|
||||
res
|
||||
|
||||
let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *)
|
||||
match l with
|
||||
| a :: ((_ :: _) as r) ->
|
||||
let new_c, new_cl = List.fold_left add_res a r in
|
||||
assert (equal_cl cl new_cl)
|
||||
| _ -> assert false
|
||||
(* Adding new proven clauses *)
|
||||
let is_proved c = H.mem proof c
|
||||
let is_proven c = is_proved (to_list c)
|
||||
|
||||
let need_clause (c, cl) =
|
||||
if is_proved cl then
|
||||
[]
|
||||
else if not St.(c.learnt) then begin
|
||||
Log.debug 8 "Adding to hyps : %a" St.pp_clause c;
|
||||
H.add proof cl Assumption;
|
||||
[]
|
||||
let add_res (c, cl_c) (d, cl_d) =
|
||||
Log.debug 7 "Resolving clauses :";
|
||||
Log.debug 7 " %a" St.pp_clause c;
|
||||
Log.debug 7 " %a" St.pp_clause d;
|
||||
let l = List.merge compare_atoms cl_c cl_d in
|
||||
let resolved, new_clause = resolve l in
|
||||
match resolved with
|
||||
| [] -> raise (Resolution_error "No literal to resolve over")
|
||||
| [a] ->
|
||||
H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
|
||||
let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in
|
||||
Log.debug 5 "New clause : %a" St.pp_clause new_c;
|
||||
new_c, new_clause
|
||||
| _ -> raise (Resolution_error "Resolved to a tautology")
|
||||
|
||||
let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *)
|
||||
match l with
|
||||
| a :: ((_ :: _) as r) ->
|
||||
let new_c, new_cl = List.fold_left add_res a r in
|
||||
if not (equal_cl cl new_cl) then begin
|
||||
Log.debug 0 "Expected the following clauses to be equal :";
|
||||
Log.debug 0 "expected : %s" (Log.on_fmt print_cl cl);
|
||||
Log.debug 0 "found : %a" St.pp_clause new_c;
|
||||
assert false
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
let need_clause (c, cl) =
|
||||
if is_proved cl then
|
||||
[]
|
||||
else if not St.(c.learnt) then begin
|
||||
Log.debug 8 "Adding to hyps : %a" St.pp_clause c;
|
||||
H.add proof cl Assumption;
|
||||
[]
|
||||
end else
|
||||
St.(c.cpremise)
|
||||
|
||||
let rec do_clause = function
|
||||
| [] -> ()
|
||||
| c :: r ->
|
||||
let cl = to_list c in
|
||||
let l = need_clause (c, cl) in
|
||||
if l = [] then (* c is either an asusmption, or already proved *)
|
||||
do_clause r
|
||||
else
|
||||
let l' = List.rev_map (fun c -> c, to_list c) l in
|
||||
let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in
|
||||
let to_prove = List.rev_map fst to_prove in
|
||||
if to_prove = [] then begin
|
||||
(* See wether we can prove c right now *)
|
||||
add_clause cl l';
|
||||
do_clause r
|
||||
end else
|
||||
St.(c.cpremise)
|
||||
(* Or if we have to prove some other clauses first *)
|
||||
do_clause (to_prove @ (c :: r))
|
||||
|
||||
let rec do_clause = function
|
||||
| [] -> ()
|
||||
| c :: r ->
|
||||
let cl = to_list c in
|
||||
let l = need_clause (c, cl) in
|
||||
if l = [] then (* c is either an asusmption, or already proved *)
|
||||
do_clause r
|
||||
else
|
||||
let l' = List.rev_map (fun c -> c, to_list c) l in
|
||||
let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in
|
||||
let to_prove = List.rev_map fst to_prove in
|
||||
if to_prove = [] then begin
|
||||
(* See wether we can prove c right now *)
|
||||
add_clause cl l';
|
||||
do_clause r
|
||||
end else
|
||||
(* Or if we have to prove some other clauses first *)
|
||||
do_clause (to_prove @ (c :: r))
|
||||
let prove c =
|
||||
Log.debug 3 "Proving : %a" St.pp_clause c;
|
||||
do_clause [c];
|
||||
Log.debug 3 "Proved : %a" St.pp_clause c
|
||||
|
||||
let prove c =
|
||||
Log.debug 3 "Proving : %a" St.pp_clause c;
|
||||
do_clause [c];
|
||||
Log.debug 3 "Proved : %a" St.pp_clause c
|
||||
|
||||
let clause_unit a = St.(
|
||||
let l = if a.is_true then [a] else [a.neg] in
|
||||
make_clause (fresh_name ()) l 1 true a.var.vpremise
|
||||
let clause_unit a = St.(
|
||||
let l = if a.is_true then [a] else [a.neg] in
|
||||
make_clause (fresh_name ()) l 1 true a.var.vpremise
|
||||
)
|
||||
|
||||
let rec prove_unsat_cl (c, cl) = match cl with
|
||||
| [] -> true
|
||||
| a :: r ->
|
||||
try
|
||||
Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
|
||||
let d = match St.(a.var.level, a.var.reason) with
|
||||
| 0, Some d -> d
|
||||
| 0, None -> clause_unit a
|
||||
| _ -> raise Exit
|
||||
in
|
||||
prove d;
|
||||
let cl_d = to_list d in
|
||||
prove_unsat_cl (add_res (c, cl) (d, cl_d))
|
||||
with Exit -> false
|
||||
|
||||
exception Cannot
|
||||
let assert_can_prove_unsat c =
|
||||
Log.debug 1 "=================== Proof =====================";
|
||||
prove c;
|
||||
if not (prove_unsat_cl (c, to_list c)) then raise Cannot
|
||||
|
||||
(* Interface exposed *)
|
||||
type proof_node = {
|
||||
conclusion : clause;
|
||||
step : step;
|
||||
}
|
||||
and proof = unit -> proof_node
|
||||
and step =
|
||||
| Hypothesis
|
||||
| Lemma of lemma
|
||||
| Resolution of proof * proof * atom
|
||||
|
||||
let rec return_proof (c, cl) () =
|
||||
Log.debug 8 "Returning proof for : %a" St.pp_clause c;
|
||||
let st = match H.find proof cl with
|
||||
| Assumption -> Hypothesis
|
||||
| Lemma l -> Lemma l
|
||||
| Resolution (a, cl_c, cl_d) ->
|
||||
Resolution (return_proof cl_c, return_proof cl_d, a)
|
||||
let rec prove_unsat_cl (c, cl) = match cl with
|
||||
| [] -> true
|
||||
| a :: r ->
|
||||
try
|
||||
Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
|
||||
let d = match St.(a.var.level, a.var.reason) with
|
||||
| 0, Some d -> d
|
||||
| 0, None -> clause_unit a
|
||||
| _ -> raise Exit
|
||||
in
|
||||
{ conclusion = c; step = st }
|
||||
prove d;
|
||||
let cl_d = to_list d in
|
||||
prove_unsat_cl (add_res (c, cl) (d, cl_d))
|
||||
with Exit -> false
|
||||
|
||||
let prove_unsat c =
|
||||
assert_can_prove_unsat c;
|
||||
return_proof (St.empty_clause, [])
|
||||
exception Cannot
|
||||
let assert_can_prove_unsat c =
|
||||
Log.debug 1 "=================== Proof =====================";
|
||||
prove c;
|
||||
if not (prove_unsat_cl (c, to_list c)) then raise Cannot
|
||||
|
||||
(* Print proof graph *)
|
||||
let _i = ref 0
|
||||
let new_id () = incr _i; "id_" ^ (string_of_int !_i)
|
||||
(* Interface exposed *)
|
||||
type proof_node = {
|
||||
conclusion : clause;
|
||||
step : step;
|
||||
}
|
||||
and proof = unit -> proof_node
|
||||
and step =
|
||||
| Hypothesis
|
||||
| Lemma of lemma
|
||||
| Resolution of proof * proof * atom
|
||||
|
||||
let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
|
||||
let c_id c =
|
||||
try
|
||||
snd (Hashtbl.find ids c)
|
||||
with Not_found ->
|
||||
let id = new_id () in
|
||||
Hashtbl.add ids c (false, id);
|
||||
id
|
||||
let rec return_proof (c, cl) () =
|
||||
Log.debug 8 "Returning proof for : %a" St.pp_clause c;
|
||||
let st = match H.find proof cl with
|
||||
| Assumption -> Hypothesis
|
||||
| Lemma l -> Lemma l
|
||||
| Resolution (a, cl_c, cl_d) ->
|
||||
Resolution (return_proof cl_c, return_proof cl_d, a)
|
||||
in
|
||||
{ conclusion = c; step = st }
|
||||
|
||||
let clear_ids () =
|
||||
Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
|
||||
let prove_unsat c =
|
||||
assert_can_prove_unsat c;
|
||||
return_proof (St.empty_clause, [])
|
||||
|
||||
let is_drawn c =
|
||||
try
|
||||
fst (Hashtbl.find ids c)
|
||||
with Not_found ->
|
||||
false
|
||||
(* Print proof graph *)
|
||||
let _i = ref 0
|
||||
let new_id () = incr _i; "id_" ^ (string_of_int !_i)
|
||||
|
||||
let has_drawn c =
|
||||
assert (Hashtbl.mem ids c);
|
||||
let b, id = Hashtbl.find ids c in
|
||||
assert (not b);
|
||||
Hashtbl.replace ids c (true, id)
|
||||
let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
|
||||
let c_id c =
|
||||
try
|
||||
snd (Hashtbl.find ids c)
|
||||
with Not_found ->
|
||||
let id = new_id () in
|
||||
Hashtbl.add ids c (false, id);
|
||||
id
|
||||
|
||||
let print_atom fmt a =
|
||||
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
|
||||
let clear_ids () =
|
||||
Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
|
||||
|
||||
let rec print_cl fmt = function
|
||||
| [] -> Format.fprintf fmt "[]"
|
||||
| [a] -> print_atom fmt a
|
||||
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r
|
||||
let is_drawn c =
|
||||
try
|
||||
fst (Hashtbl.find ids c)
|
||||
with Not_found ->
|
||||
false
|
||||
|
||||
let print_clause fmt c = print_cl fmt (to_list c)
|
||||
let has_drawn c =
|
||||
assert (Hashtbl.mem ids c);
|
||||
let b, id = Hashtbl.find ids c in
|
||||
assert (not b);
|
||||
Hashtbl.replace ids c (true, id)
|
||||
|
||||
let print_dot_rule f arg fmt cl =
|
||||
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
|
||||
(c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg
|
||||
let print_clause fmt c = print_cl fmt (to_list c)
|
||||
|
||||
let print_dot_edge c fmt d =
|
||||
Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d)
|
||||
let print_dot_rule f arg fmt cl =
|
||||
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
|
||||
(c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg
|
||||
|
||||
let rec print_dot_proof fmt p =
|
||||
match p.step with
|
||||
| Hypothesis ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>"
|
||||
print_clause p.conclusion
|
||||
in
|
||||
print_dot_rule aux () fmt p.conclusion
|
||||
| Lemma _ ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>"
|
||||
print_clause p.conclusion
|
||||
in
|
||||
print_dot_rule aux () fmt p.conclusion
|
||||
| Resolution (proof1, proof2, a) ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD></TR>"
|
||||
print_clause p.conclusion print_atom a
|
||||
in
|
||||
let p1 = proof1 () in
|
||||
let p2 = proof2 () in
|
||||
Format.fprintf fmt "%a%a%a%a%a"
|
||||
(print_dot_rule aux ()) p.conclusion
|
||||
(print_dot_edge p.conclusion) p1.conclusion
|
||||
(print_dot_edge p.conclusion) p2.conclusion
|
||||
print_dot_proof p1
|
||||
print_dot_proof p2
|
||||
let print_dot_edge c fmt d =
|
||||
Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d)
|
||||
|
||||
let print_dot fmt proof =
|
||||
clear_ids ();
|
||||
Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ())
|
||||
let rec print_dot_proof fmt p =
|
||||
match p.step with
|
||||
| Hypothesis ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>"
|
||||
print_clause p.conclusion
|
||||
in
|
||||
print_dot_rule aux () fmt p.conclusion
|
||||
| Lemma _ ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>"
|
||||
print_clause p.conclusion
|
||||
in
|
||||
print_dot_rule aux () fmt p.conclusion
|
||||
| Resolution (proof1, proof2, a) ->
|
||||
let aux fmt () =
|
||||
Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD></TR>"
|
||||
print_clause p.conclusion print_atom a
|
||||
in
|
||||
let p1 = proof1 () in
|
||||
let p2 = proof2 () in
|
||||
Format.fprintf fmt "%a%a%a%a%a"
|
||||
(print_dot_rule aux ()) p.conclusion
|
||||
(print_dot_edge p.conclusion) p1.conclusion
|
||||
(print_dot_edge p.conclusion) p2.conclusion
|
||||
print_dot_proof p1
|
||||
print_dot_proof p2
|
||||
|
||||
let print_dot fmt proof =
|
||||
clear_ids ();
|
||||
Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ())
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -15,8 +15,8 @@ module type S = sig
|
|||
@raise Cannot if it is impossible. *)
|
||||
|
||||
type proof_node = {
|
||||
conclusion : clause;
|
||||
step : step;
|
||||
conclusion : clause;
|
||||
step : step;
|
||||
}
|
||||
and proof = unit -> proof_node
|
||||
and step =
|
||||
|
|
|
|||
|
|
@ -120,9 +120,9 @@ module Make(Dummy : sig end) = struct
|
|||
let eval = SatSolver.eval
|
||||
|
||||
let get_proof () =
|
||||
match SatSolver.unsat_conflict () with
|
||||
| None -> assert false
|
||||
| Some c -> SatSolver.Proof.prove_unsat c
|
||||
match SatSolver.unsat_conflict () with
|
||||
| None -> assert false
|
||||
| Some c -> SatSolver.Proof.prove_unsat c
|
||||
|
||||
let print_proof = SatSolver.Proof.print_dot
|
||||
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@ sig
|
|||
|
||||
module Proof : Res.S with
|
||||
type atom = St.atom and
|
||||
type clause = St.clause and
|
||||
type lemma = Th.proof
|
||||
type clause = St.clause and
|
||||
type lemma = Th.proof
|
||||
|
||||
val solve : unit -> unit
|
||||
(** Try and solves the current set of assumptions.
|
||||
|
|
|
|||
|
|
@ -123,9 +123,9 @@ module Make (F : Formula_intf.S) = struct
|
|||
var, negated
|
||||
|
||||
let made_vars_info vars =
|
||||
Vec.grow_to_by_double vars !cpt_mk_var;
|
||||
MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma;
|
||||
!cpt_mk_var
|
||||
Vec.grow_to_by_double vars !cpt_mk_var;
|
||||
MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma;
|
||||
!cpt_mk_var
|
||||
|
||||
let add_atom lit =
|
||||
let var, negated = make_var lit in
|
||||
|
|
|
|||
|
|
@ -15,12 +15,12 @@ type line =
|
|||
let rec _read_word s acc i len =
|
||||
assert (len>0);
|
||||
if i+len=String.length s
|
||||
then String.sub s i len :: acc
|
||||
else match s.[i+len] with
|
||||
| ' ' | '\t' ->
|
||||
let acc = String.sub s i len :: acc in
|
||||
_skip_space s acc (i+len+1)
|
||||
| _ -> _read_word s acc i (len+1)
|
||||
then String.sub s i len :: acc
|
||||
else match s.[i+len] with
|
||||
| ' ' | '\t' ->
|
||||
let acc = String.sub s i len :: acc in
|
||||
_skip_space s acc (i+len+1)
|
||||
| _ -> _read_word s acc i (len+1)
|
||||
and _skip_space s acc i =
|
||||
if i=String.length s
|
||||
then acc
|
||||
|
|
|
|||
|
|
@ -35,26 +35,26 @@ let int_arg r arg =
|
|||
|
||||
let setup_gc_stat () =
|
||||
at_exit (fun () ->
|
||||
Gc.print_stat stdout;
|
||||
)
|
||||
Gc.print_stat stdout;
|
||||
)
|
||||
|
||||
let input_file = fun s -> file := s
|
||||
let usage = "Usage : main [options] <file>"
|
||||
let argspec = Arg.align [
|
||||
"-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
|
||||
" Enable stack traces";
|
||||
" Enable stack traces";
|
||||
"-gc", Arg.Unit setup_gc_stat,
|
||||
" Outputs statistics about the GC";
|
||||
" Outputs statistics about the GC";
|
||||
"-model", Arg.Set p_assign,
|
||||
" Outputs the boolean model found if sat";
|
||||
" Outputs the boolean model found if sat";
|
||||
"-p", Arg.Set p_proof,
|
||||
" Outputs the proof found (in dot format) if unsat";
|
||||
" Outputs the proof found (in dot format) if unsat";
|
||||
"-s", Arg.String (int_arg size_limit),
|
||||
"<s>[kMGT] Sets the size limit for the sat solver";
|
||||
"<s>[kMGT] Sets the size limit for the sat solver";
|
||||
"-t", Arg.String (int_arg time_limit),
|
||||
"<t>[smhd] Sets the time limit for the sat solver";
|
||||
"<t>[smhd] Sets the time limit for the sat solver";
|
||||
"-v", Arg.Int (fun i -> Log.set_debug i),
|
||||
"<lvl> Sets the debug verbose level";
|
||||
"<lvl> Sets the debug verbose level";
|
||||
]
|
||||
|
||||
(* Limits alarm *)
|
||||
|
|
@ -109,8 +109,8 @@ let main () =
|
|||
| S.Unsat ->
|
||||
Format.printf "Unsat@.";
|
||||
if !p_proof then begin
|
||||
let p = S.get_proof () in
|
||||
S.print_proof Format.std_formatter p
|
||||
let p = S.get_proof () in
|
||||
S.print_proof Format.std_formatter p
|
||||
end
|
||||
|
||||
let () =
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ Copyright 2014 Simon Cruanes
|
|||
(** {1 Sparse vector, filled with default value} *)
|
||||
|
||||
let _size_too_big()=
|
||||
failwith "Sparse_vec: capacity exceeds maximum array size"
|
||||
failwith "Sparse_vec: capacity exceeds maximum array size"
|
||||
|
||||
type 'a t = { default : 'a; mutable data : 'a array; mutable sz : int }
|
||||
|
||||
|
|
@ -17,8 +17,8 @@ let make sz default =
|
|||
{ default; sz; data=Array.make sz default; }
|
||||
|
||||
let init sz f default =
|
||||
if sz > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init sz (fun i -> f i); sz ; default}
|
||||
if sz > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init sz (fun i -> f i); sz ; default}
|
||||
|
||||
let length {sz} = sz
|
||||
|
||||
|
|
@ -37,7 +37,7 @@ let rec grow_to_by_double t new_capa =
|
|||
let data = t.data in
|
||||
let capa = ref (Array.length data + 1) in
|
||||
while !capa < new_capa do
|
||||
capa := min (2 * !capa) Sys.max_array_length;
|
||||
capa := min (2 * !capa) Sys.max_array_length;
|
||||
done;
|
||||
grow_to t !capa
|
||||
|
||||
|
|
|
|||
18
util/vec.ml
18
util/vec.ml
|
|
@ -14,17 +14,17 @@
|
|||
type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
|
||||
|
||||
let _size_too_big()=
|
||||
failwith "Vec: capacity exceeds maximum array size"
|
||||
failwith "Vec: capacity exceeds maximum array size"
|
||||
|
||||
let make capa d =
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.make capa d; sz = 0; dummy = d}
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.make capa d; sz = 0; dummy = d}
|
||||
|
||||
let make_empty d = {data = [||]; sz=0; dummy=d }
|
||||
|
||||
let init capa f d =
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
|
||||
if capa > Sys.max_array_length then _size_too_big();
|
||||
{data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
|
||||
|
||||
let from_array data sz d =
|
||||
assert (sz <= Array.length data);
|
||||
|
|
@ -53,16 +53,16 @@ let grow_to t new_capa =
|
|||
t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy)
|
||||
|
||||
let grow_to_double_size t =
|
||||
if Array.length t.data = Sys.max_array_length then _size_too_big();
|
||||
let size = min Sys.max_array_length (2* Array.length t.data) in
|
||||
grow_to t size
|
||||
if Array.length t.data = Sys.max_array_length then _size_too_big();
|
||||
let size = min Sys.max_array_length (2* Array.length t.data) in
|
||||
grow_to t size
|
||||
|
||||
let rec grow_to_by_double t new_capa =
|
||||
if new_capa > Sys.max_array_length then _size_too_big ();
|
||||
let data = t.data in
|
||||
let capa = ref (Array.length data + 1) in
|
||||
while !capa < new_capa do
|
||||
capa := min (2 * !capa) Sys.max_array_length;
|
||||
capa := min (2 * !capa) Sys.max_array_length;
|
||||
done;
|
||||
grow_to t !capa
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue