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

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

Revision: 1383
          http://toss.svn.sourceforge.net/toss/?rev=1383&view=rev
Author:   lukaszkaiser
Date:     2011-03-23 17:47:00 +0000 (Wed, 23 Mar 2011)

Log Message:
-----------
Cleanups, deleting unused files, www upload script and smaller release without pdfs.

Modified Paths:
--------------
    trunk/Toss/Makefile
    trunk/Toss/TossTest.ml
    trunk/Toss/WebClient/Main.js
    trunk/Toss/www/Makefile

Added Paths:
-----------
    trunk/Toss/www/upload_sourceforge.sh

Removed Paths:
-------------
    trunk/Toss/Solver/FFSolver.ml
    trunk/Toss/Solver/FFSolver.mli
    trunk/Toss/Solver/FFSolverTest.ml
    trunk/Toss/www/img/flags/
    trunk/Toss/www/xsl/authors-person-extract.xsl
    trunk/Toss/www/xsl/games.xsl
    trunk/Toss/www/xsl/layout-games.xsl

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2011-03-23 16:10:48 UTC (rev 1382)
+++ trunk/Toss/Makefile	2011-03-23 17:47:00 UTC (rev 1383)
@@ -20,6 +20,7 @@
 	rm -f toss_$(RELEASE)/www/code_doc
 	mv toss_$(RELEASE)/_build/Toss.docdir toss_$(RELEASE)/www/code_doc
 	rm -rf toss_$(RELEASE)/_build toss_$(RELEASE)/gmon.out
+	rm -rf toss_$(RELEASE)/www/pub
 	zip -r toss_$(RELEASE).zip toss_$(RELEASE)
 	rm -rf toss_$(RELEASE)
 

