--- a/src/Tools/Metis/src/Waiting.sml Tue Nov 13 17:04:16 2007 +0100
+++ b/src/Tools/Metis/src/Waiting.sml Tue Nov 13 18:29:28 2007 +0100
@@ -9,16 +9,26 @@
open Useful;
(* ------------------------------------------------------------------------- *)
-(* Chatting. *)
+(* A type of waiting sets of clauses. *)
(* ------------------------------------------------------------------------- *)
-val module = "Waiting";
-fun chatting l = tracing {module = module, level = l};
-fun chat s = (trace s; true);
+(* The parameter type controls the heuristics for clause selection. *)
+(* Increasing any of the *Weight parameters will favour clauses with low *)
+(* values of that field. *)
+
+(* Note that there is an extra parameter of inference distance from the *)
+(* starting axioms (a.k.a. time) which has a fixed weight of 1, so all *)
+(* the other parameters should be set relative to this baseline. *)
-(* ------------------------------------------------------------------------- *)
-(* A type of waiting sets of clauses. *)
-(* ------------------------------------------------------------------------- *)
+(* The first two parameters, symbolsWeight and literalsWeight, control the *)
+(* time:weight ratio, i.e., whether to favour clauses derived in a few *)
+(* steps from the axioms (time) or whether to favour small clauses (weight). *)
+(* Small can be a combination of low number of symbols (the symbolWeight *)
+(* parameter) or literals (the literalsWeight parameter). *)
+
+(* modelsWeight controls the semantic guidance. Increasing this parameter *)
+(* favours clauses that return false more often when interpreted *)
+(* modelChecks times over the given list of models. *)
type parameters =
{symbolsWeight : real,