[Toss-devel-svn] SF.net SVN: toss:[1684] trunk/Toss

[<luk...@us...>]

Revision: 1684
          http://toss.svn.sourceforge.net/toss/?rev=1684&view=rev
Author:   lukaszkaiser
Date:     2012-03-08 01:17:02 +0000 (Thu, 08 Mar 2012)
Log Message:
-----------
Using Bitvectors for unary predicates and assignments.

Modified Paths:
--------------
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/Learn/Distinguish.ml
    trunk/Toss/Solver/AssignmentSet.ml
    trunk/Toss/Solver/AssignmentSet.mli
    trunk/Toss/Solver/Assignments.ml
    trunk/Toss/Solver/Num/Bitvector.ml
    trunk/Toss/Solver/Num/Bitvector.mli
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/SolverTest.ml
    trunk/Toss/Solver/Structure.ml
    trunk/Toss/Solver/Structure.mli
    trunk/Toss/Solver/StructureTest.ml

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Arena/DiscreteRule.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -296,6 +296,8 @@
 	List.map
 	  (fun tp->List.map2 (fun v e->v,e) vars tp) tuples
     | AssignmentSet.Empty -> []
+    | AssignmentSet.FOUn _ as x ->
+      enumerate_asgns all_elems vars  (AssignmentSet.expand_unary x)
     | AssignmentSet.FO (v, els) ->
       let vars = list_remove v vars in
       concat_map (fun (e,sub)->
@@ -780,8 +782,7 @@
       (Structure.relations rule_src.lhs_struc) [] in
   let rhs_rels = SSMap.fold
     (fun rel tups rels ->
-      if STups.is_empty tups then rels
-      else
+      if STups.is_empty tups then rels else
         (rel, List.map opt_map (STups.elements tups)) :: rels)
     (Structure.relations rule_src.rhs_struc) [] in
   let nondistinct, lhs_rels =

Modified: trunk/Toss/Learn/Distinguish.ml
===================================================================
--- trunk/Toss/Learn/Distinguish.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Learn/Distinguish.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -313,7 +313,7 @@
     | FO -> ntypes s ~qr ~k
     | ExFO -> ntypes ~existential:true s ~qr ~k in
   let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
-  LOG 1 "distinguish_upto:\t neg types done";
+  LOG 1 "distinguish_upto:\t neg types done (%i): " (List.length neg_tps);
   let fails_on_negs f = not (List.exists (fun s-> check s [||] f) neg_strucs) in
   let extend_by_pos acc struc =
     if check struc [||] (Or acc) then acc else 

Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/AssignmentSet.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -15,11 +15,18 @@
 type assignment_set = 
   | Empty 
   | Any
+  | FOUn of string * Bitvector.bitvector
   | FO of string * (int * assignment_set) list
   | MSO of string * ((Elems.t * Elems.t) * assignment_set) list
   | Real of (Poly.polynomial * Formula.sign_op) list list
 
 
+let expand_unary = function
+  | FOUn (v, bv) -> 
+    FO (v, List.rev_map (fun i -> (i, Any)) (Bitvector.to_rev_list bv))
+  | x -> x
+
+
 (* --------------------- PRINTING AND HELPER FUNCTIONS --------------------- *)
 
 (* Variables assigned in an assignement set. *)
@@ -29,6 +36,7 @@
 
 let rec assigned_vars acc = function
   | Empty | Any -> acc
+  | FOUn (v, _) -> (`FO v) :: acc
   | FO (v, l) -> assigned_vars_list assigned_vars ((`FO v) :: acc) l
   | MSO (v, l) -> assigned_vars_list assigned_vars ((`MSO v) :: acc) l
   | _ -> failwith "AssignmentSet:assigned vars not implemented for reals"
@@ -50,6 +58,7 @@
 let rec str = function
   | Empty -> "{}"
   | Any -> "T"
+  | FOUn _ as x -> str (expand_unary x)
   | FO (v, map) ->
     let estr (e, a) = 
       if a = Any then v ^ "->" ^ (string_of_int e) else
@@ -70,6 +79,7 @@
 let rec named_str struc = function
   | Empty -> "{}"
   | Any -> "T"
+  | FOUn _ as x -> named_str struc (expand_unary x)
   | FO (v, map) ->
     let estr (e, a) = 
       if a = Any then v ^ "->" ^ (Structure.elem_str struc e) else
@@ -95,6 +105,7 @@
 let rec choose_fo default = function
   | Empty -> raise Not_found
   | Any -> default
+  | FOUn _ as x -> choose_fo default (expand_unary x)
   | FO (v, []) when List.mem_assoc v default -> raise Not_found
   | FO (v, (e, sub)::_) when e < 0 && List.mem_assoc v default ->
     (v, List.assoc v default) :: choose_fo (List.remove_assoc v default) sub
@@ -113,6 +124,7 @@
     List.rev_map Array.of_list 
       (Aux.product
 	 (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
+  | FOUn _ as x -> tuples elems vars (expand_unary x)
   | FO (v, (e,other_aset)::asg_list) when e < 0 ->
     let asg_list = List.map (fun e ->
       e, try List.assoc e asg_list with Not_found -> other_aset)
@@ -143,6 +155,7 @@
       let tuples = Aux.product elems in
       List.map (List.combine vars) tuples
   | Empty -> []
+  | FOUn _ as x -> fo_assgn_to_list all_elems vars (expand_unary x)
   | FO (v, (e,other_aset)::els) when e < 0 ->
     let vars = Aux.list_remove (`FO v) vars in
     let other_res =

Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/AssignmentSet.mli	2012-03-08 01:17:02 UTC (rev 1684)
@@ -11,12 +11,15 @@
 type assignment_set = 
   | Empty 
   | Any
+  | FOUn of string * Bitvector.bitvector
   | FO of string * (int * assignment_set) list
   | MSO of string * 
       ((Structure.Elems.t * Structure.Elems.t) * assignment_set) list
   | Real of (Poly.polynomial * Formula.sign_op) list list
 
+val expand_unary : assignment_set -> assignment_set
 
+
 (** {2 Printing and small helper functions.} *)
 
 (** Variables assigned in an assignement set. *)

Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Assignments.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -6,6 +6,7 @@
 
 open Structure
 open AssignmentSet
+open Bitvector
 
 
 (* ----------------------- BASIC TYPE DEFINITION -------------------------- *)
@@ -97,57 +98,64 @@
     | (Empty, _) | (_, Empty) -> Empty
     | (Any, a) -> a
     | (a, Any) -> a
+    | (FOUn (v1, bv1), FOUn (v2, bv2)) when v1 = v2 -> 
+      let bv = bv1 &&& bv2 in if is_empty bv then Empty else FOUn (v1, bv)
+    | (FO (v1, map1), FOUn (v2, _)) when compare_vars v1 v2 < 0 ->
+      fo_map v1 (join aset2) map1
+    | (FOUn (v1, _), FO (v2, map2)) when compare_vars v1 v2 > 0 ->
+      fo_map v2 (join aset1) map2
+    | (FOUn _, _) -> join (expand_unary aset1) aset2
+    | (_, FOUn _ ) -> join aset1 (expand_unary aset2)
     | (FO (v1, map1), FO (v2, map2)) -> (
       match compare_vars v1 v2 with
-            0 -> 
-              let res_map = List.rev (join_maps_rev [] (map1, map2)) in
-		if res_map = [] then Empty else FO (v1, res_map)
-	  | x when x < 0 -> fo_map v1 (join aset2) map1
-	  | x -> fo_map v2 (join aset1) map2
-      )
+        | 0 -> 
+          let res_map = List.rev (join_maps_rev [] (map1, map2)) in
+	  if res_map = [] then Empty else FO (v1, res_map)
+	| x when x < 0 -> fo_map v1 (join aset2) map1
+	| x -> fo_map v2 (join aset1) map2
+    )
     | (FO (v, map), MSO _) -> fo_map v (join aset2) map
     | (FO (v, map), Real _) -> fo_map v (join aset2) map
     | (MSO _, FO (v, map)) -> fo_map v (join aset1) map
     | (Real _, FO (v, map)) -> fo_map v (join aset1) map
     | (MSO (v1, disj1), MSO (v2, disj2)) -> (
 	match compare_vars (v1) (v2) with
-             0 -> 
-               let res_disj = small_simp (join_disj [] disj1 disj2) in
-		 if res_disj = [] then Empty else MSO (v1, res_disj)
-	   | x when x < 0 -> mso_map v1 (join aset2) disj1
-	   | x -> mso_map v2 (join aset1) disj2
-      )
+          | 0 -> 
+            let res_disj = small_simp (join_disj [] disj1 disj2) in
+	    if res_disj = [] then Empty else MSO (v1, res_disj)
+	  | x when x < 0 -> mso_map v1 (join aset2) disj1
+	  | x -> mso_map v2 (join aset1) disj2
+    )
     | (MSO (v, disj), Real _) -> mso_map v (join aset2) disj
     | (Real _, MSO (v, disj)) -> mso_map v (join aset1) disj
     | (Real poly_dnf1, Real poly_dnf2) -> 