Deleted: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml	2011-03-23 16:10:48 UTC (rev 1382)
+++ trunk/Toss/Solver/FFSolver.ml	2011-03-23 17:47:00 UTC (rev 1383)
@@ -1,1285 +0,0 @@
-(* A solver based on the FF Type Normal Form and {!AssignmentSet}s
-   without predetermined order of variables. Continuous aspects
-   (polynomials, real variables, formulas characterizing reals) are
-   not developed yet (but real expressions with [Sum]s, [Char]acteristic
-   and real functions are available).
-
-   If the first element of AssignmentSet.FO assoc list has a negative
-   number instead of an element, it stores the common assignments for
-   all context elements different than the context elements of the
-   rest of the list, and the number is the negated number of these
-   elements (so it is always smaller than zero and the rest of the
-   list can be empty). This convention is respected by modules
-   {!AssignmentSet} and {!FFSolver}, but not necessarily ohters. *)
-
-open Formula
-open Printf
-
-let debug_level = ref 0
-
-
-open Structure
-module A = AssignmentSet
-
-module Vars = Set.Make (struct
-  type t = Formula.var
-  let compare = Pervasives.compare
-end)
-let add_vars nvs vs =
-  List.fold_left (fun vs nv -> Vars.add nv vs) vs nvs
-let vars_of_list nvs =
-  add_vars nvs Vars.empty
-let sum_vars vars = List.fold_left Vars.union Vars.empty vars
-let vars_of_array nvs =
-  Array.fold_left (fun vs nv -> Vars.add nv vs) Vars.empty nvs
-
-let sb_str struc sb =
-  String.concat ", " (List.map (fun (v,e) ->
-    var_str v^"->"^Structure.elem_str struc e) sb)
-
-let rec is_unique_assoc = function
-  | [] -> true
-  | (e,_)::tl -> if List.mem_assoc e tl then false
-    else is_unique_assoc tl
-
-(*
-  let aFO lnum (v,assgns) =
-  Printf.printf "(%d:%s) %!" lnum (var_str v);
-  if is_unique_assoc assgns then A.FO (v, assgns)
-  else failwith
-  ("not unique "^string_of_int lnum^": "^A.str (A.FO (v,assgns)))
-*)
-
-(* Exception handling unwinds the stack to the most recent point
-   selecting a value for a witness.
-
-   It's possible to more thoroughly handle witnesses, by accumulating
-   all variables whose change might result in change of the resulting
-   assignment set; but unsure if it would be a considerable
-   gain. Currently witnesses are only reported for literals. *)
-exception Unsatisfiable_FO of Vars.t
-exception Unsatisfiable
-
-let rec map_try ?catch f = function
-  | [] -> []
-  | hd::tl ->
-    let try r = f hd in
-    r :: map_try ?catch f tl
-  with
-    | Unsatisfiable_FO witnesses as exc ->
-      if catch = None || Vars.mem (Aux.unsome catch) witnesses
-      then map_try ?catch f tl
-      else raise exc
-    | Unsatisfiable ->
-      map_try ?catch f tl
-
-let rec fold_try ?catch f accu = function
-  | [] -> accu
-  | hd::tl ->
-    try
-      fold_try ?catch f (f accu hd) tl
-    with
-      | Unsatisfiable_FO witnesses as exc ->
-        if catch = None || Vars.mem (Aux.unsome catch) witnesses
-        then fold_try ?catch f accu tl
-        else raise exc
-      | Unsatisfiable ->
-        fold_try ?catch f accu tl
-
-let debug_count = ref 0
-
-let list_existsi p l =
-  let rec aux i = function
-    | [] -> false
-    | a::l -> p i a || aux (i+1) l in
-  aux 0 l
-
-let explicit_v_domain v aset =
-  let rec aux = function
-    | A.FO (v1, dis_assgns) when v1 = v ->
-      let dis_assgns =
-        match dis_assgns with
-          | (e,_)::dis_assgns when e < 0 -> dis_assgns
-          | _ -> dis_assgns in
-      elems_of_list (List.map fst dis_assgns)
-    | A.FO (v1, assgns) ->
-      List.fold_left Elems.union Elems.empty
-        (List.map (fun (_,aset) -> aux aset) assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet"
-    | _ -> Elems.empty in
-  aux aset
-
-(* Remove a variable from an assignment by projecting on the given
-   element; if the variable does not admit the element, raise
-   [Unsatisfiable]. *)
-let project_v_on_elem v e aset =
-  let rec aux = function
-    | A.Empty -> raise Unsatisfiable
-    | A.Any -> A.Any
-    | A.FO (v1, dis_assgns) when v1 = v ->
-      let other_aset, dis_assgns =
-        match dis_assgns with
-          | (e,aset)::dis_assgns when e < 0 -> aset, dis_assgns
-          | _ -> A.Empty, dis_assgns in
-      (try List.assoc e dis_assgns
-      with Not_found ->
-        if other_aset = A.Empty then raise Unsatisfiable
-        else other_aset)
-    | A.FO (v1, assgns) ->
-      let assgns =
-        map_try (fun (e, aset) -> e, aux aset) assgns in
-      if assgns = [] then raise Unsatisfiable
-      else A.FO (v1, assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet" in
-  aux aset
-
-(* Remove a variable from an assignment by projecting always on the implicit
-   elements; if the variable does not admit implicit elements, raise
-   [Unsatisfiable]. (Corresponds to projecting on an element outside of
-   {!FFSolver.explicit_v_domain}.) *)
-let project_v_on_implicit v aset =
-  let rec aux = function
-    | A.Empty -> raise Unsatisfiable
-    | A.Any -> A.Any
-    | A.FO (v1, (e,aset)::_) when e < 0 && v1 = v -> aset
-    | A.FO (v1, _) when v1 = v -> raise Unsatisfiable
-    | A.FO (v1, assgns) ->
-      let assgns =
-        map_try (fun (e, aset) -> e, aux aset) assgns in
-      if assgns = [] then raise Unsatisfiable
-      else A.FO (v1, assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet" in
-  aux aset
-
-let rec aset_fo_vars = function
-  | A.Empty | A.Any -> []
-  | A.FO (v, assgns) ->
-    v :: Aux.concat_map aset_fo_vars (List.map snd assgns)
-  | A.Real _ | A.MSO _ ->
-    failwith "FFSolver: Real/MSO assignments not supported yet"
-
-(* For debugging. Brute force check. *)
-(* FIXME: doesn't handle "other element contexts"
-let aset_subsumed all_elems a b =
-  let vars = aset_fo_vars a in
-  let asbs = A.fo_assgn_to_list all_elems vars a in
-  let asbs =
-    Aux.unique (=) (List.map (List.sort Pervasives.compare) asbs) in
-  let bsbs = A.fo_assgn_to_list all_elems vars b in
-  let bsbs =
-    Aux.unique (=) (List.map (List.sort Pervasives.compare) bsbs) in
- (* {{{ log entry *)
-  if !debug_level > 3 then (
-    printf "subsumption: test %d <= %d\n%!"
-      (List.length asbs) (List.length bsbs);
-  );
-  (* }}} *)
-  List.for_all (fun asb ->
-    List.exists (fun bsb ->
-      try
-        List.for_all (fun (v,ae) ->
-          List.assoc v bsb = ae) asb
-      with Not_found -> false) bsbs) asbs
-*)
-
-(* We assume that for every "not ex psi" subformula, "ex psi" is
-   ground, and that every other occurrence of negation is in a literal
-   (it is guaranteed by {!FFTNF.ff_tnf}). We assume that every
-   existentially quantified single disjunct [Ex (vs, Or [phi])] marks
-   the fact that the body [phi] does not have universal quantifiers
-   (guaranteed by {!FFSolver.add_locvar_info}).
-
-   We use the structure of the formula to organize search and build
-   the result on the recursive stack. Accumulated substitution stores
-   the most recent variable first, it represents the path from root to
-   the current position in the aset being built. Our approach
-   resembles constraint propagation: we split the "search space" by
-   assigning values to a variable once we encounter the first "good"
-   constraint on that variable. We organize conjunctive constraints
-   into three queues: currently handled, delayed1: positive has more
-   than one undefined position or negative with exactly one undefined
-   position, delayed2: would have to split on all elements. We fold
-   over disjunctive constraints by keeping the aset subtree to which
-   we merge from the current context to produce the final answer. (It
-   is initialized with Empty aset.) In the same way we fold over
-   assignments for local variables: existentially quantified variables
-   that do not have a universal quantifier in their scope.
-
-   The rules to merge (disjoin) the current aset (cur-aset) and the
-   current position (cur-pos):
-
-   (a) cur-aset=Any: return Any (subsumption)
-
-   (b) no more conjuncts in subformula: return Any (subsumption the
-   other way round) -- descending the recursion stack will rebuild the
-   final aset
-
-   (c) introducing a variable v that is also the root of cur-aset:
-
-   (c1) map-try over the cur-pos values of v, passing as aset to disjoin
-   the corresponding cur-aset subtree, or Empty if cur-aset does not
-   admit given value
-
-   (c2) if map-try returned non-empty, add to it cur-aset subtrees of v
-   values outside of map-try results (if empty, raise Unsatisfiable)
-
-   (d) introducing a (non-local) variable v that does not occur in cur-aset:
-   (includes case cur-aset=Empty)
-
-   (d1) map-try over the cur-pos values of v, passing as aset to disjoin
-   the whole cur-aset
-
-   (d2) if map-try returned non-empty, add to it the whole cur-aset
-   for v set to all elements outside of map-try results (unless
-   cur-aset is Empty); if map-try returned empty, raise Unsatisfiable
-   [TODO: this can benefit from extending the definition of asets with
-   "other-than" subtree]
-
-   (e) introducing a variable v that occurs in cur-aset:
-
-   (e1) cut the cur-aset into a forest: the aset without v (for each
-   occurrence of v in cur-aset removing the corresponding assignment
-   of its parent variable, perhaps recursively if it was a single
-   assignment), and the asets composed of a single path to each
-   occurrence of v and its subtree ("flower-trees")
-
-   (e2) pull-out v by copying the trunk in front of each child-subtree
-   of v, for each "flower-tree"
-
-   (e3) merge the resulting trees starting with "cur-aset with holes",
-   observing that they have the same order of variables as
-   "accumulator" on relevant paths, with v at root
-
-   (e1-e3) observe that during merger, the "cur-aset with holes" will
-   be cloned over, and the v-occurrence-child-subtrees will either be
-   reintroduced to their original places or the holes kept, depending
-   on what v-assignment the clone belongs to; this observation is used
-   for the actual implementation
-
-   (e4) apply the case (c)
-
-   (f) introducing a local variable v (it cannot occur in cur-aset):
-   fold-try over the cur-pos values of v, passing as the initial aset
-   to disjoin the whole cur-aset.
-
-   If the first element of [dis_assgns] assoc list has a negative
-   number instead of an element, it stores the common assignments for
-   all context elements different than the context elements of the
-   rest of the list. This convention is respected by modules
-   {!AssignmentSet} and {!FFSolver}, but not ohters.
-*)
-(* Model used only for debugging. *)
-let merge model all_elems num_elems is_local v init_domain
-    sb cur_aset eval_cont =
-  let rec aux = function                (* v not in local_vars *)
-    | A.MSO _ | A.Real _ -> failwith
-      "FFSolver.evaluate: MSO and Real not supported yet"
-    (* a *)
-    | A.Any -> A.Any
-    (* c *)
-    | A.FO (v1, dis_assgns) when v1 = v ->
-      let other_aset, num_implicit, dis_assgns =
-        match dis_assgns with
-          | (e,aset)::dis_assgns when e < 0 -> aset, ~-e, dis_assgns
-          | _ -> A.Empty, 10000 (*ignored*), dis_assgns in
-      let num_anys = ref 0 and other_used = ref 0 in
-      let choose e =
-        let ret_aset =
-          eval_cont ((v, e)::sb)
-            (try List.assoc e dis_assgns
-             with Not_found -> incr other_used; other_aset) in
-        if ret_aset = A.Any then incr num_anys;
-        e, ret_aset in
-      (* c1 *)
-      let pos_assgns =
-        map_try ~catch:(v :> var) choose init_domain in
-      if pos_assgns = [] then raise Unsatisfiable
-      else
-        (* c2 *)
-        let more_assgns = Aux.map_some (fun ((e,aset) as e_aset) ->
-          if List.mem_assoc e pos_assgns
-          then None else (
-            if aset = A.Any then incr num_anys;
-            Some e_aset))
-          dis_assgns in
-        let new_implicit = num_implicit - !other_used in
-        let other_assgns =
-          if other_aset = A.Empty || new_implicit <= 0
-          then []
-          else [~-new_implicit, other_aset] in
-        if other_aset = A.Any then
-          num_anys := !num_anys + new_implicit;
-        if !num_anys >= num_elems then A.Any
-        else A.FO (v, other_assgns @ pos_assgns @ more_assgns)
-      
-    (* d *)
-    | _ when not (A.mem_assoc v cur_aset) ->
-      (* Unlikely to be useful, but for completeness... *)
-      let num_anys = ref 0 in
-      let choose e =
-        let ret_aset =
-          eval_cont ((v, e)::sb) cur_aset in
-        if ret_aset = A.Any then incr num_anys;
-        e, ret_aset in
-      (* d1 *)
-      let pos_assgns =
-        map_try ~catch:(v :> var) choose init_domain in
-      if pos_assgns = [] then raise Unsatisfiable
-      else if !num_anys = num_elems then A.Any
-      else if cur_aset = A.Empty
-      then A.FO (v, pos_assgns)
-      else
-        (* d2 *)
-        let num_implicit = num_elems - List.length pos_assgns in
-        let other_assgns =
-          if num_implicit <= 0 then []
-          else [~-num_implicit, cur_aset] in
-        A.FO (v, other_assgns @ pos_assgns)
-
-    (* e *)
-    | _ ->                              (*  when A.mem_assoc v cur_aset *)
-      let domain = explicit_v_domain v cur_aset in
-      let pull_v e =
-        e, project_v_on_elem v e cur_aset in
-      let pos_assgns = map_try pull_v (Elems.elements domain) in
-      let num_implicit = num_elems - List.length pos_assgns in
-      let other_assgns =
-        if num_implicit <= 0 then []
-        else try
-               [~-num_implicit, project_v_on_implicit v cur_aset]
-          with Unsatisfiable -> [] in
-      let assgns = other_assgns @ pos_assgns in
-      if assgns = [] then raise Unsatisfiable
-      else aux (A.FO (v, assgns)) in
-
-  if is_local then
-    (* f *)
-    let choose cur_aset e =
-      eval_cont ((v, e)::sb) cur_aset in
-    let pos_assgns =
-      fold_try ~catch:(v :> var) choose cur_aset init_domain in
-    if pos_assgns = A.Empty then raise Unsatisfiable
-    else pos_assgns
-
-  else aux cur_aset
-
-
-(* Use a bigger assignment set as the first argument. *)
-(* Model used only for debugging. *)
-let rec sum_assignment_sets model all_elems num_elems aset1 aset2 =
-  (* [sb] always has the form [v, e] *)
-  let rec cont disjs sb aset1 =
-    aux aset1 (List.assoc (snd (List.hd sb)) disjs)
-  and aux aset1 = function
-    | A.Empty -> aset1
-    | A.Any -> A.Any                    (* subsumption *)
-    | A.FO (v, (impl, other_aset2)::dis_assgns) when impl < 0 ->
-      (* doing some of [merge] work to avoid enumerating all elements
-         as the init_domain *)
-      if A.mem_assoc v aset1 then       
-        let domain = explicit_v_domain v aset1 in
-        let domain = add_elems (List.map fst dis_assgns) domain in
-        (* {{{ log entry *)
-        if !debug_level > 4 then (
-          printf "sum: var %s -- explicit domain: %s\n%!" (var_str v)
-            (String.concat ", " (List.map (Structure.elem_str model)
-                                   (Elems.elements domain)));
-        );
-        (* }}} *)
-        let num_anys = ref 0 in
-        let assgns = List.map (fun e ->
-          let aset2 =
-            try List.assoc e dis_assgns with Not_found -> other_aset2 in
-          let aset1 =
-            try project_v_on_elem v e aset1
-            with Unsatisfiable -> A.Empty in
-          let aset = aux aset1 aset2 in
-          assert (aset <> A.Empty);
-          if aset = A.Any then incr num_anys;
-          e, aset) (Elems.elements domain) in
-        let num_implicit = num_elems - (Elems.cardinal domain) in
-        if !num_anys >= num_elems then A.Any
-        else if num_implicit <= 0 then A.FO (v, assgns)
-        else
-          let other_aset1 = project_v_on_implicit v aset1 in
-          A.FO (v,(~-num_implicit, aux other_aset1 other_aset2)::assgns)
-      else                              (* project v *)
-        let assgns = List.map snd dis_assgns in
-        let aset2 = List.fold_left aux other_aset2 assgns in
-        aux aset1 aset2
-    | A.FO (v, assgns) ->
-      let init_domain = List.map fst assgns in
-      merge model all_elems num_elems false v init_domain
-        [] aset1 (cont assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "Real/MSO assignments not supported yet" in
-  aux aset1 aset2
-
-(* Remove existentially quantified variables from the solution. *)
-(* Model used only for debugging. *)
-and project model all_elems num_elems aset v =
-  match aset with
-    | A.Empty -> A.Empty
-    | A.Any -> A.Any
-    | A.FO (_, []) -> assert false
-    | A.FO (v1, [e, aset]) when v1 = v -> aset
-    | A.FO (v1, (_, aset)::assgns) when v1 = v ->
-      List.fold_left (sum_assignment_sets model all_elems num_elems) aset
-        (List.map snd assgns)
-    | A.FO (v1, assgns) ->
-      A.FO (v1, List.map (fun (e, aset) ->
-        e, project model all_elems num_elems aset v) assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet"
-
-(* "Negate" the assignment set wrt. [all_elems]. *)
-let rec complement all_elems num_elems = function
-    | A.Empty -> A.Any
-    | A.Any -> A.Empty
-    | A.FO (_, []) -> assert false
-    | A.FO (v, (impl, A.Any)::dis_assgns) when impl < 0 ->
-      let deeper = Aux.map_some
-        (fun (e, aset) ->
-          let assgn = complement all_elems num_elems aset in
-          if assgn = A.Empty then None else Some (e, assgn))
-        dis_assgns in
-      if deeper = [] then A.Empty else A.FO (v, deeper)
-    | A.FO (v, all_assgns) ->
-      let other_aset, num_implicit, dis_assgns =
-        match all_assgns with
-          | (impl, other_aset)::dis_assgns when impl < 0 ->
-            other_aset, ~-impl, dis_assgns
-          | _ -> A.Empty, num_elems - List.length all_assgns, all_assgns in
-      let dropout = ref false in
-      let deeper = Aux.map_some
-        (fun (e, aset) ->
-          let assgn = complement all_elems num_elems aset in
-          if assgn = A.Empty then (dropout := true; None)
-          else Some (e, assgn))
-        dis_assgns in
-      let other_aset = complement all_elems num_elems other_aset in
-      if not !dropout then
-        A.FO (v, (~-num_implicit, other_aset)::deeper)
-      else
-        let other_assgns = Aux.map_some (fun e->
-          if List.mem_assoc e dis_assgns then None
-          else Some (e, other_aset)) all_elems in
-        let assgns = deeper @ other_assgns in
-        if assgns = [] then A.Empty else A.FO (v, assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet"
-
-(* Join several assignment sets using de Morgan laws. *)
-(* TODO: optimize! write "join" analogous to "merge" to avoid going
-   through complement *)
-(* Model used only for debugging. *)
-let intersect_assignment_sets model all_elems num_elems asets =
-  match asets with
-    | [] -> A.Any
-    | [aset] -> aset
-    | aset::asets ->
-      let negated = List.map (complement all_elems num_elems) asets in
-      let neg_aset = complement all_elems num_elems aset in
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        printf "intersect: negated asets: %s\n%!"
-          (String.concat "; " (
-            List.map (AssignmentSet.named_str model) ((neg_aset::negated))));
-      );
-      (* }}} *)
-      let union =
-        List.fold_left (sum_assignment_sets model all_elems num_elems)
-          neg_aset negated in
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        printf "intersect: union negated: %s\n%!"
-          (AssignmentSet.named_str model union);
-      );
-      (* }}} *)
-      let res = complement all_elems num_elems union in
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        printf "intersect: result: %s\n%!"
-          (AssignmentSet.named_str model res);
-      );
-      (* }}} *)
-      res
-
-(* Remove universally quantified variables from the solution. *)
-(* Model used only for debugging. *)
-let universal model all_elems num_elems aset v =
-  let rec aux = function
-    | A.Empty -> raise Unsatisfiable
-    | A.Any -> A.Any
-    | A.FO (_, []) -> assert false
-    | A.FO (v1, all_assgns) when v1 = v ->
-      let other_aset, num_implicit, dis_assgns =
-        match all_assgns with
-          | (e,aset)::dis_assgns when e < 0 -> aset, ~-e, dis_assgns
-          | _ -> A.Empty, num_elems - List.length all_assgns, all_assgns in
-      if other_aset = A.Empty && num_implicit > 0
-      then (
-        (* {{{ log entry *)
-        if !debug_level > 3 then (
-          printf "universal: v=%s -- not enough elements\n%!"
-            (Formula.var_str v);
-        );
-        (* }}} *)
-        raise Unsatisfiable
-      ) else
-        let aset =
-          intersect_assignment_sets model all_elems num_elems
-            (List.map snd all_assgns) in
-        if aset = A.Empty then (
-          (* {{{ log entry *)
-          if !debug_level > 3 then (
-            printf "universal: v=%s -- no common subassignment\n%!"
-              (Formula.var_str v);
-          );
-          (* }}} *)
-          raise Unsatisfiable
-        ) else aset
-    | A.FO (v1, assgns) ->
-      let assgns =
-        map_try (fun (e, aset) -> e, aux aset) assgns in
-      if assgns = [] then raise Unsatisfiable
-      else A.FO (v1, assgns)
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet" in
-  aux aset
-
-
-(* "Negate" the second assignment set wrt. [all_elems] and add it to the
-   first aset. *)
-(* Model used only for debugging. *)
-(* FIXME: handle "other element contexts". *)
-let rec add_complement model all_elems num_elems disj_aset = function
-    | A.Empty -> A.Any
-    | A.Any ->
-      if disj_aset = A.Empty then raise Unsatisfiable;
-      disj_aset
-    | A.FO (_, []) -> assert false
-    | A.FO (v, assgns) ->
-      let add_cont sb dset =
-        let e = snd (List.hd sb) in
-        let cset =
-          (* Empty will turn into Any on recursive callback *)
-          try List.assoc e assgns with Not_found -> A.Empty in
-        add_complement model all_elems num_elems dset cset in
-      merge model all_elems num_elems false v all_elems [] disj_aset add_cont
-
-    | A.Real _ | A.MSO _ ->
-      failwith "FFSolver: Real/MSO assignments not supported yet"
-
-
-let evaluate model ?(sb=[]) ?(disj_aset=A.Empty) phi =
-  (* {{{ log entry *)
-  let guard_number = ref 0 in
-  if !debug_level > 1 then (
-    printf "evaluate: phi=%s; sb=%s; disj_aset=%s\n%!"
-      (Formula.str phi) (sb_str model sb)
-      (AssignmentSet.named_str model disj_aset);
-  );
-  (* }}} *)
-  let all_elems = Elems.elements model.elements in
-  let num_elems = Elems.cardinal model.elements in
-
-  (* Process conjunctions by passing the remaining conjuncts a la CPS,
-     filtering according to subsumption with the current alternative
-     (cur-aset), accumulating assignments in a substitution and
-     rebuilding the resulting aset on return. Disjunctions are
-     processed by fold-try of the solution process with cur-aset as
-     accumulator. Branch on a variable when it is first encountered in
-     a literal. Eliminate a variable (and sum its branches) from the
-     assignment set when exiting an existential quantifier [TODO:
-     optimize].  Check universally quantified variables for coverage.
-
-     Do not return [A.Empty], raise [Unsatisfiable] instead. *)
-  let rec solve local_vars delayed2 delayed1 conj_cont sb cur_aset =
-    (* {{{ log entry *)
-    if !debug_level > 3 then (
-      printf "solve: remaining=%s\nsolve: sb=%s\nsolve: disj_aset=%s\n%!"
-        (Formula.str (And (conj_cont @ delayed1 @ delayed2)))
-        (sb_str model sb) (AssignmentSet.named_str model cur_aset);
-    );
-    (* }}} *)
-    (* a *)
-    if cur_aset = A.Any then (
-      (* {{{ log entry *)
-      if !debug_level > 2 then (
-        printf "a: cur_aset=Any subsuming phi=%s\n%!"
-          (Formula.str (And (conj_cont @ delayed1 @ delayed2)))
-      );
-      (* }}} *)
-      A.Any
-    ) else match conj_cont with
-      | [] ->
-        if delayed1 <> []
-        then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
-        else if delayed2 <> []
-        then solve local_vars [] [] (List.rev delayed2) sb cur_aset
-        (* b *)
-        else (
-          (* {{{ log entry *)
-          if !debug_level > 2 then (
-            printf "b: phi=[] subsuming cur_aset=%s\n%!"
-              (AssignmentSet.named_str model cur_aset);
-          );
-          (* }}} *)
-          A.Any                        (* subsuming [cur_aset] *)
-        )
-      | Rel (relname, vtup) as atom :: conj_cont ->
-        let tuples_s =
-          try StringMap.find relname model.relations
-          with Not_found -> Tuples.empty in
-        (let try tup = Array.map (fun v->List.assoc v sb) vtup in
-         if not (Tuples.mem tup tuples_s)
-         then raise (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
-         else if conj_cont <> []
-         then solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-         else if delayed1 <> []
-         then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
-         else solve local_vars [] [] (List.rev delayed2) sb cur_aset
-         with Not_found ->
-           (* we will add new variables one at a time *)
-           let nvi =
-             Aux.array_argfind (fun v->not (List.mem_assoc v sb)) vtup in
-           let nvar = vtup.(nvi) in
-           let oldvars =
-             Aux.array_find_all (fun v->List.mem_assoc v sb) vtup in
-           let multi_unkn = Aux.array_existsi
-             (fun i v->i>nvi && not (List.mem v oldvars)) vtup in
-           if multi_unkn && conj_cont <> [] then (* delay *)
-             solve local_vars delayed2 (atom::delayed1) conj_cont
-               sb cur_aset
-           else
-             (* to narrow the domain, lookup incidence of known vars,
-                filter for partial match and project on the nvar
-                position *)
-             let tuples_i =
-               try StringMap.find relname model.incidence
-               with Not_found -> IntMap.empty in
-             let tups_sets = List.map (fun v->
-               try IntMap.find (List.assoc v sb) tuples_i
-               with Not_found -> Tuples.empty) oldvars in
-             let tuples =
-               match tups_sets with
-                 | [] -> tuples_s
-                 | [tups] -> tups
-                 | tups::tups_sets ->
-                   List.fold_left Tuples.inter tups tups_sets in
-             if Tuples.is_empty tuples
-             then raise
-               (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
-             else
-               let known_tup = Array.map
-                 (fun v -> try List.assoc v sb with Not_found -> -1)
-                 vtup in
-               let init_domain =
-                 Tuples.fold (fun tup dom ->
-                   if Aux.array_for_all2 (fun known asked->
-                     known = -1 || known = asked) known_tup tup
-                     && not (List.mem tup.(nvi) dom)
-                   then tup.(nvi)::dom
-                   else dom) tuples [] in
-               (* {{{ log entry *)
-               if !debug_level > 2 then (
-                 printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
-                   (sb_str model sb) (Formula.str atom)
-                   (String.concat ", " (List.map (Structure.elem_str model)
-                                          init_domain));
-               );
-               (* }}} *)
-               if init_domain = []
-               then raise
-                 (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
-               else if not multi_unkn && conj_cont = [] && delayed1 = [] &&
-                      delayed2 = []
-               then                     (* no more vars and conjuncts *)
-                 merge model all_elems num_elems
-                   (Vars.mem (nvar :> var) local_vars)
-                   nvar init_domain sb cur_aset
-                   (fun _ _ -> A.Any)   (* subsume *)
-               else
-                 let conj_cont =
-                   if multi_unkn then atom::conj_cont else conj_cont in
-                 (* If not [multi_unkn] then for elements in [init_domain]
-                    rel holds *)
-                 merge model all_elems num_elems
-                   (Vars.mem (nvar :> var) local_vars)
-                   nvar init_domain sb cur_aset
-                   (solve local_vars delayed2 delayed1 conj_cont)
-        )
-
-      (* by analogy to the [Rel (relname, vtup)] case *)
-      | Eq (x, y) as atom :: conj_cont ->
-        let vtup = [x; y] in
-        (try
-           if not (List.assoc x sb = List.assoc y sb)
-           then raise (Unsatisfiable_FO (vars_of_list (vtup :> var list)))
-           else
-             solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-         with Not_found ->
-           (* we will add new variables one at a time *)
-           let nvi, nvar =
-             if List.mem_assoc x sb then 1, y else 0, x in
-           let oldvars =
-             List.filter (fun v->List.mem_assoc v sb) vtup in
-           let multi_unkn = list_existsi
-             (fun i v->i>nvi && not (List.mem v oldvars)) vtup in
-           if multi_unkn && (conj_cont <> [] || delayed1 <> [])
-           then (* delay *)
-             solve local_vars (atom::delayed2) delayed1 conj_cont
-               sb cur_aset
-           else if multi_unkn then
-             let conj_cont = atom::conj_cont in
-             (* {{{ log entry *)
-             if !debug_level > 2 then (
-               printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS\n%!"
-                 (sb_str model sb) (Formula.str atom);
-               );
-             (* }}} *)
-             merge model all_elems num_elems
-               (Vars.mem (nvar :> var) local_vars)
-               nvar all_elems sb cur_aset
-               (solve local_vars delayed2 delayed1 conj_cont)
-           else
-             let ovar = if nvi = 1 then x else y in
-             let e = List.assoc ovar sb in
-             (* {{{ log entry *)
-             if !debug_level > 2 then (
-               printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
-                 (sb_str model sb) (Formula.str atom)
-                 (Structure.elem_str model e);
-             );
-             (* }}} *)
-             merge model all_elems num_elems
-               (Vars.mem (nvar :> var) local_vars)
-               nvar [e] sb cur_aset
-               (solve local_vars delayed2 delayed1 conj_cont)
-        )
-
-      (* by analogy to the [Rel (relname, vtup)] case *)
-      | Not (Rel (relname, vtup)) as literal :: conj_cont ->
-        let tuples_s =
-          try StringMap.find relname model.relations
-          with Not_found -> Tuples.empty in
-        (let try tup = Array.map (fun v->List.assoc v sb) vtup in
-         if Tuples.mem tup tuples_s
-         then raise
-           (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
-         else if conj_cont <> []
-         then solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-         else if delayed1 <> []
-         then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
-         else solve local_vars [] [] (List.rev delayed2) sb cur_aset
-         with Not_found ->
-           (* we will add new variables one at a time *)
-           let nvi =
-             Aux.array_argfind (fun v->not (List.mem_assoc v sb)) vtup in
-           let nvar = vtup.(nvi) in
-           let oldvars =
-             Aux.array_find_all (fun v->List.mem_assoc v sb) vtup in
-           let multi_unkn = Aux.array_existsi
-             (fun i v->i>nvi && not (List.mem v oldvars)) vtup in
-           if multi_unkn && (conj_cont <> [] || delayed1 <> [])
-           then (* delay *)
-             solve local_vars (literal::delayed2) delayed1 conj_cont
-               sb cur_aset
-           else if not multi_unkn && conj_cont <> []
-           then
-             solve local_vars delayed2 (literal::delayed1) conj_cont
-               sb cur_aset
-           else if multi_unkn then
-             (* we cannot easily optimize *)
-             let conj_cont = [literal] in
-             merge model all_elems num_elems
-               (Vars.mem (nvar :> var) local_vars)
-               nvar all_elems sb cur_aset
-               (solve local_vars delayed2 delayed1 conj_cont)
-           else
-             let tuples_i =
-               try StringMap.find relname model.incidence
-               with Not_found -> IntMap.empty in
-             let tups_sets = List.map (fun v->
-               try IntMap.find (List.assoc v sb) tuples_i
-               with Not_found -> Tuples.empty) oldvars in
-             let tuples =
-               match tups_sets with
-                 | [] -> tuples_s
-                 | [tups] -> tups
-                 | tups::tups_sets ->
-                   List.fold_left Tuples.inter tups tups_sets in
-             let init_domain =
-               if Tuples.is_empty tuples
-               then all_elems
-               else
-                 let known_tup = Array.map
-                   (fun v -> try List.assoc v sb with Not_found -> -1)
-                   vtup in
-                 let init_domain_co =
-                   Tuples.fold (fun tup dom ->
-                     if Aux.array_for_all2 (fun known asked->
-                       known = -1 || known = asked) known_tup tup
-                     then Elems.add tup.(nvi) dom
-                     else dom) tuples Elems.empty in
-                 Elems.elements (Elems.diff model.elements init_domain_co) in
-             (* {{{ log entry *)
-             if !debug_level > 2 then (
-               printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
-                 (sb_str model sb) (Formula.str literal)
-                 (String.concat ", " (List.map (Structure.elem_str model)
-                                        init_domain));
-             );
-             (* }}} *)
-             if init_domain = []
-             then raise Unsatisfiable
-             else
-               (* If not [multi_unkn] then for elements in [init_domain]
-                  rel does not hold *)
-               merge model all_elems num_elems
-                 (Vars.mem (nvar :> var) local_vars)
-                 nvar init_domain sb cur_aset
-                 (solve local_vars delayed2 delayed1 conj_cont)
-        )
-
-      (* by analogy to both [Eq] and [not Rel] cases *)
-      | Not (Eq (x, y)) as literal :: conj_cont ->
-        let vtup = [x; y] in
-        (try
-           if List.assoc x sb = List.assoc y sb
-           then raise (Unsatisfiable_FO (vars_of_list ([x; y] :> var list)))
-           else
-             solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-         with Not_found ->
-           (* we will add new variables one at a time *)
-           let nvi, nvar =
-             if List.mem_assoc x sb then 1, y else 0, x in
-           let oldvars =
-             List.filter (fun v->List.mem_assoc v sb) vtup in
-           let multi_unkn = list_existsi
-             (fun i v->i>nvi && not (List.mem v oldvars)) vtup in
-           if multi_unkn && (conj_cont <> [] || delayed1 <> [])
-           then (* delay *)
-             solve local_vars (literal::delayed2) delayed1 conj_cont
-               sb cur_aset
-           else if not multi_unkn && conj_cont <> [] then
-             solve local_vars delayed2 (literal::delayed1) conj_cont
-               sb cur_aset
-           else if multi_unkn then begin
-             (* {{{ log entry *)
-             if !debug_level > 2 then (
-               printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS\n%!"
-                 (sb_str model sb) (Formula.str literal);
-               );
-             (* }}} *)
-             merge model all_elems num_elems
-               (Vars.mem (nvar :> var) local_vars)
-               nvar all_elems sb cur_aset
-               (solve local_vars delayed2 delayed1 (literal :: conj_cont))
-           end else                     (* optimize *)
-             let ovar = if nvi = 1 then x else y in
-             let e = List.assoc ovar sb in
-             (* {{{ log entry *)
-             if !debug_level > 2 then (
-               printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS - %s\n%!"
-                 (sb_str model sb) (Formula.str literal)
-                 (Structure.elem_str model e);
-               );
-             (* }}} *)
-             let init_domain =
-               Elems.elements (Elems.remove e model.elements) in
-             merge model all_elems num_elems
-               (Vars.mem (nvar :> var) local_vars)
-               nvar init_domain sb cur_aset
-               (solve local_vars delayed2 delayed1 conj_cont)
-        )
-
-      | Or [_] :: _ | And [_] :: _ -> assert false
-
-      (* use associativity, but don't invert the order *)
-      | And conj :: conj_cont ->
-        let conj_cont =
-          if conj_cont = [] then conj else conj @ conj_cont in
-        solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-
-      (* Propagate implication constraints. *)
-      | Or fl :: conj_cont when List.exists
-          (function Not _ -> true | _ -> false) fl ->
-        (* {{{ log entry *)
-        let cur_guard = !guard_number in
-        if !debug_level > 2 then (
-          printf "Computing guard no %d..." cur_guard; incr guard_number;
-        );
-        (* }}} *)
-        let guard, body = Aux.partition_map
-          (function Not phi -> Aux.Left phi | phi -> Aux.Right phi) fl in
-        (* assignments of the guard alone *)
-        let guard_set =
-          try solve local_vars [] [] guard sb A.Empty
-          with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Guard: no %d guard_set=%s\nBody: %s\n%!" cur_guard
-            (AssignmentSet.named_str model guard_set) (Formula.str (Or body));
-        );
-        (* }}} *)
-        let cur_aset =
-          add_complement model all_elems num_elems cur_aset guard_set in
-        if body = [] || guard_set = A.Empty then
-          (* the positive part is in effect false -- discard it *)
-          solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-        else
-          (* hopefully more constrained
-             (TODO: don't redo the guard?) *)
-          let concl =
-            match body with
-              | [concl] -> concl | _ -> Or body in
-          solve local_vars delayed2 delayed1
-            (guard @ [concl] @ conj_cont) sb cur_aset
-
-      (* Continue in each branch folding disjuncts; "Or []" is OK. *)
-      | Or fl :: conj_cont ->
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Folding-disjunctively-over: %s\ndisjunct-continuation: %s\n%!"
-            (Formula.str (Or fl)) (Formula.str (And conj_cont));
-        );
-        (* }}} *)
-        fold_try (fun dset phi ->
-          (* {{{ log entry *)
-          if !debug_level > 3 then (
-            printf "disjunct: %s; prior dset=%s\n%!"
-              (Formula.str phi) (AssignmentSet.named_str model dset);
-            );
-          (* }}} *)
-          (* DNF-style: if there are remaining conjuncts, solve them
-             in each branch of disjunction. *)
-          solve local_vars delayed2 delayed1 (phi::conj_cont) sb dset)
-          cur_aset fl
-
-      | Ex ([], phi) :: _ | All ([], phi) :: _ -> assert false
-
-      (* Local variables -- handled by merging online. *)
-      | Ex (vl, Or [phi]) :: conj_cont ->
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solving-for-local-variables: %s...\n%!"
-            (String.concat ", " (List.map Formula.var_str vl));
-        );
-        (* }}} *)
-        let local_vars = add_vars vl local_vars in
-        (* FIXME: after debugging return to tail call *)
-        let aset =
-          solve local_vars delayed2 delayed1 (phi::conj_cont) sb
-            cur_aset in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solved-local-variables: %s; aset=%s\n%!"
-            (String.concat ", " (List.map Formula.var_str vl))
-            (AssignmentSet.named_str model aset);
-        );
-        (* }}} *)
-        (* TODO: handle other kinds *)
-        aset        
-
-      (* Only project, as the mechanics of existential variables is
-         handled at the site of their first occurrence. *)
-      | Ex (vl, phi) :: conj_cont ->
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solving-for-existential-variables: %s...\n%!"
-            (String.concat ", " (List.map Formula.var_str vl));
-        );
-        (* }}} *)
-        let aset =
-          solve local_vars delayed2 delayed1 (phi::conj_cont) sb cur_aset in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solved-existential-variables: %s; aset=%s\n%!"
-            (String.concat ", " (List.map Formula.var_str vl))
-            (AssignmentSet.named_str model aset);
-        );
-        (* }}} *)
-        (* TODO: handle other kinds *)
-        let vl = List.map to_fo vl in
-        let aset =
-          List.fold_left (project model all_elems num_elems) aset vl in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Eliminated-variables: %s; aset=%s\n%!"
-            (String.concat ", " (List.map Formula.var_str vl))
-            (AssignmentSet.named_str model aset);
-        );
-        (* }}} *)
-        aset        
-
-      (* Check whether assignment set covers all elements for variables
-         [vl]. *)
-      | All (vl, phi) :: conj_cont ->
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solving-for-universal-variables: %s...\n%!"
-            (String.concat ", " (List.map Formula.var_str vl));
-        );
-        (* }}} *)
-        let aset =
-          solve local_vars delayed2 delayed1 (phi::conj_cont) sb cur_aset in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solved-universal-variables: %s; aset=%s\n%!"
-            (String.concat ", " (List.map Formula.var_str vl))
-            (AssignmentSet.named_str model aset);
-        );
-        (* }}} *)
-        (* TODO: handle other kinds *)
-        let vl = List.map to_fo vl in
-        let aset =
-          List.fold_left (universal model all_elems num_elems) aset vl in
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Eliminated-variables: %s; aset=%s\n%!"
-            (String.concat ", " (List.map Formula.var_str vl))
-            (AssignmentSet.named_str model aset);
-        );
-        (* }}} *)
-        aset
-          
-      (* By assumption that [phi] is ground, check it
-         separately and proceed or fail. *)
-      | Not phi as subtask :: conj_cont ->
-        (* {{{ log entry *)
-        if !debug_level > 2 then (
-          printf "Solving-a-subtask: %s...\n" (Formula.str subtask);
-        );
-        (* }}} *)
-        let aset =
-          (* solving in empty context! *)
-          try solve local_vars [] [] [phi] [] A.Empty
-          with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty in
-        if !debug_level > 2 then (
-          printf "Solved-subtask: %s\nsubtask: aset=%s\n%!"
-            (Formula.str subtask) (AssignmentSet.named_str model aset);
-        );
-        if aset = A.Empty then
-          solve local_vars delayed2 delayed1 conj_cont sb cur_aset
-        else raise Unsatisfiable
-          
-      | RealExpr _ :: _ | In _ :: _ ->
-        failwith
-          "FFSolver: MSO and Reals not implemented yet."
-          
-  (*      
-          and solve_db sb delayed2 delayed1 conj_cont =
-          let count = !debug_count in
-          incr debug_count;
-          printf "solve: #%d, sb=%s, conj_cont=%s\n%!" count
-          ("["^String.concat ", "(List.map (fun (v,e)->
-          Formula.var_str v^":"^string_of_int e) sb)^"]")
-          (String.concat "; " (List.map Formula.str conj_cont));
-          let aset = solve sb delayed2 delayed1 conj_cont in
-          printf "solve-ret: #%d, aset=%s\n%!" count (Assignments.str aset);
-          aset
-  *)    
-  in
-  try solve Vars.empty [] [] [phi] sb disj_aset
-  with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty
-
-(* Assignments of a single variable that are supported by all
-   assignments for remaining variables. *)
-let rec assgn_of struc var = function
-  | A.Any ->
-    struc.elements
-  | A.Empty -> Elems.empty
-  | A.FO (v, (e,_)::els) when v = var && e < 0 ->
-    struc.elements
-  | A.FO (v, els) when v = var ->
-    List.fold_right Elems.add (List.map fst els) Elems.empty
-  | A.FO (_, els) ->
-    List.fold_left Elems.union
-      (assgn_of struc var (snd (List.hd els)))
-      (List.map (fun suba -> assgn_of struc var (snd suba))
-         (List.tl els))
-  | A.MSO (_, els) ->
-    List.fold_left Elems.union
-      (assgn_of struc var (snd (List.hd els)))
-      (List.map (fun suba -> assgn_of struc var (snd suba))
-         (List.tl els))
-  | A.Real _ ->
-    failwith "FFSolver: MSO and Reals not implemented yet."
-
-let rec check_formula struc ?sb ?disj_aset = function
-  | Ex (vs, phi) -> check_formula struc ?sb ?disj_aset phi
-  | Or (fl) -> List.exists (check_formula struc ?sb ?disj_aset) fl
-  | phi -> evaluate struc ?sb ?disj_aset phi <> A.Empty
-
-let get_real_val expr struc =
-  let all_elems = Structure.Elems.elements struc.elements in
-  let rec aux sb = function
-    | Char phi ->
-      if !debug_level > 5 then
-        printf "get_real_val: computing %s ..%!" (Formula.str phi);
-      let res = if check_formula struc ~sb phi then 1. else 0. in
-      if !debug_level > 5 then printf ". %f\n%!" res;
-      res
-    | Const v -> v
-    | Times (e1, e2) -> aux sb e1 *. aux sb e2
-    | Plus (e1, e2) -> aux sb e1 +. aux sb e2
-    | Sum (vl, guard, r) ->
-      let aset = evaluate struc ~sb guard in
-      let assgns =
-        A.fo_assgn_to_list all_elems vl aset in
-      List.fold_left (fun acc assgn ->
-        acc +. aux (assgn @ sb) r
-      ) 0. assgns
-    | Fun (s, v) ->
-      (let try e = List.assoc v sb in
-       IntMap.find e (StringMap.find s struc.functions)
-       with Not_found ->
-        failwith
-          ("Heuristic.get_real_val:" ^
-              " function application "^s^"("^var_str (v :> var) ^
-              ") to undefined variable"))
-   
-    | RVar _ ->
-      failwith "FFSolver: MSO and Reals not implemented yet." in
-  if !debug_level > 4 then
-    printf "get_real_val: %s\n%!" (Formula.real_str expr);
-  aux [] expr
-
-(** {2 Structure-based helper functions for {!FFTNF}.} *)
-
-(* Promote literals with less satisfying tuples, but prefer
-   equalities to other literal and disequalities less than other literals. *)
-let promote_for model lit1 lit2 =
-  match lit1, lit2 with
-    | (Rel (r1, _) | Not (Rel (r1, _))), (Rel (r2, _) | Not (Rel (r2, _)))
-      ->
-      let tups1 =
-        try Structure.StringMap.find r1 model.Structure.relations
-        with Not_found -> Structure.Tuples.empty in
-      let tups2 =
-        try Structure.StringMap.find r2 model.Structure.relations
-        with Not_found -> Structure.Tuples.empty in
-      let n1, n2 =
-        Structure.Tuples.cardinal tups1, Structure.Tuples.cardinal tups2 in
-      begin match lit1, lit2 with
-        | Rel _, Rel _ -> n1 < n2
-        | Not (Rel _), Rel _ -> false
-        | Rel _, Not (Rel _) -> true
-        | Not (Rel _), Not (Rel _) -> n1 > n2
-        | _ -> assert false
-      end
-    | (Rel (r1, _) | Not (Rel (r1, _))), Not (Eq _) -> true
-    | Eq _, (Rel (r2, _) | Not (Rel (r2, _))) -> true
-    | _ -> false
-
-let normalize_for_model model ?fvars phi =
-  let fvars = match fvars with
-    | Some fv -> fv
-    | None -> FormulaOps.free_vars phi in
-  let phi =
-    Ex (fvars, FormulaOps.rename_quant_avoiding fvars phi) in
-  let rec erase_q = function
-    | Ex (vs, phi) ->
-      let nvs =
-        List.filter (fun v -> not (List.mem v fvars)) vs in
-      if nvs = [] then erase_q phi
-      else Ex (nvs, erase_q phi)
-    | All (vs, phi) ->
-      let nvs =
-        List.filter (fun v -> not (List.mem v fvars)) vs in
-      if nvs = [] then erase_q phi
-      else All (nvs, erase_q phi)
-    | And fs -> And (List.map erase_q fs)
-    | Or fs -> Or (List.map erase_q fs)
-    | Not phi -> Not (erase_q phi)
-    | (Rel _ | Eq _ | RealExpr _ | In _) as atom -> atom in
-  erase_q (FFTNF.ff_tnf (promote_for model) phi)
-
-let normalize_expr_for_model model expr =
-  let norm phi =
-    FFTNF.ff_tnf (promote_for model) phi in
-  let rec aux = function
-    | RVar _ 
-    | Const _
-    | Fun _ as expr -> expr
-    | Times (a, b) -> Times (aux a, aux b)
-    | Plus (a, b) -> Plus (aux a, aux b)
-    | Char phi -> Char (norm phi)
-    | Sum (vl, gd, e) -> Sum (vl, norm gd, aux e) in
-  aux expr
-
-let add_locvar_info phi =
-  let rec has_univ = function
-    | All _ -> true
-    | Or js | And js -> List.exists has_univ js
-    | Ex (_, phi) -> has_univ phi
-    | _ -> false in                     (* assumes (partial) NNF *)
-  let rec aux = function
-    | Ex (vs, phi) when not (has_univ phi) ->
-      Ex (vs, Or [aux phi])
-    | Ex (vs, phi) -> Ex (vs, aux phi)
-    | All (vs, phi) -> All (vs, aux phi)
-    | Not phi -> Not (aux phi)          (* subtasks also apply *)
-    | Or [phi] -> aux phi
-    | And [phi] -> aux phi
-    | Or djs -> Or (List.map aux djs)
-    | And cjs -> And (List.map aux cjs)
-    | atom -> atom in
-  aux phi
-
-let rec add_locvar_info_expr = function
-  | Times (a,b) ->
-    Times (add_locvar_info_expr a, add_locvar_info_expr b)
-  | Plus (a,b) ->
-    Plus (add_locvar_info_expr a, add_locvar_info_expr b)
-  | Char (phi) -> Char (add_locvar_info phi)
-  | Sum (vs, guard, expr) ->
-    Sum (vs, add_locvar_info guard, add_locvar_info_expr expr)
-  | simple -> simple
-
-(* Interface to {!SolverIntf}. *)
-module M = struct
-  (* Store whether the formula has been preprocessed. *)
-  type registered_formula = (Formula.formula * bool) ref
-  type registered_real_expr = (Formula.real_expr * bool) ref
-  let register_formula phi = ref (phi, false)
-  let register_real_expr expr = ref (expr, false)
-  (* before {!FFSolver.M.evaluate} to avoid name conflict. *)
-  let evaluate_partial struc sb reg_phi =
-    if not (snd !reg_phi) then
-      reg_phi :=
-        add_locvar_info
-        (normalize_for_model struc
-           ((* FormulaOps.simplify *) (fst !reg_phi))), true;
-    evaluate struc ~sb (fst !reg_phi)
-  let evaluate struc reg_phi =
-    if not (snd !reg_phi) then
-      reg_phi :=
-        add_locvar_info
-        (normalize_for_model struc
-           ((* FormulaOps.simplify *) (fst !reg_phi))), true;
-    evaluate struc (fst !reg_phi)
-  let check_formula struc reg_phi =
-    if not (snd !reg_phi) then
-      reg_phi :=
-        add_locvar_info
-        (normalize_for_model struc (fst !reg_phi)), true;
-    check_formula struc (fst !reg_phi)
-  let get_real_val reg_expr struc =
-    if not (snd !reg_expr) then
-      reg_expr :=
-        add_locvar_info_expr
-        (normalize_expr_for_model struc (fst !reg_expr)), true;
-    get_real_val (fst !reg_expr) struc
-  let formula_str reg_phi =
-    if not (snd !reg_phi) then
-      (* TODO: inconsistent with other defs *)
-      (* to increase consistency of display *)
-      reg_phi := FormulaOps.simplify (fst !reg_phi), false;
-    Formula.str (fst !reg_phi)
-end

