[Toss-devel-svn] SF.net SVN: toss:[1416] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1416] trunk/Toss
|
From: <luk...@us...> - 2011-04-17 14:05:36
|
Revision: 1416
http://toss.svn.sourceforge.net/toss/?rev=1416&view=rev
Author: lukaszkaiser
Date: 2011-04-17 14:05:28 +0000 (Sun, 17 Apr 2011)
Log Message:
-----------
Moving Sat tests to OUnit and adding to TossTest, code style cleanups in BoolFormula.
Modified Paths:
--------------
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/Sat/Makefile
trunk/Toss/Makefile
trunk/Toss/TossTest.ml
Added Paths:
-----------
trunk/Toss/Formula/Sat/SatTest.ml
Removed Paths:
-------------
trunk/Toss/Formula/Sat/Test.ml
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2011-04-17 01:25:17 UTC (rev 1415)
+++ trunk/Toss/Formula/BoolFormula.ml 2011-04-17 14:05:28 UTC (rev 1416)
@@ -5,7 +5,7 @@
(* 0 : no generation is performed and to_cnf transforms a DNF
1 : use Tseitin to construct a CNF with auxiliary variables
- 2 : (default) use Plaisted-Greenbaum to construct a CNF with auxiliary variables *)
+ 2 : use Plaisted-Greenbaum to construct a CNF with auxiliary variables *)
let auxcnf_generation = ref 2
let set_auxcnf i = (auxcnf_generation := i)
@@ -32,7 +32,8 @@
(* ----------------------- BASIC TYPE CONVERSIONS -------------------------- *)
-let int_of_lit lit = match lit with BVar v -> v | _ -> failwith ("This is not a literal!")
+let int_of_lit lit =
+ match lit with BVar v -> v | _ -> failwith ("This is not a literal!")
let lit_of_int v = BVar v
@@ -112,12 +113,17 @@
(* Convert a Boolean combination into reduced form (over 'not' and 'or') *)
let rec to_reduced_form ?(neg=false) = function
BVar v -> if neg then BVar (-1 * v) else BVar v
- | BNot phi -> if neg then to_reduced_form ~neg:false phi else to_reduced_form ~neg:true phi
+ | BNot phi ->
+ if neg then to_reduced_form ~neg:false phi else
+ to_reduced_form ~neg:true phi
| BAnd [f] | BOr [f] -> to_reduced_form ~neg f
- | BOr (bflist) when neg -> BNot (BOr (List.rev_map (to_reduced_form ~neg:false) bflist))
+ | BOr (bflist) when neg ->
+ BNot (BOr (List.rev_map (to_reduced_form ~neg:false) bflist))
| BOr (bflist) -> BOr (List.rev_map (to_reduced_form ~neg:false) bflist)
- | BAnd (bflist) when neg -> BOr (List.rev_map (to_reduced_form ~neg:true) bflist)
- | BAnd (bflist) -> BNot (BOr (List.rev_map (to_reduced_form ~neg:true) bflist))
+ | BAnd (bflist) when neg ->
+ BOr (List.rev_map (to_reduced_form ~neg:true) bflist)
+ | BAnd (bflist) ->
+ BNot (BOr (List.rev_map (to_reduced_form ~neg:true) bflist))
(* Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
@@ -190,7 +196,8 @@
let id = Hashtbl.find ids phi in if pos then id else -1 * id
with Not_found ->
if !debug_level > 2 then
- print_endline ("Added " ^ (Formula.str phi) ^ " as " ^ (string_of_int !free_id));
+ print_endline ("Added " ^ (Formula.str phi) ^ " as " ^
+ (string_of_int !free_id));
Hashtbl.add ids phi (!free_id);
Hashtbl.add rev_ids (!free_id) phi;
Hashtbl.add rev_ids (-1 * !free_id) (Formula.Not phi);
@@ -199,10 +206,14 @@
let rec bool_formula ?(pos=true) = function
Formula.Not (phi) when pos -> bool_formula ~pos:false phi
| Formula.Not (phi) -> bool_formula ~pos:true phi
- | Formula.And (flist) when pos -> BAnd (List.rev_map (bool_formula ~pos:true) flist)
- | Formula.And (flist) -> BNot (BAnd (List.rev_map (bool_formula ~pos:true) flist))
- | Formula.Or (flist) when pos -> BOr (List.rev_map (bool_formula ~pos:true) flist)
- | Formula.Or (flist) -> BNot (BOr (List.rev_map (bool_formula ~pos:true) flist))
+ | Formula.And (flist) when pos ->
+ BAnd (List.rev_map (bool_formula ~pos:true) flist)
+ | Formula.And (flist) ->
+ BNot (BAnd (List.rev_map (bool_formula ~pos:true) flist))
+ | Formula.Or (flist) when pos ->
+ BOr (List.rev_map (bool_formula ~pos:true) flist)
+ | Formula.Or (flist) ->
+ BNot (BOr (List.rev_map (bool_formula ~pos:true) flist))
| phi -> BVar (get_id ~pos:pos phi) in
bool_formula phi
@@ -217,13 +228,17 @@
let rec formula ?(pos=true) = function
BNot (phi) when pos -> formula ~pos:false phi
| BNot (phi) -> formula ~pos:true phi
- | BAnd (flist) when pos -> Formula.And (List.rev_map (formula ~pos:true) flist)
- | BAnd (flist) -> Formula.Not (Formula.And (List.rev_map (formula ~pos:true) flist))
- | BOr (flist) when pos -> Formula.Or (List.rev_map (formula ~pos:true) flist)
- | BOr (flist) -> Formula.Not (Formula.Or (List.rev_map (formula ~pos:true) flist))
- | BVar id -> try
- (Hashtbl.find rev_ids id)
- with Not_found -> failwith ("Boolean combination contains a non-hashed literal!") in
+ | BAnd (flist) when pos ->
+ Formula.And (List.rev_map (formula ~pos:true) flist)
+ | BAnd (flist) ->
+ Formula.Not (Formula.And (List.rev_map (formula ~pos:true) flist))
+ | BOr (flist) when pos ->
+ Formula.Or (List.rev_map (formula ~pos:true) flist)
+ | BOr (flist) ->
+ Formula.Not (Formula.Or (List.rev_map (formula ~pos:true) flist))
+ | BVar id -> try (Hashtbl.find rev_ids id) with
+ Not_found ->
+ failwith ("Boolean combination contains a non-hashed literal!") in
formula phi
@@ -234,215 +249,257 @@
let is_literal = function BNot (BVar _) | BVar _ -> true | _ -> false in
let rec flatten phi =
match phi with
- BNot (BNot psi) -> psi
+ | BNot (BNot psi) -> psi
| BNot (BVar v) -> BVar (-v)
| BNot psi -> BNot (flatten psi)
| BOr (flist) ->
- if not (List.exists is_disjunction flist)
- then BOr (List.map flatten flist)
- else (BOr (List.flatten (List.map (fun psi -> match psi with
- BOr psis -> List.map flatten psis
- | _ -> [flatten psi] ) flist)))
+ if not (List.exists is_disjunction flist) then
+ BOr (List.map flatten flist)
+ else
+ (BOr (List.flatten (List.map
+ (function
+ | BOr psis -> List.map flatten psis
+ | psi -> [flatten psi] ) flist)))
| BAnd (flist) ->
- if not (List.exists is_conjunction flist)
- then BAnd (List.map flatten flist)
- else (BAnd (List.flatten (List.map (fun psi -> match psi with
- BAnd psis -> List.map flatten psis
- | _ -> [flatten psi] ) flist)))
+ if not (List.exists is_conjunction flist) then
+ BAnd (List.map flatten flist)
+ else (BAnd (List.flatten (List.map
+ (function
+ | BAnd psis -> List.map flatten psis
+ | psi -> [flatten psi] ) flist)))
| _ -> phi in
let rec neutral_absorbing = function
- BVar _ as lit -> lit
+ | BVar _ as lit -> lit
| BNot psi -> BNot (neutral_absorbing phi)
- | BOr psis -> let filtered = List.filter (fun psi -> psi <> BOr []) psis in
- if (List.exists (fun psi -> psi = BAnd []) filtered)
- then (BAnd []) else BOr (List.map neutral_absorbing filtered)
- | BAnd psis -> let filtered = List.filter (fun psi -> psi <> BAnd []) psis in
- if (List.exists (fun psi -> psi = BOr []) filtered)
- then (BOr []) else BAnd (List.map neutral_absorbing filtered) in
+ | BOr psis ->
+ let filtered = List.filter (fun psi -> psi <> BOr []) psis in
+ if (List.exists (fun psi -> psi = BAnd []) filtered) then (BAnd []) else
+ BOr (List.map neutral_absorbing filtered)
+ | BAnd psis ->
+ let filtered = List.filter (fun psi -> psi <> BAnd []) psis in
+ if (List.exists (fun psi -> psi = BOr []) filtered) then (BOr []) else
+ BAnd (List.map neutral_absorbing filtered) in
let rec singularise unsorted_phi =
let phi = sort unsorted_phi in (* this should be done more elegantly!!! *)
let rec neg_occurrence = function
- (* check whether a _sorted_ "uniqued" list contains a pair (phi,not phi)
- at the moment this only works for literals due to the implementation of compare! *)
- [] | [_] -> false
- | a :: b :: xs -> if (compare a b) = 0 then true else neg_occurrence (b :: xs) in
+ (* check whether a _sorted_ uniqued list contains a pair (phi,not phi)
+ for now only works for literals due to implementation of compare! *)
+ | [] | [_] -> false
+ | a :: b :: xs ->
+ if (compare a b) = 0 then true else neg_occurrence (b :: xs) in
match phi with
- BVar _ -> phi
+ | BVar _ -> phi
| BNot psi -> BNot (singularise psi)
- | BOr psis -> let unique_psis = Aux.unique (=) psis in
- let lits = List.filter is_literal unique_psis in
- if neg_occurrence lits then BAnd [] else BOr (List.map singularise unique_psis)
- | BAnd psis -> let unique_psis = Aux.unique (=) psis in
- let lits = List.filter is_literal unique_psis in
- if neg_occurrence lits then BOr [] else BAnd (List.map singularise unique_psis) in
+ | BOr psis ->
+ let unique_psis = Aux.unique (=) psis in
+ let lits = List.filter is_literal unique_psis in
+ if neg_occurrence lits then BAnd [] else
+ BOr (List.map singularise unique_psis)
+ | BAnd psis ->
+ let unique_psis = Aux.unique (=) psis in
+ let lits = List.filter is_literal unique_psis in
+ if neg_occurrence lits then BOr [] else
+ BAnd (List.map singularise unique_psis) in
let rec subsumption phi =
let subclause a b =
match (a,b) with
- (BOr psis, BOr thetas)
- | (BAnd psis, BAnd thetas) -> List.for_all (fun x -> List.exists (fun y -> y=x) thetas) psis
- | (_, _) -> false in
+ | (BOr psis, BOr thetas)
+ | (BAnd psis, BAnd thetas) ->
+ List.for_all (fun x -> List.exists (fun y -> y=x) thetas) psis
+ | (_, _) -> false in
let subformula psi theta =
match theta with
- BOr thetas
+ | BOr thetas
| BAnd thetas -> List.exists (fun theta -> theta = psi) thetas
- | _ -> false in
+ | _ -> false in
match phi with
- BVar _ | BNot _ -> phi
+ | BVar _ | BNot _ -> phi
| BAnd psis ->
- let (disjnctns,non_disjnctns) = List.partition is_disjunction psis in
- BAnd(non_disjnctns @ List.filter
- (fun theta ->
- (List.for_all (fun phi -> phi=theta or not (subformula phi theta)) non_disjnctns)
- & (List.for_all (fun phi -> phi=theta or not (subclause phi theta)) disjnctns))
- disjnctns)
+ let (disjnctns,non_disjnctns) = List.partition is_disjunction psis in
+ BAnd(non_disjnctns @ List.filter
+ (fun theta ->
+ (List.for_all (fun phi -> phi=theta or
+ not (subformula phi theta)) non_disjnctns)
+ & (List.for_all (fun phi -> phi=theta or
+ not (subclause phi theta)) disjnctns))
+ disjnctns)
| BOr psis ->
- let (conjnctns,non_conjnctns) = List.partition is_conjunction psis in
- BOr(non_conjnctns @ List.filter
+ let (conjnctns,non_conjnctns) = List.partition is_conjunction psis in
+ BOr(non_conjnctns @ List.filter
(fun theta ->
- (List.for_all (fun phi -> phi=theta or not (subformula phi theta)) non_conjnctns)
- & (List.for_all (fun phi -> phi=theta or not (subclause phi theta)) conjnctns))
+ (List.for_all (fun phi -> phi=theta or
+ not (subformula phi theta)) non_conjnctns)
+ & (List.for_all (fun phi -> phi=theta or
+ not (subclause phi theta)) conjnctns))
conjnctns) in
let unit_propagation phi =
(* beware that unit_propagation might introduce the subformula true,
- and hence should be followed by neutral_absorbing before starting the next fixed-point iteration *)
+ and hence should be followed by neutral_absorbing before
+ starting the next fixed-point iteration *)
match phi with
- BAnd phis ->
- let units = List.map (fun lit -> match lit with BVar v -> v | _ -> failwith ("not a literal!"))
- (List.filter is_literal phis) in
- let rec propagate units phi =
- match phi with
- BVar v -> if List.exists (fun unit -> v=unit) units then BAnd [] else phi
- | BNot psi -> BNot (propagate units psi)
- | BAnd psis -> BAnd (List.map (propagate units) psis)
- | BOr psis -> BOr (List.map (propagate units) psis) in
- BAnd ((List.map (fun v -> BVar v) units) @ (List.map (propagate units) phis))
+ | BAnd phis ->
+ let units = List.map
+ (function | BVar v -> v | _ -> failwith ("not a literal!"))
+ (List.filter is_literal phis) in
+ let rec propagate units phi =
+ match phi with
+ | BVar v ->
+ if List.exists (fun unit -> v=unit) units then BAnd [] else phi
+ | BNot psi -> BNot (propagate units psi)
+ | BAnd psis -> BAnd (List.map (propagate units) psis)
+ | BOr psis -> BOr (List.map (propagate units) psis) in
+ BAnd ((List.map (fun v -> BVar v) units) @
+ (List.map (propagate units) phis))
| _ -> phi in
let rec resolution phi =
match phi with
- BVar v -> phi
+ | BVar v -> phi
| BNot psi -> BNot (resolution psi)
| BOr psis ->
- let res_psis = List.map resolution psis in
- let neg_phi = to_nnf (BNot (BOr res_psis)) in
- let res_neg_phi = resolution neg_phi in
- to_nnf (BNot res_neg_phi)
+ let res_psis = List.map resolution psis in
+ let neg_phi = to_nnf (BNot (BOr res_psis)) in
+ let res_neg_phi = resolution neg_phi in
+ to_nnf (BNot res_neg_phi)
| BAnd psis ->
- let (clauses,non_clauses) = List.partition (fun psi -> is_disjunction psi or is_literal psi) psis in
- let resolvent cl1 cl2 =
- (* construct the resolvent of clauses cl1 and cl2 and tag it with the reserved literal 0 *)
- let rec split_clause (acc_lits, acc_rest) = function
- BVar v -> (v :: acc_lits, acc_rest)
- | BOr phis -> (match phis with
- [] -> (acc_lits, acc_rest)
- | psi :: psis -> if (is_literal psi)
- then split_clause ((int_of_lit psi)::acc_lits, acc_rest) (BOr psis)
- else split_clause (acc_lits, psi::acc_rest) (BOr psis)
- )
- | _ -> failwith ("this is not a clause feasible for resolution!") in
- let (cl1_lits,cl1_rest) = split_clause ([],[]) cl1 in
- let (cl2_lits,cl2_rest) = split_clause ([],[]) cl2 in
- let res_lits = (* obtain list of feasible pivot-literals *)
- List.filter (fun lit1 -> List.exists (fun lit2 -> lit2 = -lit1) cl2_lits) cl1_lits in
- if !debug_level > 3 then
- print_endline ("res_lits: " ^ String.concat ", " (List.map string_of_int res_lits));
- (* if there is more than one possible pivot-literal, the resulting clause will be
- equivalent to true, so we don't care *)
- if (List.length res_lits) <> 1 then BAnd []
- else (* construct a resolvent and mark it with the unused literal 0 *)
- let lit = List.nth res_lits 0 in (* construct the resolvent of cl1 and cl2 using pivot-literal lit *)
- BOr ((lit_of_int 0) :: (List.map lit_of_int (List.filter (fun lit1 -> lit1 <> lit) cl1_lits
- @ List.filter (fun lit2 -> lit2 <> -lit) cl2_lits))
- @ cl1_rest @ cl2_rest) in
- let res_clauses = ref [] in
- let subsumed = ref [] in
- (* Construct all possible resolvents, and check for each new resolvent whether it is
- subsumed by some existing clause.
- In fact, the following does not work: "If this is the case, we can remove the two initial
- clauses (i.e. add them to the list subsumed)."
+ let (clauses, non_clauses) = List.partition
+ (fun psi -> is_disjunction psi or is_literal psi) psis in
+ let resolvent cl1 cl2 =
+ (* construct the resolvent of clauses cl1 and cl2 and
+ tag it with the reserved literal 0 *)
+ let rec split_clause (acc_lits, acc_rest) = function
+ | BVar v -> (v :: acc_lits, acc_rest)
+ | BOr phis -> (match phis with
+ | [] -> (acc_lits, acc_rest)
+ | psi :: psis ->
+ if (is_literal psi) then
+ split_clause ((int_of_lit psi)::acc_lits, acc_rest)
+ (BOr psis)
+ else split_clause (acc_lits, psi::acc_rest) (BOr psis)
+ )
+ | _ -> failwith ("this is not a clause feasible for resolution!") in
+ let (cl1_lits,cl1_rest) = split_clause ([],[]) cl1 in
+ let (cl2_lits,cl2_rest) = split_clause ([],[]) cl2 in
+ let res_lits = (* obtain list of feasible pivot-literals *)
+ List.filter (fun lit1 ->
+ List.exists (fun lit2 -> lit2 = -lit1) cl2_lits) cl1_lits in
+ if !debug_level > 3 then
+ print_endline ("res_lits: " ^ String.concat ", "
+ (List.map string_of_int res_lits));
+ (* if there is more than one possible pivot-literal, the resulting
+ clause will be equivalent to true, so we don't care *)
+ if (List.length res_lits) <> 1 then BAnd []
+ else (* construct a resolvent and mark it with the unused literal 0 *)
+ let lit = List.nth res_lits 0 in
+ (* construct resolvent of cl1 and cl2 using pivot-literal lit *)
+ BOr ((lit_of_int 0) ::
+ (List.map lit_of_int
+ (List.filter (fun lit1 -> lit1 <> lit) cl1_lits
+ @ List.filter (fun lit2 -> lit2 <> -lit) cl2_lits))
+ @ cl1_rest @ cl2_rest) in
+ let res_clauses = ref [] in
+ let subsumed = ref [] in
+ (* Construct all possible resolvents and check each new resolvent
+ whether it is subsumed by some existing clause.
+ In fact, the following does not work: If this is the case we can
+ remove two initial clauses (ie add them to the list subsumed).
Instead, we discard the resolved but subsumed clause directly.
- *)
- List.iter (fun cl1 -> (List.iter
- (fun cl2 ->
- let cl_res = resolvent cl1 cl2 in
- let subclause a b = (* i.e. a \subseteq b *)
- match (a,b) with
- ((BVar v as lit), BOr thetas)
- | ((BVar v as lit), BAnd thetas) -> List.exists (fun y -> y=lit) thetas
- | (BOr psis, (BVar v as lit))
- | (BAnd psis, (BVar v as lit)) -> List.for_all (fun x -> x=lit) psis
- | (BOr psis, BOr thetas)
- | (BAnd psis, BAnd thetas) -> List.for_all (fun x -> List.exists
- (fun y -> y=x) thetas) psis
- | (_, _) -> false in
- if (List.exists (fun clause -> subclause clause cl_res) clauses)
- then (
- (* do nothing, since the resolvent is useless *)
- (*
- res_clauses := !res_clauses;
- subsumed := cl1 :: cl2 :: !subsumed;
- if !debug_level > 3 then (
- print_endline(" Subsumed clauses: " ^ str cl1 ^ " and " ^ str cl2);
- print_endline(" current resolvents: " ^ String.concat ", " (List.map str !res_clauses));
- print_endline(" current subsumed clauses: " ^ String.concat ", " (List.map str !subsumed))
- )*)
- )
- else
- res_clauses := cl_res :: !res_clauses;
- ) clauses)) clauses;
- if !debug_level > 2 then (
- print_endline("Resolvents: " ^ String.concat ", " (List.map str !res_clauses));
- print_endline("Subsumed clauses: " ^ String.concat ", " (List.map str !subsumed));
- print_endline("Reduced Resolvents: " ^ str (singularise (BAnd !res_clauses)));
- );
- let total = (List.filter (fun clause -> not (List.exists (fun sub -> clause=sub) !subsumed)) clauses)
- @ !res_clauses @ non_clauses in
- singularise (neutral_absorbing (BAnd total)) in
+ *)
+ List.iter (fun cl1 ->
+ (List.iter
+ (fun cl2 ->
+ let cl_res = resolvent cl1 cl2 in
+ let subclause a b = (* i.e. a \subseteq b *)
+ match (a,b) with
+ | ((BVar v as lit), BOr thetas)
+ | ((BVar v as lit), BAnd thetas) ->
+ List.exists (fun y -> y=lit) thetas
+ | (BOr psis, (BVar v as lit))
+ | (BAnd psis, (BVar v as lit)) ->
+ List.for_all (fun x -> x=lit) psis
+ | (BOr psis, BOr thetas)
+ | (BAnd psis, BAnd thetas) ->
+ List.for_all
+ (fun x -> List.exists (fun y -> y=x) thetas) psis
+ | (_, _) -> false in
+ if
+ (List.exists (fun clause -> subclause clause cl_res) clauses)
+ then ( (* do nothing, since the resolvent is useless *) ) else
+ res_clauses := cl_res :: !res_clauses;
+ ) clauses)) clauses;
+ if !debug_level > 2 then (
+ print_endline("Resolvents: " ^
+ String.concat ", " (List.map str !res_clauses));
+ print_endline("Subsumed clauses: " ^
+ String.concat ", " (List.map str !subsumed));
+ print_endline("Reduced Resolvents: " ^
+ str (singularise (BAnd !res_clauses)));
+ );
+ let total =
+ (List.filter
+ (fun clause ->
+ not (List.exists (fun sub -> clause=sub) !subsumed)) clauses)
+ @ !res_clauses @ non_clauses in
+ singularise (neutral_absorbing (BAnd total)) in
let choose_resolvents phi =
(* check the resolvents for "good" ones (at the moment these are clauses
that subsume clauses in the original formula) and discard the rest *)
let rec filter_by_subsumption = function
- BOr psis ->
- let filtered_psis = List.map filter_by_subsumption psis in
- let neg_phi = to_nnf (BNot (BOr filtered_psis)) in
- let filtered_neg_phi = filter_by_subsumption neg_phi in
- to_nnf (BNot filtered_neg_phi)
+ | BOr psis ->
+ let filtered_psis = List.map filter_by_subsumption psis in
+ let neg_phi = to_nnf (BNot (BOr filtered_psis)) in
+ let filtered_neg_phi = filter_by_subsumption neg_phi in
+ to_nnf (BNot filtered_neg_phi)
| BAnd psis ->
- let subclause a b = (* here, a is a resolvent, so we should not consider the literal 0! *)
- match (a,b) with
- ((BVar v as lit), BOr thetas)
- | ((BVar v as lit), BAnd thetas) -> List.exists (fun y -> y=lit) thetas
- | (BOr psis, (BVar v as lit))
- | (BAnd psis, (BVar v as lit)) -> List.for_all (fun x -> x=lit or x=(lit_of_int 0)) psis
- | (BOr psis, BOr thetas)
- | (BAnd psis, BAnd thetas) -> List.for_all (fun x -> x=(lit_of_int 0) or List.exists
- (fun y -> y=x) thetas) psis
- | (_, _) -> false in
- let (clauses,non_clauses) = List.partition (fun phi -> is_disjunction phi or is_literal phi) psis in
- let (resolvents,non_resolvents) = List.partition
- (fun clause ->
- (* actually these clauses do not necessarily contain only literals but maybe
- also more complex subformulas! *)
- let lits = (*print_endline("checking clause: " ^ str clause); *)
- match clause with
- BOr lits -> lits
- | BVar v as lit -> [lit]
- | _ -> failwith("[filter_by_subsumption] This is not a clause!") in
- (is_disjunction clause &&
+ let subclause a b =
+ (* here, a is a resolvent, so we should not consider the literal 0! *)
+ match (a,b) with
+ | ((BVar v as lit), BOr thetas)
+ | ((BVar v as lit), BAnd thetas) ->
+ List.exists (fun y -> y=lit) thetas
+ | (BOr psis, (BVar v as lit))
+ | (BAnd psis, (BVar v as lit)) ->
+ List.for_all (fun x -> x=lit or x=(lit_of_int 0)) psis
+ | (BOr psis, BOr thetas)
+ | (BAnd psis, BAnd thetas) ->
+ List.for_all
+ (fun x -> x=(lit_of_int 0) or List.exists (fun y-> y=x) thetas)
+ psis
+ | (_, _) -> false in
+ let (clauses, non_clauses) =
+ List.partition (fun phi -> is_disjunction phi or is_literal phi)
+ psis in
+ let (resolvents, non_resolvents) = List.partition
+ (fun clause ->
+ (* actually these clauses do not necessarily contain only
+ literals but maybe also more complex subformulas! *)
+ let lits = (*print_endline("checking clause: " ^ str clause); *)
+ match clause with
+ | BOr lits -> lits
+ | BVar v as lit -> [lit]
+ | _ ->
+ failwith("[filter_by_subsumption] This is not a clause!") in
+ (is_disjunction clause &&
List.exists (fun lit -> lit=(lit_of_int 0)) lits)) clauses in
- let useful_resolvents = List.filter
- (fun resolvent -> List.exists (fun phi -> subclause resolvent phi) non_resolvents) resolvents in
- if !debug_level > 2 then
- print_endline("Useful resolvents: " ^ String.concat ", " (List.map str useful_resolvents));
- let new_clauses = List.map (fun resolvent ->
- match resolvent with
- BOr lits -> BOr (List.filter (fun lit -> lit <> (lit_of_int 0)) lits)
- | _ -> failwith ("trying to remove literals from a non-clause!")
- ) useful_resolvents in
- BAnd (new_clauses @ non_resolvents @ (List.map filter_by_subsumption non_clauses))
+ let useful_resolvents = List.filter
+ (fun resolvent ->
+ List.exists (fun phi -> subclause resolvent phi) non_resolvents)
+ resolvents in
+ if !debug_level > 2 then
+ print_endline("Useful resolvents: " ^
+ String.concat ", " (List.map str useful_resolvents));
+ let new_clauses =
+ List.map (function
+ | BOr lits ->
+ BOr (List.filter (fun lit -> lit <> (lit_of_int 0)) lits)
+ | _ -> failwith ("trying to remove literals from a non-clause!")
+ ) useful_resolvents in
+ BAnd (new_clauses @ non_resolvents @
+ (List.map filter_by_subsumption non_clauses))
| BNot psi -> BNot (filter_by_subsumption psi)
- | BVar v as lit -> if (v=0) then failwith ("There should not be empty resolved clauses!") else lit in
- filter_by_subsumption phi
- in
+ | BVar v as lit ->
+ if v=0 then failwith "There should not be empty resolved clauses!" else
+ lit in
+ filter_by_subsumption phi in
let simplified =
let simp_resolution = fun phi ->
if ((!simplification lsr 2) land 1) > 0 then
@@ -450,27 +507,28 @@
else phi in
let simp_fun = fun phi ->
(simp_resolution
- (neutral_absorbing
- (unit_propagation
- (subsumption
- (singularise
- (neutral_absorbing
- (flatten
- (to_nnf phi)))))))) in
+ (neutral_absorbing
+ (unit_propagation
+ (subsumption
+ (singularise
+ (neutral_absorbing
+ (flatten
+ (to_nnf phi)))))))) in
let rec fp f x =
let y = f x in
- if y=x then x else fp f y in
- fp (fun phi -> (simp_fun phi)) phi in
- if !debug_level > 1 then
- print_endline ("Simplification:\nphi " ^ str phi ^ "\nwas simplified to " ^ str simplified);
- simplified
-
+ if y=x then x else fp f y in
+ fp (fun phi -> (simp_fun phi)) phi in
+ if !debug_level > 1 then
+ print_endline ("Simplification:\nphi " ^ str phi ^
+ "\nwas simplified to " ^ str simplified);
+ simplified
-(* Convert a reduced Boolean combination into a CNF with auxiliary variables (Tseitin) *)
+
+(* Convert reduced Boolean combination into CNF with aux variables (Tseitin) *)
let auxcnf_of_bool_formula phi =
let max_abs m lit = if lit < 0 then max m (-lit) else max m lit in
let rec get_max_lit m = function
- BVar v -> max_abs m v
+ | BVar v -> max_abs m v
| BNot phi -> get_max_lit m phi
| BAnd [] | BOr [] -> m
| BAnd (bflist) | BOr (bflist) -> List.fold_left get_max_lit m bflist in
@@ -478,14 +536,15 @@
let (clauses, free_idx) = (ref [], ref max_lit) in
let bv l = List.rev_map (fun i -> BVar i) l in
let rec index_formula = function
- BVar v -> v
+ | BVar v -> v
| BNot phi -> - (index_formula phi)
| BOr bflist ->
- let indlist = List.rev_map index_formula bflist in
- free_idx := !free_idx + 1;
- List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses) indlist;
- clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
- !free_idx
+ let indlist = List.rev_map index_formula bflist in
+ free_idx := !free_idx + 1;
+ List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses)
+ indlist;
+ clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
+ !free_idx
| _ -> failwith "auxcnf_to_bool_formula: converting non-reduced formula" in
let res_var = index_formula (to_reduced_form phi) in
(max_lit + 1, BAnd ((BOr [BVar (- res_var)]) :: !clauses))
@@ -496,7 +555,7 @@
let pg_auxcnf_of_bool_formula phi =
let max_abs m lit = if lit < 0 then max m (-lit) else max m lit in
let rec get_max_lit m = function
- BVar v -> max_abs m v
+ | BVar v -> max_abs m v
| BNot phi -> get_max_lit m phi
| BAnd [] | BOr [] -> m
| BAnd (bflist) | BOr (bflist) -> List.fold_left get_max_lit m bflist in
@@ -504,41 +563,46 @@
let (clauses, free_idx) = (ref [], ref max_lit) in
let bv l = List.rev_map (fun i -> BVar i) l in
let rec index_formula ?(neg=false) = function
- BVar v -> v
+ | BVar v -> v
| BNot phi -> - index_formula ~neg:(not neg) phi
| BOr bflist ->
- let indlist = List.rev_map (index_formula ~neg:neg) bflist in
- free_idx := !free_idx + 1;
- if neg then
- List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses) indlist
- else
- clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
- !free_idx
+ let indlist = List.rev_map (index_formula ~neg:neg) bflist in
+ free_idx := !free_idx + 1;
+ if neg then
+ List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses)
+ indlist
+ else
+ clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
+ !free_idx
| BAnd bflist ->
- let indlist = List.rev_map (index_formula ~neg:neg) bflist in
- free_idx := !free_idx + 1;
- if neg then
- clauses := BOr (bv (!free_idx :: (List.rev_map (fun i -> -i) indlist))) :: !clauses
- else
- List.iter (fun i -> clauses := (BOr (bv [i; (- !free_idx)])) :: !clauses) indlist;
- !free_idx in
+ let indlist = List.rev_map (index_formula ~neg:neg) bflist in
+ free_idx := !free_idx + 1;
+ if neg then
+ clauses :=
+ BOr (bv (!free_idx :: (List.rev_map (fun i -> -i) indlist))) ::
+ !clauses
+ else
+ List.iter
+ (fun i -> clauses := (BOr (bv [i; (- !free_idx)])) :: !clauses)
+ indlist;
+ !free_idx in
let res_var =
match phi with
- BNot psi -> - index_formula ~neg:false psi
+ | BNot psi -> - index_formula ~neg:false psi
| _ -> index_formula ~neg:true phi in
(max_lit + 1, BAnd ((BOr [BVar (- res_var)]) :: !clauses))
let listcnf_of_boolcnf phi =
let int_of_literal = function
- BVar v -> v
+ | BVar v -> v
| _ -> raise (FormulaError "Clauses must not contain non-literals!") in
let list_of_clause = function
- BVar v -> [v]
+ | BVar v -> [v]
| BOr (bflist) -> List.map int_of_literal bflist
| _ -> raise (FormulaError "This is not a clause!") in
match phi with
- BVar v -> [[v]]
+ | BVar v -> [[v]]
| BAnd (bflist) -> List.map list_of_clause bflist
| _ -> raise (FormulaError "This is not a CNF!")
@@ -550,16 +614,17 @@
let convert phi =
- (* input is a Boolean combination; output is a list of list of integers interpreted as a cnf *)
+ (* input is a Boolean combination; output is a list of list of integers
+ interpreted as a cnf *)
let (aux_separator, aux_cnf_formula) =
match !auxcnf_generation with
- 0 -> failwith ("this function must not be called without auxcnf-converion")
+ | 0 -> failwith "this function must not be called w/o auxcnf-converion"
| 1 -> (* use Tseitin conversion *)
- auxcnf_of_bool_formula (to_reduced_form (flatten_sort (to_nnf ~neg:false phi)))
+ auxcnf_of_bool_formula
+ (to_reduced_form (flatten_sort (to_nnf ~neg:false phi)))
| 2 -> (* or Plaisted-Greenbaum conversion *)
- pg_auxcnf_of_bool_formula (flatten_sort (to_nnf ~neg:false phi))
- | _ -> failwith ("undefined parameter value")
- in
+ pg_auxcnf_of_bool_formula (flatten_sort (to_nnf ~neg:false phi))
+ | _ -> failwith "undefined parameter value" in
if !debug_level > 0 then (
print_endline ("Separator is: " ^ string_of_int aux_separator);
print_endline ("Converting Aux-CNF: " ^ str aux_cnf_formula);
@@ -568,25 +633,31 @@
let cnf_llist = Sat.convert_aux_cnf aux_separator aux_cnf in
if !debug_level > 0 then
print_endline ("Converted CNF: " ^ (Sat.cnf_str cnf_llist));
- let simplified = if (!simplification land 1) > 0 then subsumption_filter cnf_llist else cnf_llist in
+ let simplified =
+ if (!simplification land 1) > 0 then
+ subsumption_filter cnf_llist
+ else cnf_llist in
if !debug_level > 1 then (
- if (!simplification land 1) > 0 then print_endline ("Subsumption turned on");
+ if (!simplification land 1) > 0 then
+ print_endline ("Subsumption turned on");
print_endline ("Simplified CNF: " ^ (Sat.cnf_str simplified))
);
- simplified
-
+ simplified
+
(* given a formula, convert to CNF. *)
let formula_to_cnf phi =
let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in
let boolean_phi = bool_formula_of_formula_arg phi (ids, rev_ids, free_id) in
let cnf_llist = convert boolean_phi in
- let bool_cnf = BAnd (List.map (fun literals -> BOr (List.map lit_of_int literals)) cnf_llist) in
- let simplified = if ((!simplification lsr 1) land 1) > 0 then simplify bool_cnf else bool_cnf in
- if !debug_level > 1 then (
- if ((!simplification lsr 1) land 1) > 0 then print_endline ("Simplification turned on");
-(* print_endline ("Simplified CNF: " ^ (Sat.cnf_str simplified))*)
- );
- let formula_cnf = formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
- formula_cnf
+ let bool_cnf =
+ BAnd (List.map (fun literals -> BOr (List.map lit_of_int literals))
+ cnf_llist) in
+ let simplified =
+ if ((!simplification lsr 1) land 1) > 0 then
+ simplify bool_cnf
+ else bool_cnf in
+ let formula_cnf =
+ formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
+ formula_cnf
Modified: trunk/Toss/Formula/Sat/Makefile
===================================================================
--- trunk/Toss/Formula/Sat/Makefile 2011-04-17 01:25:17 UTC (rev 1415)
+++ trunk/Toss/Formula/Sat/Makefile 2011-04-17 14:05:28 UTC (rev 1416)
@@ -1,26 +1,8 @@
MINISATDIR = minisat
-# mode is communicated by top-level make
-#MODE=debug
-
-ifeq ($(MODE),debug)
- # The option -dtypes emits types, e.g. for emacs editing in Tuareg mode
- OCAML = ocamlc -g
-
all: SatSolver.o MiniSATWrap.o
-#all: Sat.cma qbf
-else
- # The option -dtypes emits types, e.g. for emacs editing in Tuareg mode
- OCAML = ocamlopt -g
-all: SatSolver.o MiniSATWrap.o
-#all: Sat.cmxa qbf
-
-endif
-
-
-
SatSolver.o: $(MINISATDIR)/Solver.C
if [ ! -e minisat/SatSolver.o ]; then \
g++ -O2 -fPIC -c -I $(MINISATDIR) $(MINISATDIR)/Solver.C -o SatSolver.o; \
@@ -33,65 +15,18 @@
mv MiniSATWrap.o minisat/; \
fi
-MiniSAT.cmi: MiniSAT.mli
- $(OCAML) -c MiniSAT.mli
+%Test:
+ make -C ../.. Formula/Sat/$@
-MiniSAT.cmx: MiniSAT.ml MiniSAT.cmi
- $(OCAML) -c MiniSAT.ml
+qbf: qbf.ml
+ make -C ../.. Formula/Sat/qbf.native
+ cp ../../qbf.native qbf
-MiniSAT.cmo: MiniSAT.ml MiniSAT.cmi
- $(OCAML) -c MiniSAT.ml
+tests: SatTest
+ ./SatTest
-IntSet.cmi: IntSet.mli
- $(OCAML) -c IntSet.mli
-IntSet.cmx: IntSet.ml IntSet.cmi
- $(OCAML) -c IntSet.ml
-
-IntSet.cmo: IntSet.ml IntSet.cmi
- $(OCAML) -c IntSet.ml
-
-Sat.cmi: Sat.mli
- $(OCAML) -c Sat.mli
-
-Sat.cmx: Sat.ml Sat.cmi MiniSAT.cmi IntSet.cmi
- $(OCAML) -c Sat.ml
-
-Sat.cmxa: Sat.cmx SatSolver.o MiniSATWrap.o MiniSAT.cmx IntSet.cmx
- $(OCAML) -a -cclib -lstdc++ SatSolver.o MiniSATWrap.o MiniSAT.cmx \
- IntSet.cmx Sat.cmx -o Sat.cmxa
-
-Sat.cmo: Sat.ml Sat.cmi MiniSAT.cmi IntSet.cmi
- $(OCAML) -c Sat.ml
-
-Sat.cma: Sat.cmo SatSolver.o MiniSATWrap.o MiniSAT.cmo IntSet.cmo
- $(OCAML) -a -cclib -lstdc++ -custom SatSolver.o MiniSATWrap.o MiniSAT.cmo \
- IntSet.cmo Sat.cmo -o Sat.cma
-
-ifeq ($(MODE),debug)
-qbf: qbf.ml Sat.cma
- $(OCAML) str.cma Sat.cma qbf.ml -o qbf
-
-Test: Test.ml Sat.cma
- $(OCAML) Sat.cma Test.ml -o Test
-
-tests: Test
- ./Test
-
-else
-qbf: qbf.ml Sat.cmxa
- $(OCAML) str.cmxa Sat.cmxa qbf.ml -o qbf
-
-Test: Test.ml Sat.cmxa
- $(OCAML) Sat.cmxa Test.ml -o Test
-
-tests: Test
- ./Test
-
-endif
-
-
clean:
- rm -f *.o *.cmo *.cma *.cmi *~ *.cmxa *.cmx *.a *.annot Sat.cmxa Test qbf
- rm -f *.o *.cmo *.cmo *.cmi *~ *.cma *.cmo *.a *.annot Test_debug qbf
+ rm -f *.cma *.cmi *~ *.cmxa *.cmx *.a *.annot Sat.cmxa SatTest qbf
+ rm -f *.o *.cmo *.cmo *.cmi *~ *.cma *.cmo *.a *.annot qbf
rm -f minisat/SatSolver.o minisat/MiniSATWrap.o
Copied: trunk/Toss/Formula/Sat/SatTest.ml (from rev 1415, trunk/Toss/Formula/Sat/Test.ml)
===================================================================
--- trunk/Toss/Formula/Sat/SatTest.ml (rev 0)
+++ trunk/Toss/Formula/Sat/SatTest.ml 2011-04-17 14:05:28 UTC (rev 1416)
@@ -0,0 +1,215 @@
+(* Simple MiniSAT cnf-dnf tests. *)
+open OUnit
+
+Sat.set_debug_level 0 ;;
+
+let assert_eq_string arg msg x y =
+ let full_msg = msg ^ " (argument: " ^ arg ^ ")" in
+ assert_equal ~printer:(fun x -> x) ~msg:full_msg
+ ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
+
+let test phi res_cnf =
+ assert_eq_string (Sat.dnf_str phi) "DNF to CNF conversion"
+ res_cnf (Sat.cnf_str (Sat.convert phi))
+
+let test_nbr_clauses nbr phi =
+ assert_eq_string (Sat.dnf_str phi) "Number of clauses in converted CNF"
+ (string_of_int nbr) (string_of_int (List.length (Sat.convert phi)))
+
+let rec list n = if n < 3 then [n] else n :: list (n-1)
+
+let tests = "Sat" >::: [
+ "basic dnf to cnf" >::
+ (fun () ->
+ test [[1; 2]; [3]] "(2 | 3) & (1 | 3)";
+ test [[1; 2]; [-1; -2]] "(-1 | 2) & (1 | -2)";
+ test [[1; 2; 3]] "(2) & (1) & (3)";
+ test [[1; -1]] "F";
+ test [[1]; [-1; 2]; [-2; 3]; [-3]] "T";
+ test [[1]; [-1; 2]; [-2; 3]; [-3; 4]] "(1 | 2 | 3 | 4)";
+ test [[1; 2]; [3; 4]] "(2 | 3) & (2 | 4) & (1 | 3) & (1 | 4)";
+ );
+
+ "conversion to cnf on larger classes" >::
+ (fun () ->
+ test_nbr_clauses 128
+ [[7]; [8]; [1; 2]; [3; 4]; [5; 6]; [9; 10]; [11;12]; [13;14]; [15;16]];
+
+ test_nbr_clauses 799 [[1]; list 800];
+
+ (* Nice multiply-out tests. *)
+ let p n = [-1 :: (list n); [1; -(n+1)]; [1; -(n+2)]; [-1;n+1; n+2]] in
+ test_nbr_clauses 59 (p 30);
+
+ let q n = [-1 :: (List.map (fun i -> (-i)) (list n));
+ [1; -(n+1)]; [1; -(n+2)]; [-1; n+1; n+2]] in
+ test_nbr_clauses 59 (q 30);
+ );
+
+ "examples from tnf calculations" >::
+ (fun () ->
+ (* A more complex example; all literals positive. *)
+ let t = [[1]; [33]; [2; 3]; [4; 5; 6; 7; 8; 9]; [10; 5; 6; 8; 9];
+ [11; 5; 6; 12; 8; 9]; [13; 5; 6; 12; 8]; [14; 5; 12; 7; 8];
+ [15; 5; 12; 8]; [16; 5; 6; 12; 8; 17]; [18; 5; 12; 8; 17];
+ [19; 5; 6; 12; 8]; [20; 5; 12; 8]; [21; 5; 6; 7; 8];
+ [22; 5; 6; 7]; [23; 5; 6; 12; 7; 8; 17];
+ [24; 5; 6; 12; 8; 17]; [25; 5; 6; 8; 9]; [26; 5; 6; 8];
+ [27; 5; 12; 7; 8; 9]; [21; 5; 12; 7; 8]; [22; 5; 7]; [28; 5];
+ [29; 5; 8; 9]; [28; 5; 9]; [15; 6; 12; 7; 8]; [30; 6; 7; 8];
+ [31; 6; 12; 9]; [32; 6; 9]; [30; 6; 8]; [34; 6; 12; 7; 8];
+ [35; 6; 12; 7]; [36; 6; 7; 8]; [37; 6; 8]; [38; 6; 7; 9];
+ [39; 6; 9]; [40; 12; 7; 8; 17]; [41; 12; 8; 17];
+ [42; 7; 8; 17]; [43; 7; 17]; [44; 5; 6; 12; 7; 8; 9];
+ [4; 5; 12; 7; 8; 9]; [45; 5; 6; 12; 7; 8; 17];
+ [46; 5; 12; 7; 8; 17]; [36; 5; 6; 12; 7; 8];
+ [47; 5; 12; 7; 8]; [48; 5; 6; 12; 8; 17]; [42; 5; 12; 8; 17];
+ [49; 5; 6; 8; 9; 17]; [50; 5; 8; 9; 17];
+ [51; 5; 6; 12; 8; 9]; [15; 5; 6; 12; 8]; [36; 5; 6; 7; 8; 17];
+ [47; 5; 7; 8; 17]; [37; 5; 6; 8; 17]; [30; 5; 8; 17];
+ [52; 5; 6; 7; 17]; [53; 5; 6; 17]; [38; 5; 6; 7; 17];
+ [54; 5; 7; 17]; [55; 5; 6; 8; 9; 17]; [10; 5; 8; 9; 17];
+ [48; 5; 6; 8; 9; 17]; [42; 5; 8; 9; 17];
+ [56; 5; 6; 12; 7; 8; 9]; [57; 5; 6; 12; 7; 8];
+ [58; 5; 6; 12; 9]; [59; 5; 6; 12]; [44; 5; 6; 7; 8; 9];
+ [55; 5; 6; 8; 9]; [60; 5; 12; 7; 8; 9]; [51; 5; 12; 8; 9];
+ [46; 5; 7; 8; 17]; [42; 5; 8; 17]; [61; 5; 7; 17];
+ [43; 5; 17]; [30; 5; 8]; [4; 5; 7; 8; 9]; [62; 5; 7; 9];
+ [47; 5; 7; 8]; [54; 5; 7]; [63; 5; 6; 12; 8; 9; 17];
+ [64; 5; 12; 8; 9; 17]; [65; 5; 6; 12; 7; 8];
+ [66; 5; 12; 7; 8]; [25; 5; 6; 7; 8; 9]; [26; 5; 6; 7; 8];
+ [27; 5; 6; 7; 8; 9]; [67; 5; 6; 7; 9]; [68; 5; 6; 8; 9];
+ [29; 5; 6; 8]; [65; 5; 6; 12; 7; 8; 17];
+ [19; 5; 6; 12; 8; 17]; [69; 5; 6; 7; 8; 9; 17];
+ [70; 5; 6; 7; 9; 17]; [71; 5; 6; 7; 8; 17]; [72; 5; 6; 7; 17];
+ [73; 5; 6; 7; 8]; [57; 5; 6; 7]; [74; 5; 7; 17]; [75; 5; 17];
+ [68; 5; 8; 9]; [76; 5; 9]; [77; 6; 12; 7; 9]; [62; 6; 7; 9];
+ [14; 6; 12; 7; 8]; [47; 6; 7; 8]; [78; 6; 12; 7; 8; 9];
+ [11; 6; 12; 8; 9]; [79; 6; 7; 8; 9; 17]; [80; 6; 8; 9; 17];
+ [54; 6; 7; 9]; [81; 6; 12; 7; 9; 17]; [79; 6; 7; 9; 17];
+ [36; 6; 12; 7; 8]; [38; 6; 12; 7]; [82; 6; 12; 9; 17];
+ [80; 6; 9; 17]; [83; 6; 12; 9]; [84; 6; 9]; [38; 6; 7];
+ [47; 12; 7; 8]; [30; 12; 8]; [54; 12; 7]; [46; 12; 7; 8; 17];
+ [42; 12; 8; 17]; [14; 12; 7; 8; 17]; [15; 12; 8; 17];
+ [62; 12; 7; 9]; [32; 12; 9]; [60; 12; 7; 8; 9];
+ [77; 12; 7; 9]; [51; 12; 8; 9]; [31; 12; 9]; [46; 7; 8; 17];
+ [61; 7; 17]; [10; 8; 9]; [30; 8]; [85; 9; 17]; [43; 17];
+ [32; 9]; [63; 5; 6; 12; 7; 8; 9; 17];
+ [64; 5; 12; 7; 8; 9; 17]; [16; 5; 6; 12; 7; 8; 17];
+ [18; 5; 12; 7; 8; 17]; [34; 5; 6; 12; 7; 8];
+ [86; 5; 6; 7; 9]; [84; 5; 6; 9]; [39; 5; 6; 17];
+ [45; 5; 6; 7; 8; 17]; [48; 5; 6; 8; 17];
+ [70; 5; 6; 12; 7; 9; 17]; [72; 5; 6; 12; 7; 17];
+ [70; 5; 6; 12; 7; 8; 9; 17]; [72; 5; 6; 12; 7; 8; 17];
+ [87; 5; 6; 12; 9; 17]; [88; 5; 6; 12; 17]; [89; 5; 6; 12; 9];
+ [90; 5; 6; 12]; [91; 5; 6; 12; 7; 9; 17];
+ [92; 5; 6; 12; 7; 17]; [93; 5; 12; 7; 8]; [94; 5; 12; 8];
+ [10; 5; 8; 9]; [32; 5; 9]; [71; 5; 6; 12; 7; 8; 17];
+ [95; 5; 12; 7; 8; 17]; [96; 5; 6; 12; 7; 8; 9];
+ [73; 5; 6; 12; 7; 8]; [97; 5; 12; 7; 8; 9];
+ [98; 5; 6; 12; 8; 9]; [99; 5; 12; 8; 9];
+ [100; 5; 12; 7; 8; 17]; [101; 5; 12; 8; 17];
+ [102; 5; 6; 7; 8; 9; 17]; [103; 5; 6; 7; 9; 17];
+ [95; 5; 6; 7; 8; 17]; [74; 5; 6; 7; 17]; [96; 5; 6; 7; 8; 9];
+ [56; 5; 6; 7; 9]; [95; 5; 7; 8; 17]; [18; 5; 8; 17];
+ [21; 5; 7; 8]; [29; 5; 8]; [38; 6; 7; 8; 9]; [39; 6; 8; 9];
+ [44; 6; 12; 7; 8; 9]; [55; 6; 12; 8; 9];
+ [104; 6; 12; 7; 8; 9; 17]; [105; 6; 12; 8; 9; 17];
+ [40; 6; 12; 7; 8; 17]; [46; 6; 7; 8; 17]; [35; 6; 12; 7; 9];
+ [106; 6; 12; 9]; [107; 6; 12; 7; 9; 17]; [108; 6; 7; 9; 17];
+ [109; 6; 12; 9; 17]; [85; 6; 9; 17]; [41; 6; 12; 8; 17];
+ [42; 6; 8; 17]; [110; 6; 12; 17]; [43; 6; 17]; [15; 6; 12; 8];
+ [111; 6; 12]; [112; 6; 12; 7; 8; 9]; [83; 6; 12; 8; 9];
+ [113; 6; 12; 7; 8; 9; 17]; [114; 6; 12; 8; 9; 17];
+ [86; 6; 7; 8; 9]; [84; 6; 8; 9]; [44; 6; 7; 8; 9];
+ [55; 6; 8; 9]; [13; 6; 12; 8]; [106; 6; 12]; [39; 6];
+ [112; 6; 12; 7; 9]; [86; 6; 7; 9]; [4; 12; 7; 8; 9];
+ [10; 12; 8; 9]; [14; 12; 7; 8]; [15; 12; 8]; [115; 12; 7];
+ [111; 12]; [116; 7; 8; 9; 17]; [108; 7; 9; 17]; [50; 8; 9; 17];
+ [42; 8; 17]; [117; 5; 6; 12; 7; 9]; [118; 5; 6; 12; 9];
+ [69; 5; 6; 12; 7; 8; 9; 17]; [102; 5; 12; 7; 8; 9; 17];
+ [104; 5; 6; 12; 7; 8; 17]; [40; 5; 12; 7; 8; 17];
+ [105; 5; 6; 12; 8; 17]; [41; 5; 12; 8; 17];
+ [119; 5; 6; 12; 7; 8; 9]; [36; 5; 6; 7; 8]; [37; 5; 6; 8];
+ [38; 5; 6; 7]; [39; 5; 6]; [79; 5; 6; 7; 9; 17];
+ [108; 5; 7; 9; 17]; [80; 5; 6; 9; 17]; [85; 5; 9; 17];
+ [120; 5; 6; 12; 8; 9; 17]; [121; 5; 6; 12; 8; 17];
+ [56; 5; 6; 12; 7; 9]; [57; 5; 6; 12; 7];
+ [120; 5; 6; 12; 9; 17]; [121; 5; 6; 12; 17];
+ [122; 5; 6; 12; 7; 9]; [123; 5; 6; 12; 7]; [93; 5; 12; 7];
+ [94; 5; 12]; [87; 5; 6; 9; 17]; [88; 5; 6; 17];
+ [63; 5; 6; 8; 9; 17]; [16; 5; 6; 8; 17];
+ [102; 5; 7; 8; 9; 17]; [64; 5; 8; 9; 17]; [103; 5; 7; 9; 17];
+ [124; 5; 9; 17]; [27; 5; 7; 8; 9]; [67; 5; 7; 9];
+ [125; 6; 12; 7; 8; 9; 17]; [49; 6; 12; 8; 9; 17];
+ [115; 6; 12; 7]; [54; 6; 7]; [34; 6; 12; 7; 8; 9];
+ [13; 6; 12; 8; 9]; [126; 6; 12; 7; 9; 17]; [127; 6; 12; 9; 17];
+ [81; 6; 12; 7; 8; 9; 17]; [82; 6; 12; 8; 9; 17];
+ [125; 6; 7; 8; 9; 17]; [49; 6; 8; 9; 17];
+ [104; 6; 12; 7; 8; 17]; [45; 6; 7; 8; 17]; [105; 6; 12; 8; 17];
+ [48; 6; 8; 17]; [127; 6; 12; 17]; [53; 6; 17];
+ [107; 12; 7; 9; 17]; [109; 12; 9; 17]; [128; 12; 7; 8; 9; 17];
+ [129; 12; 8; 9; 17]; [4; 7; 8; 9]; [62; 7; 9]; [47; 7; 8];
+ [54; 7]; [93; 5; 6; 12; 7]; [94; 5; 6; 12];
+ [25; 5; 6; 12; 8; 9]; [68; 5; 12; 8; 9]; [26; 5; 6; 12; 8];
+ [29; 5; 12; 8]; [130; 5; 6; 12; 7; 8; 9; 17];
+ [131; 5; 12; 7; 8; 9; 17]; [132; 5; 6; 12; 8; 9; 17];
+ [133; 5; 12; 8; 9; 17]; [125; 5; 6; 7; 8; 9; 17];
+ [116; 5; 7; 8; 9; 17]; [89; 5; 6; 12; 8; 9];
+ [90; 5; 6; 12; 8]; [117; 5; 12; 7; 9]; [118; 5; 12; 9];
+ [58; 5; 6; 9]; [59; 5; 6]; [53; 6; 9; 17]; [126; 6; 12; 7; 17];
+ [134; 12; 7; 17]; [110; 12; 17]; [135; 5; 12; 7; 17];
+ [136; 5; 12; 17]; [52; 6; 7; 17]; [137; 5; 12; 7; 9; 17];
+ [138; 5; 12; 9; 17] ] in
+ test_nbr_clauses 256 t;
+
+ (* Example from SL6 conversion *)
+ let s =
+ [[2; -1]; [-3];
+ [2; -1]; [-7; -6; -5; -4]; [-11; -10; -9; -4; -8]; [-12; -10; -9; -8];
+ [-13; -6; -5]; [-15; -6; -14; -5; -9; -4; -8]; [-16; -10; -8];
+ [-17; -14; -10; -8]; [-18; -10; -4; -8]; [-19; -14; -5; -9; -4; -8];
+ [-20; -14; -10; -5]; [-21; -6; -14; -10; -5;-8]; [-22;-6;-5;-9;-4;-8];
+ [-23; -6; -4]; [-24; -6; -14; -5; -4]; [-25; -14; -10; -9; -8];
+ [-26; -14; -5; -9; -8]; [-27; -10; -9; -4]; [-28; -6; -10; -4];
+ [-29; -6; -5; -9; -8]; [-30; -6; -14; -5; -9; -8]; [-31;-6;-5;-9;-4];
+ [-32; -10; -4]; [-33; -14; -10]; [-34;-6;-14;-9;-8]; [-35;-10;-5;-8];
+ [-36; -10; -5; -4]; [-37; -14; -10; -9; -4]; [-38; -5; -9; -4];
+ [-39; -6; -14; -5; -9]; [-40; -6; -14; -5]; [-41; -10; -5; -4; -8];
+ [-42; -6; -14; -5; -8]; [-43; -6; -14; -5;-4;-8]; [-44;-14;-9;-4;-8];
+ [-45; -6; -14; -10; -5; -4]; [-46; -6; -10; -9; -8]; [-47; -4];
+ [-48; -6; -9; -4]; [-49; -6; -10; -9; -4; -8]; [-50; -6; -9; -4; -8];
+ [-51; -6; -10; -5; -4]; [-52; -6; -10; -5; -8]; [-53; -14; -5; -9; -4];
+ [-54; -14; -5; -9]; [-55; -14; -5]; [-56; -14; -10; -5; -9; -8];
+ [-57; -6; -10; -5; -9; -8]; [-58;-14;-10;-9;-4;-8]; [-59;-6;-14;-4];
+ [-60; -6; -5; -8]; [-61; -14; -9; -8]; [-62;-14;-9;-4]; [-63;-9;-4];
+ [-64; -6; -5; -9]; [-65; -6; -4; -8]; [-66; -6; -10; -5; -4; -8];
+ [-67; -6; -14; -9]; [-68; -14; -9]; [-69; -14]; [-70;-6;-10;-9;-4];
+ [-71;-14;-5;-4]; [-72;-14;-10;-5;-8]; [-73;-6;-10;-5]; [-74;-6;-10];
+ [-75; -6; -5; -4; -8]; [-76;-5;-4;-8]; [-77;-5;-4]; [-78;-6;-10;-9];
+ [-79; -10; -9]; [-80; -10; -5]; [-81; -6; -10; -5; -9; -4; -8];
+ [-82; -14; -10; -4]; [-83; -14; -10; -5; -4; -8]; [-84; -6; -10; -8];
+ [-85; -6; -9; -8]; [-86; -6; -9]; [-87; -14; -4]; [-88;-14;-5;-4;-8];
+ [-89; -14; -4; -8]; [-90; -14; -5; -8]; [-91; -14; -10; -9];
+ [-92; -6; -14; -10; -9; -8]; [-93; -6; -14; -9; -4; -8]; [-94; -9];
+ [-95; -9; -8]; [-96; -5]; [-97;-14;-10;-5;-4]; [-98;-14;-10;-5;-9;-4];
+ [-99; -14; -8]; [-100; -6; -10; -5; -9; -4]; [-101; -6; -10; -5; -9];
+ [-102; -14; -10; -5; -9]; [-103; -10; -5; -9; -4]; [-104; -10; -5; -9];
+ [-105; -6; -14; -8]; [-106; -14; -10; -4; -8]; [-107;-6;-14;-10;-8];
+ [-108; -6; -14; -4; -8]; [-109;-6;-10;-4;-8]; [-110;-6;-14;-10;-4;-8];
+ [-111; -10; -5; -9; -8]; [-112; -5; -9]; [-113; -5; -9; -8];
+ [-114; -6; -14; -9; -4]; [-115;-6;-14;-10;-4]; [-116;-6;-14;-10;-9;-4];
+ [-117; -6; -14; -10; -9]; [-118; -6; -8]; [-119; -10]; [-120; -5; -8];
+ [-121; -6; -14; -5; -9; -4]; [-122; -6; -14; -10; -9; -4; -8];
+ [-123; -6; -14; -10; -5; -4; -8]; [-124; -6; -14; -10; -5; -9; -8];
+ [-125; -14; -10; -5; -9; -4; -8]; [-126; -10; -5; -9; -4; -8];
+ [-127; -5; -9; -4; -8]; [-128; -9; -4; -8]; [-129; -4; -8]; [-130;-8];
+ [-131]; [-132; -6]; [-133; -6; -14]; [-134; -6; -14; -10];
+ [-135; -6; -14; -10; -5]; [-136; -6; -14; -10; -5; -9];
+ [-137;-6;-14;-10;-5;-9;-4]; [-138;-6;-14;-10;-5;-9;-4;-8]; [-139] ] in
+ test_nbr_clauses 277 s;
+ );
+]
+
+
+let exec = Aux.run_test_if_target "SatTest" tests
Deleted: trunk/Toss/Formula/Sat/Test.ml
===================================================================
--- trunk/Toss/Formula/Sat/Test.ml 2011-04-17 01:25:17 UTC (rev 1415)
+++ trunk/Toss/Formula/Sat/Test.ml 2011-04-17 14:05:28 UTC (rev 1416)
@@ -1,203 +0,0 @@
-(* Simple MiniSAT cnf-dnf tests. *)
-
-let test phi =
- print_endline ("DNF: " ^ Sat.dnf_str phi);
- print_endline ("CNF: " ^ Sat.cnf_str (Sat.convert phi));
- print_endline ""
-;;
-
-Sat.set_debug_level 0 ;;
-
-test [[1; 2]; [3]];;
-
-test [[1; 2]; [-1; -2]];;
-
-test [[1; 2; 3]];;
-
-test [[1; -1]];;
-
-test [[1]; [-1; 2]; [-2; 3]; [-3]];;
-
-test [[1]; [-1; 2]; [-2; 3]; [-3; 4]];;
-
-test [[1; 2]; [3; 4]];;
-
-test [[7]; [8]; [1; 2]; [3; 4]; [5; 6]; [9; 10]; [11; 12]; [13; 14]; [15;16]];;
-
-let rec list n = if n < 3 then [n] else n :: list (n-1) ;;
-
-(* Nice multiply-out test. *)
-let p n = test [-1 :: (list n); [1; -(n+1)]; [1; -(n+2)]; [-1; n+1; n+2]] ;;
-p 30 ;;
-
-let q n = test [-1 :: (List.map (fun i -> (-i)) (list n));
- [1; -(n+1)]; [1; -(n+2)]; [-1; n+1; n+2]] ;;
-q 30 ;;
-
-test [[1]; list 800];;
-
-
-(* A more complex example from TNF calculations; all literals positive. *)
-let t () = test [[1]; [33]; [2; 3]; [4; 5; 6; 7; 8; 9]; [10; 5; 6; 8; 9];
- [11; 5; 6; 12; 8; 9]; [13; 5; 6; 12; 8]; [14; 5; 12; 7; 8];
- [15; 5; 12; 8]; [16; 5; 6; 12; 8; 17]; [18; 5; 12; 8; 17];
- [19; 5; 6; 12; 8]; [20; 5; 12; 8]; [21; 5; 6; 7; 8];
- [22; 5; 6; 7]; [23; 5; 6; 12; 7; 8; 17];
- [24; 5; 6; 12; 8; 17]; [25; 5; 6; 8; 9]; [26; 5; 6; 8];
- [27; 5; 12; 7; 8; 9]; [21; 5; 12; 7; 8]; [22; 5; 7]; [28; 5];
- [29; 5; 8; 9]; [28; 5; 9]; [15; 6; 12; 7; 8]; [30; 6; 7; 8];
- [31; 6; 12; 9]; [32; 6; 9]; [30; 6; 8]; [34; 6; 12; 7; 8];
- [35; 6; 12; 7]; [36; 6; 7; 8]; [37; 6; 8]; [38; 6; 7; 9];
- [39; 6; 9]; [40; 12; 7; 8; 17]; [41; 12; 8; 17];
- [42; 7; 8; 17]; [43; 7; 17]; [44; 5; 6; 12; 7; 8; 9];
- [4; 5; 12; 7; 8; 9]; [45; 5; 6; 12; 7; 8; 17];
- [46; 5; 12; 7; 8; 17]; [36; 5; 6; 12; 7; 8];
- [47; 5; 12; 7; 8]; [48; 5; 6; 12; 8; 17]; [42; 5; 12; 8; 17];
- [49; 5; 6; 8; 9; 17]; [50; 5; 8; 9; 17];
- [51; 5; 6; 12; 8; 9]; [15; 5; 6; 12; 8]; [36; 5; 6; 7; 8; 17];
- [47; 5; 7; 8; 17]; [37; 5; 6; 8; 17]; [30; 5; 8; 17];
- [52; 5; 6; 7; 17]; [53; 5; 6; 17]; [38; 5; 6; 7; 17];
- [54; 5; 7; 17]; [55; 5; 6; 8; 9; 17]; [10; 5; 8; 9; 17];
- [48; 5; 6; 8; 9; 17]; [42; 5; 8; 9; 17];
- [56; 5; 6; 12; 7; 8; 9]; [57; 5; 6; 12; 7; 8];
- [58; 5; 6; 12; 9]; [59; 5; 6; 12]; [44; 5; 6; 7; 8; 9];
- [55; 5; 6; 8; 9]; [60; 5; 12; 7; 8; 9]; [51; 5; 12; 8; 9];
- [46; 5; 7; 8; 17]; [42; 5; 8; 17]; [61; 5; 7; 17];
- [43; 5; 17]; [30; 5; 8]; [4; 5; 7; 8; 9]; [62; 5; 7; 9];
- [47; 5; 7; 8]; [54; 5; 7]; [63; 5; 6; 12; 8; 9; 17];
- [64; 5; 12; 8; 9; 17]; [65; 5; 6; 12; 7; 8];
- [66; 5; 12; 7; 8]; [25; 5; 6; 7; 8; 9]; [26; 5; 6; 7; 8];
- [27; 5; 6; 7; 8; 9]; [67; 5; 6; 7; 9]; [68; 5; 6; 8; 9];
- [29; 5; 6; 8]; [65; 5; 6; 12; 7; 8; 17];
- [19; 5; 6; 12; 8; 17]; [69; 5; 6; 7; 8; 9; 17];
- [70; 5; 6; 7; 9; 17]; [71; 5; 6; 7; 8; 17]; [72; 5; 6; 7; 17];
- [73; 5; 6; 7; 8]; [57; 5; 6; 7]; [74; 5; 7; 17]; [75; 5; 17];
- [68; 5; 8; 9]; [76; 5; 9]; [77; 6; 12; 7; 9]; [62; 6; 7; 9];
- [14; 6; 12; 7; 8]; [47; 6; 7; 8]; [78; 6; 12; 7; 8; 9];
- [11; 6; 12; 8; 9]; [79; 6; 7; 8; 9; 17]; [80; 6; 8; 9; 17];
- [54; 6; 7; 9]; [81; 6; 12; 7; 9; 17]; [79; 6; 7; 9; 17];
- [36; 6; 12; 7; 8]; [38; 6; 12; 7]; [82; 6; 12; 9; 17];
- [80; 6; 9; 17]; [83; 6; 12; 9]; [84; 6; 9]; [38; 6; 7];
- [47; 12; 7; 8]; [30; 12; 8]; [54; 12; 7]; [46; 12; 7; 8; 17];
- [42; 12; 8; 17]; [14; 12; 7; 8; 17]; [15; 12; 8; 17];
- [62; 12; 7; 9]; [32; 12; 9]; [60; 12; 7; 8; 9];
- [77; 12; 7; 9]; [51; 12; 8; 9]; [31; 12; 9]; [46; 7; 8; 17];
- [61; 7; 17]; [10; 8; 9]; [30; 8]; [85; 9; 17]; [43; 17];
- [32; 9]; [63; 5; 6; 12; 7; 8; 9; 17];
- [64; 5; 12; 7; 8; 9; 17]; [16; 5; 6; 12; 7; 8; 17];
- [18; 5; 12; 7; 8; 17]; [34; 5; 6; 12; 7; 8];
- [86; 5; 6; 7; 9]; [84; 5; 6; 9]; [39; 5; 6; 17];
- [45; 5; 6; 7; 8; 17]; [48; 5; 6; 8; 17];
- [70; 5; 6; 12; 7; 9; 17]; [72; 5; 6; 12; 7; 17];
- [70; 5; 6; 12; 7; 8; 9; 17]; [72; 5; 6; 12; 7; 8; 17];
- [87; 5; 6; 12; 9; 17]; [88; 5; 6; 12; 17]; [89; 5; 6; 12; 9];
- [90; 5; 6; 12]; [91; 5; 6; 12; 7; 9; 17];
- [92; 5; 6; 12; 7; 17]; [93; 5; 12; 7; 8]; [94; 5; 12; 8];
- [10; 5; 8; 9]; [32; 5; 9]; [71; 5; 6; 12; 7; 8; 17];
- [95; 5; 12; 7; 8; 17]; [96; 5; 6; 12; 7; 8; 9];
- [73; 5; 6; 12; 7; 8]; [97; 5; 12; 7; 8; 9];
- [98; 5; 6; 12; 8; 9]; [99; 5; 12; 8; 9];
- [100; 5; 12; 7; 8; 17]; [101; 5; 12; 8; 17];
- [102; 5; 6; 7; 8; 9; 17]; [103; 5; 6; 7; 9; 17];
- [95; 5; 6; 7; 8; 17]; [74; 5; 6; 7; 17]; [96; 5; 6; 7; 8; 9];
- [56; 5; 6; 7; 9]; [95; 5; 7; 8; 17]; [18; 5; 8; 17];
- [21; 5; 7; 8]; [29; 5; 8]; [38; 6; 7; 8; 9]; [39; 6; 8; 9];
- [44; 6; 12; 7; 8; 9]; [55; 6; 12; 8; 9];
- [104; 6; 12; 7; 8; 9; 17]; [105; 6; 12; 8; 9; 17];
- [40; 6; 12; 7; 8; 17]; [46; 6; 7; 8; 17]; [35; 6; 12; 7; 9];
- [106; 6; 12; 9]; [107; 6; 12; 7; 9; 17]; [108; 6; 7; 9; 17];
- [109; 6; 12; 9; 17]; [85; 6; 9; 17]; [41; 6; 12; 8; 17];
- [42; 6; 8; 17]; [110; 6; 12; 17]; [43; 6; 17]; [15; 6; 12; 8];
- [111; 6; 12]; [112; 6; 12; 7; 8; 9]; [83; 6; 12; 8; 9];
- [113; 6; 12; 7; 8; 9; 17]; [114; 6; 12; 8; 9; 17];
- [86; 6; 7; 8; 9]; [84; 6; 8; 9]; [44; 6; 7; 8; 9];
- [55; 6; 8; 9]; [13; 6; 12; 8]; [106; 6; 12]; [39; 6];
- [112; 6; 12; 7; 9]; [86; 6; 7; 9]; [4; 12; 7; 8; 9];
- [10; 12; 8; 9]; [14; 12; 7; 8]; [15; 12; 8]; [115; 12; 7];
- [111; 12]; [116; 7; 8; 9; 17]; [108; 7; 9; 17]; [50; 8; 9; 17];
- [42; 8; 17]; [117; 5; 6; 12; 7; 9]; [118; 5; 6; 12; 9];
- [69; 5; 6; 12; 7; 8; 9; 17]; [102; 5; 12; 7; 8; 9; 17];
- [104; 5; 6; 12; 7; 8; 17]; [40; 5; 12; 7; 8; 17];
- [105; 5; 6; 12; 8; 17]; [41; 5; 12; 8; 17];
- [119; 5; 6; 12; 7; 8; 9]; [36; 5; 6; 7; 8]; [37; 5; 6; 8];
- [38; 5; 6; 7]; [39; 5; 6]; [79; 5; 6; 7; 9; 17];
- [108; 5; 7; 9; 17]; [80; 5; 6; 9; 17]; [85; 5; 9; 17];
- [120; 5; 6; 12; 8; 9; 17]; [121; 5; 6; 12; 8; 17];
- [56; 5; 6; 12; 7; 9]; [57; 5; 6; 12; 7];
- [120; 5; 6; 12; 9; 17]; [121; 5; 6; 12; 17];
- [122; 5; 6; 12; 7; 9]; [123; 5; 6; 12; 7]; [93; 5; 12; 7];
- [94; 5; 12]; [87; 5; 6; 9; 17]; [88; 5; 6; 17];
- [63; 5; 6; 8; 9; 17]; [16; 5; 6; 8; 17];
- [102; 5; 7; 8; 9; 17]; [64; 5; 8; 9; 17]; [103; 5; 7; 9; 17];
- [124; 5; 9; 17]; [27; 5; 7; 8; 9]; [67; 5; 7; 9];
- [125; 6; 12; 7; 8; 9; 17]; [49; 6; 12; 8; 9; 17];
- [115; 6; 12; 7]; [54; 6; 7]; [34; 6; 12; 7; 8; 9];
- [13; 6; 12; 8; 9]; [126; 6; 12; 7; 9; 17]; [127; 6; 12; 9; 17];
- [81; 6; 12; 7; 8; 9; 17]; [82; 6; 12; 8; 9; 17];
- [125; 6; 7; 8; 9; 17]; [49; 6; 8; 9; 17];
- [104; 6; 12; 7; 8; 17]; [45; 6; 7; 8; 17]; [105; 6; 12; 8; 17];
- [48; 6; 8; 17]; [127; 6; 12; 17]; [53; 6; 17];
- [107; 12; 7; 9; 17]; [109; 12; 9; 17]; [128; 12; 7; 8; 9; 17];
- [129; 12; 8; 9; 17]; [4; 7; 8; 9]; [62; 7; 9]; [47; 7; 8];
- [54; 7]; [93; 5; 6; 12; 7]; [94; 5; 6; 12];
- [25; 5; 6; 12; 8; 9]; [68; 5; 12; 8; 9]; [26; 5; 6; 12; 8];
- [29; 5; 12; 8]; [130; 5; 6; 12; 7; 8; 9; 17];
- [131; 5; 12; 7; 8; 9; 17]; [132; 5; 6; 12; 8; 9; 17];
- [133; 5; 12; 8; 9; 17]; [125; 5; 6; 7; 8; 9; 17];
- [116; 5; 7; 8; 9; 17]; [89; 5; 6; 12; 8; 9];
- [90; 5; 6; 12; 8]; [117; 5; 12; 7; 9]; [118; 5; 12; 9];
- [58; 5; 6; 9]; [59; 5; 6]; [53; 6; 9; 17]; [126; 6; 12; 7; 17];
- [134; 12; 7; 17]; [110; 12; 17]; [135; 5; 12; 7; 17];
- [136; 5; 12; 17]; [52; 6; 7; 17]; [137; 5; 12; 7; 9; 17];
- [138; 5; 12; 9; 17] ];;
-
-t () ;;
-
-(* Example from SL6 conversion *)
-let s () = test [[2; -1]; [-3];
- [2; -1]; [-7; -6; -5; -4]; [-11; -10; -9; -4; -8]; [-12; -10; -9; -8];
- [-13; -6; -5]; [-15; -6; -14; -5; -9; -4; -8]; [-16; -10; -8];
- [-17; -14; -10; -8]; [-18; -10; -4; -8]; [-19; -14; -5; -9; -4; -8];
- [-20; -14; -10; -5]; [-21; -6; -14; -10; -5; -8]; [-22; -6; -5; -9; -4; -8];
- [-23; -6; -4]; [-24; -6; -14; -5; -4]; [-25; -14; -10; -9; -8];
- [-26; -14; -5; -9; -8]; [-27; -10; -9; -4]; [-28; -6; -10; -4];
- [-29; -6; -5; -9; -8]; [-30; -6; -14; -5; -9; -8]; [-31; -6; -5; -9; -4];
- [-32; -10; -4]; [-33; -14; -10]; [-34; -6; -14; -9; -8]; [-35; -10; -5; -8];
- [-36; -10; -5; -4]; [-37; -14; -10; -9; -4]; [-38; -5; -9; -4];
- [-39; -6; -14; -5; -9]; [-40; -6; -14; -5]; [-41; -10; -5; -4; -8];
- [-42; -6; -14; -5; -8]; [-43; -6; -14; -5; -4; -8]; [-44; -14; -9; -4; -8];
- [-45; -6; -14; -10; -5; -4]; [-46; -6; -10; -9; -8]; [-47; -4];
- [-48; -6; -9; -4]; [-49; -6; -10; -9; -4; -8]; [-50; -6; -9; -4; -8];
- [-51; -6; -10; -5; -4]; [-52; -6; -10; -5; -8]; [-53; -14; -5; -9; -4];
- [-54; -14; -5; -9]; [-55; -14; -5]; [-56; -14; -10; -5; -9; -8];
- [-57; -6; -10; -5; -9; -8]; [-58; -14; -10; -9; -4; -8]; [-59; -6; -14; -4];
- [-60; -6; -5; -8]; [-61; -14; -9; -8]; [-62; -14; -9; -4]; [-63; -9; -4];
- [-64; -6; -5; -9]; [-65; -6; -4; -8]; [-66; -6; -10; -5; -4; -8];
- [-67; -6; -14; -9]; [-68; -14; -9]; [-69; -14]; [-70; -6; -10; -9; -4];
- [-71; -14; -5; -4]; [-72; -14; -10; -5; -8]; [-73; -6; -10; -5]; [-74; -6;-10];
- [-75; -6; -5; -4; -8]; [-76; -5; -4; -8]; [-77; -5; -4]; [-78; -6; -10; -9];
- [-79; -10; -9]; [-80; -10; -5]; [-81; -6; -10; -5; -9; -4; -8];
- [-82; -14; -10; -4]; [-83; -14; -10; -5; -4; -8]; [-84; -6; -10; -8];
- [-85; -6; -9; -8]; [-86; -6; -9]; [-87; -14; -4]; [-88; -14; -5; -4; -8];
- [-89; -14; -4; -8]; [-90; -14; -5; -8]; [-91; -14; -10; -9];
- [-92; -6; -14; -10; -9; -8]; [-93; -6; -14; -9; -4; -8]; [-94; -9];
- [-95; -9; -8]; [-96; -5]; [-97; -14; -10; -5; -4]; [-98; -14; -10; -5; -9; -4];
- [-99; -14; -8]; [-100; -6; -10; -5; -9; -4]; [-101; -6; -10; -5; -9];
- [-102; -14; -10; -5; -9]; [-103; -10; -5; -9; -4]; [-104; -10; -5; -9];
- [-105; -6; -14; -8]; [-106; -14; -10; -4; -8]; [-107; -6; -14; -10; -8];
- [-108; -6; -14; -4; -8]; [-109; -6; -10; -4; -8]; [-110; -6; -14; -10; -4; -8];
- [-111; -10; -5; -9; -8]; [-112;...
[truncated message content] |