-        let app_2 l p = List.rev_append 
-          (List.rev_map (fun q -> List.rev_append p q) poly_dnf2) l in
-        let all_polys = List.fold_left app_2 [] poly_dnf1 in
-        let poly_dnf = List.filter RealQuantElim.sat all_polys in
-          if poly_dnf = [] then Empty else Real (poly_dnf)
+      let app_2 l p = List.rev_append 
+        (List.rev_map (fun q -> List.rev_append p q) poly_dnf2) l in
+      let all_polys = List.fold_left app_2 [] poly_dnf1 in
+      let poly_dnf = List.filter RealQuantElim.sat all_polys in
+      if poly_dnf = [] then Empty else Real (poly_dnf)
 
 and join_maps_rev acc = function
   | ([], _) -> acc
   | (_, []) -> acc
   | ((e1, a1) :: r1, (e2, a2) :: r2) ->
-      match compare_elems e1 e2 with
-	  0 -> 
-	    let a = join a1 a2 in
-	      if a = Empty then join_maps_rev acc (r1, r2) else
-		join_maps_rev ((e1, a) :: acc) (r1, r2)
-	| x when x < 0 -> join_maps_rev acc (r1, ((e2, a2) :: r2))
-	| x -> join_maps_rev acc (((e1, a1) :: r1), r2)
+    match compare_elems e1 e2 with
+      | 0 -> 
+	let a = join a1 a2 in
+	if a = Empty then join_maps_rev acc (r1, r2) else
+	  join_maps_rev ((e1, a) :: acc) (r1, r2)
+      | x when x < 0 -> join_maps_rev acc (r1, ((e2, a2) :: r2))
+      | x -> join_maps_rev acc (((e1, a1) :: r1), r2)
 
 and join_disj acc disj1 = function
   | [] -> acc
   | ((pos2, neg2), a2) :: rest ->
-      let adjoin_one acc ((pos1, neg1), a1) =
-        let (pos, neg) = (Elems.union pos2 pos1, Elems.union neg2 neg1) in
-          if Elems.is_empty (Elems.inter pos neg) then 
-            ((pos, neg), join a1 a2) :: acc
-          else acc 
-      in
-        join_disj (List.fold_left adjoin_one acc disj1) disj1 rest
+    let adjoin_one acc ((pos1, neg1), a1) =
+      let (pos, neg) = (Elems.union pos2 pos1, Elems.union neg2 neg1) in
+      if Elems.is_empty (Elems.inter pos neg) then 
+        ((pos, neg), join a1 a2) :: acc
+      else acc in
+    join_disj (List.fold_left adjoin_one acc disj1) disj1 rest
 
 
 (* ------------------------------ EQUAL -------------------------------- *)
@@ -155,6 +163,11 @@
 (* Enforce [aset] and additionally that the FO variable [v] is set to [e]. *)
 let rec set_equal uneq els v e = function
   | Empty -> Empty
