Switch on ifeq bonus depending on settings.

nick8325 · Sep 8, 2017 · 946e0fb · 946e0fb
1 parent bf5dd7f
commit 946e0fb
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 6 deletions.
diff --git a/executable/Main.hs b/executable/Main.hs
@@ -25,6 +25,7 @@ import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Lemma)
 import Jukebox.Tools.EncodeTypes
 import Jukebox.TPTP.Print
 import Jukebox.Tools.Clausify(ClausifyFlags(..), clausify)
+import Jukebox.Tools.HornToUnit
 import qualified Data.IntMap.Strict as IntMap
 import System.IO
 import System.Exit
@@ -53,7 +54,7 @@ parseMainFlags =
 parseConfig :: OptionParser Config
 parseConfig =
   Config <$> maxSize <*> maxCPs <*> maxCPDepth <*> simplify <*> normPercent <*>
-    (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor) <*>
+    (CP.Config <$> lweight <*> rweight <*> funweight <*> varweight <*> depthweight <*> dupcost <*> dupfactor <*> ifeqBonus) <*>
     (Join.Config <$> ground_join <*> connectedness <*> set_join) <*>
     (Proof.Config <$> all_lemmas <*> flat_proof <*> show_instances)
   where
@@ -145,6 +146,13 @@ parseConfig =
       flag name [desc ++ " (" ++ show def ++ " by default)."] def parser
       where
         def = field defaultConfig
+    ifeqBonus = p <$> hornFlags
+      where
+        p flags =
+          case encoding flags of
+            Symmetric -> True
+            Asymmetric1 -> True
+            Asymmetric2 -> False
 
 parsePrecedence :: OptionParser [String]
 parsePrecedence =

diff --git a/src/Twee.hs b/src/Twee.hs
@@ -80,7 +80,8 @@ defaultConfig =
         cfg_varweight = 6,
         cfg_depthweight = 16,
         cfg_dupcost = 7,
-        cfg_dupfactor = 0 },
+        cfg_dupfactor = 0,
+        cfg_ifeq_bonus = False },
     cfg_join = Join.defaultConfig,
     cfg_proof_presentation = Proof.defaultConfig }
 

diff --git a/src/Twee/CP.hs b/src/Twee/CP.hs
@@ -141,7 +141,8 @@ data Config =
     cfg_varweight :: !Int,
     cfg_depthweight :: !Int,
     cfg_dupcost :: !Int,
-    cfg_dupfactor :: !Int }
+    cfg_dupfactor :: !Int,
+    cfg_ifeq_bonus :: !Bool }
 
 -- We compute:
 --   cfg_lhsweight * size l + cfg_rhsweight * size r
@@ -162,9 +163,11 @@ score Config{..} Overlap{..} =
     size' n (Cons t ts)
       | len t > 1, t `isSubtermOfList` ts =
         size' (n+cfg_dupcost+cfg_dupfactor*size t) ts
-    size' n (Cons (App f (Cons a (Cons b ts))) us)
-      | isIfeq (fun_value f), isJust (unify a b) =
-        size' (size' (n+1) ts) us
+    size' n ts
+      | cfg_ifeq_bonus,
+        Cons (App f (Cons a (Cons b us))) vs <- ts,
+        isIfeq (fun_value f), isJust (unify a b) =
+        size' (size' (n+1) us) vs
     size' n (Cons (Var _) ts) =
       size' (n+cfg_varweight) ts
     size' n (ConsSym (App f _) ts) =