[Toss-devel-svn] SF.net SVN: toss:[1417] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1417] trunk/Toss
|
From: <luk...@us...> - 2011-04-18 18:28:33
|
Revision: 1417
http://toss.svn.sourceforge.net/toss/?rev=1417&view=rev
Author: lukaszkaiser
Date: 2011-04-18 18:28:26 +0000 (Mon, 18 Apr 2011)
Log Message:
-----------
Moving QBF to BoolFormula, adding timeout support in MiniSat, Sat and BoolFormula.
Modified Paths:
--------------
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Formula/BoolFormulaTest.ml
trunk/Toss/Formula/Sat/Makefile
trunk/Toss/Formula/Sat/MiniSAT.ml
trunk/Toss/Formula/Sat/MiniSAT.mli
trunk/Toss/Formula/Sat/MiniSATWrap.C
trunk/Toss/Formula/Sat/Sat.ml
trunk/Toss/Formula/Sat/Sat.mli
trunk/Toss/Formula/Sat/minisat/Solver.C
trunk/Toss/Formula/Sat/minisat/Solver.h
trunk/Toss/Makefile
trunk/Toss/TossFullTest.ml
Removed Paths:
-------------
trunk/Toss/Formula/Sat/qbf.ml
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/BoolFormula.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -1,7 +1,12 @@
(* Represent Boolean combinations of integer literals. *)
let debug_level = ref 0
-let set_debug_level i = Sat.set_debug_level (i-1); (debug_level := i)
+let debug_elim = ref false
+let set_debug_level i = (
+ Sat.set_debug_level (i-1);
+ debug_level := i;
+ if i > 0 then debug_elim := true
+)
(* 0 : no generation is performed and to_cnf transforms a DNF
1 : use Tseitin to construct a CNF with auxiliary variables
@@ -9,7 +14,7 @@
let auxcnf_generation = ref 2
let set_auxcnf i = (auxcnf_generation := i)
-let simplification = ref 2
+let simplification = ref 7
let set_simplification i = (simplification := i)
(* bit 0 : subsumption test after cnf conversion
bit 1 : full-fledged simplification
@@ -104,12 +109,21 @@
let rec sort phi =
match phi with
- BVar _ -> phi
+ | BVar _ -> phi
| BNot psi -> BNot (sort psi)
| BOr psis -> BOr (List.sort compare (List.map sort psis))
| BAnd psis -> BAnd (List.sort compare (List.map sort psis))
+let rec subst vars = function
+ | BVar v when (List.mem v vars) -> BAnd []
+ | BVar v when (List.mem (-v) vars) -> BOr []
+ | BVar v -> BVar v
+ | BNot f -> subst vars f
+ | BOr fs -> BOr (List.map (subst vars) fs)
+ | BAnd fs -> BAnd (List.map (subst vars) fs)
+
+
(* 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
@@ -242,43 +256,56 @@
formula phi
+(* Flatten conjunctions and disjunctions. *)
+let rec flatten phi =
+ let is_conjunction = function BAnd _ -> true | _ -> false in
+ let is_disjunction = function BOr _ -> true | _ -> false in
+ match phi with
+ | 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
+ (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
+ (function
+ | BAnd psis -> List.map flatten psis
+ | psi -> [flatten psi] ) flist)))
+ | _ -> phi
+
+
+(* Absorb trues and falses *)
+let rec neutral_absorbing = function
+ | BVar _ as lit -> lit
+ | BNot psi -> BNot (neutral_absorbing psi)
+ | BOr psis ->
+ if (List.exists (fun psi -> psi = BAnd []) psis) then (BAnd []) else
+ let filtered_once = List.filter (fun psi -> psi <> BOr []) psis in
+ let new_psis = List.map neutral_absorbing filtered_once in
+ let filtered = List.filter (fun psi -> psi <> BOr []) new_psis in
+ if (List.exists (fun psi -> psi = BAnd []) filtered) then (BAnd []) else
+ BOr filtered
+ | BAnd psis ->
+ if (List.exists (fun psi -> psi = BOr []) psis) then (BOr []) else
+ let filtered_once = List.filter (fun psi -> psi <> BAnd []) psis in
+ let new_psis = List.map neutral_absorbing filtered_once in
+ let filtered = List.filter (fun psi -> psi <> BAnd []) new_psis in
+ if (List.exists (fun psi -> psi = BOr []) filtered) then (BOr []) else
+ BAnd filtered
+
(* Simplify a Boolean combination *)
let rec simplify phi =
let is_conjunction = function BAnd _ -> true | _ -> false in
let is_disjunction = function BOr _ -> true | _ -> false in
let is_literal = function BNot (BVar _) | BVar _ -> true | _ -> false in
- let rec flatten phi =
- match phi with
- | 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
- (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
- (function
- | BAnd psis -> List.map flatten psis
- | psi -> [flatten psi] ) flist)))
- | _ -> phi in
- let rec neutral_absorbing = function
- | 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
let rec singularise unsorted_phi =
let phi = sort unsorted_phi in (* this should be done more elegantly!!! *)
let rec neg_occurrence = function
@@ -318,18 +345,18 @@
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
+ (List.for_all (fun phi -> phi=theta ||
not (subformula phi theta)) non_disjnctns)
- & (List.for_all (fun phi -> phi=theta or
+ && (List.for_all (fun phi -> phi=theta ||
not (subclause phi theta)) disjnctns))
disjnctns)
| BOr psis ->
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
+ (List.for_all (fun phi -> phi=theta ||
not (subformula phi theta)) non_conjnctns)
- & (List.for_all (fun phi -> phi=theta or
+ && (List.for_all (fun phi -> phi=theta ||
not (subclause phi theta)) conjnctns))
conjnctns) in
let unit_propagation phi =
@@ -362,7 +389,7 @@
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
+ (fun psi -> is_disjunction psi || 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 *)
@@ -458,15 +485,15 @@
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
+ List.for_all (fun x -> x=lit || 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)
+ (fun x -> x=(lit_of_int 0) || 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)
+ List.partition (fun phi -> is_disjunction phi || is_literal phi)
psis in
let (resolvents, non_resolvents) = List.partition
(fun clause ->
@@ -523,6 +550,12 @@
"\nwas simplified to " ^ str simplified);
simplified
+let subst_simp vars f =
+ let mem_simp = !simplification in
+ simplification := 2;
+ let res = simplify (subst vars f) in
+ simplification := mem_simp;
+ res
(* Convert reduced Boolean combination into CNF with aux variables (Tseitin) *)
let auxcnf_of_bool_formula phi =
@@ -661,3 +694,306 @@
formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
formula_cnf
+
+(* ------- Boolean quantifier elimination using CNF conversion ------- *)
+
+let to_cnf_basic phi =
+ let cnf = convert phi in
+ neutral_absorbing
+ (BAnd (List.rev_map (fun lits -> BOr (List.map lit_of_int lits)) cnf))
+
+let to_cnf ?(tm=1200.) phi =
+ try
+ Sat.set_timeout tm;
+ let res = to_cnf_basic phi in
+ Sat.clear_timeout ();
+ Some (res)
+ with Aux.Timeout _ -> None
+
+let try_cnf tm phi =
+ match to_cnf ~tm phi with None -> phi | Some psi -> psi
+
+let to_dnf_basic phi = to_nnf ~neg:true (to_cnf_basic (to_nnf ~neg:true phi))
+
+let to_dnf ?(tm=1200.) phi =
+ match to_cnf ~tm (to_nnf ~neg:true phi) with
+ | None -> None
+ | Some psi -> Some (to_nnf ~neg:true psi)
+
+let try_dnf tm phi =
+ match to_dnf ~tm phi with None -> phi | Some psi -> psi
+
+let univ ?(dbg=0) v phi =
+ if dbg > 0 then Printf.printf "Univ subst in %s\n%!" (str phi);
+ let simp1 = subst_simp [v] phi in
+ if dbg > 0 then Printf.printf "Univ subst POS: %s\n%!" (str simp1);
+ let simp2 = subst_simp [-v] phi in
+ if dbg > 0 then Printf.printf "Univ subst NEG: %s\n%!" (str simp2);
+ BAnd [simp1; simp2]
+
+
+let sort_freq phi vars =
+ let rec occ v acc = function
+ | BVar w -> if abs v = abs w then acc + 1 else acc
+ | BNot f -> occ v acc f
+ | BOr fl | BAnd fl -> List.fold_left (occ v) acc fl in
+ let freqs = Hashtbl.create (List.length vars) in
+ List.iter (fun v -> Hashtbl.add freqs v (occ v 0 phi)) vars;
+ let fq v = Hashtbl.find freqs v in
+ List.sort (fun v w -> (fq v) - (fq w)) vars
+
+let (tm_jump, cutvar, has_vars_mem) = (1.1, 3, Hashtbl.create 31)
+
+let _ = debug_elim := false
+
+(* Returns a quantifier-free formula equivalent to All (vars, phi).
+ The list [vars] contains only positive literals and [phi] is in NNF. *)
+let rec elim_all_rec ?(nocheck=false) prefix tout vars in_phi =
+ if List.length vars = 0 then in_phi else match in_phi with
+ | BVar v -> if List.mem (abs v) vars then BOr [] else (BVar v)
+ | BNot _ -> failwith "error (elim_all_rec): BNot in NNF Boolean formula"
+ | BAnd fs ->
+ if !debug_elim then Printf.printf "%s vars %i list %i (same sign)\n%!"
+ prefix (List.length vars) (List.length fs);
+ let do_elim (acc, i) f =
+ if f = BOr [] || acc = [BOr []] then ([BOr []], i+1) else
+ let new_pref = prefix ^ (string_of_int i) ^ ":" in
+ let elim_f = elim_all_rec new_pref tout vars f in
+ if elim_f = BOr [] then ([BOr []], i+1) else
+ if elim_f = BAnd [] then (acc, i+1) else (elim_f :: acc, i+1) in
+ let (simp_fs, _) = List.fold_left do_elim ([], 0) fs in
+ if !debug_elim then Printf.printf "%s done %!" prefix;
+ let res = match to_dnf ~tm:(5. *. tout) (BAnd simp_fs) with
+ | None ->
+ if !debug_elim then
+ Printf.printf "(non-dnf %i)\n%!" (size (BAnd simp_fs));
+ BAnd simp_fs
+ | Some psi ->
+ if !debug_elim then Printf.printf "(dnf %i)\n%!" (size psi);
+ psi in
+ neutral_absorbing (flatten res)
+ | BOr [] -> BOr []
+ | BOr [f] -> elim_all_rec prefix tout vars f
+ | BOr fs when List.for_all (function BVar _ -> true | _ -> false) fs ->
+ let is_univ_quant = function
+ | BVar v -> List.mem (abs v) vars
+ | _ -> failwith "error (elim_all_rec): non-BVar in BVar-only list" in
+ BOr (List.filter (fun v -> not (is_univ_quant v)) fs)
+ | BOr fs as phi ->
+ let rec has_vars sgn vl = function (* check if any var occurs *)
+ | BVar v -> if sgn then List.mem v vl else List.mem (abs v) vl
+ | BNot f -> has_vars sgn vl f
+ | BOr fl | BAnd fl -> List.exists (has_vars sgn vl) fl in
+ let has_vars_memo sgn vl =
+ try Hashtbl.find has_vars_mem (sgn, vl) with Not_found ->
+ let res = has_vars sgn vl in
+ Hashtbl.add has_vars_mem (sgn, vl) res;
+ res in
+ if !debug_elim && prefix <> "S" then
+ Printf.printf "%s vars %i list %i (partition)\n%!" prefix
+ (List.length vars) (List.length fs);
+ let (fs_yes, fs_no) = List.partition (has_vars_memo false vars) fs in
+ if Hashtbl.length has_vars_mem > 10000 then Hashtbl.clear has_vars_mem;
+ if fs_no <> [] then (
+ let elim_yes = elim_all_rec prefix tout vars (BOr fs_yes) in
+ neutral_absorbing (flatten (BOr (elim_yes :: fs_no)))
+ ) else if List.length vars = 1 then (
+ let sub = univ (List.hd vars) phi in
+ if prefix = "S" then simplify (to_dnf_basic sub) else
+ let (res, msg ) = match to_dnf ~tm:(5. *. tout) sub with
+ | None -> (simplify sub, "no dnf")
+ | Some dnf -> (simplify dnf, "dnf") in
+ if !debug_elim then
+ Printf.printf "%s vars %i list %i (%s)\n%!" prefix
+ (List.length vars) (List.length fs) msg;
+ res
+ ) else if List.length vars < cutvar then (
+ let insert psi v = neutral_absorbing (flatten (univ v psi)) in
+ let sub = List.fold_left insert phi vars in
+ let (res, msg ) = match to_dnf ~tm:(3. *. tout) sub with
+ | None -> (simplify sub, "no dnf")
+ | Some dnf -> (simplify dnf, "dnf") in
+ if !debug_elim then
+ Printf.printf "%s vars %i list %i (%s)\n%!" prefix
+ (List.length vars) (List.length fs) msg;
+ res
+ ) else (
+ if !debug_elim then
+ Printf.printf "%s vars %i list %i (inside %i)\n%!" prefix
+ (List.length vars) (List.length fs) (size phi);
+ try
+ if nocheck then raise (Aux.Timeout "!!out");
+ if !debug_elim then
+ Printf.printf "%s vars %i list %i (cnf conv) %!" prefix
+ (List.length vars) (List.length fs);
+ let bool_cnf = match to_cnf ~tm:(3. *. tout) phi with
+ | None -> raise (Aux.Timeout "!!none")
+ | Some psi -> psi in
+ if !debug_elim then Printf.printf "success \n%!";
+ let cnf = elim_all_rec prefix tout vars bool_cnf in
+ let xsize = function BAnd l -> List.length l | _ -> 0 in
+ if !debug_elim then
+ Printf.printf "%s vars %i list %i (cnf after conv %i) %!" prefix
+ (List.length vars) (List.length fs) (xsize cnf);
+ match to_dnf ~tm:(5. *. tout) cnf with
+ | None -> if !debug_elim then Printf.printf "\n%!"; cnf
+ | Some dnf ->
+ if !debug_elim then Printf.printf "(dnf) \n%!"; dnf
+ with Aux.Timeout s ->
+ if !debug_elim && s<>"!!out" then Printf.printf "failed\n%!";
+ let elim nbr_left timeout psi v =
+ try
+ if !debug_elim then
+ Printf.printf "%s eliminating %i%!" prefix v;
+ if nbr_left > 2 then (
+ Sat.set_timeout (timeout);
+ ) else ( Sat.set_timeout (3. *. timeout) );
+ let res = elim_all_rec "S" tout [v] psi in
+ Sat.clear_timeout ();
+ if !debug_elim then Printf.printf " success.\n%!";
+ Some res
+ with Aux.Timeout _ ->
+ if !debug_elim then Printf.printf " failed\n%!";
+ None in
+ let try_elim_var timeout (left_vars,cur_phi,elim_nbr,step,all_nbr) v =
+ if not (has_vars_memo true [-v] cur_phi) then (
+ if !debug_elim then
+ Printf.printf "%s elimineted %i (only pos)\n%!" prefix v;
+ (left_vars, subst_simp [-v] cur_phi, elim_nbr+1, step+1, all_nbr)
+ ) else if not (has_vars_memo true [v] cur_phi) then (
+ if !debug_elim then
+ Printf.printf "%s elimineted %i (only neg)\n%!" prefix v;
+ (left_vars, subst_simp [v] cur_phi, elim_nbr+1, step+1, all_nbr)
+ ) else if 2*step > all_nbr && elim_nbr > 0 &&
+ step+2 < all_nbr && all_nbr - elim_nbr > cutvar then
+ (v :: left_vars, cur_phi, elim_nbr, step + 1, all_nbr)
+ else match elim (all_nbr - step) timeout cur_phi v with
+ | None -> (v :: left_vars, cur_phi, elim_nbr, step + 1, all_nbr)
+ | Some psi -> (left_vars, psi, elim_nbr + 1, step + 1, all_nbr) in
+ let (left_vars, new_phi, elim_nbr, _, all_nbr) =
+ List.fold_left (try_elim_var tout) ([], phi,0,0, List.length vars)
+ (sort_freq phi vars) in
+ if elim_nbr > 0 then
+ elim_all_rec prefix tout left_vars new_phi
+ else
+ let (big_v, rest_vars) = (List.hd left_vars, List.tl left_vars) in
+ if !debug_elim then Printf.printf "branch %i\n%!" big_v;
+ elim_all_rec prefix (tm_jump *.tout) rest_vars (univ big_v new_phi)
+ )
+
+(* Returns a quantifier-free formula equivalent to All (vars, phi). *)
+let elim_all vars phi =
+ elim_all_rec " " 0.3 (List.map (fun v -> abs v) vars) (to_nnf phi)
+
+(* Returns a quantifier-free formula equivalent to Ex (vars, phi). *)
+let elim_ex vars phi =
+ to_nnf ~neg:true (elim_all vars (to_nnf ~neg:true phi))
+
+
+(* ------ Reading and reducing QBF --------- *)
+
+(* Type for quantified Boolean formulas. *)
+type qbf =
+ | QFree of bool_formula
+ | QEx of int list * qbf
+ | QAll of int list * qbf
+
+(* Print a QBF formula. *)
+let rec qbf_str = function
+ | QFree phi -> str phi
+ | QEx (vars, phi) ->
+ "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^
+ " " ^ qbf_str phi ^ ")"
+ | QAll (vars, phi) ->
+ "(ex " ^ (String.concat ", " (List.map string_of_int vars)) ^
+ " " ^ qbf_str phi ^ ")"
+
+
+(* Read a qdimacs description of a QBF from [in_ch]. *)
+let read_qdimacs in_ch =
+ (* Read the starting 'c' comment lines, and the first 'p' line.
+ Set the number of variables and the number of clauses. *)
+ let rec read_header () =
+ let line = input_line in_ch in
+ if line.[0] = 'c' then read_header () else
+ Scanf.sscanf line "p cnf %i %i" (fun x y -> (x, y)) in
+
+ (* Read one clause from a line. *)
+ let read_clause line =
+ let (s, i, clause) = (ref "", ref 0, ref []) in
+ while (line.[!i] != '0' || line.[!i - 1] != ' ') do
+ if line.[!i] = ' ' then (
+ i := !i + 1;
+ let lit = int_of_string !s in
+ clause := lit :: !clause;
+ s := "";
+ ) else (
+ s := !s ^ (String.make 1 line.[!i]);
+ i := !i + 1;
+ )
+ done;
+ !clause in
+
+ let list_int line =
+ let split = Str.split (Str.regexp "[ \t]+") line in
+ List.rev (List.tl (List.rev_map
+ (fun s -> int_of_string s) (List.tl split))) in
+
+ let read_formula () =
+ let (no_var, no_cl) = read_header () in
+ let rec read_phi () =
+ let line = input_line in_ch in
+ if line.[0] == 'a' then
+ QAll (list_int line, read_phi ())
+ else if line.[0] == 'e' then
+ QEx (list_int line, read_phi ())
+ else (
+ let cls = ref [read_clause (line)] in
+ for i = 1 to (no_cl-1) do
+ cls := (read_clause (input_line in_ch)) :: !cls
+ done;
+ QFree (
+ BAnd (List.map (fun lits -> BOr (List.map lit_of_int lits)) !cls))
+ ) in
+ read_phi () in
+
+ read_formula ()
+
+
+(* Eliminating quantifiers from QBF formulas. *)
+let rec elim_quant = function
+ | QFree (phi) -> phi
+ | QEx (vars, qphi) ->
+ Hashtbl.clear has_vars_mem;
+ let inside, len = elim_quant qphi, List.length vars in
+ if !debug_elim then Printf.printf "EX %i START\n%!" len;
+ let res_raw = elim_ex vars (inside) in
+ let res = match to_dnf ~tm:3. res_raw with
+ | None ->
+ if !debug_elim then (
+ Printf.printf "EX ELIM NO DNF\n%!";
+ Printf.printf "%s \n%!" (str res_raw);
+ );
+ res_raw
+ | Some r ->
+ if !debug_elim then Printf.printf "EX ELIM IN DNF\n%!";
+ r in
+ if !debug_elim then Printf.printf "EX %i FIN\n%!" len;
+ res
+ | QAll (vars, qphi) ->
+ Hashtbl.clear has_vars_mem;
+ let inside, len = elim_quant qphi, List.length vars in
+ if !debug_elim then Printf.printf "ALL %i START\n%!" len;
+ let res_raw = elim_all vars (inside) in
+ let res = match to_cnf ~tm:3. res_raw with
+ | None ->
+ if !debug_elim then (
+ Printf.printf "ALL ELIM NO CNF\n%!";
+ Printf.printf "%s \n%!" (str res_raw);
+ );
+ res_raw
+ | Some r ->
+ if !debug_elim then Printf.printf "ALL ELIM IN CNF\n%!";
+ r in
+ if !debug_elim then Printf.printf "ALL %i FIN\n%!" len;
+ res
Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/BoolFormula.mli 2011-04-18 18:28:26 UTC (rev 1417)
@@ -55,13 +55,34 @@
val formula_to_cnf : Formula.formula -> Formula.formula
+(** {2 Boolean Quantifier Elimination and QBF} *)
-(** {2 Debugging.} *)
+(** Returns a quantifier-free formula equivalent to All (vars, phi). *)
+val elim_all : int list -> bool_formula -> bool_formula
+(** Returns a quantifier-free formula equivalent to Ex (vars, phi). *)
+val elim_ex : int list -> bool_formula -> bool_formula
+
+(** Type for quantified Boolean formulas. *)
+type qbf =
+ | QFree of bool_formula
+ | QEx of int list * qbf
+ | QAll of int list * qbf
+
+(** Print a QBF formula. *)
+val qbf_str : qbf -> string
+
+(** Read a qdimacs description of a QBF from [in_ch]. *)
+val read_qdimacs : in_channel -> qbf
+
+(** Eliminating quantifiers from QBF formulas. *)
+val elim_quant : qbf -> bool_formula
+
+
+(** {3 Debugging} *)
+
(** Debugging information. At level 0 nothing is printed out. *)
val set_debug_level : int -> unit
-
-
val set_auxcnf : int -> unit
val set_simplification : int -> unit
Modified: trunk/Toss/Formula/BoolFormulaTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFormulaTest.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/BoolFormulaTest.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -3,7 +3,6 @@
open BoolFormula;;
BoolFormula.set_debug_level 0;;
-BoolFormula.set_simplification 6;; (* w/ resolution: 6; w/o resolution: 2 *)
BoolFormula.set_auxcnf 2;; (* Tseitin: 1 Plaisted-Greenbaum: 2 *)
let formula_of_string s =
@@ -226,6 +225,188 @@
test_cnf_string (fun x -> String.length x > 9) (test_formula 200)
);
+
+ "basic Boolean quantifier elimination" >::
+ (fun () ->
+ let test_elim_ex form vars res_s =
+ let eq_s = assert_eq_string (BoolFormula.str form) in
+ eq_s "Eliminating ex quantifier" res_s
+ (BoolFormula.str (elim_ex vars form)) in
+
+ (* ex X [ (X or Y) and (not X or Z) ] = (Y or Z) *)
+ let b = BAnd [BOr [BVar 1; BVar 2]; BOr [BVar (-1); BVar 3]] in
+ test_elim_ex b [1] "(2 or 3)";
+ );
]
+
+let bigtests = "BoolFormulaBig" >::: [
+ "simple QBF solving" >::
+ (fun () ->
+ let test_elim qbf res_s =
+ let eq_s = assert_eq_string (qbf_str qbf) in
+ eq_s "Eliminating quantifiers from QBF" res_s
+ (BoolFormula.str (elim_quant qbf)) in
+
+ let s27_d2_s = "p cnf 85 142
+e 4 5 6 7 1 2 3 9 10 11 12 13 14 15 16 17 32 33 34 35 37 38 39 40 41 42 43 44 45 0
+a 18 19 20 21 23 25 26 27 28 29 0
+e 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 0
+-1 0
+-2 0
+-3 0
+4 9 0
+-4 -9 0
+-1 -10 0
+-15 -10 0
+1 15 10 0
+9 -11 0
+2 -11 0
+-9 -2 11 0
+-13 12 0
+-11 12 0
+13 11 -12 0
+-5 -13 0
+-3 -13 0
+5 3 13 0
+-7 14 0
+-11 14 0
+7 11 -14 0
+14 15 0
+12 15 0
+-14 -12 -15 0
+-9 -16 0
+-10 -16 0
+9 10 16 0
+-6 -17 0
+-13 -17 0
+6 13 17 0
+32 37 0
+-32 -37 0
+-16 -38 0
+-43 -38 0
+16 43 38 0
+37 -39 0
+10 -39 0
+-37 -10 39 0
+-41 40 0
+-39 40 0
+41 39 -40 0
+-33 -41 0
+-17 -41 0
+33 17 41 0
+-35 42 0
+-39 42 0
+35 39 -42 0
+42 43 0
+40 43 0
+-42 -40 -43 0
+-37 -44 0
+-38 -44 0
+37 38 44 0
+-34 -45 0
+-41 -45 0
+34 41 45 0
+-18 60 0
+-23 60 0
+18 23 -60 0
+18 61 0
+23 61 0
+-18 -23 -61 0
+1 62 0
+38 62 0
+-1 -38 -62 0
+29 63 0
+38 63 0
+-29 -38 -63 0
+-1 64 0
+-29 64 0
+-38 64 0
+1 29 38 -64 0
+-23 65 0
+25 65 0
+23 -25 -65 0
+-2 66 0
+25 66 0
+2 -25 -66 0
+23 67 0
+2 67 0
+-25 67 0
+-23 -2 25 -67 0
+27 68 0
+-26 68 0
+-27 26 -68 0
+25 69 0
+-26 69 0
+-25 26 -69 0
+-27 70 0
+-25 70 0
+26 70 0
+27 25 -26 -70 0
+19 71 0
+27 71 0
+-19 -27 -71 0
+3 72 0
+27 72 0
+-3 -27 -72 0
+-19 73 0
+-3 73 0
+-27 73 0
+19 3 27 -73 0
+21 74 0
+-28 74 0
+-21 28 -74 0
+25 75 0
+-28 75 0
+-25 28 -75 0
+-21 76 0
+-25 76 0
+28 76 0
+21 25 -28 -76 0
+-28 77 0
+-29 77 0
+28 29 -77 0
+-26 78 0
+-29 78 0
+26 29 -78 0
+28 79 0
+26 79 0
+29 79 0
+-28 -26 -29 -79 0
+23 80 0
+44 80 0
+-23 -44 -80 0
+38 81 0
+44 81 0
+-38 -44 -81 0
+-23 82 0
+-38 82 0
+-44 82 0
+23 38 44 -82 0
+20 83 0
+45 83 0
+-20 -45 -83 0
+27 84 0
+45 84 0
+-27 -45 -84 0
+-20 85 0
+-27 85 0
+-45 85 0
+20 27 45 -85 0
+-60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 0
+" in
+
+ let f = open_out "tmp_testfile_28721.bf" in
+ output_string f s27_d2_s;
+ close_out f;
+ let f = open_in "tmp_testfile_28721.bf" in
+ let qbf = read_qdimacs f in
+ close_in f;
+ Sys.remove "tmp_testfile_28721.bf";
+ test_elim qbf "true";
+ );
+]
+
let exec = Aux.run_test_if_target "BoolFormulaTest" tests
+
+let execbig = Aux.run_test_if_target "BoolFormulaTest" bigtests
Modified: trunk/Toss/Formula/Sat/Makefile
===================================================================
--- trunk/Toss/Formula/Sat/Makefile 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/Makefile 2011-04-18 18:28:26 UTC (rev 1417)
@@ -18,15 +18,11 @@
%Test:
make -C ../.. Formula/Sat/$@
-qbf: qbf.ml
- make -C ../.. Formula/Sat/qbf.native
- cp ../../qbf.native qbf
-
tests: SatTest
./SatTest
clean:
- 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 *.cma *.cmi *~ *.cmxa *.cmx *.a *.annot Sat.cmxa SatTest
+ rm -f *.o *.cmo *.cmo *.cmi *~ *.cma *.cmo *.a *.annot
rm -f minisat/SatSolver.o minisat/MiniSATWrap.o
Modified: trunk/Toss/Formula/Sat/MiniSAT.ml
===================================================================
--- trunk/Toss/Formula/Sat/MiniSAT.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/MiniSAT.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -1,7 +1,7 @@
type var = int
type lit = int
type value = int (* F | T | X *)
-type solution = SAT | UNSAT
+type solution = SAT | UNSAT | TIMEOUT
external reset : unit -> unit = "minisat_reset"
external new_var : unit -> var = "minisat_new_var"
@@ -12,6 +12,7 @@
external solve_with_assumption : lit list -> solution = "minisat_solve_with_assumption"
external value_of : var -> value = "minisat_value_of"
external set_threshold : int -> unit = "minisat_set_threshold"
+external set_timeout : float -> unit = "minisat_set_timeout"
let string_of_value (v: value): string =
match v with
Modified: trunk/Toss/Formula/Sat/MiniSAT.mli
===================================================================
--- trunk/Toss/Formula/Sat/MiniSAT.mli 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/MiniSAT.mli 2011-04-18 18:28:26 UTC (rev 1417)
@@ -1,7 +1,7 @@
type var = int
type lit = int
type value = int (* F | T | X *)
-type solution = SAT | UNSAT
+type solution = SAT | UNSAT | TIMEOUT
external reset : unit -> unit = "minisat_reset"
external new_var : unit -> var = "minisat_new_var"
@@ -12,4 +12,5 @@
external solve_with_assumption : lit list -> solution = "minisat_solve_with_assumption"
external value_of : var -> value = "minisat_value_of"
external set_threshold : int -> unit = "minisat_set_threshold"
+external set_timeout : float -> unit = "minisat_set_timeout"
val string_of_value : value -> string
Modified: trunk/Toss/Formula/Sat/MiniSATWrap.C
===================================================================
--- trunk/Toss/Formula/Sat/MiniSATWrap.C 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/MiniSATWrap.C 2011-04-18 18:28:26 UTC (rev 1417)
@@ -47,6 +47,13 @@
return Val_unit;
}
+extern "C" value minisat_set_timeout(value c) {
+ double t = Double_val(c);
+ solver->setTimeout(t);
+
+ return Val_unit;
+}
+
/*extern "C" value minisat_simplify_db(value unit) {
solver->simplifyDB();
@@ -58,8 +65,10 @@
if(solver->solve()) {
r = Val_int(0);
+ } else if (solver->sat_timeout > 0) {
+ r = Val_int(1);
} else {
- r = Val_int(1);
+ r = Val_int(2);
}
return r;
@@ -72,8 +81,10 @@
if(solver->solve(assumption)) {
r = Val_int(0);
+ } else if (solver->sat_timeout > 0) {
+ r = Val_int(1);
} else {
- r = Val_int(1);
+ r = Val_int(2);
}
return r;
Modified: trunk/Toss/Formula/Sat/Sat.ml
===================================================================
--- trunk/Toss/Formula/Sat/Sat.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/Sat.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -3,6 +3,18 @@
let debug_level = ref 0
let set_debug_level i = (debug_level := i)
+let timeout = ref 0.
+let minisat_timeout = ref 900.
+let check_timeout msg =
+ if !timeout > 0.5 && Unix.gettimeofday () > !timeout then
+ (timeout := 0.; raise (Aux.Timeout msg))
+
+let set_timeout t =
+ minisat_timeout := 5. *. t; (* if MiniSat does it, it's important *)
+ timeout := Unix.gettimeofday () +. t
+
+let clear_timeout () = (timeout := 0.; minisat_timeout := 900.)
+
module IntSet = Set.Make
(struct type t = int let compare x y = x - y end)
@@ -44,6 +56,7 @@
(* Reset global variables and the minisat state. *)
let reset () =
MiniSAT.reset ();
+ MiniSAT.set_timeout !minisat_timeout;
var_map := Hashtbl.create 32;
var_rev_map := Hashtbl.create 32;
lit_frequencies := Hashtbl.create 32;
@@ -159,7 +172,9 @@
let solve () =
(* MiniSAT.simplify_db (); *)
match MiniSAT.solve () with
- MiniSAT.UNSAT -> None
+ | MiniSAT.UNSAT -> None
+ | MiniSAT.TIMEOUT ->
+ raise (Aux.Timeout "MiniSat")
| MiniSAT.SAT ->
let res = ref [] in
let update mv v =
@@ -206,6 +221,7 @@
(* Recursive formula performing conversion to cnf, accumulates clauses. *)
let rec perform_conversion disc_vars orig_lits orig_phi bound cl_acc =
+ check_timeout "Sat.perform_conversion";
match solve () with
None -> cl_acc
| Some vars ->
Modified: trunk/Toss/Formula/Sat/Sat.mli
===================================================================
--- trunk/Toss/Formula/Sat/Sat.mli 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/Sat.mli 2011-04-18 18:28:26 UTC (rev 1417)
@@ -3,6 +3,12 @@
(* ------- Main functions ------- *)
+(** Set timeout function for conversions. *)
+val set_timeout : float -> unit
+(** Clear timeout function. *)
+val clear_timeout : unit -> unit
+
+
(* Given a list of literals to set to true, simplify the given CNF formula. *)
val simplify : int list -> int list list -> int list list
Modified: trunk/Toss/Formula/Sat/minisat/Solver.C
===================================================================
--- trunk/Toss/Formula/Sat/minisat/Solver.C 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/minisat/Solver.C 2011-04-18 18:28:26 UTC (rev 1417)
@@ -46,6 +46,7 @@
, clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
, ok (true)
+ , sat_timeout (900)
, cla_inc (1)
, var_inc (1)
, qhead (0)
@@ -79,6 +80,11 @@
//=================================================================================================
// Minor methods:
+bool Solver::setTimeout(double t)
+{
+ sat_timeout = t;
+ return true;
+}
// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
@@ -712,17 +718,21 @@
// Search:
while (status == l_Undef){
- if (verbosity >= 1)
- reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% %6.3f |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100, ((double)clock()-(double)t)/(double)CLOCKS_PER_SEC), fflush(stdout);
- status = search((int)nof_conflicts, (int)nof_learnts);
- nof_conflicts *= restart_inc;
- nof_learnts *= learntsize_inc;
- if ((double)(clock() - t) / CLOCKS_PER_SEC >= 900) {
+ if (verbosity >= 1)
+ reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% %6.3f |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100, ((double)clock()-(double)t)/(double)CLOCKS_PER_SEC), fflush(stdout);
+
+ status = search((int)nof_conflicts, (int)nof_learnts);
+ nof_conflicts *= restart_inc;
+ nof_learnts *= learntsize_inc;
+ if ((double)(clock() - t) / CLOCKS_PER_SEC >= sat_timeout) {
+ sat_timeout = -1;
+ if (verbosity >= 1) {
std::cout << "******************************************\n";
std::cout << "********************TIMEOUT***************\n";
std::cout << "******************************************\n";
- break;
- }
+ };
+ break;
+ }
}
if (verbosity >= 1)
@@ -806,7 +816,7 @@
//reportf("number of solutions: %d\n",numSolutions);
cancelUntil(0);
- return status == l_True;
+ return (status == l_True && sat_timeout > 0);
}
//=================================================================================================
Modified: trunk/Toss/Formula/Sat/minisat/Solver.h
===================================================================
--- trunk/Toss/Formula/Sat/minisat/Solver.h 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/minisat/Solver.h 2011-04-18 18:28:26 UTC (rev 1417)
@@ -42,6 +42,8 @@
~Solver();
int var_threshold;
+ double sat_timeout;
+ bool setTimeout (double t);
// Problem specification:
//
Deleted: trunk/Toss/Formula/Sat/qbf.ml
===================================================================
--- trunk/Toss/Formula/Sat/qbf.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Formula/Sat/qbf.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -1,171 +0,0 @@
-(* ----
- Simple QBF Solver (reads QBF in simplified QDIMACS format)
- ----
-*)
-
-type qbf =
- Cnf of int list list
- | Dnf of int list list
- | Ex of int list * qbf
- | All of int list * qbf
-
-
-(* ---------------------- READING QDIMACS INPUT ---------------------------- *)
-
-let var_freq = ref (Array.make 1 0.)
-let no = ref 0
-
-(* Read the starting 'c' comment lines, and the first 'p' line.
- Set the number of variables and the number of clauses.
-*)
-let rec read_header () =
- let line = read_line () in
- if line.[0] = 'c' then read_header () else
- Scanf.sscanf line "p cnf %i %i" (fun x y -> (x, y))
-
-let read_clause line =
- let (s, i, clause) = (ref "", ref 0, ref []) in
- while (line.[!i] != '0' || line.[!i - 1] != ' ') do
- if line.[!i] = ' ' then (
- i := !i + 1;
- let lit = int_of_string !s in
- clause := lit :: !clause;
- s := "";
- ) else (
- s := !s ^ (String.make 1 line.[!i]);
- i := !i + 1;
- )
- done;
- let len = log (float (List.length !clause)) in
- List.iter (fun l -> !var_freq.(abs l) <- !var_freq.(abs l) +. len) !clause;
- !clause
-
-let update_freq cls =
- for i = 0 to (Array.length !var_freq) - 1 do !var_freq.(i) <- 0. done;
- let update_cl cl =
- let len = log (float (List.length cl)) in
- List.iter (fun l -> !var_freq.(abs l) <- !var_freq.(abs l) +. len) cl in
- List.iter update_cl cls
-
-let list_int line =
- let split = Str.split (Str.regexp "[ \t]+") line in
- List.rev (List.tl (List.rev_map (fun s -> int_of_string s) (List.tl split)))
-
-let read_formula () =
- let (no_var, no_cl) = read_header () in
- var_freq := Array.make (no_var + 1) 0.;
- let rec read_phi () =
- let line = read_line () in
- if line.[0] == 'a' then
- All (list_int line, read_phi ())
- else if line.[0] == 'e' then
- Ex (list_int line, read_phi ())
- else (
- let cls = ref [read_clause (line)] in
- for i = 1 to (no_cl-1) do
- cls := (read_clause (read_line ())) :: !cls
- done;
- Cnf (!cls)
- ) in
- read_phi ()
-
-
-(* ------------------------- PRINTING -------------------------------------- *)
-
-let string_of_cl sep cl =
- "(" ^ (String.concat sep (List.map (fun i -> string_of_int i) cl)) ^ ")"
-
-let rec string_of_formula = function
- Ex (vars, phi) -> "e " ^ (String.concat " " (List.map string_of_int vars)) ^
- " | " ^ (string_of_formula phi)
- | All (vars, phi) -> "a " ^ (String.concat " " (List.map string_of_int vars))^
- " | " ^ (string_of_formula phi)
- | Cnf (cls) ->
- if cls = [] then "T" else if cls = [[]] then "F" else
- String.concat " /\\ " (List.map (string_of_cl " \\/ ") cls)
- | Dnf (cls) ->
- if cls = [] then "F" else if cls = [[]] then "T" else
- String.concat " \\/ " (List.map (string_of_cl " /\\ ") cls)
-
-
-(* ------------------------------ SOLVER ---------------------------------- *)
-
-let covered vars cl = List.exists (fun l -> List.mem (abs l) vars) cl
-
-let sort_freq d vars =
- List.sort (fun v w -> d * (compare !var_freq.(abs v) !var_freq.(abs w))) vars
-
-let filter vars cls =
- List.map (fun cl -> List.filter (fun l -> not (List.mem (abs l) vars)) cl) cls
-
-exception FalseEx
-let conv_bound = ref 40
-
-let elim_var (cls, vacc) v =
- no := !no + 1;
- if !var_freq.(v)>(float !conv_bound)/.2. then (cls, v :: vacc) (*hack*) else (
- print_endline ("ex v. "^(string_of_int v) ^ " (" ^ (string_of_int !no) ^
- ", " ^ (string_of_float !var_freq.(v)) ^ ")");
- let (cls_v, cls_nv) = List.partition (fun cl -> covered [v] cl) cls in
- try
- let conv_v = Sat.convert ~disc_vars:[v] cls_v ~bound:(Some !conv_bound) in
- if conv_v=[] then raise FalseEx else if conv_v = [[]] then (cls_nv, vacc)
- else (List.rev_append cls_nv
- (Sat.convert ~bound:(Some (!conv_bound * 4)) conv_v), vacc)
- with
- Sat.OverBound -> print_endline " elim failed"; (cls, v :: vacc)
- )
-
-let rec solve = function
- Cnf (cls) -> Cnf (cls)
- | Dnf (cls) -> Dnf (cls)
- | Ex ([], phi) ->
- print_endline (" formula ex empty " ^ (string_of_formula phi)); phi
- | All ([], phi) -> phi
- | All (vars, Cnf cls) as phi ->
- print_endline (" formula all " ^ (string_of_formula phi));
- Cnf (filter vars cls)
- | Ex (vars, Dnf cls) as phi ->
- print_endline (" formula ex " ^ (string_of_formula phi));
- Dnf (filter vars cls)
- | Ex (vars, Cnf cls) ->
- if cls = [] then Dnf([]) else if List.mem [] cls then Dnf ([[]]) else
- let len = List.length vars in
- if len < 3 then
- let conv = Sat.convert ~disc_vars:vars cls in
- if conv = [] then Dnf ([]) else Dnf conv
- else (
- update_freq cls;
- no := 0;
- let vs = sort_freq 1 vars in
- try
- let (ecls, left_vs) = List.fold_left elim_var (cls, []) vs in
- if left_vs = [] then Cnf ecls else (
- print_endline (" Left " ^ (string_of_int (List.length left_vs)) ^
- " from " ^ (string_of_int len) ^ " vars.");
- try
- if !conv_bound < 70 then raise Sat.OverBound;
- Sat.set_debug_level 2;
- let conv =
- Sat.convert ~disc_vars:left_vs ~bound:(Some !conv_bound) ecls
- in if conv = [] then Dnf ([]) else Dnf conv
- with Sat.OverBound ->
- Sat.set_debug_level 0;
- conv_bound := (3 * (!conv_bound)) / 2;
- solve (Ex (left_vs, Cnf ecls))
- )
- with FalseEx -> Dnf []
- )
- | All (vars, Dnf (cls)) ->
- if cls = [] then Dnf([]) else if List.mem [] cls then Dnf ([[]]) else
- let conv = Sat.convert ~disc_vars:vars cls in
- if conv = [] then Dnf ([]) else solve (All (vars, Cnf conv))
- | Ex (vars, phi) -> solve (Ex (vars, solve phi))
- | All (vars, phi) -> solve (All (vars, solve phi))
-
-let _ =
- let phi = read_formula () in
- print_endline ("Solving formula " ^ (string_of_formula phi));
- Sat.set_debug_level 0;
- print_endline ("Solved: " ^ (string_of_formula (solve phi)));
-;;
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/Makefile 2011-04-18 18:28:26 UTC (rev 1417)
@@ -59,7 +59,7 @@
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
FormulaINCSatINC=Formula
-FormulaINC=Formula/Sat
+FormulaINC=Formula,Formula/Sat
SolverINC=Formula,Formula/Sat,Solver/RealQuantElim
ArenaINC=Formula,Formula/Sat,Solver/RealQuantElim,Solver
PlayINC=Formula,Formula/Sat,Solver/RealQuantElim,Solver,Arena
Modified: trunk/Toss/TossFullTest.ml
===================================================================
--- trunk/Toss/TossFullTest.ml 2011-04-17 14:05:28 UTC (rev 1416)
+++ trunk/Toss/TossFullTest.ml 2011-04-18 18:28:26 UTC (rev 1417)
@@ -1,6 +1,14 @@
open OUnit
-let formula_tests = TossTest.formula_tests
+let formula_tests = "Formula" >::: [
+ AuxTest.tests;
+ FormulaTest.tests;
+ SatTest.tests;
+ BoolFormulaTest.tests;
+ BoolFormulaTest.bigtests;
+ FormulaOpsTest.tests;
+ FFTNFTest.tests;
+]
let solver_tests = TossTest.solver_tests
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|