[Toss-devel-svn] SF.net SVN: toss:[1635] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1635] trunk/Toss
|
From: <luk...@us...> - 2011-11-17 23:56:48
|
Revision: 1635
http://toss.svn.sourceforge.net/toss/?rev=1635&view=rev
Author: lukaszkaiser
Date: 2011-11-17 23:56:41 +0000 (Thu, 17 Nov 2011)
Log Message:
-----------
Corrections in Distinguish, adding and cleaning up code documentation, removing old unused modules.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRule.mli
trunk/Toss/Formula/FormulaMap.mli
trunk/Toss/Formula/FormulaSubst.mli
trunk/Toss/Formula/Sat/Sat.mli
trunk/Toss/GGP/GameSimpl.mli
trunk/Toss/GGP/TranslateFormula.mli
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/Server/DB.mli
trunk/Toss/Server/Picture.mli
trunk/Toss/Server/ReqHandler.mli
trunk/Toss/Solver/AssignmentSet.mli
trunk/Toss/Solver/Assignments.mli
trunk/Toss/Solver/Distinguish.ml
trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli
trunk/Toss/Solver/RealQuantElim/OrderedPolySet.mli
trunk/Toss/Solver/RealQuantElim/Poly.mli
trunk/Toss/Solver/RealQuantElim/RealQuantElim.mli
trunk/Toss/Solver/RealQuantElim/SignTable.mli
trunk/Toss/Solver/Structure.mli
trunk/Toss/Toss.odocl
Removed Paths:
-------------
trunk/Toss/Formula/Sat/IntSet.ml
trunk/Toss/Formula/Sat/IntSet.mli
Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Arena/DiscreteRule.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(** {1 Discrete Structure Rewriting Rules and Rewriting.} *)
+(** Discrete structure rewriting rules construction and rewriting. *)
val debug_level : int ref
Modified: trunk/Toss/Formula/FormulaMap.mli
===================================================================
--- trunk/Toss/Formula/FormulaMap.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Formula/FormulaMap.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,3 +1,5 @@
+(** Maps, iterators and folds over formulas and real-valued expressions. *)
+
open Formula
(** {2 Basic maps - to literals and atoms.} *)
Modified: trunk/Toss/Formula/FormulaSubst.mli
===================================================================
--- trunk/Toss/Formula/FormulaSubst.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Formula/FormulaSubst.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,3 +1,5 @@
+(** Substitutions in formulas and real-valued expressions. *)
+
open Formula
(** {2 Basic Substitution Functions} *)
Deleted: trunk/Toss/Formula/Sat/IntSet.ml
===================================================================
--- trunk/Toss/Formula/Sat/IntSet.ml 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Formula/Sat/IntSet.ml 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,688 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2.1, with the special exception on linking *)
-(* described in file LICENSE. *)
-(* *)
-(* This software is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
-(* *)
-(**************************************************************************)
-
-(*i $Id: ptset.ml,v 1.17 2008-07-22 06:44:06 filliatr Exp $ i*)
-
-(*s Sets of integers implemented as Patricia trees, following Chris
- Okasaki and Andrew Gill's paper {\em Fast Mergeable Integer Maps}
- ({\tt\small http://www.cs.columbia.edu/\~{}cdo/papers.html\#ml98maps}).
- Patricia trees provide faster operations than standard library's
- module [Set], and especially very fast [union], [subset], [inter]
- and [diff] operations. *)
-
-(*s The idea behind Patricia trees is to build a {\em trie} on the
- binary digits of the elements, and to compact the representation
- by branching only one the relevant bits (i.e. the ones for which
- there is at least on element in each subtree). We implement here
- {\em little-endian} Patricia trees: bits are processed from
- least-significant to most-significant. The trie is implemented by
- the following type [t]. [Empty] stands for the empty trie, and
- [Leaf k] for the singleton [k]. (Note that [k] is the actual
- element.) [Branch (m,p,l,r)] represents a branching, where [p] is
- the prefix (from the root of the trie) and [m] is the branching
- bit (a power of 2). [l] and [r] contain the subsets for which the
- branching bit is respectively 0 and 1. Invariant: the trees [l]
- and [r] are not empty. *)
-
-(*i*)
-type elt = int
-(*i*)
-
-type t =
- | Empty
- | Leaf of int
- | Branch of int * int * t * t
-
-(*s Example: the representation of the set $\{1,4,5\}$ is
- $$\mathtt{Branch~(0,~1,~Leaf~4,~Branch~(1,~4,~Leaf~1,~Leaf~5))}$$
- The first branching bit is the bit 0 (and the corresponding prefix
- is [0b0], not of use here), with $\{4\}$ on the left and $\{1,5\}$ on the
- right. Then the right subtree branches on bit 2 (and so has a branching
- value of $2^2 = 4$), with prefix [0b01 = 1]. *)
-
-(*s Empty set and singletons. *)
-
-let empty = Empty
-
-let is_empty = function Empty -> true | _ -> false
-
-let singleton k = Leaf k
-
-let is_singleton = function Leaf _ -> true | _ -> false
-
-(*s Testing the occurrence of a value is similar to the search in a
- binary search tree, where the branching bit is used to select the
- appropriate subtree. *)
-
-let zero_bit k m = (k land m) == 0
-
-let rec mem k = function
- | Empty -> false
- | Leaf j -> k == j
- | Branch (_, m, l, r) -> mem k (if zero_bit k m then l else r)
-
-(*s The following operation [join] will be used in both insertion and
- union. Given two non-empty trees [t0] and [t1] with longest common
- prefixes [p0] and [p1] respectively, which are supposed to
- disagree, it creates the union of [t0] and [t1]. For this, it
- computes the first bit [m] where [p0] and [p1] disagree and create
- a branching node on that bit. Depending on the value of that bit
- in [p0], [t0] will be the left subtree and [t1] the right one, or
- the converse. Computing the first branching bit of [p0] and [p1]
- uses a nice property of twos-complement representation of integers. *)
-
-let lowest_bit x = x land (-x)
-
-let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
-
-let mask p m = p land (m-1)
-
-let join (p0,t0,p1,t1) =
- let m = branching_bit p0 p1 in
- if zero_bit p0 m then
- Branch (mask p0 m, m, t0, t1)
- else
- Branch (mask p0 m, m, t1, t0)
-
-(*s Then the insertion of value [k] in set [t] is easily implemented
- using [join]. Insertion in a singleton is just the identity or a
- call to [join], depending on the value of [k]. When inserting in
- a branching tree, we first check if the value to insert [k]
- matches the prefix [p]: if not, [join] will take care of creating
- the above branching; if so, we just insert [k] in the appropriate
- subtree, depending of the branching bit. *)
-
-let match_prefix k p m = (mask k m) == p
-
-let add k t =
- let rec ins = function
- | Empty -> Leaf k
- | Leaf j as t ->
- if j == k then t else join (k, Leaf k, j, t)
- | Branch (p,m,t0,t1) as t ->
- if match_prefix k p m then
- if zero_bit k m then
- Branch (p, m, ins t0, t1)
- else
- Branch (p, m, t0, ins t1)
- else
- join (k, Leaf k, p, t)
- in
- ins t
-
-(*s The code to remove an element is basically similar to the code of
- insertion. But since we have to maintain the invariant that both
- subtrees of a [Branch] node are non-empty, we use here the
- ``smart constructor'' [branch] instead of [Branch]. *)
-
-let branch = function
- | (_,_,Empty,t) -> t
- | (_,_,t,Empty) -> t
- | (p,m,t0,t1) -> Branch (p,m,t0,t1)
-
-let remove k t =
- let rec rmv = function
- | Empty -> Empty
- | Leaf j as t -> if k == j then Empty else t
- | Branch (p,m,t0,t1) as t ->
- if match_prefix k p m then
- if zero_bit k m then
- branch (p, m, rmv t0, t1)
- else
- branch (p, m, t0, rmv t1)
- else
- t
- in
- rmv t
-
-(*s One nice property of Patricia trees is to support a fast union
- operation (and also fast subset, difference and intersection
- operations). When merging two branching trees we examine the
- following four cases: (1) the trees have exactly the same
- prefix; (2/3) one prefix contains the other one; and (4) the
- prefixes disagree. In cases (1), (2) and (3) the recursion is
- immediate; in case (4) the function [join] creates the appropriate
- branching. *)
-
-let rec merge = function
- | Empty, t -> t
- | t, Empty -> t
- | Leaf k, t -> add k t
- | t, Leaf k -> add k t
- | (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
- if m == n && match_prefix q p m then
- (* The trees have the same prefix. Merge the subtrees. *)
- Branch (p, m, merge (s0,t0), merge (s1,t1))
- else if m < n && match_prefix q p m then
- (* [q] contains [p]. Merge [t] with a subtree of [s]. *)
- if zero_bit q m then
- Branch (p, m, merge (s0,t), s1)
- else
- Branch (p, m, s0, merge (s1,t))
- else if m > n && match_prefix p q n then
- (* [p] contains [q]. Merge [s] with a subtree of [t]. *)
- if zero_bit p n then
- Branch (q, n, merge (s,t0), t1)
- else
- Branch (q, n, t0, merge (s,t1))
- else
- (* The prefixes disagree. *)
- join (p, s, q, t)
-
-let union s t = merge (s,t)
-
-(*s When checking if [s1] is a subset of [s2] only two of the above
- four cases are relevant: when the prefixes are the same and when the
- prefix of [s1] contains the one of [s2], and then the recursion is
- obvious. In the other two cases, the result is [false]. *)
-
-let rec subset s1 s2 = match (s1,s2) with
- | Empty, _ -> true
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | Branch _, Leaf _ -> false
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- subset l1 l2 && subset r1 r2
- else if m1 > m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then
- subset l1 l2 && subset r1 l2
- else
- subset l1 r2 && subset r1 r2
- else
- false
-
-(*s To compute the intersection and the difference of two sets, we
- still examine the same four cases as in [merge]. The recursion is
- then obvious. *)
-
-let rec inter s1 s2 = match (s1,s2) with
- | Empty, _ -> Empty
- | _, Empty -> Empty
- | Leaf k1, _ -> if mem k1 s2 then s1 else Empty
- | _, Leaf k2 -> if mem k2 s1 then s2 else Empty
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (inter l1 l2, inter r1 r2)
- else if m1 < m2 && match_prefix p2 p1 m1 then
- inter (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 > m2 && match_prefix p1 p2 m2 then
- inter s1 (if zero_bit p1 m2 then l2 else r2)
- else
- Empty
-
-let rec diff s1 s2 = match (s1,s2) with
- | Empty, _ -> Empty
- | _, Empty -> s1
- | Leaf k1, _ -> if mem k1 s2 then Empty else s1
- | _, Leaf k2 -> remove k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (diff l1 l2, diff r1 r2)
- else if m1 < m2 && match_prefix p2 p1 m1 then
- if zero_bit p2 m1 then
- merge (diff l1 s2, r1)
- else
- merge (l1, diff r1 s2)
- else if m1 > m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
- else
- s1
-
-(*s All the following operations ([cardinal], [iter], [fold], [for_all],
- [exists], [filter], [partition], [choose], [elements]) are
- implemented as for any other kind of binary trees. *)
-
-let rec cardinal = function
- | Empty -> 0
- | Leaf _ -> 1
- | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
-
-let rec iter f = function
- | Empty -> ()
- | Leaf k -> f k
- | Branch (_,_,t0,t1) -> iter f t0; iter f t1
-
-let rec fold f s accu = match s with
- | Empty -> accu
- | Leaf k -> f k accu
- | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
-
-let rec for_all p = function
- | Empty -> true
- | Leaf k -> p k
- | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
-
-let rec exists p = function
- | Empty -> false
- | Leaf k -> p k
- | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
-
-let rec filter pr = function
- | Empty -> Empty
- | Leaf k as t -> if pr k then t else Empty
- | Branch (p,m,t0,t1) -> branch (p, m, filter pr t0, filter pr t1)
-
-let partition p s =
- let rec part (t,f as acc) = function
- | Empty -> acc
- | Leaf k -> if p k then (add k t, f) else (t, add k f)
- | Branch (_,_,t0,t1) -> part (part acc t0) t1
- in
- part (Empty, Empty) s
-
-let rec choose = function
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
-
-let elements s =
- let rec elements_aux acc = function
- | Empty -> acc
- | Leaf k -> k :: acc
- | Branch (_,_,l,r) -> elements_aux (elements_aux acc l) r
- in
- (* unfortunately there is no easy way to get the elements in ascending
- order with little-endian Patricia trees *)
- List.sort Pervasives.compare (elements_aux [] s)
-
-let split x s =
- let coll k (l, b, r) =
- if k < x then add k l, b, r
- else if k > x then l, b, add k r
- else l, true, r
- in
- fold coll s (Empty, false, Empty)
-
-(*s There is no way to give an efficient implementation of [min_elt]
- and [max_elt], as with binary search trees. The following
- implementation is a traversal of all elements, barely more
- efficient than [fold min t (choose t)] (resp. [fold max t (choose
- t)]). Note that we use the fact that there is no constructor
- [Empty] under [Branch] and therefore always a minimal
- (resp. maximal) element there. *)
-
-let rec min_elt = function
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,s,t) -> min (min_elt s) (min_elt t)
-
-let rec max_elt = function
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,s,t) -> max (max_elt s) (max_elt t)
-
-(*s Another nice property of Patricia trees is to be independent of the
- order of insertion. As a consequence, two Patricia trees have the
- same elements if and only if they are structurally equal. *)
-
-let equal = (=)
-
-let compare = compare
-
-(*i*)
-let make l = List.fold_right add l empty
-(*i*)
-
-(*s Additional functions w.r.t to [Set.S]. *)
-
-let rec intersect s1 s2 = match (s1,s2) with
- | Empty, _ -> false
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | _, Leaf k2 -> mem k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- intersect l1 l2 || intersect r1 r2
- else if m1 < m2 && match_prefix p2 p1 m1 then
- intersect (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 > m2 && match_prefix p1 p2 m2 then
- intersect s1 (if zero_bit p1 m2 then l2 else r2)
- else
- false
-
-
-(*s Big-endian Patricia trees *)
-
-module Big = struct
-
- type elt = int
-
- type t_ = t
- type t = t_
-
- let empty = Empty
-
- let is_empty = function Empty -> true | _ -> false
-
- let singleton k = Leaf k
-
- let zero_bit k m = (k land m) == 0
-
- let rec mem k = function
- | Empty -> false
- | Leaf j -> k == j
- | Branch (_, m, l, r) -> mem k (if zero_bit k m then l else r)
-
- let mask k m = (k lor (m-1)) land (lnot m)
-
- (* we first write a naive implementation of [highest_bit]
- only has to work for bytes *)
- let naive_highest_bit x =
- assert (x < 256);
- let rec loop i =
- if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
- in
- loop 7
-
- (* then we build a table giving the highest bit for bytes *)
- let hbit = Array.init 256 naive_highest_bit
-
- (* to determine the highest bit of [x] we split it into bytes *)
- let highest_bit_32 x =
- let n = x lsr 24 in if n != 0 then hbit.(n) lsl 24
- else let n = x lsr 16 in if n != 0 then hbit.(n) lsl 16
- else let n = x lsr 8 in if n != 0 then hbit.(n) lsl 8
- else hbit.(x)
-
- let highest_bit_64 x =
- let n = x lsr 32 in if n != 0 then (highest_bit_32 n) lsl 32
- else highest_bit_32 x
-
- let highest_bit = match Sys.word_size with
- | 32 -> highest_bit_32
- | 64 -> highest_bit_64
- | _ -> assert false
-
- let branching_bit p0 p1 = highest_bit (p0 lxor p1)
-
- let join (p0,t0,p1,t1) =
- (*i let m = function Branch (_,m,_,_) -> m | _ -> 0 in i*)
- let m = branching_bit p0 p1 (*EXP (m t0) (m t1) *) in
- if zero_bit p0 m then
- Branch (mask p0 m, m, t0, t1)
- else
- Branch (mask p0 m, m, t1, t0)
-
- let match_prefix k p m = (mask k m) == p
-
- let add k t =
- let rec ins = function
- | Empty -> Leaf k
- | Leaf j as t ->
- if j == k then t else join (k, Leaf k, j, t)
- | Branch (p,m,t0,t1) as t ->
- if match_prefix k p m then
- if zero_bit k m then
- Branch (p, m, ins t0, t1)
- else
- Branch (p, m, t0, ins t1)
- else
- join (k, Leaf k, p, t)
- in
- ins t
-
- let remove k t =
- let rec rmv = function
- | Empty -> Empty
- | Leaf j as t -> if k == j then Empty else t
- | Branch (p,m,t0,t1) as t ->
- if match_prefix k p m then
- if zero_bit k m then
- branch (p, m, rmv t0, t1)
- else
- branch (p, m, t0, rmv t1)
- else
- t
- in
- rmv t
-
- let rec merge = function
- | Empty, t -> t
- | t, Empty -> t
- | Leaf k, t -> add k t
- | t, Leaf k -> add k t
- | (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
- if m == n && match_prefix q p m then
- (* The trees have the same prefix. Merge the subtrees. *)
- Branch (p, m, merge (s0,t0), merge (s1,t1))
- else if m > n && match_prefix q p m then
- (* [q] contains [p]. Merge [t] with a subtree of [s]. *)
- if zero_bit q m then
- Branch (p, m, merge (s0,t), s1)
- else
- Branch (p, m, s0, merge (s1,t))
- else if m < n && match_prefix p q n then
- (* [p] contains [q]. Merge [s] with a subtree of [t]. *)
- if zero_bit p n then
- Branch (q, n, merge (s,t0), t1)
- else
- Branch (q, n, t0, merge (s,t1))
- else
- (* The prefixes disagree. *)
- join (p, s, q, t)
-
- let union s t = merge (s,t)
-
- let rec subset s1 s2 = match (s1,s2) with
- | Empty, _ -> true
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | Branch _, Leaf _ -> false
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- subset l1 l2 && subset r1 r2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then
- subset l1 l2 && subset r1 l2
- else
- subset l1 r2 && subset r1 r2
- else
- false
-
- let rec inter s1 s2 = match (s1,s2) with
- | Empty, _ -> Empty
- | _, Empty -> Empty
- | Leaf k1, _ -> if mem k1 s2 then s1 else Empty
- | _, Leaf k2 -> if mem k2 s1 then s2 else Empty
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (inter l1 l2, inter r1 r2)
- else if m1 > m2 && match_prefix p2 p1 m1 then
- inter (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- inter s1 (if zero_bit p1 m2 then l2 else r2)
- else
- Empty
-
- let rec diff s1 s2 = match (s1,s2) with
- | Empty, _ -> Empty
- | _, Empty -> s1
- | Leaf k1, _ -> if mem k1 s2 then Empty else s1
- | _, Leaf k2 -> remove k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- merge (diff l1 l2, diff r1 r2)
- else if m1 > m2 && match_prefix p2 p1 m1 then
- if zero_bit p2 m1 then
- merge (diff l1 s2, r1)
- else
- merge (l1, diff r1 s2)
- else if m1 < m2 && match_prefix p1 p2 m2 then
- if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
- else
- s1
-
- (* same implementation as for little-endian Patricia trees *)
- let cardinal = cardinal
- let iter = iter
- let fold = fold
- let for_all = for_all
- let exists = exists
- let filter = filter
-
- let partition p s =
- let rec part (t,f as acc) = function
- | Empty -> acc
- | Leaf k -> if p k then (add k t, f) else (t, add k f)
- | Branch (_,_,t0,t1) -> part (part acc t0) t1
- in
- part (Empty, Empty) s
-
- let choose = choose
-
- let elements s =
- let rec elements_aux acc = function
- | Empty -> acc
- | Leaf k -> k :: acc
- | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
- in
- (* we still have to sort because of possible negative elements *)
- List.sort Pervasives.compare (elements_aux [] s)
-
- let split x s =
- let coll k (l, b, r) =
- if k < x then add k l, b, r
- else if k > x then l, b, add k r
- else l, true, r
- in
- fold coll s (Empty, false, Empty)
-
- (* could be slightly improved (when we now that a branch contains only
- positive or only negative integers) *)
- let min_elt = min_elt
- let max_elt = max_elt
-
- let equal = (=)
-
- let compare = compare
-
- let make l = List.fold_right add l empty
-
- let rec intersect s1 s2 = match (s1,s2) with
- | Empty, _ -> false
- | _, Empty -> false
- | Leaf k1, _ -> mem k1 s2
- | _, Leaf k2 -> mem k2 s1
- | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
- if m1 == m2 && p1 == p2 then
- intersect l1 l2 || intersect r1 r2
- else if m1 > m2 && match_prefix p2 p1 m1 then
- intersect (if zero_bit p2 m1 then l1 else r1) s2
- else if m1 < m2 && match_prefix p1 p2 m2 then
- intersect s1 (if zero_bit p1 m2 then l2 else r2)
- else
- false
-
-end
-
-(*s Big-endian Patricia trees with non-negative elements only *)
-
-module BigPos = struct
-
- include Big
-
- let singleton x = if x < 0 then invalid_arg "BigPos.singleton"; singleton x
-
- let add x s = if x < 0 then invalid_arg "BigPos.add"; add x s
-
- (* Patricia trees are now binary search trees! *)
-
- let rec mem k = function
- | Empty -> false
- | Leaf j -> k == j
- | Branch (p, _, l, r) -> if k <= p then mem k l else mem k r
-
- let rec min_elt = function
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,s,_) -> min_elt s
-
- let rec max_elt = function
- | Empty -> raise Not_found
- | Leaf k -> k
- | Branch (_,_,_,t) -> max_elt t
-
- (* we do not have to sort anymore *)
- let elements s =
- let rec elements_aux acc = function
- | Empty -> acc
- | Leaf k -> k :: acc
- | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
- in
- elements_aux [] s
-
-end
-
-(*s EXPERIMENT: Big-endian Patricia trees with swapped bit sign *)
-
-module Bigo = struct
-
- include Big
-
- (* swaps the sign bit *)
- let swap x = if x < 0 then x land max_int else x lor min_int
-
- let mem x s = mem (swap x) s
-
- let add x s = add (swap x) s
-
- let singleton x = singleton (swap x)
-
- let remove x s = remove (swap x) s
-
- let elements s = List.map swap (elements s)
-
- let choose s = swap (choose s)
-
- let iter f = iter (fun x -> f (swap x))
-
- let fold f = fold (fun x a -> f (swap x) a)
-
- let for_all f = for_all (fun x -> f (swap x))
-
- let exists f = exists (fun x -> f (swap x))
-
- let filter f = filter (fun x -> f (swap x))
-
- let partition f = partition (fun x -> f (swap x))
-
- let split x s = split (swap x) s
-
- let rec min_elt = function
- | Empty -> raise Not_found
- | Leaf k -> swap k
- | Branch (_,_,s,_) -> min_elt s
-
- let rec max_elt = function
- | Empty -> raise Not_found
- | Leaf k -> swap k
- | Branch (_,_,_,t) -> max_elt t
-
-end
-
-let test empty add mem =
- let seed = Random.int max_int in
- Random.init seed;
- let s =
- let rec loop s i =
- if i = 1000 then s else loop (add (Random.int max_int) s) (succ i)
- in
- loop empty 0
- in
- Random.init seed;
- for i = 0 to 999 do assert (mem (Random.int max_int) s) done
-
-
Deleted: trunk/Toss/Formula/Sat/IntSet.mli
===================================================================
--- trunk/Toss/Formula/Sat/IntSet.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Formula/Sat/IntSet.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,111 +0,0 @@
-(**************************************************************************)
-(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
-(* *)
-(* This software is free software; you can redistribute it and/or *)
-(* modify it under the terms of the GNU Library General Public *)
-(* License version 2.1, with the special exception on linking *)
-(* described in file LICENSE. *)
-(* *)
-(* This software is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
-(* *)
-(**************************************************************************)
-
-(*i $Id: ptset.mli,v 1.10 2008-07-21 14:53:06 filliatr Exp $ i*)
-
-(*s Sets of integers implemented as Patricia trees. The following
- signature is exactly [Set.S with type elt = int], with the same
- specifications. This is a purely functional data-structure. The
- performances are similar to those of the standard library's module
- [Set]. The representation is unique and thus structural comparison
- can be performed on Patricia trees. *)
-
-type t
-
-type elt = int
-
-val empty : t
-
-val is_empty : t -> bool
-
-val mem : int -> t -> bool
-
-val add : int -> t -> t
-
-val singleton : int -> t
-
-val is_singleton : t -> bool
-
-val remove : int -> t -> t
-
-val union : t -> t -> t
-
-val subset : t -> t -> bool
-
-val inter : t -> t -> t
-
-val diff : t -> t -> t
-
-val equal : t -> t -> bool
-
-val compare : t -> t -> int
-
-val elements : t -> int list
-
-val choose : t -> int
-
-val cardinal : t -> int
-
-val iter : (int -> unit) -> t -> unit
-
-val fold : (int -> 'a -> 'a) -> t -> 'a -> 'a
-
-val for_all : (int -> bool) -> t -> bool
-
-val exists : (int -> bool) -> t -> bool
-
-val filter : (int -> bool) -> t -> t
-
-val partition : (int -> bool) -> t -> t * t
-
-val split : int -> t -> t * bool * t
-
-(*s Warning: [min_elt] and [max_elt] are linear w.r.t. the size of the
- set. In other words, [min_elt t] is barely more efficient than [fold
- min t (choose t)]. *)
-
-val min_elt : t -> int
-val max_elt : t -> int
-
-(*s Additional functions not appearing in the signature [Set.S] from ocaml
- standard library. *)
-
-(* [intersect u v] determines if sets [u] and [v] have a non-empty
- intersection. *)
-
-val intersect : t -> t -> bool
-
-
-(*s Big-endian Patricia trees *)
-
-module Big : sig
- include Set.S with type elt = int
- val intersect : t -> t -> bool
-end
-
-
-(*s Big-endian Patricia trees with non-negative elements. Changes:
- - [add] and [singleton] raise [Invalid_arg] if a negative element is given
- - [mem] is slightly faster (the Patricia tree is now a search tree)
- - [min_elt] and [max_elt] are now O(log(N))
- - [elements] returns a list with elements in ascending order
- *)
-
-module BigPos : sig
- include Set.S with type elt = int
- val intersect : t -> t -> bool
-end
-
-
Modified: trunk/Toss/Formula/Sat/Sat.mli
===================================================================
--- trunk/Toss/Formula/Sat/Sat.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Formula/Sat/Sat.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,46 +1,49 @@
-(* Basic interface to a sat solver and convertion between cnf and dnf formulas.
- Variables are given by positive integers and we use -n to denote 'not n'. *)
+(** Basic interface to a sat solver and convertion between cnf and dnf formulas.
+ Variables are given by positive integers and we use -n to denote 'not n'. *)
-(* ------- Main functions ------- *)
+(** {2 Main Functions} *)
(** Set timeout function for conversions. *)
val set_timeout : float -> unit
+
(** Clear timeout function. *)
val clear_timeout : unit -> unit
-
-(* Given a list of literals to set to true, simplify the given CNF formula. *)
+(** Given a list of literals to set to true, simplify the given CNF formula. *)
val simplify : int list -> int list list -> int list list
-(* Check satisfiability of a formula in CNF, return a satisfying assignment. *)
+(** Check satisfiability of a formula in CNF, return a satisfying assignment. *)
val sat : int list list -> int list option
+
+(** Check satisfiability of a formula in CNF, return just true or false. *)
val is_sat : int list list -> bool
-(* Convert a DNF formula to CNF (or equivalently, CNF to DNF). *)
exception OverBound
+
+(** Convert a DNF formula to CNF (or equivalently, CNF to DNF). *)
val convert : ?disc_vars: int list -> ?bound: int option -> int list list ->
int list list
-(* Convert a auxiliary CNF formula to "real" CNF (or, equivalently, to DNF). *)
+(** Convert a auxiliary CNF formula to "real" CNF (or, equivalently, to DNF). *)
val convert_aux_cnf : ?disc_vars: int list -> ?bound: int option ->
int -> int list list -> int list list
-(* ----- Printing helpers ------ *)
+(** {2 Printing} *)
-(* Return the given clause (disjunction of literals) as string. *)
+(** Return the given clause (disjunction of literals) as string. *)
val clause_str : int list -> string
-(* Return the given CNF formula as string. *)
+(** Return the given CNF formula as string. *)
val cnf_str : int list list -> string
-(* Return the given conjunction of literals as string. *)
+(** Return the given conjunction of literals as string. *)
val conjunct_str : int list -> string
-(* Return the given DNF formula as string. *)
+(** Return the given DNF formula as string. *)
val dnf_str : int list list -> string
-(* ------------------------- DEBUGGING ------------------------------------- *)
+(** {2 Debugging} *)
-(* Debugging information. At level 0 nothing is printed out. *)
+(** Debugging information. At level 0 nothing is printed out. *)
val set_debug_level : int -> unit
Modified: trunk/Toss/GGP/GameSimpl.mli
===================================================================
--- trunk/Toss/GGP/GameSimpl.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/GGP/GameSimpl.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(** {2 Simplification of Toss Games.}
+(** {2 Simplification of Toss games.}
Whole-game simplifications and helper functions that consider both
a structure and a formula.
Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/GGP/TranslateFormula.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,3 +1,5 @@
+(** Translating formulas from GDL to Toss. *)
+
val debug_level : int ref
(** Whether to add root predicates. Note that not adding root
Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/GGP/TranslateGame.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,3 +1,5 @@
+(** Translating games from GDL to Toss. *)
+
(** Local level of logging. *)
val debug_level : int ref
val generate_test_case : string option ref
Modified: trunk/Toss/Server/DB.mli
===================================================================
--- trunk/Toss/Server/DB.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Server/DB.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,3 +1,6 @@
+(** Interface to the Toss database through Sqlite. *)
+
+
exception DBError of string
val debug_level : int ref
Modified: trunk/Toss/Server/Picture.mli
===================================================================
--- trunk/Toss/Server/Picture.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Server/Picture.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(** Processing Pictures to create Structures *)
+(** Processing pictures to create structures *)
(** {2 Debugging} *)
Modified: trunk/Toss/Server/ReqHandler.mli
===================================================================
--- trunk/Toss/Server/ReqHandler.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Server/ReqHandler.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(** Main Request Handler for Toss. *)
+(** Main request handler for Toss. *)
(** {2 Debugging} *)
@@ -35,5 +35,5 @@
req_state * bool
-(* Client db game setting - public only for caching reasons. *)
+(** Client db game setting - public only for caching reasons. *)
val client_set_game : string -> unit
Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/AssignmentSet.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,5 +1,4 @@
-(** This module contains the main type for partial assignments of
- values to variables. *)
+(** Main type for partial assignments of elements to variables. *)
(** {2 Basic type definition.} *)
Modified: trunk/Toss/Solver/Assignments.mli
===================================================================
--- trunk/Toss/Solver/Assignments.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/Assignments.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,7 +1,4 @@
-(** This module contains functions for handling partial assignments of
- values to variables. The main type [assignmnent_set] represents
- a set of assignments of values to variables and the main functions
- are [join], [sum], [project] and [complement] with natural meanings. *)
+(** Handling partial assignments of elements to variables. *)
(** {2 Basic Type Definition} *)
Modified: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/Distinguish.ml 2011-11-17 23:56:41 UTC (rev 1635)
@@ -190,7 +190,7 @@
(* Helper function: remove atoms from a formula if [cond] is still satisfied.
Note that this is just a greedy heuristic, only And/Or and into Ex/All. *)
-let rec greedy_remove cond phi =
+let rec greedy_remove ?(pos=false) cond phi =
let rec greedy_remove_list constructor acc = function
| [] -> acc
| x :: xs ->
@@ -200,8 +200,10 @@
greedy_remove_list constructor (minx::acc) xs in
match phi with
| And fl -> And (greedy_remove_list (fun l -> And l) [] (List.rev fl))
- | Or fl -> Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
- | Not f -> Not (greedy_remove (fun x -> cond (Not x)) f)
+ | Or fl -> if pos then Or fl else
+ Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
+ | Not f -> if pos then Not f else
+ Not (greedy_remove (fun x -> cond (Not x)) f)
| Ex (vs, f) -> Ex (vs, greedy_remove (fun x -> cond (Ex (vs, x))) f)
| All (vs, f) -> All (vs, greedy_remove (fun x -> cond (All (vs, x))) f)
| phi -> phi
@@ -231,20 +233,21 @@
| GuardedFO -> guarded_types s ~qr ~k
| FO -> ntypes s ~qr ~k in
let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
- let pos_tps = Aux.unique_sorted ~cmp:!compare_types (
- Aux.map_some (min_type_omitting ~logic ~qr ~k neg_tps) pos_strucs) in
- let fails_neg f = not (List.exists (fun s -> check s [||] f) neg_strucs) in
- let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_strucs in
- let rec find_type acc = function
- | [] -> []
- | x :: xs -> if succ_pos (x::acc) then x :: acc else
- find_type (x::acc) xs in
- let dtypes = find_type [] pos_tps in
- if dtypes = [] then None else
- let is_ok f = fails_neg f && succ_pos [f] in
- let mintp = greedy_remove is_ok (Or dtypes) in
- let fv = FormulaSubst.free_vars mintp in
- Some (FormulaOps.rename_quant_avoiding fv mintp)
+ 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
+ match min_type_omitting ~logic ~qr ~k neg_tps struc with
+ | None -> raise Not_found
+ | Some f -> (greedy_remove ~pos:true fails_on_negs f) :: acc in
+ let pos_formulas =
+ try List.fold_left extend_by_pos [] pos_strucs with Not_found -> [] in
+ let pos_formulas = Aux.unique_sorted ~cmp:!compare_types pos_formulas in
+ if pos_formulas = [] then None else
+ let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_strucs in
+ let is_ok f = fails_on_negs f && succ_pos [f] in
+ let minimized = greedy_remove is_ok (Or pos_formulas) in
+ let fv = FormulaSubst.free_vars minimized in
+ Some (FormulaOps.rename_quant_avoiding fv minimized)
(* Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
Modified: trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,31 +1,31 @@
-(* Polynomials with ordered variables, integer coefficients.*)
+(** Polynomials with ordered variables and integer coefficients.*)
-(* ----------------------- BASIC TYPE DEFINITIONS --------------------------- *)
+(** {2 Basic Type Definitions} *)
type polynomial = Const of Num.num | Poly of string * (polynomial * int) list
-type t = polynomial (* to be compatible with OrderedType signature *)
+type t = polynomial (** to be compatible with OrderedType signature *)
exception Unmatched_variables
-(* Constructur 'Const' but taking normal integers. *)
+(** Constructur 'Const' but taking normal integers. *)
val const : int -> polynomial
-(* ------------------------- PRINTING FUNCTION ------------------------------ *)
+(** {2 Printing} *)
val str : polynomial -> string
-(* ------------------------- EQUALITY AND COMPARISON ------------------------ *)
+(** {2 Equality and Comparison} *)
val is_zero : polynomial -> bool
val equal : polynomial -> polynomial -> bool
val compare : polynomial -> polynomial -> int
-(* ------------------------- BASIC HELPER FUNCTIONS ------------------------- *)
+(** {Basic Operations} *)
val var : polynomial -> string
val lower : polynomial -> polynomial
@@ -39,7 +39,7 @@
val constant_factors : polynomial -> polynomial -> (Num.num * Num.num) option
-(* -------------------------- ARITHMETIC FUNCTIONS -------------------------- *)
+(** {2 Arithmetic Functions} *)
val add : polynomial -> polynomial -> polynomial
val neg : polynomial -> polynomial
@@ -51,11 +51,11 @@
polynomial * polynomial
-(* -------------------------- DIFFERENTIATION ------------------------------- *)
+(** {2 Differentiation} *)
val diff : polynomial -> polynomial
-(* ------------------------- MODIFIED REMAINDER ----------------------------- *)
+(** {2 Modified remainder} *)
val modified_remainder : polynomial -> polynomial -> polynomial
Modified: trunk/Toss/Solver/RealQuantElim/OrderedPolySet.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/OrderedPolySet.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/RealQuantElim/OrderedPolySet.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,11 +1,11 @@
-(* Represent set of ordered polynomials and operate on it. *)
+(** Represent set of ordered polynomials and operate on it. *)
module PSet : Set.S with type elt = OrderedPoly.polynomial
type pset = PSet.t
-(* ------------------------ BASIC SET OPERATIONS ---------------------------- *)
+(** {2 Basic Set Operations} *)
val empty : PSet.t
val add : OrderedPoly.polynomial -> PSet.t -> PSet.t
@@ -15,50 +15,50 @@
val elements : PSet.t -> OrderedPoly.polynomial list
-(* ------------------------ PRINTING FUNCTION ------------------------------- *)
+(** {2 Printing} *)
-(* Print the given set as string. *)
+(** Print the given set as string. *)
val str : PSet.t -> string
-(* ------------- MAPPING WITH DEGREE DETECTION AND BASIC MAPS --------------- *)
+(** {2 Mapping with degree detection and basic maps} *)
-(* Maps a function to all polynomials in the set. Returns non-empty
- resulting polynomials of degree 0 and greater separately. *)
+(** Maps a function to all polynomials in the set. Returns non-empty
+ resulting polynomials of degree 0 and greater separately. *)
val map : (OrderedPoly.polynomial -> OrderedPoly.polynomial) -> PSet.t ->
PSet.t * PSet.t
-(* Extract leading coefficients from all polynomials in the set. *)
+(** Extract leading coefficients from all polynomials in the set. *)
val leading_coeff : PSet.t -> PSet.t
-(* Omit leading coefficients from all polynomials in the given set.
- Return resulting polynomials of degree 0 and greater separately. *)
+(** Omit leading coefficients from all polynomials in the given set.
+ Return resulting polynomials of degree 0 and greater separately. *)
val omit_leading : PSet.t -> PSet.t * PSet.t
-(* Differentiate all polynomials in the given set.
- Return resulting polynomials of degree 0 and greater separately. *)
+(** Differentiate all polynomials in the given set.
+ Return resulting polynomials of degree 0 and greater separately. *)
val differentiate: PSet.t -> PSet.t * PSet.t
-(* Compute factors r such that for some p,q in [ps,qs] holds p = r*q. *)
+(** Compute factors r such that for some p,q in [ps,qs] holds p = r*q. *)
val div : PSet.t -> PSet.t -> PSet.t
-(* ------------ MODIFIED REMAINDER OF ALL PAIRS BETWEEN TWO SETS ------------ *)
+(** {2 Modified remainder of all pairs between two sets} *)
-(* Compute the modified remainder for all pairs of polynomials p from
- ps1 and q!=p from qs1 such that the degree of p >= degree of q.
- Return resulting polynomials of degree 0 and greater separately. *)
+(** Compute the modified remainder for all pairs of polynomials p from
+ ps1 and q!=p from qs1 such that the degree of p >= degree of q.
+ Return resulting polynomials of degree 0 and greater separately. *)
val modified_remainder : PSet.t * PSet.t -> PSet.t * PSet.t
-(* ---------------- CLOSURE UNDER 4 ABOVE OPERATIONS ------------------------ *)
+(** {2 Closure under the 4 operations above} *)
exception Closure_count_exceeded of int
-(* Closure of a set of polynomials [polys] under the operations:
- - extracting the leading coefficient (if deg > 0)
- - omitting the leading term (if deg > 0)
- - taking the derivative (if deg > 0)
- - taking the modified remainder MR(p, q) for deg p >= deg q.
- Return resulting polynomials of degree 0 and greater separately. *)
+(** Closure of a set of polynomials [polys] under the operations:
+ - extracting the leading coefficient (if deg > 0)
+ - omitting the leading term (if deg > 0)
+ - taking the derivative (if deg > 0)
+ - taking the modified remainder MR(p, q) for deg p >= deg q.
+ Return resulting polynomials of degree 0 and greater separately. *)
val closure : ?upto : int -> PSet.t -> PSet.t * PSet.t
Modified: trunk/Toss/Solver/RealQuantElim/Poly.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/Poly.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/RealQuantElim/Poly.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,6 +1,6 @@
-(* Represent polynomials as written and convert to ordered form. *)
+(** Represent polynomials as written and convert to ordered form. *)
-(* ---------------------- BASIC TYPE DEFINITION ----------------------------- *)
+(** {2 Basic Type Definition} *)
type polynomial =
Var of string
@@ -9,22 +9,22 @@
| Plus of polynomial * polynomial
-(* ------------------------ PRINTING FUNCTION ------------------------------- *)
+(** {2 Printing} *)
-(* Print a polynomial as a string. *)
+(** Print a polynomial as a string. *)
val str : polynomial -> string
-(* ------------------ HELPER POWER FUNCTION USED IN PARSER ------------------ *)
+(** {Basic Functions used in Parser} *)
-(* Power function used in parser. *)
+(** Power function used in parser. *)
val pow : polynomial -> int -> polynomial
-(* Basic simplification, reduces constant polynomials to integers. *)
+(** Basic simplification, reduces constant polynomials to integers. *)
val simp_const : polynomial -> polynomial
-(* ----------------- CONVERTION TO UNORDERED POLYNOMIALS -------------------- *)
+(** {2 Convertion to Unordered Polynomials} *)
val make_unordered : OrderedPoly.polynomial -> polynomial
@@ -32,24 +32,24 @@
(polynomial * 'a) list
-(* ------------------ CONVERTION TO ORDERED POLYNOMIALS --------------------- *)
+(** {2 Convertion to Ordered Polynomials} *)
-(* List variables in the given polynomial. *)
+(** List variables in the given polynomial. *)
val vars : polynomial -> string list
-(* List variables in the given polynomial list. *)
+(** List variables in the given polynomial list. *)
val vars_list : polynomial list -> string list
-(* Make an ordered polynomial from [p] with [prio_list] order on variables, i.e.
- if x appears in [prio_list] before y then x < y. Strings not appearing
- in [prio_list] at all are considered smaller than any string that appears. *)
+(** Make an ordered polynomial from [p] with [prio_list] order on variables,i.e.
+ if x appears in [prio_list] before y then x < y. Strings not appearing
+ in [prio_list] at all are considered smaller than any string that appears.*)
val make_ordered : string list -> polynomial -> OrderedPoly.polynomial
-(* Make ordered polynomials from [ps] with [prio_list] order on variables. *)
+(** Make ordered polynomials from [ps] with [prio_list] order on variables. *)
val make_ordered_list : string list -> polynomial list ->
OrderedPoly.polynomial list
-(* Make ordered polynomials from first components of [ps], [prio_list] order. *)
+(** Make ordered polynomials from first components of [ps], [prio_list] order.*)
val make_ordered_pair_list : string list -> (polynomial * 'a) list ->
(OrderedPoly.polynomial * 'a) list
Modified: trunk/Toss/Solver/RealQuantElim/RealQuantElim.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/RealQuantElim.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/RealQuantElim/RealQuantElim.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(* Simplify existentially quantified conjunction of polynomial inequalities. *)
+(** Simplify existentially quantified conjunction of polynomial inequalities. *)
open OrderedPolySet
Modified: trunk/Toss/Solver/RealQuantElim/SignTable.mli
===================================================================
--- trunk/Toss/Solver/RealQuantElim/SignTable.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/RealQuantElim/SignTable.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,42 +1,42 @@
-(* Handling Sign Tables for quantifier elimination. *)
+(** Handling sign tables for quantifier elimination. *)
open Formula
val poly_sign_op_cmp : OrderedPoly.polynomial * sign_op ->
OrderedPoly.polynomial * sign_op -> int
-(* Exception raised when contraditing ops are given to join_sign_ops. *)
+(** Exception raised when contraditing ops are given to join_sign_ops. *)
exception Contradicting_sign_ops
-(* Given two sign_ops [x] and [y] return a sign op for "x and y". *)
+(** Given two sign_ops [x] and [y] return a sign op for "x and y". *)
val join_sign_ops : sign_op -> sign_op -> sign_op
-(* Print a sign_op as string. *)
+(** Print a sign_op as string. *)
val sign_op_str : sign_op -> string
-(* Check if given float has sign as required by the sign_op. *)
+(** Check if given float has sign as required by the sign_op. *)
val check_sign : float -> sign_op -> bool
-(* Negate a sign_op. *)
+(** Negate a sign_op. *)
val neg_sign_op : sign_op -> sign_op
-(* Print a case, i.e. a list of polynomials and their signs, as string. *)
+(** Print a case, i.e. a list of polynomials and their signs, as string. *)
val int_case_str : (OrderedPoly.polynomial * int) list -> string
val case_str : (OrderedPoly.polynomial * sign_op) list -> string
-(* Estimate the (base-3) logarithm of the number of cases needed for [pset]. *)
+(** Estimate the (base-3) logarithm of the number of cases needed for [pset]. *)
val log_no_cases : ?upto: int -> (OrderedPoly.polynomial * sign_op) list -> int
-(* Build the array of polynomials and cases to check given set of polynomials.*)
+(** Build array of polynomials and cases to check given set of polynomials. *)
val build_cases : (OrderedPoly.polynomial * sign_op) list ->
(OrderedPoly.polynomial * int) list list * OrderedPoly.polynomial array
-(* Given cases and polynomial array as constructed by [build_cases] and
- requirement list for some polynomials, return all satisfying cases. *)
+(** Given cases and polynomial array as constructed by [build_cases] and
+ requirement list for some polynomials, return all satisfying cases. *)
val solve : (OrderedPoly.polynomial * int) list list *
OrderedPoly.polynomial array -> (OrderedPoly.polynomial * sign_op) list ->
(OrderedPoly.polynomial * sign_op) list list
-(* Debugging information. At level 0 nothing is printed out. *)
+(** Debugging information. At level 0 nothing is printed out. *)
val set_debug_level : int -> unit
Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Solver/Structure.mli 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,4 +1,4 @@
-(** Representing Relational Structures with Real-Valued Functions *)
+(** Representing relational structures with real-valued functions. *)
(** {2 Modules used in structure representation.} *)
Modified: trunk/Toss/Toss.odocl
===================================================================
--- trunk/Toss/Toss.odocl 2011-11-17 17:12:44 UTC (rev 1634)
+++ trunk/Toss/Toss.odocl 2011-11-17 23:56:41 UTC (rev 1635)
@@ -1,5 +1,8 @@
Formula/Formula
Formula/FormulaParser
+Formula/FormulaMap
+Formula/FormulaSubst
+Formula/Sat/Sat
Formula/BoolFormula
Formula/BoolFunction
Formula/FFTNF
@@ -8,9 +11,16 @@
Solver/StructureParser
Solver/AssignmentSet
Solver/Assignments
+Solver/RealQuantElim/OrderedPoly
+Solver/RealQuantElim/OrderedPolySet
+Solver/RealQuantElim/Poly
+Solver/RealQuantElim/SignTable
+Solver/RealQuantElim/RealQuantElim
+Solver/RealQuantElim/RealQuantElimParser
Solver/Solver
Solver/Class
Solver/ClassParser
+Solver/Distinguish
Arena/Term
Arena/TermParser
Arena/DiscreteRule
@@ -25,5 +35,10 @@
Play/Play
GGP/GDL
GGP/GDLParser
+GGP/TranslateFormula
+GGP/TranslateGame
GGP/GameSimpl
Server/Picture
+Server/LearnGame
+Server/DB
+Server/ReqHandler
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