Deleted: trunk/Toss/Solver/FFSolver.mli
===================================================================
--- trunk/Toss/Solver/FFSolver.mli	2011-03-23 16:10:48 UTC (rev 1382)
+++ trunk/Toss/Solver/FFSolver.mli	2011-03-23 17:47:00 UTC (rev 1383)
@@ -1,70 +0,0 @@
-(** A solver based on the FF Type Normal Form and
-    {!Assignments}. Continuous aspects (polynomials, real variables,
-    formulas characterizing reals) are not developed. Also fixes some
-    [Solver.Sum] computation bug.
-
-*)
-
-
-val debug_level : int ref
-
-
-(** Find satisfying substitutions for free variables of a formula that
-    extend the given substitution. *)
-val evaluate : Structure.structure ->
-  ?sb:((Formula.fo_var * Structure.Elems.elt) list) ->
-  ?disj_aset:AssignmentSet.assignment_set ->
-  Formula.formula -> AssignmentSet.assignment_set
-
-(** Find satisfying substitutions for free variables of a formula (or
-    check if it holds if it is ground). Does not handle real
-    expressions and second-order variables currently. *)
-
-(** Find satisfying substitutions for free variables of a formula (or
-    check if it holds if it is ground). Does not handle real
-    expressions and second-order variables currently. *)
-val check_formula :
-  Structure.structure ->
-  ?sb:((Formula.fo_var * Structure.Elems.elt) list) ->
-  ?disj_aset:AssignmentSet.assignment_set ->
-  Formula.formula -> bool
-
-(** Compute the value of an expresssion in a structure. Does not
-    handle polynomials. *)
-val get_real_val : Formula.real_expr -> Structure.structure -> float
-
-
-(** Promote relations of smaller cardinality in the example
-    structure. For use with {!FFTNF.ff_tnf}. *)
-val promote_for :
-  Structure.structure -> Formula.formula -> Formula.formula -> bool
-
-(** An interface to {!FFTNF.ff_tnf} that uses {!promote_for}. *)
-val normalize_for_model :
-  Structure.structure -> ?fvars:Formula.var list -> Formula.formula ->
-  Formula.formula
-
-(** Perform {!FFTNF.ff_tnf} (using {!promote_for}) on formulas
-    occurring in an expression. *)
-val normalize_expr_for_model :
-  Structure.structure -> Formula.real_expr -> Formula.real_expr
-
-(* Interface to {!SolverIntf}. *)
-module M : sig
-  type registered_formula
-  type registered_real_expr
-  val register_formula :
-    Formula.formula -> registered_formula
-  val register_real_expr :
-    Formula.real_expr -> registered_real_expr
-  val evaluate : Structure.structure ->
-    registered_formula -> AssignmentSet.assignment_set
-  val evaluate_partial :
-    Structure.structure -> (Formula.fo_var * int) list ->
-    registered_formula -> AssignmentSet.assignment_set
-  val check_formula : Structure.structure ->
-    registered_formula -> bool
-  val get_real_val :
-    registered_real_expr -> Structure.structure -> float
-  val formula_str : registered_formula -> string
-end