+  | FOUn (u, b) when u = v ->
+    let nb = if uneq then clear_bit b e else 
+	if get_bit b e then set_bit empty e else empty in
+    if is_empty nb then Empty else FOUn (u, nb)
+  | FOUn _ as x -> set_equal uneq els v e (expand_unary x)
   | FO (u, map) as aset -> (
       match compare_vars u v with
         | 0 -> 
@@ -180,6 +193,7 @@
 (* Enforce that in [aset] the variable [u] is equal to [w]; assumes u < w. *)
 let rec eq_vars uneq els u w = function
   | Empty -> Empty
+  | FOUn _ as x -> eq_vars uneq els u w (expand_unary x)
   | FO (v, map) as aset -> (
     match compare_vars v u with
       | 0 -> 
@@ -226,6 +240,11 @@
     | (Any, _) | (_, Any) -> Any
     | (Empty, a) -> a
     | (a, Empty) -> a
+    | (FOUn (v1, bv1), FOUn (v2, bv2)) when v1 = v2 -> 
+      let bv = bv1 ||| bv2 in 
+      if nbr_set_bits bv = sllen elems then Any else FOUn (v1, bv)
+    | (FOUn _, _) -> sum elems (expand_unary aset1) aset2
+    | (_, FOUn _) -> sum elems aset1 (expand_unary aset2)
     | (FO (v1, map1), FO (v2, map2)) -> (
 	match compare_vars v1 v2 with
 	  | 0 -> 
@@ -302,6 +321,7 @@
 let rec project elems v = function
     | Empty -> Empty
     | Any -> Any
+    | FOUn (u, _) as x -> if u = v then Any else x
     | FO (u, m) when u = v -> (* Sum the assignments below *)
       List.fold_left (fun s (_, a) -> sum elems s a) Empty m
     | FO (u, m) -> 
@@ -344,6 +364,8 @@
 let rec universal elems v = function
   | Empty -> Empty
   | Any -> Any
+  | FOUn (u, b) as x ->
+    if u <> v then x else if nbr_set_bits b < sllen elems then Empty else Any
   | FO (u, m) when u = v -> (* Join the assignments below *)
     if List.length m < sllen elems then Empty else
       List.fold_left (fun s (_, a) -> join s a) Any m
@@ -390,6 +412,7 @@
 let rec complement elems = function
   | Empty -> Any
   | Any -> Empty
+  | FOUn _ as x -> complement elems (expand_unary x)
   | FO (v, map) -> 
     let compl_map = 
       List.rev (complement_map_rev elems [] (slist elems, map)) in
@@ -447,6 +470,8 @@
     | (Empty, _) | (_, Any) -> Empty
     | (Any, a) -> complement elems a
     | (a, Empty) -> a
+    | (FOUn _ as x, y) -> complement_join elems (expand_unary x) y
+    | (x, (FOUn _ as y)) -> complement_join elems x (expand_unary y)
     | (FO (v1, map1), FO (v2, map2)) when v1 = v2 ->
         let resm = List.rev (complement_join_map_rev elems [] (map1, map2)) in
 	if resm = [] then Empty else FO (v1, resm)
@@ -507,6 +532,8 @@
 let rec join_rel aset vars tuples_set incidence_map all_elems =
   match aset with (* TODO: better use of incidence map? *)
     | Empty -> Empty
+    | FOUn (v, _) when Aux.array_mem v vars ->
+      join_rel (expand_unary aset) vars tuples_set incidence_map all_elems
     | FO (v, map) when Aux.array_mem v vars -> 
       let tps e =
 	if e < Array.length incidence_map then incidence_map.(e) else 
@@ -529,8 +556,15 @@
   | (_, a1) :: (((_, a2) :: _) as r) when a1 = a2 -> same_asg r
   | _ -> false
 
+let rec all_any = function
+  | [] -> true
+  | (_, a) :: rest when a = Any -> all_any rest
+  | _ -> false
+
 let rec compress no_elems = function
   | FO (v, map) when List.length map = no_elems && same_asg map ->
     compress no_elems (snd (List.hd map))
+  | FO (v, map) when all_any map -> 
+    FOUn (v, Bitvector.of_list (List.rev_map fst map))
   | FO (v, map) -> FO (v, map_snd (compress no_elems) map)
   | x -> x

Modified: trunk/Toss/Solver/Num/Bitvector.ml
===================================================================
--- trunk/Toss/Solver/Num/Bitvector.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Num/Bitvector.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -6,6 +6,20 @@
 (* Empty bitvector. *)
 let empty = ref (Naturals.nat_of_int 0)
 
+(* Check if a bitvector is empty. *)
+let is_empty v = !v.(0) = 0 && Aux.array_for_all (fun i -> i = 0) !v
+
+(* Number of bits set in a vector. *)
+let nbr_set_bits v =
+  let res = ref 0 in
+  let add_bits_i i =
+    for j = 0 to MiscNum.length_of_int - 1 do
+      if 1 lsl (1 lsl j) > 0 then incr res;
+    done; in
+  Array.iter (fun i -> if i <> 0 then add_bits_i i) !v;
+  !res
+
+
 (* Helper function: coordinates of i-th bit *)
 let coord i = i / MiscNum.length_of_int, i mod MiscNum.length_of_int
 
@@ -37,16 +51,19 @@
 (* Mark the bits at positions given in the list. *)
 let of_list l = List.fold_left set_bit empty l
 
-(* The list of set bits. *)
-let to_list v =
+(* The list of set bits, in reverse order. *)
+let to_rev_list v =
   let r = Aux.range MiscNum.length_of_int in
   let list_bits p i = 
     Aux.map_some (fun j-> if i land (1 lsl j) > 0 then Some(j+p) else None) r in
-  let revbits_pos = List.fold_left (fun (listed, pos) i -> 
+  fst (List.fold_left (fun (listed, pos) i -> 
     (List.rev_append (list_bits pos i) listed, pos+MiscNum.length_of_int)
-  ) ([], 0) (Array.to_list !v) in
-  List.rev (fst revbits_pos)
+  ) ([], 0) (Array.to_list !v))
 
+(* The list of set bits. *)
+let to_list v = List.rev (to_rev_list v)
+
+
 (* Print the bit vector to string. *)
 let str v =
   let r = Aux.range MiscNum.length_of_int in

Modified: trunk/Toss/Solver/Num/Bitvector.mli
===================================================================
--- trunk/Toss/Solver/Num/Bitvector.mli	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Num/Bitvector.mli	2012-03-08 01:17:02 UTC (rev 1684)
@@ -5,6 +5,12 @@
 (** Empty bit vector. *)
 val empty : bitvector
 
+(** Check if a bitvector is empty. *)
+val is_empty : bitvector -> bool
+
+(** Number of bits set in a vector. *)
+val nbr_set_bits : bitvector -> int
+
 (** Get the bit at the given position. *)
 val get_bit : bitvector -> int -> bool
 
@@ -21,6 +27,9 @@
 (** The list of set bits. *)
 val to_list : bitvector -> int list
 
+(** The list of set bits, in reverse order. *)
+val to_rev_list : bitvector -> int list
+
 (** Print the bit vector to string. *)
 val str : bitvector -> string
 

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Solver.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -1,11 +1,11 @@
 (* Solver for checking if formulas hold on structures. *)
 
+open Bitvector
 open AssignmentSet
 open Assignments
 open Structure
 open Formula
 
-
 (* CACHE *)
 
 type cachetbl = 
@@ -78,7 +78,18 @@
 
 let get_formula solver i = Hashtbl.find solver.formulas_eval i
 
+let phi_rels phi =
+  let rels = ref [] in
+  let app_rel = function Rel (s, _) as r -> rels := s :: !rels; r | x -> x in
+  let app_re = function Fun _ -> raise Not_found | x -> x in
+  try 
+    let _ = FormulaMap.map_to_atoms_full app_rel app_re phi in
+    let rs = Aux.unique_sorted ~cmp:String.compare !rels in
+    LOG 2 "F: %s %s" (Formula.str phi) (String.concat ", " rs);
+    Some rs
+  with Not_found -> None
 
+
 (* ------------------------------ EVALUATION ------------------------------- *)
 
 (* Helper function: remove duplicates from sorted list of variables. *)
@@ -125,7 +136,12 @@
     if nxt = a then nxt else fixpnt v vs psi nxt in
   let simp a = Assignments.compress (Assignments.sllen elems) a in
   if aset = Empty then Empty else
+    let foun_var = match aset with FOUn (v,_) -> v | _ -> "" in
     match phi with
+      | Rel (relname, [|v|]) ->
+	let bv = Structure.pred_vector model relname in
+	if Bitvector.is_empty bv then Empty else
+	  report (join aset (FOUn (var_str v, bv)))
       | Rel (relname, vl) ->
 	let tuples_s = Structure.rel_graph relname model in
 	let inc_map = Structure.rel_incidence relname model in
@@ -166,14 +182,53 @@
         let (_, asets) = List.fold_left step_or (aset, []) fl in
         report (List.fold_left (sum elems) Empty asets)
       | Ex ([], phi) | All ([], phi) -> failwith "evaluating empty quantifier"
-      | Ex (vl, phi) ->
+      | Ex ([v], And (Rel (r1, v1):: Rel (r2, v2):: rest)) as ephi when
+	  foun_var <> "" && ( let vfo = to_fo v in (* an often occurring join *)
+	    (v1 = [|vfo|] && v2 = [|vfo; `FO foun_var|]) ||
+	      (v1 = [|vfo|] && v2 = [|`FO foun_var; vfo|]) ||
+	      (v2 = [|vfo|] && v1 = [|vfo; `FO foun_var|]) ||
+	      (v2 = [|vfo|] && v1 = [|`FO foun_var; vfo|]) ) &&
+	    not (List.mem (`FO foun_var) (FormulaSubst.free_vars (And rest)))->(
+	      LOG 1 "special join on %s for %s" foun_var (str ephi);
+	      let pred, rbin, vpred, vbin =
+		if Array.length v1= 1 then r1, r2, v1, v2 else r2, r1, v2, v1 in
+	      let othpos = if vpred.(0) = vbin.(0) then 0 else 1 in
+	      let inc_map = Structure.rel_incidence rbin model in
+	      let av = match aset with FOUn (_, av) -> av | _-> failwith "av" in
+	      let add_to_bitvec b e = 
+		if e >= Array.length inc_map then b else
+		  Tuples.fold (fun t b -> set_bit b t.(othpos)) inc_map.(e) b in
+	      let b0 = List.fold_left add_to_bitvec Bitvector.empty 
+		(Bitvector.to_rev_list av) in
+	      let b = b0 &&& (Structure.pred_vector model pred) in
+	      if Bitvector.is_empty b then Empty else
+		let r = eval fp model elems (FOUn (var_str v, b)) (And rest) in
+		if r = Empty then Empty else
+		  let ag = eval fp model elems r (Rel (rbin, vbin)) in
+		  report (simp (join aset (project_list elems ag [var_str v])))
+	    )
+      | Ex (vl, phi) as ephi ->
 	check_timeout "Solver.eval.Ex";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
-	let in_aset =
-	  if List.exists (fun v->List.mem v aset_vars) vl then Any else aset in
-        let phi_asgn = eval fp model elems in_aset phi in
-        report (simp (join aset 
-			(project_list elems phi_asgn (List.map var_str vl))))
+	if (fp = [] && 
+	    ((List.exists (fun v->List.mem v aset_vars) vl) ||
+		(aset_vars <> [] && FormulaSubst.free_vars ephi = []))) then
+	  let phi_asgn = 
+	    try
+	      let (res, _) = Hashtbl.find !cache_results phi in
+	      LOG 2 "In-Eval found in cache: %s" (Formula.str phi);
+	      res
+	    with Not_found ->
+	      LOG 1 "In-Eval_m %s" (str phi);
+	      let phi_asgn = eval fp model elems Any phi in
+	      Hashtbl.add !cache_results phi (phi_asgn, phi_rels phi);
+	      phi_asgn in
+          report (simp (join aset 
+			  (project_list elems phi_asgn (List.map var_str vl))))
+	else
+          let phi_asgn = eval fp model elems aset phi in
+          report (simp (join aset 
+			  (project_list elems phi_asgn (List.map var_str vl))))
       | All (vl, phi) ->
 	check_timeout "Solver.eval.All";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
@@ -217,8 +272,8 @@
   let fo_vars_real re = 
     remove_dup_vars [] (List.sort compare_vars (fo_vars_r_rec re)) in
   let rec sum_polys = function
-      Empty -> Poly.Const 0.
-    | Any -> failwith "absolute assignement for sum, impossible to calculate"
+    | Empty -> Poly.Const 0.
+    | Any | FOUn _ -> failwith "absolute assignement for sum,impossible to calc"
     | FO (_, alist) ->
         let addp p (_, a) = Poly.Plus (p, sum_polys a) in
         List.fold_left addp (Poly.Const 0.) alist
@@ -292,17 +347,6 @@
 	(b, pair :: nl)
 
 
-let phi_rels phi =
-  let rels = ref [] in
-  let app_rel = function Rel (s, _) as r -> rels := s :: !rels; r | x -> x in
-  let app_re = function Fun _ -> raise Not_found | x -> x in
-  try 
-    let _ = FormulaMap.map_to_atoms_full app_rel app_re phi in
-    let rs = Aux.unique_sorted ~cmp:String.compare !rels in
-    LOG 2 "F: %s %s" (Formula.str phi) (String.concat ", " rs);
-    Some rs
-  with Not_found -> None
-
 let re_rels re =
   let rels = ref [] in
   let app_rel = function Rel (s, _) as r -> rels := s :: !rels; r | x -> x in

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/SolverTest.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -36,6 +36,8 @@
 let tests = "Solver" >::: [
   "eval: first-order quantifier free" >::
     (fun () ->
+      eval_eq "[ | P { (1) }; R:1 {} | ]" "P(x0)" "{ x0->1 }";
+      eval_eq "[ | P:1 {}; R { (1) } | ]" "P(x0)" "{}";
       eval_eq "[ | R { (a, b); (a, c) } | ]" "x = y" 
 	"{ y->1{ x->1 } , y->2{ x->2 } , y->3{ x->3 }  }";
       eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y"

Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Structure.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -50,7 +50,8 @@
 type structure = {
   rel_signature    : int StringMap.t ;
   elements     : Elems.t ;
-  relations    : Tuples.t StringMap.t ;
+  predicates   : Bitvector.bitvector StringMap.t ; (* unary relations *)
+  relations    : Tuples.t StringMap.t ; (* binary (or more-ary) relations *)
   functions    : (float IntMap.t) StringMap.t ;
   incidence    : (TIntMap.t) StringMap.t ;
   names        : int StringMap.t ;
@@ -62,12 +63,14 @@
 
 let compare s1 s2 =
   if s1 == s2 then 0 else
-    let c = StringMap.compare Tuples.compare s1.relations s2.relations in
+    let c = Elems.compare s1.elements s2.elements in
     if c <> 0 then c else
-      let d = Elems.compare s1.elements s2.elements in
+      let d = StringMap.compare Tuples.compare s1.relations s2.relations in
       if d <> 0 then d else
-        StringMap.compare (IntMap.compare Pervasives.compare)
-          s1.functions s2.functions
+	let e = StringMap.compare Pervasives.compare s1.predicates s2.predicates
+	in if e <> 0 then e else
+            StringMap.compare (IntMap.compare Pervasives.compare)
+              s1.functions s2.functions
 
 let equal s1 s2 = (compare s1 s2 = 0)
 
@@ -80,15 +83,21 @@
 let inv_names s = s.inv_names
 let replace_names s nms inms = { s with names = nms; inv_names = inms }
 let functions s = s.functions
-let relations s = s.relations
+let tuples_of_bitvec b =
+  let append_sg tps e = Tuples.add [|e|] tps in
+  List.fold_left append_sg Tuples.empty (Bitvector.to_rev_list b)
+let relations s = StringMap.fold (fun pred bv acc ->
+  StringMap.add pred (tuples_of_bitvec bv) acc) s.predicates s.relations
 
+
 (* ----------------------- 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
+  try Tuples.cardinal (StringMap.find rel struc.relations)
+  with Not_found ->
+    try Bitvector.nbr_set_bits (StringMap.find rel struc.predicates)
+    with Not_found -> 0
 
 (* Reverse a map: make a string IntMap from an int StringMap. *)
 let rev_string_to_int_map map =
@@ -101,6 +110,7 @@
 (* Return the empty structure. *)
 let empty_structure () = {
   elements = Elems.empty ;
+  predicates = StringMap.empty ;
   relations = StringMap.empty ;
   functions = StringMap.empty ;
   incidence = StringMap.empty ;
@@ -110,28 +120,39 @@
 }
   
 let rel_signature struc =
-  StringMap.fold (fun r ar si -> (r,ar)::si)
-    struc.rel_signature []
+  StringMap.fold (fun r ar si -> (r,ar)::si) struc.rel_signature []
 
 let rel_sizes struc =
-  StringMap.fold (fun r tups si -> (r,Tuples.cardinal tups)::si)
-    struc.relations []
+  let rs = StringMap.fold (fun r tups si -> (r, Tuples.cardinal tups)::si)
+    struc.relations [] in
+  StringMap.fold (fun r bv si -> (r, Bitvector.nbr_set_bits bv)::si)
+    struc.predicates rs
+  
+let pred_vector struc pred = 
+  try StringMap.find pred struc.predicates with Not_found -> Bitvector.empty
 
-
 (* Return the list of relation tuples incident to an element [e] in [struc]. *)
 let incident struc e =
   let acc_incident rname inc_map acc = 
     let tps = TIntMap.find e inc_map in
     if Tuples.is_empty tps then acc else (rname, Tuples.elements tps) :: acc in
-  StringMap.fold acc_incident struc.incidence []
+  let acc_inc_pred pred bv acc =
+    if Bitvector.get_bit bv e then (pred, [[|e|]]) :: acc else acc in
+  StringMap.fold acc_inc_pred struc.predicates 
+    (StringMap.fold acc_incident struc.incidence [])
 
 
 (* Check if a relation holds for a tuple. *)
 let check_rel struc rel tp =
-  try
-    let tups = StringMap.find rel struc.relations in
-    Tuples.mem tp tups
-  with Not_found -> false
+  if Array.length tp > 1 then
+    try
+      let tups = StringMap.find rel struc.relations in
+      Tuples.mem tp tups
+    with Not_found -> false
+  else
+    try
+      Bitvector.get_bit (StringMap.find rel struc.predicates) tp.(0)
+    with Not_found -> false
 
 (* Return the value of function [f] on [e] in [struc]. *)
 let fun_val struc f e =
@@ -146,7 +167,9 @@
 (* Find a relation in a model. *)
 let rel_graph relname model =
   try StringMap.find relname model.relations
-  with Not_found -> Tuples.empty
+  with Not_found -> 
+    try tuples_of_bitvec (StringMap.find relname model.predicates)
+    with Not_found -> Tuples.empty
 
 (* Incidences of a relation in a model. *)
 let rel_incidence relname model = 
@@ -218,53 +241,54 @@
 (* Ensure relation named [rn] exists in [struc], check arity, add the
    relation if needed. *)
 let add_rel_name rn arity struc =
-  if StringMap.mem rn struc.relations then
-    let old_arity = StringMap.find rn struc.rel_signature in
-    if arity <> old_arity then
-      raise (Structure_mismatch
-               (Printf.sprintf
-                  "arity mismatch for %s: expected %d, given %d"
-                  rn old_arity arity));
-    struc
+  if arity = 1 then 
+    if StringMap.mem rn struc.predicates then struc else
+      { struc with rel_signature = StringMap.add rn 1 struc.rel_signature;
+	predicates = StringMap.add rn Bitvector.empty struc.predicates; }
   else
-    { struc with
-      rel_signature = StringMap.add rn arity struc.rel_signature;
-      relations = StringMap.add rn Tuples.empty struc.relations;
-      incidence = StringMap.add rn TIntMap.empty struc.incidence; }
+    if StringMap.mem rn struc.relations then
+      let old_arity = StringMap.find rn struc.rel_signature in
+      if arity <> old_arity then
+	raise (Structure_mismatch
+		 (Printf.sprintf "arity mismatch for %s: expected %d, given %d"
+                    rn old_arity arity));
+      struc
+    else
+      { struc with
+	rel_signature = StringMap.add rn arity struc.rel_signature;
+	relations = StringMap.add rn Tuples.empty struc.relations;
+	incidence = StringMap.add rn TIntMap.empty struc.incidence; }
 
 let empty_with_signat signat =
-  List.fold_right (fun (rn,ar) -> add_rel_name rn ar) signat
+  List.fold_right (fun (rn, ar) -> add_rel_name rn ar) signat
     (empty_structure ())
 
-(* Add empty relation named [rn] to [struc], with given arity,
-   regardless of whether it already existed. *)
-let force_add_rel_name rn arity struc =
-  { struc with
-    rel_signature = StringMap.add rn arity struc.rel_signature;
-    relations = StringMap.add rn Tuples.empty struc.relations;
-    incidence = StringMap.add rn TIntMap.empty struc.incidence; }
-
 (* Add tuple [tp] to relation [rn] in structure [struc]. *)
 let add_rel struc rn tp =
   let new_struc =
     Array.fold_left (fun struc e -> add_elem struc e)
       (add_rel_name rn (Array.length tp) struc) tp in
-  let add_to_relmap rmap = 
-    let tps = StringMap.find rn rmap in
-    StringMap.add rn (Tuples.add tp tps) rmap in
-  let new_rel = add_to_relmap new_struc.relations in
-  let add_to_imap imap e = 
-    try
-      TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
-    with Not_found -> 
-      TIntMap.add e (Tuples.singleton tp) imap  in
-  let new_incidence_imap = 
-    try
-      Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
-    with Not_found -> 
-      Array.fold_left add_to_imap TIntMap.empty tp in
-  let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
-    { new_struc with relations = new_rel ; incidence = new_incidence }
+  if Array.length tp = 1 then (
+    let b = StringMap.find rn new_struc.predicates in
+    let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) new_struc.predicates
+    in { new_struc with predicates = np; }
+  ) else
+    let add_to_relmap rmap = 
+      let tps = StringMap.find rn rmap in
+      StringMap.add rn (Tuples.add tp tps) rmap in
+    let new_rel = add_to_relmap new_struc.relations in
+    let add_to_imap imap e = 
+      try
+	TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+      with Not_found -> 
+	TIntMap.add e (Tuples.singleton tp) imap  in
+    let new_incidence_imap = 
+      try
+	Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
+      with Not_found -> 
+	Array.fold_left add_to_imap TIntMap.empty tp in
+    let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence
+    in { new_struc with relations = new_rel ; incidence = new_incidence }
 
 (* Add tuple [tp] to relation [rn] in structure [struc]. *)
 let add_rel_named_elems struc rn tp =
@@ -274,26 +298,31 @@
       struc, e::tp) tp
       ((add_rel_name rn (Array.length tp) struc), []) in
   let tp = Array.of_list tp in
-  let add_to_relmap rmap = 
-    let tps = StringMap.find rn rmap in
-    StringMap.add rn (Tuples.add tp tps) rmap in
-  let new_rel = add_to_relmap new_struc.relations in
-  let add_to_imap imap e = 
-    try
-      TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
-    with Not_found -> 
-      TIntMap.add e (Tuples.singleton tp) imap  in
-  let new_incidence_imap = 
-    try
-      Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
-    with Not_found -> 
-      Array.fold_left add_to_imap TIntMap.empty tp in
-  let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
-    { new_struc with relations = new_rel ; incidence = new_incidence }
+  if Array.length tp = 1 then (
+    let b = StringMap.find rn new_struc.predicates in
+    let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) new_struc.predicates
+    in { new_struc with predicates = np; }
+  ) else
+    let add_to_relmap rmap = 
+      let tps = StringMap.find rn rmap in
+      StringMap.add rn (Tuples.add tp tps) rmap in
+    let new_rel = add_to_relmap new_struc.relations in
+    let add_to_imap imap e = 
+      try
+	TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+      with Not_found -> 
+	TIntMap.add e (Tuples.singleton tp) imap  in
+    let new_incidence_imap = 
+      try
+	Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
+      with Not_found -> 
+	Array.fold_left add_to_imap TIntMap.empty tp in
+    let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence 
+    in { new_struc with relations = new_rel ; incidence = new_incidence }
 
 
-(* Return a structure with a single relation, over a single tuple, of
-   different elements. *)
+(* Return a structure with a single relation, over a single tuple,
+   of different elements. *)
 let free_for_rel rel arity =
   let tup = Array.init arity (fun i->i+1) in
   add_rel (empty_structure ()) rel tup
@@ -302,20 +331,25 @@
    checking whether it and its elements already exist in the structure
    and without checking arity. *)
 let unsafe_add_rel struc rn tp =
-  let new_rel =
+  if Array.length tp = 1 then (
+    let b = StringMap.find rn struc.predicates in
+    let np = StringMap.add rn (Bitvector.set_bit b tp.(0)) struc.predicates
+    in { struc with predicates = np; }
+  ) else
+    let new_rel =
       let tps = StringMap.find rn struc.relations in
       StringMap.add rn (Tuples.add tp tps) struc.relations in
-  let add_to_imap imap e = 
-    try
-      TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
-    with Not_found -> 
-      TIntMap.add e (Tuples.singleton tp) imap  in
-  let new_incidence_imap = 
-    try
-      Array.fold_left add_to_imap (StringMap.find rn struc.incidence) tp
-    with Not_found -> 
-      Array.fold_left add_to_imap TIntMap.empty tp in
-  let new_incidence = StringMap.add rn new_incidence_imap struc.incidence in
+    let add_to_imap imap e = 
+      try
+	TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
+      with Not_found -> 
+	TIntMap.add e (Tuples.singleton tp) imap  in
+    let new_incidence_imap = 
+      try
+	Array.fold_left add_to_imap (StringMap.find rn struc.incidence) tp
+      with Not_found -> 
+	Array.fold_left add_to_imap TIntMap.empty tp in
+    let new_incidence = StringMap.add rn new_incidence_imap struc.incidence in
     { struc with relations = new_rel ; incidence = new_incidence }
 
 
@@ -407,17 +441,22 @@
 
 (* Remove the tuple [tp] from relation [rn] in structure [struc]. *)
 let del_rel struc rn tp = 
-  let del_rmap rmap = 
-    try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap
-    with Not_found -> rmap in
-  let new_rel = del_rmap struc.relations in  
-  let del_imap imap e = 
-    try TIntMap.add e (Tuples.remove tp (TIntMap.find e imap)) imap
-    with Not_found -> imap in
-  let new_incidence = 
-    let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp in
-    StringMap.add rn imap struc.incidence in
-  { struc with relations = new_rel ; incidence = new_incidence }
+  if Array.length tp = 1 then (
+    let b = StringMap.find rn struc.predicates in
+    let np = StringMap.add rn (Bitvector.clear_bit b tp.(0)) struc.predicates
+    in { struc with predicates = np; }
+  ) else
+    let del_rmap rmap = 
+      try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap
+      with Not_found -> rmap in
+    let new_rel = del_rmap struc.relations in  
+    let del_imap imap e = 
+      try TIntMap.add e (Tuples.remove tp (TIntMap.find e imap)) imap
+      with Not_found -> imap in
+    let new_incidence = 
+      let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp
+      in StringMap.add rn imap struc.incidence in
+    { struc with relations = new_rel ; incidence = new_incidence }
 
 (* Remove the tuples [tps] from relation [rn] in structure [struc]. *)
 let del_rels struc rn tps = 
@@ -425,26 +464,24 @@
 
 (* Remove the given relation [rn] in [struc]. *)
 let clear_rel remove_from_sig struc rn =
-  let new_rels = StringMap.remove rn struc.relations in
-  let new_inc = StringMap.remove rn struc.incidence in
-  let new_rel_sig =
-    if remove_from_sig then
+  let new_rel_sig = if remove_from_sig then
       StringMap.remove rn struc.rel_signature
     else struc.rel_signature in
-  { struc with relations = new_rels ; incidence = new_inc ;
-    rel_signature = new_rel_sig }
+  if StringMap.find rn struc.rel_signature = 1 then
+    let np = StringMap.remove rn struc.predicates in
+    { struc with predicates = np; rel_signature = new_rel_sig }
+  else
+    let new_rels = StringMap.remove rn struc.relations in
+    let new_inc = StringMap.remove rn struc.incidence in
+    { struc with relations = new_rels ; incidence = new_inc ;
+      rel_signature = new_rel_sig }
 
 (* Remove all relations that meet predicate [p] in [struc]. *)
 let clear_rels ?(remove_from_sig=true) struc p =
   let p_rels = ref [] in
   let _ = StringMap.iter (fun r _ -> if p r then p_rels := r :: !p_rels)
-    struc.relations in
+    struc.rel_signature in
   List.fold_left (clear_rel remove_from_sig) struc !p_rels
-(*  {struc with
-    relations = StringMap.mapi (fun rel tups ->
-      if p rel then Tuples.empty else tups) struc.relations;
-    incidence = StringMap.mapi (fun rel inctups ->
-      if p rel then IntMap.empty else inctups) struc.incidence} *)
 
 (* Remove the element [e] and all incident relation tuples from [struc]. *)
 let del_elem struc e =
@@ -452,8 +489,8 @@
   let del_rels_struc = 
     List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
   let del_fun fmap = IntMap.remove e fmap in
-    { del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
-        functions = StringMap.map del_fun del_rels_struc.functions ; }
+  { del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
+    functions = StringMap.map del_fun del_rels_struc.functions ; }
 
 (* Remove the elements [es] and all incident relation tuples from
    [struc]; return the deleted relation tuples. *)
@@ -569,10 +606,10 @@
       (fun rn ts ->
         if show_empty || not (Tuples.is_empty ts) then
           rel_s := !rel_s ^ "; " ^ rel_str struc rn ts)
-      struc.relations;
+      (relations struc);
     StringMap.iter
       (fun fn vals -> fun_s := !fun_s ^ "; " ^ fun_str struc fn vals)
-      struc.functions;
+      (functions struc);
     "[" ^ elem_s ^ " | " ^ (omit 2 !rel_s) ^ " | " ^ (omit 2 !fun_s) ^ "]"
 
 (** {2 Printing of rectangular boards.}
@@ -964,17 +1001,8 @@
               let tup = [|elem|] in
               let predicates = List.filter
                 (fun pred ->
-                  let tmap =
-                    try StringMap.find pred !ret.relations
-                    with Not_found -> Tuples.empty in
-                  Tuples.mem tup tmap &&
-                    let rmap =
-                      try StringMap.find pred !ret.incidence
-                      with Not_found -> TIntMap.empty in
-                    not (Tuples.is_empty (
-                      try TIntMap.find elem rmap
-                      with Not_found -> Tuples.empty)))
-                all_predicates in
+                  try Tuples.mem tup (StringMap.find pred (relations !ret))
+                  with Not_found -> false) all_predicates in
               let up_line = String.make 3 ' '
               and lo_line = String.make 3 ' ' in
               if kind = `Plain then 
@@ -1046,16 +1074,16 @@
             else struc
           with Not_found -> struc in
         ret := List.fold_left clear_empty !ret ["x"; "y"; "vx"; "vy"];
-                  (* relations that are in the structure for the sake of
-                     signature, i.e. they're empty *)
+        (* relations that are in the structure for the sake of
+           signature, i.e. they're empty *)
         let signat_rels =
           StringMap.fold (fun rel tups acc ->
             if Tuples.is_empty tups then rel::acc else acc)
-            struc.relations [] in
+            (relations struc) [] in
         ret := clear_rels !ret (fun rel ->
           not (List.mem rel signat_rels) &&
             (try List.assoc rel uniq_long = rel with Not_found -> true) &&
-            try Tuples.is_empty (StringMap.find rel !ret.relations)
+            try Tuples.is_empty (StringMap.find rel (relations !ret))
             with Not_found -> true);
 	span_rels ^ init_pos ^ dx_dy ^ "\"\n" ^
           board ^ "\"",
@@ -1091,7 +1119,7 @@
     StringMap.fold (fun k v acc ->
       if show_empty || not (Tuples.is_empty v) then
         (k,v)::acc
-      else acc) struc.relations [] in
+      else acc) (relations struc) [] in
   let funs =
     StringMap.fold (fun k v acc -> (k,v)::acc) struc.functions [] in
   let rels = List.rev rels and funs = List.rev funs in
@@ -1141,8 +1169,9 @@
     with Not_found -> raise (Diff_result (
       "Element "^name^" not found in the "^other^" structure")) in
   Elems.iter (fun e -> ignore (map_elem e)) s1.elements;
+  let s2_relations = relations s2 in
   StringMap.iter (fun rel tups ->
-    (let try tups2 = StringMap.find rel s2.relations in
+    (let try tups2 = StringMap.find rel s2_relations in
      Tuples.iter (fun tup ->
        let tup2 = Array.map map_elem tup in
        if not (Tuples.mem tup2 tups2)
@@ -1155,7 +1184,7 @@
      ) tups
      with Not_found -> raise (Diff_result (
        "Relation "^rel^" not found in the "^other^" structure"))
-    )) s1.relations;
+    )) (relations s1);
   StringMap.iter (fun fn vals ->
     (let try vals2 = StringMap.find fn s2.functions in
      IntMap.iter (fun e v ->
@@ -1185,8 +1214,13 @@
 let diff_elems s1 s2 =
   let rels, _ = List.split (rel_signature s1) in
   let elems = Elems.elements s1.elements in
-  let inc s r e = try TIntMap.find e (StringMap.find r s.incidence) with
-      Not_found -> Tuples.empty in
+  let inc s r e = 
+    try TIntMap.find e (StringMap.find r s.incidence) with Not_found ->
+      try
+	if Bitvector.get_bit (StringMap.find r s.predicates) e then
+	  Tuples.singleton [|e|]
+	else Tuples.empty
+      with Not_found -> Tuples.empty in
   let diff_elem_rel e r = not (Tuples.equal (inc s1 r e) (inc s2 r e)) in
   let diff_rels e = (e, List.filter (diff_elem_rel e) rels) in
   List.filter (fun (_, rs) -> rs <> []) (List.rev_map diff_rels elems)
@@ -1199,12 +1233,13 @@
       try
 	Tuples.equal (StringMap.find rel map) tp
       with Not_found -> false in
-    let is_eq_in1, is_eq_in2 = is_eq_in s1.relations, is_eq_in s2.relations in
+    let s1_relations, s2_relations = relations s1, relations s2 in
+    let is_eq_in1, is_eq_in2 = is_eq_in s1_relations, is_eq_in s2_relations in
     let diffrels = ref [] in
     let appdiff1 r tp = if not (is_eq_in1 r tp) then diffrels := r::!diffrels in
     let appdiff2 r tp = if not (is_eq_in2 r tp) then diffrels := r::!diffrels in
-    StringMap.iter appdiff1 s2.relations;
-    StringMap.iter appdiff2 s1.relations;
+    StringMap.iter appdiff1 s2_relations;
+    StringMap.iter appdiff2 s1_relations;
     LOG 2 "SOME DIFF: %s" (String.concat ", " !diffrels);
     Some (Aux.unique_sorted !diffrels)
   else None

Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/Structure.mli	2012-03-08 01:17:02 UTC (rev 1684)
@@ -45,6 +45,9 @@
 (** Functions in the structure. *)
 val functions : structure -> (float IntMap.t) StringMap.t
 
+(** The bitvector for a given predicate. *)
+val pred_vector : structure -> string -> Bitvector.bitvector
+
 (** {3 Elements and their names.} *)
 
 (** The integer corresponding to a given element name. *)

Modified: trunk/Toss/Solver/StructureTest.ml
===================================================================
--- trunk/Toss/Solver/StructureTest.ml	2012-03-07 03:56:13 UTC (rev 1683)
+++ trunk/Toss/Solver/StructureTest.ml	2012-03-08 01:17:02 UTC (rev 1684)
@@ -69,7 +69,7 @@
       test_incident "[a, b | R (a, b) | ]"
         ["R {(a, b)}"; "R {(a, b)}"];
       test_incident "[a, b | R { (a, b) }; P { a } | ]"
-        ["R {(a, b)}; P {(a)}"; "R {(a, b)}"];
+        ["P {(a)}; R {(a, b)}"; "R {(a, b)}"];
     );
 
   "del" >::

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.