# HG changeset patch
# User blanchet
# Date 1284553469 -7200
# Node ID 9e6faecea4126dd9a1dab637e345801bf255c3e5
# Parent  a91b59c6d310223f12a8c3f2ed93035d2452dbb8
apply Larry's hacks directly to the "src" files;
these hacks modify the defaults of Metis heuristics and are necessary for backward compatibility

diff -r a91b59c6d310 -r 9e6faecea412 src/Tools/Metis/src/Clause.sml
--- a/src/Tools/Metis/src/Clause.sml	Wed Sep 15 11:47:25 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml	Wed Sep 15 14:24:29 2010 +0200
@@ -60,7 +60,7 @@
 
 val default : parameters =
     {ordering = KnuthBendixOrder.default,
-     orderLiterals = PositiveLiteralOrder,
+     orderLiterals = UnsignedLiteralOrder (* PositiveLiteralOrder *) (* MODIFIED by Jasmin Blanchette *),
      orderTerms = true};
 
 fun mk info = Clause info
diff -r a91b59c6d310 -r 9e6faecea412 src/Tools/Metis/src/Waiting.sml
--- a/src/Tools/Metis/src/Waiting.sml	Wed Sep 15 11:47:25 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sml	Wed Sep 15 14:24:29 2010 +0200
@@ -40,16 +40,17 @@
 (* ------------------------------------------------------------------------- *)
 
 val defaultModels : modelParameters list =
-    [{model = Model.default,
+    [(* MODIFIED by Jasmin Blanchette
+      {model = Model.default,
       initialPerturbations = 100,
       maxChecks = SOME 20,
       perturbations = 0,
-      weight = 1.0}];
+      weight = 1.0} *)];
 
 val default : parameters =
      {symbolsWeight = 1.0,
-      literalsWeight = 1.0,
-      variablesWeight = 1.0,
+      literalsWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
+      variablesWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
       models = defaultModels};
 
 fun size (Waiting {clauses,...}) = Heap.size clauses;
@@ -162,7 +163,7 @@
         val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight)
         val variablesW = Math.pow (clauseVariables lits, variablesWeight)
         val literalsW = Math.pow (clauseLiterals lits, literalsWeight)
-        val modelsW = checkModels models mods mcl
+        val modelsW = (* checkModels models mods mcl *) 1.0 (* MODIFIED by Jasmin Blanchette *)
 (*MetisTrace4
         val () = trace ("Waiting.clauseWeight: dist = " ^
                         Real.toString dist ^ "\n")