Deleted: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml	2011-03-23 16:10:48 UTC (rev 1382)
+++ trunk/Toss/Solver/FFSolverTest.ml	2011-03-23 17:47:00 UTC (rev 1383)
@@ -1,358 +0,0 @@
-open OUnit
-open Aux
-open Printf
-
-let my_cmp_float x y =
-  abs_float (x -. y) <= 0.01
- 
-let struc_of_str s = 
-  StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
-
-let formula_of_str s = 
-  FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-
-let real_of_str s = 
-  FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
- 
-let winQxyz =
-  "ex x, y, z ((((Q(x) and Q(y)) and Q(z)) and ((((R(x, y) and R(y, z)) or (C(x, y) and C(y, z))) or ex u, v ((((R(x, v) and C(v, y)) and R(y, u)) and C(u, z)))) or ex u, v ((((R(x, v) and C(y, v)) and R(y, u)) and C(z, u))))))"
-
-let winPxyz =
-  "ex x, y, z ((((P(x) and P(y)) and P(z)) and ((((R(x, y) and R(y, z)) or (C(x, y) and C(y, z))) or ex u, v ((((R(x, v) and C(v, y)) and R(y, u)) and C(u, z)))) or ex u, v ((((R(x, v) and C(y, v)) and R(y, u)) and C(z, u))))))"
-
-let winQvwxyz =
-  "ex v, w, x, y, z ((((((Q(v) and Q(w)) and Q(x)) and Q(y)) and Q(z)) and ((((((R(v, w) and R(w, x)) and R(x, y)) and R(y, z)) or (((C(v, w) and C(w, x)) and C(x, y)) and C(y, z))) or ex r, s, t, u ((((((((R(v, r) and C(r, w)) and R(w, s)) and C(s, x)) and R(x, t)) and C(t, y)) and R(y, u)) and C(u, z)))) or ex r, s, t, u ((((((((R(v, r) and C(w, r)) and R(w, s)) and C(x, s)) and R(x, t)) and C(y, t)) and R(y, u)) and C(z, u))))))"
-
-let breakW_expanded = "ex y8 ((W(y8) and ex y7 ((C(y7, y8) and ex y6 ((C(y6, y7) and ex y5 ((C(y5, y6) and ex y4 ((C(y4, y5) and ex y3 ((C(y3, y4) and ex y2 ((C(y2, y3) and ex y1 (C(y1, y2))))))))))))))))"
-
-let winQvwxyz_expanded = "ex z ((Q(z) and (ex u0 ((C(u0, z) and ex y ((R(y, u0) and Q(y) and ex t0 ((C(t0, y) and ex x ((R(x, t0) and Q(x) and ex s0 ((C(s0, x) and ex w ((R(w, s0) and Q(w) and ex r0 ((C(r0, w) and ex v ((R(v, r0) and Q(v))))))))))))))))) or ex u ((C(z, u) and ex y ((R(y, u) and Q(y) and ex t ((C(y, t) and ex x ((R(x, t) and Q(x) and ex s ((C(x, s) and ex w ((R(w, s) and Q(w) and ex r ((C(w, r) and ex v ((R(v, r) and Q(v))))))))))))))))) or ex y ((C(y, z) and Q(y) and ex x ((C(x, y) and Q(x) and ex w ((C(w, x) and Q(w) and ex v ((C(v, w) and Q(v))))))))) or ex y ((R(y, z) and Q(y) and ex x ((R(x, y) and Q(x) and ex w ((R(w, x) and Q(w) and ex v ((R(v, w) and Q(v))))))))))))"
-
-(* alfa-conversion of the above *)
-let winQvwxyz_idempotent = "ex z ((Q(z) and (ex u0 ((C(u0, z) and ex y2 ((R(y2, u0) and Q(y2) and ex t0 ((C(t0, y2) and ex x2 ((R(x2, t0) and Q(x2) and ex s0 ((C(s0, x2) and ex w2 ((R(w2, s0) and Q(w2) and ex r0 ((C(r0, w2) and ex v2 ((R(v2, r0) and Q(v2))))))))))))))))) or ex u ((C(z, u) and ex y1 ((R(y1, u) and Q(y1) and ex t ((C(y1, t) and ex x1 ((R(x1, t) and Q(x1) and ex s ((C(x1, s) and ex w1 ((R(w1, s) and Q(w1) and ex r ((C(w1, r) and ex v1 ((R(v1, r) and Q(v1))))))))))))))))) or ex y0 ((C(y0, z) and Q(y0) and ex x0 ((C(x0, y0) and Q(x0) and ex w0 ((C(w0, x0) and Q(w0) and ex v0 ((C(v0, w0) and Q(v0))))))))) or ex y ((R(y, z) and Q(y) and ex x ((R(x, y) and Q(x) and ex w ((R(w, x) and Q(w) and ex v ((R(v, w) and Q(v))))))))))))"
-
-let eval_eq struc_s phi_s aset_s =
-  let struc = struc_of_str struc_s in
-  let f = FFSolver.M.register_formula (formula_of_str phi_s) in
-  assert_equal ~printer:(fun x -> x) aset_s
-    (AssignmentSet.named_str struc (FFSolver.M.evaluate struc f))
-;;
-
-let real_val_eq struc_s expr_s x =
-  let struc = struc_of_str struc_s in
-  let expr =
-    FFSolver.M.register_real_expr (real_of_str expr_s) in
-  assert_equal ~printer:(fun x -> string_of_float x) ~msg:expr_s
-    x (FFSolver.M.get_real_val expr struc)
-
-let tests = "FFSolver" >::: [
-  "eval: first-order quantifier free from SolverTest.ml" >::
-    (fun () ->
-      eval_eq "[ | R { (a, b); (a, c) } | ]" "x = y" 
-	"{ x->a{ y->a } , x->b{ y->b } , x->c{ y->c }  }";
-      eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y"
-	"{ x->b{ y->b }  }";
-      eval_eq "[ | R { (a, b); (a, c) } | ]" "R(x, y) and x = y" 
-	"{}";
-      eval_eq "[ | R { (a, a); (a, b) } | ]" "R(x, y) and x = y"
-	"{ x->a{ y->a }  }";
-      eval_eq "[ | R { (a, b); (a, c) } | ]" "not x = y" 
-	"{ x->a{ y->b, y->c } , x->b{ y->a, y->c } , x->c{ y->a, y->b }  }";
-      eval_eq "[ | R { (a, a); (a, c) } | ]" "R (x, y) and not x = y" 
-	"{ x->a{ y->c }  }";
-    );
-
-  "eval: first-order ...
 
[truncated message content]