[Toss-devel-svn] SF.net SVN: toss:[1387] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1387] trunk/Toss
|
From: <luk...@us...> - 2011-03-24 18:05:56
|
Revision: 1387
http://toss.svn.sourceforge.net/toss/?rev=1387&view=rev
Author: lukaszkaiser
Date: 2011-03-24 18:05:50 +0000 (Thu, 24 Mar 2011)
Log Message:
-----------
Size-based predicate ordering in formula compilation.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Makefile
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/SolverTest.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/Solver/Structure.mli
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Formula/FormulaOps.ml 2011-03-24 18:05:50 UTC (rev 1387)
@@ -1307,9 +1307,9 @@
let is_fo = function `FO _ -> true | _ -> false in
List.filter is_fo (free_vars f)
-let rec order_by_fv acc_fv = function
+let rec order_by_fv structure acc_fv = function
| [] -> []
- | [f] -> [order_by_fv_phi acc_fv f]
+ | [f] -> [order_by_fv_phi structure acc_fv f]
| l ->
let cross x =
let fv = free_vars x in
@@ -1317,27 +1317,36 @@
let (cf, o) = List.partition cross l in
if cf = [] then (
let new_fv = free_vars (List.hd l) in
- order_by_fv new_fv l
+ order_by_fv structure new_fv l
) else (
let new_fv = acc_fv @ (free_vars_fo (And cf)) in
- (List.map (order_by_fv_phi acc_fv) cf) @ (order_by_fv new_fv o)
+ (List.map (order_by_fv_phi structure acc_fv) cf) @
+ (order_by_fv structure new_fv o)
)
-and order_by_fv_phi acc_fv = function
+and order_by_fv_phi structure acc_fv = function
| And fl ->
let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
- let (p, np) = List.partition is_pred fl in
- let res = And (order_by_fv acc_fv (p @ np)) in
+ let (p_raw, np) = List.partition is_pred fl in
+ let p = match structure with | None -> p_raw | Some struc ->
+ let card = function | Rel (r,_) -> Structure.rel_size struc r | _-> 0 in
+ let cmp x y = (card x) - (card y) in
+ List.sort cmp p_raw in
+ let res = And (order_by_fv structure acc_fv (p @ np)) in
if !debug_level > 1 then print_endline ("fvordered and: " ^ (str res));
res
| Or fl ->
let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
- let (p, np) = List.partition is_pred fl in
- let res = Or (order_by_fv acc_fv (p @ np)) in
+ let (p_raw, np) = List.partition is_pred fl in
+ let p = match structure with | None -> p_raw | Some struc ->
+ let card = function | Rel (r,_) -> Structure.rel_size struc r | _-> 0 in
+ let cmp x y = (card x) - (card y) in
+ List.sort cmp p_raw in
+ let res = Or (order_by_fv structure acc_fv (p @ np)) in
if !debug_level > 1 then print_endline ("fvordered or: " ^ (str res));
res
- | Ex (vs, phi) -> Ex (vs, order_by_fv_phi acc_fv phi)
- | All (vs, phi) -> All (vs, order_by_fv_phi acc_fv phi)
+ | Ex (vs, phi) -> Ex (vs, order_by_fv_phi structure acc_fv phi)
+ | All (vs, phi) -> All (vs, order_by_fv_phi structure acc_fv phi)
| f -> f
let rec push_in_quant phi =
@@ -1364,12 +1373,12 @@
let rec push_quant f = push_in_quant (flatten_sort (f))
-let tnf_fv phi =
+let tnf_fv ?structure phi =
let fv = free_vars phi in
let psi = rename_quant_avoiding [] (Ex (fv, phi)) in
match mso_last (flatten (del_vars_quant fv (tnf psi))) with
- | Or fl -> Or (List.map (order_by_fv_phi []) fl)
- | f -> order_by_fv_phi [] f
+ | Or fl -> Or (List.map (order_by_fv_phi structure []) fl)
+ | f -> order_by_fv_phi structure [] f
(* Assign emptyset to the MSO-variable v by replacing "x in X" with "false". *)
let assign_emptyset v phi =
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Formula/FormulaOps.mli 2011-03-24 18:05:50 UTC (rev 1387)
@@ -187,7 +187,8 @@
in a NNF form which pushes quantifiers inside as strongly as possible. *)
val tnf : formula -> formula
val tnf_re : real_expr -> real_expr
-val tnf_fv : formula -> formula (** first existentially quantifies free vars *)
+val tnf_fv : ?structure : Structure.structure ->
+ formula -> formula (** first existentially quantifies free vars *)
(** {2 Convert to CNF or DNF} *)
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Makefile 2011-03-24 18:05:50 UTC (rev 1387)
@@ -57,8 +57,8 @@
OCAMLBUILDNOPP=ocamlbuild -log build.log -j 8 -menhir ../menhir_conf \
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
-FormulaINC=Formula/Sat
-SolverINC=Formula,Formula/Sat,Solver/RealQuantElim
+FormulaINC=Formula/Sat,Formula,Solver
+SolverINC=Formula,Solver,Formula/Sat,Solver/RealQuantElim
ArenaINC=Formula,Formula/Sat,Solver/RealQuantElim,Solver
PlayINC=Formula,Formula/Sat,Solver/RealQuantElim,Solver,Arena
GGPINC=Formula,Formula/Sat,Solver/RealQuantElim,Solver,Arena,Play
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Solver/Solver.ml 2011-03-24 18:05:50 UTC (rev 1387)
@@ -39,7 +39,7 @@
formulas_check = Hashtbl.create 3 ;
}
-let register_formula_do solver phi =
+let register_formula_do struc solver phi =
let rec check_form = function
Ex (vs, phi) -> check_form phi
| phi -> phi in
@@ -49,7 +49,7 @@
(Hashtbl.find solver.formulas_eval res, res)
with Not_found ->
if !debug_level > 0 then print_endline ("Entered " ^ (str phi));
- let psi = FormulaOps.tnf_fv phi in
+ let psi = FormulaOps.tnf_fv ~structure:struc phi in
if !debug_level > 0 then print_endline ("Registering " ^ (str psi));
let id = Hashtbl.length solver.formulas_eval + 1 in
Hashtbl.add solver.reg_formulas phi id;
@@ -57,7 +57,7 @@
Hashtbl.add solver.formulas_check id (check_form psi);
(psi, id)
-let register_formula_s solver phi =
+let register_formula_s struc solver phi =
try
let res = Hashtbl.find solver.reg_formulas phi in
if !debug_level > 0 then print_endline ("DirectFound " ^ (str phi));
@@ -65,14 +65,15 @@
with Not_found ->
match Formula.flatten phi with
| And fl ->
- let rfl = List.map (fun f -> fst (register_formula_do solver f)) fl in
+ let rfl = List.map (fun f ->
+ fst (register_formula_do struc solver f)) fl in
let id = Hashtbl.length solver.formulas_eval + 1 in
let psi = Formula.flatten (Or (FormulaOps.to_dnf (And rfl))) in
Hashtbl.add solver.reg_formulas phi id;
Hashtbl.add solver.formulas_eval id psi;
Hashtbl.add solver.formulas_check id psi;
id
- | _ -> let (_, id) = register_formula_do solver phi in id
+ | _ -> let (_, id) = register_formula_do struc solver phi in id
let get_formula solver i = Hashtbl.find solver.formulas_eval i
@@ -357,7 +358,8 @@
let phi_id = Hashtbl.find solver.reg_formulas phi in
Hashtbl.find solver.formulas_eval phi_id
with Not_found ->
- Hashtbl.find solver.formulas_eval (snd(register_formula_do solver phi)) in
+ Hashtbl.find solver.formulas_eval
+ (snd(register_formula_do struc solver phi)) in
let eval_no_fv phi =
if FormulaOps.free_vars phi = [] then (
if !debug_level > 1 then
@@ -472,14 +474,14 @@
let solver = new_solver ()
let evaluate struc phi =
- evaluate solver ~formula:(register_formula_s solver phi) struc
+ evaluate solver ~formula:(register_formula_s struc solver phi) struc
let evaluate_real = evaluate_real
let evaluate_partial struc intpr phi =
- evaluate_partial_aset solver ~formula:(register_formula_s solver phi)
+ evaluate_partial_aset solver ~formula:(register_formula_s struc solver phi)
struc intpr
let check struc phi =
- check solver ~formula:(register_formula_s solver phi) struc
+ check solver ~formula:(register_formula_s struc solver phi) struc
let get_real_val re struc = get_real_val_cache solver struc re
let formula_str phi =
(* let phi = Hashtbl.find solver.formulas_check phi in *)
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Solver/SolverTest.ml 2011-03-24 18:05:50 UTC (rev 1387)
@@ -259,7 +259,7 @@
] ;;
-let a () =
+let a =
match test_filter [""] tests with
| Some tests -> Aux.run_test_if_target "SolverTest" tests
| None -> ()
Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Solver/Structure.ml 2011-03-24 18:05:50 UTC (rev 1387)
@@ -57,6 +57,12 @@
(* ----------------------- BASIC HELPER FUNCTIONS --------------------------- *)
+(* Number of tuples in a relation. *)
+let rel_size struc rel =
+ try
+ Tuples.cardinal (StringMap.find rel struc.relations)
+ with Not_found -> 0
+
(* Reverse a map: make a string IntMap from an int StringMap. *)
let rev_string_to_int_map map =
StringMap.fold (fun n e m -> IntMap.add e n m) map IntMap.empty
Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli 2011-03-24 16:08:04 UTC (rev 1386)
+++ trunk/Toss/Solver/Structure.mli 2011-03-24 18:05:50 UTC (rev 1387)
@@ -34,6 +34,8 @@
(** {2 Basic helper functions} *)
+(** Size of a relation, i.e. number of tuples in it. *)
+val rel_size : structure -> string -> int
(** Reverse a map: make a string IntMap from an int StringMap. *)
val rev_string_to_int_map : int StringMap.t -> string IntMap.t
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
