[feat] Added TTA sync strategies

Rule.fs

@@ -76,3 +76,6 @@ let normalize(rule.Rule(_, body, head)) =
     let eqs = List.concat eqs
 
     clARule (atoms @ eqs) head
+
+let fold f z (Rule(_, body, head)) = 
+    List.fold f z (head::body) 

Terms.fs

@@ -122,8 +122,9 @@ module Terms =
     let mapFold = List.mapFold
     let map = List.map
 
+    let length = List.length
     let collectFreeVars = List.collect Term.collectFreeVars >> List.unique
-
+    let numVars ts = collectFreeVars ts |> List.length
     let generateVariablesFromVars vars = List.map Term.generateVariableWithPrefix vars
     let generateVariablesFromOperation = Operation.argumentTypes >> List.map Term.generateVariable
 

Tests/SolverRuns.fs

@@ -89,6 +89,6 @@ type SampleSolverTests () =
     member x.tta_mccarthy () =
         x.RunTTAAloneCVCTIP "mccarthy91_M2.smt2" ".tta" 10
 
-    [<Test; Ignore("tta does not yet work")>]
+    [<Test>]
     member x.tta_prop20 () =
         x.RunTTAAloneCVCTIP "prop_20.smt2" ".tta" 10

Tests/Transformations.fs

@@ -77,8 +77,8 @@ type TTATests () =
     [<Test>]
     member x.ltZSPattern () =
         let ttaTraverser = TtaTransform.ToTTATraverser(1)
-        let pred = predicate "isEven" [nat]
-        let xs = [Z; S (S nNat)]
+        let pred = predicate "lt" [nat; nat]
+        let xs = [Z; S nNat]
         let automaton = ttaTraverser.GetOrAddApplicationAutomaton pred xs
         let decls = List.map toString automaton.Declarations
         ()
@@ -100,6 +100,7 @@ type TTATests () =
         let automaton = ttaTraverser.GetOrAddApplicationAutomaton pred xs
         let decls = List.map toString automaton.Declarations
         ()
+
     [<Test>]
     member x.patternLeafNode () =
         let ttaTraverser = TtaTransform.ToTTATraverser(2)
@@ -117,3 +118,35 @@ type TTATests () =
         let automaton = ttaTraverser.GetOrAddApplicationAutomaton pred xs
         let decls = List.map toString automaton.Declarations
         ()
+
+    [<Test>]
+    member x.strategiesTest1 () =
+        let ttaTraverser = TtaTransform.ToTTATraverser(2)
+        let pred = predicate "pred" [tree; tree]
+        let patterns = [
+            TtaTransform.Pattern([leaf; node xTree yTree])
+            TtaTransform.Pattern([node xTree yTree; node vTree wTree])
+            TtaTransform.Pattern([xTree; yTree])
+        ]
+        let auts = ttaTraverser.GeneratePatternAutomata true pred patterns
+        ()
+
+    [<Test>]
+    member x.strategiesTest2 () =
+        let ttaTraverser = TtaTransform.ToTTATraverser(2)
+        let pred = predicate "pred" [tree; tree]
+        let patterns = [
+            TtaTransform.Pattern([xTree; yTree])
+        ]
+        let auts = ttaTraverser.GeneratePatternAutomata true pred patterns
+        ()
+
+    [<Test>]
+    member x.strategiesTest3 () =
+        let ttaTraverser = TtaTransform.ToTTATraverser(2)
+        let pred = predicate "pred" [tree; tree]
+        let patterns = [
+            TtaTransform.Pattern([node xTree yTree; node vTree wTree])
+        ]
+        let auts = ttaTraverser.GeneratePatternAutomata true pred patterns
+        ()