[Toss-devel-svn] SF.net SVN: toss:[1228] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1228] trunk/Toss
|
From: <luk...@us...> - 2010-12-06 00:34:39
|
Revision: 1228
http://toss.svn.sourceforge.net/toss/?rev=1228&view=rev
Author: lukaszkaiser
Date: 2010-12-06 00:34:31 +0000 (Mon, 06 Dec 2010)
Log Message:
-----------
Documentation corrections, removing SolverIntf.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/Arena.mli
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/ContinuousRule.mli
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Arena/DiscreteRule.mli
trunk/Toss/Arena/DiscreteRuleTest.ml
trunk/Toss/Arena/Term.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Formula/Formula.mli
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/Play/Game.ml
trunk/Toss/Play/GameTest.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Solver/AssignmentSet.mli
trunk/Toss/Solver/Assignments.mli
trunk/Toss/Solver/Class.mli
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/Solver.mli
trunk/Toss/Toss.odocl
Removed Paths:
-------------
trunk/Toss/Solver/SolverIntf.ml
trunk/Toss/Solver/SolverIntf.mli
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/Arena.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -22,7 +22,7 @@
id : int ;
player : int ;
payoffs : Formula.real_expr array ;
- payoffs_pp : SolverIntf.M.registered_real_expr array ;
+ payoffs_pp : Solver.M.registered_real_expr array ;
moves : (label * int) list ;
}
@@ -33,7 +33,7 @@
num_players : int;
player_names : (string * int) list ;
defined_rels : (string * (string list * Formula.formula *
- SolverIntf.M.registered_formula)) list ;
+ Solver.M.registered_formula)) list ;
}
(* State of the game and additional information. *)
@@ -54,7 +54,7 @@
graph=Array.make 1
{ id = 0; player = 0; payoffs = [|zero|];
payoffs_pp =
- [|SolverIntf.M.register_real_expr zero|];
+ [|Solver.M.register_real_expr zero|];
moves = [] };
player_names = ["1", 0] ;
defined_rels = [] ;
@@ -71,8 +71,8 @@
(* Add a defined relation to a structure. *)
let add_def_rel_single struc (r_name, vars, def_phi) =
- let def_asg = SolverIntf.M.evaluate struc
- (SolverIntf.M.register_formula def_phi) in
+ let def_asg = Solver.M.evaluate struc
+ (Solver.M.register_formula def_phi) in
match def_asg with
| AssignmentSet.Empty ->
Structure.add_rel_name r_name (List.length vars) struc
@@ -144,7 +144,7 @@
let payoffs =
array_of_players zero player_names payoffs in
let payoffs_pp =
- Array.map SolverIntf.M.register_real_expr payoffs in
+ Array.map Solver.M.register_real_expr payoffs in
{ id = id; player = player;
payoffs = payoffs; payoffs_pp = payoffs_pp;
moves = moves }
@@ -215,7 +215,7 @@
List.map (fun (rel, args, body) -> (rel, (args, body))) defined_rels in
let defined_rels =
List.map (fun (rel, args, body) ->
- rel, (args, body, SolverIntf.M.register_formula body))
+ rel, (args, body, Solver.M.register_formula body))
defined_rels in
let player_names =
Array.to_list (Array.mapi (fun i pname->pname, i)
@@ -242,7 +242,7 @@
if old_locs = [] then old_locs
else
let zero = Formula.Const 0.0 in
- let pp_zero = SolverIntf.M.register_real_expr zero in
+ let pp_zero = Solver.M.register_real_expr zero in
let add_payoffs loc =
let more = num_players - Array.length loc.payoffs in
{loc with
@@ -255,7 +255,7 @@
let add_def_rel loc =
let ps = Array.map (FormulaOps.subst_rels_expr def_rels_pure) loc.payoffs in
let reg_ps =
- Array.map SolverIntf.M.register_real_expr ps in
+ Array.map Solver.M.register_real_expr ps in
{ loc with payoffs = ps; payoffs_pp = reg_ps } in
(* {{{ log entry *)
if !debug_level > 2 then (
@@ -389,7 +389,7 @@
let add_new_player state pname =
let player = state.game.num_players in
let zero = Formula.Const 0.0 in
- let pp_zero = SolverIntf.M.register_real_expr zero in
+ let pp_zero = Solver.M.register_real_expr zero in
let add_payoff loc =
{loc with
payoffs = Array.append loc.payoffs [|zero|];
@@ -694,7 +694,7 @@
(Array.mapi (fun i v->string_of_int i,v)
state.game.graph.(state.cur_loc).payoffs_pp) in
let ev (p,e) =
- p^": "^(string_of_float (SolverIntf.M.get_real_val e struc)) in
+ p^": "^(string_of_float (Solver.M.get_real_val e struc)) in
(state, String.concat ", " (List.sort compare (List.map ev payoffs)))
| SetLocMoves (i, moves) ->
if i < 0 || i > Array.length state.game.graph then
Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/Arena.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,10 +1,8 @@
-(* Represent the game arena and operate on it. *)
+(** Represent the game arena and operate on it. *)
val debug_level : int ref
-(* ------------------------ BASIC TYPE DEFINITIONS -------------------------- *)
-
-(* A single move consists of applying a rewrite rule for a time from the
+(** A single move consists of applying a rewrite rule for a time from the
[time_in] interval, and parameters from the interval list. *)
type label = {
rule : string ;
@@ -12,29 +10,29 @@
parameters_in : (string * (float * float)) list ;
}
-(* A game has locations from which a player (single for now) can move,
+(** A game has locations from which a player (single for now) can move,
with a label, to one of the next positions, or get a
payoff. Players are indexed continuously starting from 0. *)
type location = {
id : int ;
player : int ;
payoffs : Formula.real_expr array ;
- payoffs_pp : SolverIntf.M.registered_real_expr array ;
+ payoffs_pp : Solver.M.registered_real_expr array ;
moves : (label * int) list ;
}
-(* The basic type of Arena. *)
+(** The basic type of Arena. *)
type game = {
rules : (string * ContinuousRule.rule) list;
graph : location array;
num_players : int;
player_names : (string * int) list ;
defined_rels : (string * (string list * Formula.formula *
- SolverIntf.M.registered_formula)) list ;
+ Solver.M.registered_formula)) list ;
}
-(* State of the game. *)
+(** State of the game. *)
type game_state = {
game : game ;
struc : Structure.structure ;
@@ -49,18 +47,16 @@
(string * string list * Formula.formula) list -> Structure.structure
-(* ------------------------ PRINTING FUNCTIONS ------------------------------ *)
-
-(* Print a label as a string. *)
+(** Print a label as a string. *)
val label_str : label -> string
val move_str : (label * int) -> string
-(* Print a game as a string. *)
+(** Print a game as a string. *)
val str : game -> string
-(* Print the whole state: the game, structure, time and aux data. *)
+(** Print the whole state: the game, structure, time and aux data. *)
val state_str : game_state -> string
-(* Whether to print relation definitions as equations, or using the C
+(** Whether to print relation definitions as equations, or using the C
syntax. Defaults to [true]. *)
val equational_def_style : bool ref
@@ -68,9 +64,7 @@
val print_state : game_state -> unit
val sprint_state : game_state -> string
-(* -------------------- PARSER HELPER ------------------------------ *)
-
-(* The order of following entries matters: [DefPlayers] adds more
+(** The order of following entries matters: [DefPlayers] adds more
players, with consecutive numbers starting from first available;
later [StateStruc], [StateTime] and [StateLoc] entries override
earlier ones; later [DefLoc] with already existing location ID
@@ -82,16 +76,16 @@
(string * int) list ->
(string * (string list * Formula.formula)) list -> string ->
ContinuousRule.rule)
- (* add a rule *)
+ (** add a rule *)
| DefLoc of ((string * int) list -> location)
- (* add location to graph *)
- | DefPlayers of string list (* add players (fresh numbers) *)
+ (** add location to graph *)
+ | DefPlayers of string list (** add players (fresh numbers) *)
| DefRel of string * string list * Formula.formula
- (* add a defined relation *)
- | StateStruc of Structure.structure (* initial/saved state *)
- | StateTime of float (* initial/saved time *)
- | StateLoc of int (* initial/saved location *)
- | StateData of (string * string) list (* saved data *)
+ (** add a defined relation *)
+ | StateStruc of Structure.structure (** initial/saved state *)
+ | StateTime of float (** initial/saved time *)
+ | StateLoc of int (** initial/saved location *)
+ | StateData of (string * string) list (** saved data *)
exception Arena_definition_error of string
@@ -109,45 +103,45 @@
| `PlayerName of string ]
list -> (string * int) list -> location
-(* Create a game state, possibly by extending an old state, from a
+(** Create a game state, possibly by extending an old state, from a
list of definitions (usually corresponding to a ".toss" file.) *)
val process_definition :
?extend_state:game_state -> definition list -> game_state
-(* ------------------ REQUESTS TO THE ARENA USED IN OPERATION --------------- *)
+(** ------------------ REQUESTS TO THE ARENA USED IN OPERATION --------------- *)
-(* Location of a structure: either arena or left or right-hand side of a rule *)
+(** Location of a structure: either arena or left or right-hand side of a rule *)
type struct_loc = Struct | Left of string | Right of string
-(* Requests which we handle. *)
+(** Requests which we handle. *)
type request =
- AddElem of struct_loc (* Add element to location *)
- | AddRel of struct_loc * string * string list (* Add relation tuple *)
- | DelElem of struct_loc * string (* Del element at location *)
- | DelRel of struct_loc * string * string list (* Del relation tuple *)
- | GetRelSignature of struct_loc (* List rel names and arities *)
- | GetFunSignature of struct_loc (* List function names *)
- | GetAllTuples of struct_loc * string (* Get all tuples in relation *)
- | GetAllElems of struct_loc (* List all elements *)
- | SetFun of struct_loc * string * string * float (* Set function value *)
- | GetFun of struct_loc * string * string (* Get function value *)
- | SetData of string * string (* Set data under a name *)
- | GetData of string (* Get data *)
- | SetArity of string * int (* Set arity of a relation *)
- | GetArity of string (* Get arity of a relation *)
- | RenamePlayer of string * string (* Replace player name *)
- | SetLoc of int (* Set current location *)
- | GetLoc (* Get current and # locs. *)
- | SetLocPlayer of int * string (* Set player at location *)
- | GetLocPlayer of int (* Get player at location *)
- | SetLocPayoff of int * string * Formula.real_expr(* Set payoff for player *)
- | GetLocPayoff of int * string (* Get payoff for player *)
- | GetCurPayoffs (* Payoffs in current loc *)
- | SetLocMoves of int * (label * int) list (* Set moves at location *)
- | GetLocMoves of int (* Get moves at location *)
+ AddElem of struct_loc (** Add element to location *)
+ | AddRel of struct_loc * string * string list (** Add relation tuple *)
+ | DelElem of struct_loc * string (** Del element at location *)
+ | DelRel of struct_loc * string * string list (** Del relation tuple *)
+ | GetRelSignature of struct_loc (** List rel names and arities *)
+ | GetFunSignature of struct_loc (** List function names *)
+ | GetAllTuples of struct_loc * string (** Get all tuples in relation *)
+ | GetAllElems of struct_loc (** List all elements *)
+ | SetFun of struct_loc * string * string * float (** Set function value *)
+ | GetFun of struct_loc * string * string (** Get function value *)
+ | SetData of string * string (** Set data under a name *)
+ | GetData of string (** Get data *)
+ | SetArity of string * int (** Set arity of a relation *)
+ | GetArity of string (** Get arity of a relation *)
+ | RenamePlayer of string * string (** Replace player name *)
+ | SetLoc of int (** Set current location *)
+ | GetLoc (** Get current and # locs. *)
+ | SetLocPlayer of int * string (** Set player at location *)
+ | GetLocPlayer of int (** Get player at location *)
+ | SetLocPayoff of int * string * Formula.real_expr(** Set payoff for player *)
+ | GetLocPayoff of int * string (** Get payoff for player *)
+ | GetCurPayoffs (** Payoffs in current loc *)
+ | SetLocMoves of int * (label * int) list (** Set moves at location *)
+ | GetLocMoves of int (** Get moves at location *)
| SuggestLocMoves of int * int * int * string * int option *
(string * Formula.real_expr) list array option * float option
- (* Suggested moves at loc, with timeout in so many seconds, for so
+ (** Suggested moves at loc, with timeout in so many seconds, for so
much computational effort if possible before timeout, using given
search method ("maximax", "alpha_beta", "alpha_beta_ord",
"uct_random_playouts",
@@ -155,32 +149,32 @@
"uct_no_playouts"), with optional horizon for playouts, with
location-dependent heuristics, with advancement ratio for
generating heuristics if they're not given *)
- | EvalFormula of Formula.formula (* Evaluate formula *)
- | EvalRealExpr of Formula.real_expr (* Evaluate real expr *)
+ | EvalFormula of Formula.formula (** Evaluate formula *)
+ | EvalRealExpr of Formula.real_expr (** Evaluate real expr *)
| SetRule of string *
((string * int) list ->
(string * (string list * Formula.formula)) list -> string ->
ContinuousRule.rule)
- (* Set a rule as given *)
- | GetRule of string (* Get a rule as string *)
- | SetRuleUpd of string*string *string *Term.term (* Set a rule update eq *)
- | GetRuleUpd of string * string * string (* Get a rule update eq *)
- | SetRuleDyn of string*string *string *Term.term (* Set a rule dynamics eq *)
- | GetRuleDyn of string * string * string (* Get a rule dynamics eq *)
+ (** Set a rule as given *)
+ | GetRule of string (** Get a rule as string *)
+ | SetRuleUpd of string*string *string *Term.term (** Set a rule update eq *)
+ | GetRuleUpd of string * string * string (** Get a rule update eq *)
+ | SetRuleDyn of string*string *string *Term.term (** Set a rule dynamics eq *)
+ | GetRuleDyn of string * string * string (** Get a rule dynamics eq *)
| SetRuleCond of string * Formula.formula * Formula.formula * Formula.formula
- (* Set a rule's precondition, invariant and postconsition *)
- | GetRuleCond of string (* Get a rule conditions *)
- | SetRuleEmb of string * string list (* Set relations to embed *)
- | GetRuleEmb of string (* Get relations to embed *)
- | SetRuleAssoc of string * string * string list (* Set an association *)
- | GetRuleAssoc of string * string (* Get an association *)
- | GetRuleMatches of string (* Get matches of a rule *)
+ (** Set a rule's precondition, invariant and postconsition *)
+ | GetRuleCond of string (** Get a rule conditions *)
+ | SetRuleEmb of string * string list (** Set relations to embed *)
+ | GetRuleEmb of string (** Get relations to embed *)
+ | SetRuleAssoc of string * string * string list (** Set an association *)
+ | GetRuleAssoc of string * string (** Get an association *)
+ | GetRuleMatches of string (** Get matches of a rule *)
| ApplyRule of string * (string * string) list * float * (string * float) list
- (* Apply rule at match for given time and with params *)
- | GetRuleNames (* Get names of rules *)
- | SetTime of float * float (* Set time step and time *)
- | GetTime (* Get time step and time *)
- | SetState of game_state (* Set the full state *)
- | GetState (* Return the state *)
+ (** Apply rule at match for given time and with params *)
+ | GetRuleNames (** Get names of rules *)
+ | SetTime of float * float (** Set time step and time *)
+ | GetTime (** Get time step and time *)
+ | SetState of game_state (** Set the full state *)
+ | GetState (** Return the state *)
val handle_request : game_state -> request -> game_state * string
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/ContinuousRule.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -15,10 +15,10 @@
update : ((string * string) * Term.term) list; (* Update equations calT *)
(* Note that, for efficiency, the precondition is part of DiscreteRule. *)
inv : Formula.formula; (* Invariant for the evolution *)
- inv_pp : SolverIntf.M.registered_formula;
+ inv_pp : Solver.M.registered_formula;
(* Optimized invariant *)
post : Formula.formula; (* Postcondition for application *)
- post_pp : SolverIntf.M.registered_formula;
+ post_pp : Solver.M.registered_formula;
(* Optimized postcondition *)
}
@@ -31,16 +31,16 @@
let cpost = FormulaOps.subst_rels defs post in
let discrete = { discr with DiscreteRule.pre = cpre } in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defs in
+ rel, (args, body, Solver.M.register_formula body)) defs in
let obj = DiscreteRule.compile_rule signat defrels discr in
{ discrete = discrete;
compiled = obj ;
dynamics = dynamics ;
update = update ;
inv = cinv ;
- inv_pp = SolverIntf.M.register_formula cinv;
+ inv_pp = Solver.M.register_formula cinv;
post = cpost ;
- post_pp = SolverIntf.M.register_formula cpost;
+ post_pp = Solver.M.register_formula cpost;
}
@@ -108,7 +108,7 @@
let cur_vals = ref init_vals in
let all_vals = ref [] in
let end_time = !time +. t -. (0.01 *. !time_step) in (*TODO: 1% is decimals!*)
- let is_inv s = SolverIntf.M.check_formula s r.inv_pp in
+ let is_inv s = Solver.M.check_formula s r.inv_pp in
let lhs_to_model ((f, a), _) =
(* dynamics refer to elements by LHS matches *)
let e = Structure.find_elem r.discrete.DiscreteRule.lhs_struc a in
@@ -164,7 +164,7 @@
let is_ok m =
let (res_struc, _, _) =
rewrite_single_nocheck struc cur_time m r 1. [] in
- SolverIntf.M.check_formula res_struc r.post_pp in
+ Solver.M.check_formula res_struc r.post_pp in
if r.post = Formula.And [] then matches struc r else
List.filter is_ok (matches struc r)
@@ -174,7 +174,7 @@
let (res_struc, _, _ as res_struc_n_shifts) =
rewrite_single_nocheck struc cur_time m r t params in
if r.post = Formula.And [] ||
- SolverIntf.M.check_formula res_struc r.post_pp
+ Solver.M.check_formula res_struc r.post_pp
then Some res_struc_n_shifts
else None
Modified: trunk/Toss/Arena/ContinuousRule.mli
===================================================================
--- trunk/Toss/Arena/ContinuousRule.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/ContinuousRule.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,40 +1,41 @@
-(* Structure rewriting with continuous dynamics. *)
+(** Structure rewriting with continuous dynamics. *)
val get_time_step : unit -> float
val set_time_step : float -> unit
-(* ---------------- BASIC TYPE DEFINITION AND CONSTRUCTOR ------------------- *)
+(** {2 Basic Type Definition} *)
-(* Specification of a continuous rewriting rule, as in modelling document.
+(** Specification of a continuous rewriting rule, as in modelling document.
Function named foo on element i is, in a term, given by variable foo_i. *)
type rule = {
- discrete : DiscreteRule.rule; (* The discrete part *)
- compiled : DiscreteRule.rule_obj ; (* Compiled discrete part *)
- dynamics : ((string * string) * Term.term) list; (* Equation system calD *)
- update : ((string * string) * Term.term) list; (* Update equations calT *)
- (* Note that, for efficiency, the precondition is part of DiscreteRule. *)
- inv : Formula.formula; (* Invariant for the evolution *)
- inv_pp : SolverIntf.M.registered_formula;
- (* Optimized invariant *)
- post : Formula.formula; (* Postcondition for application *)
- post_pp : SolverIntf.M.registered_formula;
-(* Optimized postcondition *)
+ discrete : DiscreteRule.rule; (** The discrete part *)
+ compiled : DiscreteRule.rule_obj ; (** Compiled discrete part *)
+ dynamics : ((string * string) * Term.term) list; (** Equation system calD *)
+ update : ((string * string) * Term.term) list; (** Update equations calT *)
+ (** Note that, for efficiency, the precondition is part of DiscreteRule. *)
+ inv : Formula.formula; (** Invariant for the evolution *)
+ inv_pp : Solver.M.registered_formula;
+ (** Optimized invariant *)
+ post : Formula.formula; (** Postcondition for application *)
+ post_pp : Solver.M.registered_formula;
+ (** Optimized postcondition *)
}
-(* Create a continuous rule given a named discrete rule and other params. *)
+(** Create a continuous rule given a named discrete rule and other params. *)
val make_rule :
- (string * int) list -> (* signature *)
- (string * (string list * Formula.formula)) list -> (* defined rels *)
+ (string * int) list -> (** signature *)
+ (string * (string list * Formula.formula)) list -> (** defined rels *)
(DiscreteRule.rule) ->
Term.eq_sys -> Term.eq_sys ->
?pre:Formula.formula -> ?inv:Formula.formula ->
?post:Formula.formula -> unit -> rule
-(* -------------------------- PRINTING FUNCTION ----------------------------- *)
+(** {2 Printing function} *)
-(* Print a rule to string. *)
+
+(** Print a rule to string. *)
val str : rule -> string
val fprint : Format.formatter -> rule -> unit
@@ -42,32 +43,35 @@
val sprint : rule -> string
-(* ------------------ APPLYING FUNCTIONS TO SIDE STRUCTURES ----------------- *)
+(** {2 Applying function to side structures} *)
-(* Apply [f] to left (if [to_left]) or right side of the given rule.
+
+(** Apply [f] to left (if [to_left]) or right side of the given rule.
Return the new rule and an additional result which [f] returns. *)
val apply_to_side :
bool -> (Structure.structure -> Structure.structure * 'a) ->
- (string * int) list -> (* signature *)
- (string * (string list * Formula.formula)) list -> (* defined rels *)
+ (string * int) list -> (** signature *)
+ (string * (string list * Formula.formula)) list -> (** defined rels *)
rule -> rule * 'a
val lhs : rule -> Structure.structure
val rhs : rule -> Structure.structure
-(* ---------------------- FINDING APPLICABLE MATCHES ------------------------ *)
-(* Find all matches of [r] in [struc] which satisfy [r]'s precondition. *)
+(** {2 Finding applicable matches} *)
+
+
+(** Find all matches of [r] in [struc] which satisfy [r]'s precondition. *)
val matches : Structure.structure -> rule -> (int * int) list list
-(* Matches which satisfy postcondition with time 1 and empty params *)
+(** Matches which satisfy postcondition with time 1 and empty params *)
val matches_post : Structure.structure -> rule -> float -> (int * int) list list
-(* --------------------------- REWRITING ------------------------------------ *)
+(** {2 Rewriting} *)
-(* For now, we rewrite only single rules.
+(** For now, we rewrite only single rules.
[rewrite_single struc cur_time m r t params def_rels] rewrites
[struc] for the period [t] (unless invariant stops holding earlier)
starting in [cur_time], at matching [m], and returns the rewritten
@@ -78,8 +82,7 @@
(int * int) list -> rule -> float -> (string * float) list ->
Structure.structure * float * ((string * string) * Term.term list) list
-(* For now, we rewrite only single rules.
-
+(** For now, we rewrite only single rules.
Same as {!ContinuousRule.rewrite_single_nocheck}, but check if the
postcondition holds. Returns [None] if rewriting fails. *)
val rewrite_single :
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/DiscreteRule.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -36,7 +36,7 @@
lhs_elem_inv_names : elem_inv_names;
lhs_elem_vars : string list;
lhs_form : Formula.formula;
- lhs_form_pp : SolverIntf.M.registered_formula;
+ lhs_form_pp : Solver.M.registered_formula;
(* gets instantiated in the model *)
(* the precondition [pre] is compiled as part of [lhs_form] *)
rhs_elem_names : elem_names;
@@ -165,7 +165,7 @@
(* Find all embeddings of a rule. Does not guarantee that rewriting
will succeed for all of them. *)
let find_matchings model rule_obj =
- SolverIntf.M.evaluate model rule_obj.lhs_form_pp
+ Solver.M.evaluate model rule_obj.lhs_form_pp
(* Convert assignment to an embedding of the LHS structure. *)
let assignment_to_embedding rule_obj assgn =
@@ -564,7 +564,7 @@
if List.mem_assoc rel defined_rels then
let args, _, rphi = List.assoc rel defined_rels in
List.map fst (List.filter (fun (rel, ar) ->
- SolverIntf.M.check_formula (Structure.free_for_rel rel ar) rphi
+ Solver.M.check_formula (Structure.free_for_rel rel ar) rphi
) signat)
else [rel] in
let expand_defrel_tups (drel, tups) =
@@ -575,7 +575,7 @@
map_some (fun (brel, ar) ->
let selector = Structure.free_for_rel brel ar in
let assgn =
- SolverIntf.M.evaluate selector rphi in
+ Solver.M.evaluate selector rphi in
let btup = Array.init ar (fun i->i+1) in
(* [selector] has only [btup] with its elements *)
let selvars =
@@ -836,7 +836,7 @@
rhs_neg_tuples in
(* Optimizing the embedding formula. *)
let lhs_form_pp =
- SolverIntf.M.register_formula emb in
+ Solver.M.register_formula emb in
{
lhs_elem_names = lhs_elem_names;
lhs_elem_inv_names = lhs_elem_inv_names;
@@ -913,7 +913,7 @@
List.map (fun tup->Not (Rel (r,Array.map (fun v->`FO v) tup)))
tups)
obj.rhs_neg_tuples in
- SolverIntf.M.formula_str obj.lhs_form_pp ^ "-> " ^
+ Solver.M.formula_str obj.lhs_form_pp ^ "-> " ^
Formula.str (And (plits @ nlits))
Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/DiscreteRule.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -31,7 +31,7 @@
lhs_elem_inv_names : elem_inv_names;
lhs_elem_vars : string list;
lhs_form : Formula.formula;
- lhs_form_pp : SolverIntf.M.registered_formula;
+ lhs_form_pp : Solver.M.registered_formula;
(* gets instantiated in the model *)
(* the precondition [pre] is compiled as part of [lhs_form] *)
rhs_elem_names : elem_names;
@@ -104,7 +104,7 @@
val compile_rule :
(string * int) list ->
(string *
- (string list * Formula.formula * SolverIntf.M.registered_formula))
+ (string list * Formula.formula * Solver.M.registered_formula))
list -> rule -> rule_obj
(** Relations that can explicitly change state by rewriting (i.e. not
Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -520,7 +520,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -536,7 +536,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -552,7 +552,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -568,7 +568,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -589,7 +589,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -605,7 +605,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -621,7 +621,7 @@
let signat = ["O", 1; "P", 1; "Q", 1] in
let defrels = ["D", (["a"], formula_of_str "P(a) or Q(a)")] in
let defrels = List.map (fun (rel,(args,body)) ->
- rel, (args, body, SolverIntf.M.register_formula body)) defrels in
+ rel, (args, body, Solver.M.register_formula body)) defrels in
let rule_obj = compile_rule signat defrels
{lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
Modified: trunk/Toss/Arena/Term.mli
===================================================================
--- trunk/Toss/Arena/Term.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Arena/Term.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,6 +1,6 @@
-(* Represent terms and their operations. *)
+(** Represent terms and their operations. *)
-(* ---------------------- BASIC TYPE DEFINITION ----------------------------- *)
+(** {2 Basic Type Definition.} *)
type term =
Var of string
@@ -13,12 +13,13 @@
type eq_sys = ((string * string) * term) list
-(* ------------------------ BASIC FUNCTIONS -------------------------------- *)
+(** {2 Basic functions.} *)
-(* Print a term as a string. *)
+
+(** Print a term as a string. *)
val str : term -> string
-(* Print an equation system as a string. *)
+(** Print an equation system as a string. *)
val eq_str : ?diff : bool -> eq_sys -> string
val fprint :
@@ -32,20 +33,20 @@
val sprint_eqs : ?diff : bool -> eq_sys -> string
-(* Power function used in parser. *)
+(** Power function used in parser. *)
val pow : term -> int -> term
-(* Basic simplification, reduces constant terms to floats. *)
+(** Basic simplification, reduces constant terms to floats. *)
val simp_const : term -> term
-(* Convert a term to float, fail on non-constant term. *)
+(** Convert a term to float, fail on non-constant term. *)
val term_val : term -> float
-(* Convert an equation system to float assciation list, fail on non-consts. *)
+(** Convert an equation system to float assciation list, fail on non-consts. *)
val eq_vals : eq_sys -> ((string * string) * float) list
-(* ----------------------- SIMPLE OPERATIONS ------------------------------- *)
+(** {2 Simple operations.} *)
val add : term -> term -> term
val ladd1 : term -> term list -> term list
@@ -56,27 +57,28 @@
val lmul : term list -> term list -> term list
-(* ------------------ SUBSTITUTION FOR VARIABLES --------------------------- *)
+(** {2 Substitution for variables.} *)
-(* Substitute term [t] for variable [v] in the given term. *)
+(** Substitute term [t] for variable [v] in the given term. *)
val subst : string * term -> term -> term
-(* Substitute [vals] for [vars] in [terms] and simplify. *)
+(** Substitute [vals] for [vars] in [terms] and simplify. *)
val subst_simp : string list -> term list -> term list -> term list
-(* Substitute term [t] for function variable [f, a] in the given term. *)
+(** Substitute term [t] for function variable [f, a] in the given term. *)
val subst_f : (string * string) * term -> term -> term
-(* Substitute [vals] for function [vars] in [terms] and simplify. *)
+(** Substitute [vals] for function [vars] in [terms] and simplify. *)
val subst_simp_f : (string * string) list -> term list -> term list -> term list
-(* Substitute variables and function vals in an equation system and simplify. *)
+(** Substitute variables and function vals in an eq. system and simplify. *)
val subst_simp_eq : (string * term) list -> ((string * string) * term) list ->
eq_sys -> eq_sys
-(* ---------------- RUNGE - KUTTA METHOD FOR TERM EQUATIONS ---------------- *)
+(** {2 Runge-Kutta Method for Term Equations *)
-(* Perform a Runge-Kutta (RK4) step for [vars] with [vals_init] and right-hand
+
+(** Perform a Runge-Kutta (RK4) step for [vars] with [vals_init] and right-hand
side [eq_terms]. Time variable [tvar] starts at [tinit] and moves [tstep]. *)
val rk4_step : string -> term -> term -> eq_sys -> term list -> term list
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Formula/BoolFormula.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -38,10 +38,10 @@
(* ----------------------- PRINTING FUNCTIONS ------------------------------- *)
-(* Print a variable as a string. *)
+(** Print a variable as a string. *)
let var_str = string_of_int
-(* Print a Boolean formula as a string. *)
+(** Print a Boolean formula as a string. *)
let rec str = function
BVar v -> var_str v
| BNot phi -> "(not " ^ (str phi) ^ ")"
@@ -58,7 +58,7 @@
(* ------------------------ ORDER ON FORMULAS ------------------------------- *)
-(* Compare two variables. We assume that FO < MSO < Real. *)
+(** Compare two variables. We assume that FO < MSO < Real. *)
let compare_vars x y =
let abs lit = if lit < 0 then (-lit) else lit in
(abs x) - (abs y)
Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Formula/BoolFormula.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,8 +1,8 @@
-(* Represent Boolean combinations of integer literals. *)
+(** Represent Boolean combinations of integer literals. *)
-(* ----------------------- BASIC TYPE DEFINITIONS -------------------------- *)
+(** {2 Basic type definitions.} *)
-(* This type describes formulas of relational logic with equality.
+(** This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type bool_formula =
BVar of int
@@ -10,58 +10,55 @@
| BAnd of bool_formula list
| BOr of bool_formula list
-(* ---------------------- PRINTING FUNCTIONS ------------------------------- *)
+(** {2 Printing functions.} *)
-(* Print a variable as a string. *)
+(** Print a variable as a string. *)
val var_str : int -> string
-(* Print a formula as a string. *)
+(** Print a formula as a string. *)
val str : bool_formula -> string
-
-(* Helper function to flatten multiple or's and and's. *)
+(** Helper function to flatten multiple or's and and's. *)
val flatten_sort : bool_formula -> bool_formula
-(* ------------------------- Boolean Formulas ------------------------------ *)
+(** {3 Boolean Formulas.} *)
-(* Convert an arbitrary formula to a Boolean combination of literals *)
+(** Convert an arbitrary formula to a Boolean combination of literals *)
val bool_formula_of_formula : Formula.formula -> bool_formula
-(* Convert a Boolean combination back to a formula *)
-(*val formula_of_bool_formula : bool_formula -> Formula.formula*)
-
+(** Convert a Boolean combination back to a formula *)
val formula_of_bool_formula_arg : bool_formula ->
(Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t * int ref -> Formula.formula
val bool_formula_of_formula_arg : Formula.formula ->
(Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t * int ref -> bool_formula
-(* Simplify a Boolean combination *)
+(** Simplify a Boolean combination *)
val simplify : bool_formula -> bool_formula
-(* Sort a Boolean combination *)
+(** Sort a Boolean combination *)
val sort : bool_formula -> bool_formula
-(* Convert a reduced Boolean combination into a CNF with auxiliary variables *)
+(** Convert a reduced Boolean combination into a CNF with auxiliary variables *)
val auxcnf_of_bool_formula : bool_formula -> int * bool_formula
val pg_auxcnf_of_bool_formula : bool_formula -> int * bool_formula
-(* Convert a Boolean combination into reduced form (over 'not' and 'or') *)
+(** Convert a Boolean combination into reduced form (over 'not' and 'or') *)
val to_reduced_form : ?neg:bool -> bool_formula -> bool_formula
-(* Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
+(** Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
val to_nnf : ?neg : bool -> bool_formula -> bool_formula
val convert : bool_formula -> int list list
-(* Convert an arbitrary formula to CNF via Boolean combinations. *)
+(** Convert an arbitrary formula to CNF via Boolean combinations. *)
val formula_to_cnf : Formula.formula -> Formula.formula
-(* ------------------------- 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/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Formula/Formula.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,46 +1,46 @@
-(* Represent formulas with first-order, mso, and real variables. *)
+(** Represent formulas with first-order, mso, and real variables. *)
-(* ----------------------- BASIC TYPE DEFINITIONS -------------------------- *)
+(** {2 Basic Type Definitions.} *)
-(* Our variables can be first-order, monadic second-order or reals. *)
+(** Our variables can be first-order, monadic second-order or reals. *)
type var = [ `FO of string | `MSO of string | `Real of string ] ;;
type fo_var = [ `FO of string ];;
type mso_var = [ `MSO of string ];;
type real_var = [ `Real of string ];;
-(* We recognize if the variable is FO (x, y) or MSO (X, Y) or Real (r1, r2). *)
+(** We recognize if the variable is FO (x, y) or MSO (X, Y) or Real (r1, r2). *)
val var_of_string : string -> var
val fo_var_of_string : string -> fo_var
val mso_var_of_string : string -> mso_var
val real_var_of_string : string -> real_var
-(* Check variable type. *)
+(** Check variable type. *)
val is_fo : var -> bool
val is_mso : var -> bool
val is_real : var -> bool
-(* Casts to particular variable types. *)
+(** Casts to particular variable types. *)
val to_fo : var -> fo_var
val to_mso : var -> mso_var
val to_real : var -> real_var
val var_tup : [< var] array -> var array
-(* Compare two variables. We assume FO < MSO < Real. *)
+(** Compare two variables. We assume FO < MSO < Real. *)
val compare_vars : ([< var ] as 'a) -> 'a -> int
val compare_var_lists : ([< var ] as 'a) list -> 'a list -> int
val compare_var_tups :
([< var ] as 'a) array -> 'a array -> int
-(* Sign operands. *)
+(** Sign operands. *)
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
-(* Print a sign_op as string. *)
+(** Print a sign_op as string. *)
val sign_op_str : sign_op -> string
-(* This type describes formulas of relational logic with equality.
+(** This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type formula =
Rel of string * fo_var array
@@ -68,23 +68,23 @@
val compare : formula -> formula -> int
-(* ---------------------- PRINTING FUNCTIONS ------------------------------- *)
+(** {2 Printing Functions} *)
-(* Print a variable as a string. *)
+(** Print a variable as a string. *)
val var_str : [< `FO of string | `MSO of string | `Real of string ] -> string
-(* Print a variable list as a string. *)
+(** Print a variable list as a string. *)
val var_list_str: [< `FO of string | `MSO of string | `Real of string ] list ->
string
-(* Print a formula as a string. *)
+(** Print a formula as a string. *)
val str : formula -> string
val mona_str : formula -> string
val print : formula -> unit
val sprint : formula -> string
val fprint : Format.formatter -> formula -> unit
-(* Print a real_expr as a string. *)
+(** Print a real_expr as a string. *)
val real_str : real_expr -> string
val print_real : real_expr -> unit
val sprint_real : real_expr -> string
@@ -93,13 +93,13 @@
val fprint_prec : int -> Format.formatter -> formula -> unit
val fprint_real_prec : int -> Format.formatter -> real_expr -> unit
-(* --------------- BASIC HELPER FUNCTIONS USED IN PARSER ------------------- *)
+(** {2 Basic flattening functions.} *)
-(* Only flatten the formula. *)
+(** Only flatten the formula. *)
val flatten : formula -> formula
val flatten_re : real_expr -> real_expr
-(* Flatten and sort multiple or's and and's. *)
+(** Flatten and sort multiple or's and and's. *)
val flatten_sort : formula -> formula
val flatten_sort_re : real_expr -> real_expr
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Formula/FormulaOps.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,35 +1,35 @@
-(* Operations on formulas. *)
+(** Operations on formulas. *)
open Formula
-(* ------------------------------- NNF ------------------------------------ *)
+(** {2 NNF} *)
-(* Convert formula to NNF and additionally negate if [neg] is set. *)
+(** Convert formula to NNF and additionally negate if [neg] is set. *)
val nnf : ?neg : bool -> formula -> formula
-(* ------------------------------- VARS ------------------------------------ *)
+(** {2 Vars} *)
val all_vars : formula -> var list
val free_vars : formula -> var list
-(* Delete top-most quantification of [vs] in the formula. *)
+(** Delete top-most quantification of [vs] in the formula. *)
val del_vars_quant : var list -> formula -> formula
-(* ----------------- MAPPING TO ATOMS AND VAR SUBSTITUTION ------------------ *)
+(** {2 Mapping to atoms and variable substitution.} *)
-(* Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
+(** Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
formula. Preserves order of subformulas. *)
val map_to_literals : (formula -> formula) -> formula -> formula
val map_to_literals_expr : (formula -> formula) -> real_expr -> real_expr
-(* Map [f] to all atoms in the given formula. *)
+(** Map [f] to all atoms in the given formula. *)
val map_to_atoms : (formula -> formula) -> formula -> formula
val map_to_atoms_expr : (formula -> formula) -> real_expr -> real_expr
-(** Map [f] to all variables occurring in the formula.
- Preserves order of subformulas. *)
+(** Map @param f to all variables occurring in the formula.
+ Preserves order of subformulas. @param phi The formula to substitute in. *)
val map_to_all_vars : (var -> var) -> formula -> formula
(** Apply substitution [subst] to all free variables in the given formula
@@ -41,59 +41,59 @@
and the above-quantified ones. Does not go into real_expr. *)
val rename_quant_avoiding : var list -> formula -> formula
-(* Substitute once relations in [defs] by corresponding subformulas
+(** Substitute once relations in [defs] by corresponding subformulas
(with instantiated parameters). *)
val subst_once_rels : (string * (string list * formula)) list -> formula -> formula
val subst_once_rels_expr : (string * (string list * formula)) list -> real_expr -> real_expr
-(* Substitute recursively relations defined in [defs] by their definitions. *)
+(** Substitute recursively relations defined in [defs] by their definitions. *)
val subst_rels : (string * (string list * formula)) list -> formula -> formula
val subst_rels_expr : (string * (string list * formula)) list -> real_expr -> real_expr
-(* Assign emptyset to an MSO-variable. *)
+(** Assign emptyset to an MSO-variable. *)
val assign_emptyset : string -> formula -> formula
-(* ------------------------ Transitive Closure ---------------------------- *)
+(** {2 Transitive Closure} *)
-(* Transitive closure of phi(x, y, z) over x and y, an MSO formula. *)
+(** Transitive closure of phi(x, y, z) over x and y, an MSO formula. *)
val make_tc : string -> string -> formula -> formula
-(* First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
+(** First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
val make_fo_tc_conj : int -> string -> string -> formula -> formula
val make_fo_tc_disj : int -> string -> string -> formula -> formula
-(* -------------------------- Simplification ------------------------------ *)
+(** {2 Simplification} *)
-(* Recursively simplify a formula *)
+(** Recursively simplify a formula *)
val simplify : ?do_pnf : bool -> formula -> formula
val pnf : formula -> formula
-(* Flatten "and"s and "or"s in a formula -- i.e. associativity. *)
+(** Flatten "and"s and "or"s in a formula -- i.e. associativity. *)
val flatten_formula : formula -> formula
-(* ------------------------------- TNF ------------------------------------ *)
+(** {2 TNF} *)
-(* Convert formula to TNF; or negTNF when [neg] is set. Type normal form
+(** Convert formula to TNF; or negTNF when [neg] is set. Type normal form
in a NNF form which pushes quantifiers inside as strongly as possible. *)
val tnf : formula -> formula
val tnf_re : real_expr -> real_expr
val tnf_fv : formula -> formula (** first existentially quantifies free vars *)
-(* ----------------------------- CNF/DNF ---------------------------------- *)
+(** {2 Convert to CNF or DNF} *)
-(* Convert an arbitrary boolean combination to DNF. *)
+(** Convert an arbitrary boolean combination to DNF. *)
val to_dnf : formula -> formula list
-(* Convert an arbitrary boolean combination to CNF. *)
+(** Convert an arbitrary boolean combination to CNF. *)
val to_cnf : formula -> formula list
-(* ------------------------- 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/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Play/Game.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -612,7 +612,7 @@
let subloc = evgame.ev_game.Arena.graph.(evgame.ev_location) in
if subloc.Arena.moves = [] then (* optimization *)
Array.map (fun expr ->
- SolverIntf.M.get_real_val expr model) subloc.Arena.payoffs_pp
+ Solver.M.get_real_val expr model) subloc.Arena.payoffs_pp
else
let state =
{game_state={loc=evgame.ev_location; struc=model; time=time};
@@ -650,7 +650,7 @@
if moves = [| |] then
let payoff =
Array.map (fun expr ->
- SolverIntf.M.get_real_val expr state.struc)
+ Solver.M.get_real_val expr state.struc)
loc.Arena.payoffs_pp in
Aux.Right payoff
else
@@ -1015,7 +1015,7 @@
if moves = [| |] then
let payoff =
Array.map (fun expr ->
- SolverIntf.M.get_real_val expr state.struc)
+ Solver.M.get_real_val expr state.struc)
location.Arena.payoffs_pp in
let upscore = score_payoff payoff in
upscore, Terminal (state, upscore, heuristic, payoff)
@@ -1085,7 +1085,7 @@
| None ->
default_heuristic ~struc heur_adv_ratio game in
let heuristics_pp =
- Array.map (Array.map SolverIntf.M.register_real_expr) heuristics in
+ Array.map (Array.map Solver.M.register_real_expr) heuristics in
let evgame gloc =
{ev_game =
{Arena.rules = [];
@@ -1132,7 +1132,7 @@
| None ->
default_heuristic ~struc heur_adv_ratio game in
let heuristics_pp =
- Array.map (Array.map SolverIntf.M.register_real_expr) heuristics in
+ Array.map (Array.map Solver.M.register_real_expr) heuristics in
let agents =
Array.map (fun loc ->
{ev_game =
@@ -1158,7 +1158,7 @@
| None ->
default_heuristic ~struc default_adv_ratio orig_game in
let heuristics_pp =
- Array.map (Array.map SolverIntf.M.register_real_expr) heuristics in
+ Array.map (Array.map Solver.M.register_real_expr) heuristics in
let evgame gloc =
{ev_game =
{Arena.rules=[];
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Play/GameTest.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -124,7 +124,7 @@
player = 0;
payoffs = payoffs;
payoffs_pp =
- Array.map SolverIntf.M.register_real_expr payoffs;
+ Array.map Solver.M.register_real_expr payoffs;
moves = Array.to_list (Array.map (fun (rname, rule) ->
{Arena.rule = rname; time_in = 0.1, 0.1; parameters_in = []}, 1)
rules1);
@@ -134,7 +134,7 @@
player = 1;
payoffs = payoffs;
payoffs_pp =
- Array.map SolverIntf.M.register_real_expr payoffs;
+ Array.map Solver.M.register_real_expr payoffs;
moves = Array.to_list (Array.map (fun (rname, rule) ->
{Arena.rule = rname; time_in = 0.1, 0.1; parameters_in = []}, 0)
rules2);
@@ -620,7 +620,7 @@
in
let ev (p,e) =
p^": "^(string_of_float
- (SolverIntf.M.get_real_val e state.Arena.struc)) in
+ (Solver.M.get_real_val e state.Arena.struc)) in
let answ =
String.concat ", " (List.sort compare (List.map ev payoffs)) in
assert_equal ~msg:"black wins: direct" ~printer:(fun x->x)
Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Play/Heuristic.ml 2010-12-06 00:34:31 UTC (rev 1228)
@@ -584,8 +584,8 @@
List.map Formula.to_fo (FormulaOps.free_vars phi) in
if vars = [] then Or []
else
- let aset = SolverIntf.M.evaluate struc
- (SolverIntf.M.register_formula phi) in
+ let aset = Solver.M.evaluate struc
+ (Solver.M.register_formula phi) in
let substs =
AssignmentSet.fo_assgn_to_list elems vars aset in
(* sort substitutions; TODO: optimizable *)
@@ -633,8 +633,8 @@
(* }}} *)
let substs =
AssignmentSet.fo_assgn_to_list elems vars
- (SolverIntf.M.evaluate struc
- (SolverIntf.M.register_formula phi)) in
+ (Solver.M.evaluate struc
+ (Solver.M.register_formula phi)) in
(* sort substitutions; TODO: optimizable *)
let substs = trunc_to_vars vars substs in
let all_vars = add_strings (List.map var_str vars) all_vars in
Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Solver/AssignmentSet.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,9 +1,9 @@
-(* This module contains the main type for partial assignments of
+(** This module contains the main type for partial assignments of
values to variables. *)
-(* ------------------------- BASIC TYPE DEFINITION -------------------------- *)
+(** {2 Basic type definition.} *)
-(* We represent assignment sets as trees. Below a variable we keep a
+(** We represent assignment sets as trees. Below a variable we keep a
tree of all assignments which assign this variable the same value.
For an MSO variable X, we keep a list of elements which must be and
which must not be in X. For real-valued variables, we keep
@@ -18,32 +18,32 @@
| Real of (Poly.polynomial * Formula.sign_op) list list
-(* --------------------- PRINTING AND HELPER FUNCTIONS --------------------- *)
+(** {2 Printing and small helper functions.} *)
-(* Variables assigned in an assignement set. *)
+(** Variables assigned in an assignement set. *)
val assigned_vars : Formula.var list -> assignment_set -> Formula.var list
-(* Print the given assignment as string. *)
+(** Print the given assignment as string. *)
val str : assignment_set -> string
-(* Print the given assignment as string, using element names. *)
+(** Print the given assignment as string, using element names. *)
val named_str : Structure.structure -> assignment_set -> string
-(* Select an arbitrary assignment for first-order variables with the
+(** Select an arbitrary assignment for first-order variables with the
given names and default values. Raise [Not_found] if the assignment
set is empty. *)
val choose_fo :
(string * int) list -> assignment_set -> (string * int) list
-(* List all tuples the first-order assignment [asg] assigns to [vars]
+(** List all tuples the first-order assignment [asg] assigns to [vars]
in order in which [vars] are given. [elems] are are all elements. *)
val tuples : Structure.Elems.t -> string list -> assignment_set -> int array list
-(* Check if a variable is actually present in the assignments tree. *)
+(** Check if a variable is actually present in the assignments tree. *)
val mem_assoc : [< Formula.var ] -> assignment_set -> bool
-(* Convert the FO part of an assingment set into a list of substitutions. *)
+(** Convert the FO part of an assingment set into a list of substitutions. *)
val fo_assgn_to_list :
int list -> Formula.fo_var list -> assignment_set ->
(Formula.fo_var * Structure.Elems.elt) list list
Modified: trunk/Toss/Solver/Assignments.mli
===================================================================
--- trunk/Toss/Solver/Assignments.mli 2010-12-05 22:48:17 UTC (rev 1227)
+++ trunk/Toss/Solver/Assignments.mli 2010-12-06 00:34:31 UTC (rev 1228)
@@ -1,61 +1,69 @@
-(* This module contains functions for handling partial assignments of
+(** 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. *)
-(* ------------------------- BASIC TYPE DEFINITION -------------------------- *)
-(* We represent assignment sets as trees.
+(** {2 Basic Type Definition} *)
+
+
+(** We represent assignment sets as trees.
Variables must occur in order and below a variable we keep a table
of all assignments which assign this variable the same value.
If an assignment set is not Empty, then it cannot contain Empty leafs. *)
type assignment_set = AssignmentSet.assignment_set
-(* ------------------------------ LIST SET ---------------------------------- *)
+(** {2 List or Set Type} *)
-(* Helper type to represent a set or a list of elements with length. *)
+
+(** Helper type to represent a set or a list of elements with length. *)
type set_list = List of int * int list | Set of int * Structure.Elems.t
-(* List a set or list ref; changes from set to list if required. *)
+(** List a set or list ref; changes from set to list if required. *)
val slist : set_list ref -> int list
val sllen : set_list ref -> int
-(* -------------------------------- JOIN ------------------------------------ *)
+(** {2 Join} *)
-(* This function joins two assignment sets, i.e. if these represent
+
+(** This function joins two assignment sets, i.e. if these represent
valuations of two formulas, it computes one for the conjunction. *)
val join : assignment_set -> assignment_set -> assignment_set
-(* -------------------------------- EQUAL ----------------------------------- *)
+(** {2 Equality} *)
-(* Enforce that in [aset] the variable [u] is equal to [w]. *)
+
+(** Enforce that in [aset] the variable [u] is equal to [w]. *)
val equal_vars : set_list ref -> Formula.fo_var -> Formula.fo_var ->
assignment_set -> assignment_set
-(* -------------------------------- SUM ------------------------------------- *)
+(** {2 Sum} *)
-(* Sum of two assignments, assuming that [elems] are all assignable elements.
+
+(** Sum of two assignments, assuming that [elems] are all assignable elements.
We assume that [elems] are sorted. Corresponds to disjunction of formulas. *)
val sum : set_list ref -> assignment_set -> assignment_set -> assignment_set
-(* ----------------------------- PROJECTION --------------------------------- *)
+(** {2 Projection} *)
-(* Project assignments on a given variable. We assume that [elems] are all
+
+(** Project assignments on a given variable. We assume that [elems] are all
elements and are sorted. C...
[truncated message content] |
