Optimization for larger examples

pkg/symbolicexpr/symbolicPath.go

@@ -27,6 +27,14 @@ func (path *SymbolicPath) isSubset(other *SymbolicPath, hints *Hints) bool {
 		path.Dst.isSubset(&other.Dst, hints)
 }
 
+func (paths *SymbolicPaths) add(newPath *SymbolicPath, hints *Hints) *SymbolicPaths {
+	if newPath.isEmpty(hints) {
+		return paths
+	}
+	res := append(*paths, newPath)
+	return &res
+}
+
 func (paths *SymbolicPaths) String() string {
 	if len(*paths) == 0 {
 		return emptySet
@@ -38,17 +46,6 @@ func (paths *SymbolicPaths) String() string {
 	return strings.Join(res, "\n")
 }
 
-// remove empty SymbolicPaths; a path is empty if any of its components (src, dst, conn) is empty
-func (paths *SymbolicPaths) removeEmpty(hints *Hints) *SymbolicPaths {
-	newPaths := SymbolicPaths{}
-	for _, path := range *paths {
-		if !path.isEmpty(hints) {
-			newPaths = append(newPaths, path)
-		}
-	}
-	return &newPaths
-}
-
 // Given SymbolicPaths, removes redundant terms from each SymbolicPath
 // a term is redundant if it is a tautology or if it is implied by other terms given hints;
 // e.g., given that Slytherin and Gryffindor are disjoint, = Gryffindor implies != Slytherin
@@ -118,9 +115,10 @@ func ComputeAllowGivenDenies(allowPaths, denyPaths *SymbolicPaths, hints *Hints)
 			newComputedAllowPaths = SymbolicPaths{}
 			for _, computedAllow := range computedAllowPaths {
 				thisComputed := *computeAllowGivenAllowHigherDeny(*computedAllow, *denyPath, hints)
+				thisComputed = thisComputed.removeIsSubsetPath(hints)
 				newComputedAllowPaths = append(newComputedAllowPaths, thisComputed...)
 			}
-			computedAllowPaths = newComputedAllowPaths
+			computedAllowPaths = newComputedAllowPaths.removeIsSubsetPath(hints)
 		}
 		res = append(res, computedAllowPaths...)
 		fmt.Println()
@@ -131,27 +129,27 @@ func ComputeAllowGivenDenies(allowPaths, denyPaths *SymbolicPaths, hints *Hints)
 
 // algorithm described in README of symbolicexpr
 func computeAllowGivenAllowHigherDeny(allowPath, denyPath SymbolicPath, hints *Hints) *SymbolicPaths {
-	resAllowPaths := SymbolicPaths{}
+	resAllowPaths := &SymbolicPaths{}
 	for _, srcAtom := range denyPath.Src {
 		if !srcAtom.isTautology() {
 			srcAtomNegate := srcAtom.negate().(atomicTerm)
-			resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: *allowPath.Src.copy().add(srcAtomNegate),
-				Dst: allowPath.Dst, Conn: allowPath.Conn})
+			resAllowPaths = resAllowPaths.add(&SymbolicPath{Src: *allowPath.Src.copy().add(srcAtomNegate),
+				Dst: allowPath.Dst, Conn: allowPath.Conn}, hints)
 		}
 	}
 	for _, dstAtom := range denyPath.Dst {
 		if !dstAtom.isTautology() {
 			dstAtomNegate := dstAtom.negate().(atomicTerm)
-			resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: allowPath.Src, Dst: *allowPath.Dst.copy().add(dstAtomNegate),
-				Conn: allowPath.Conn})
+			resAllowPaths = resAllowPaths.add(&SymbolicPath{Src: allowPath.Src, Dst: *allowPath.Dst.copy().add(dstAtomNegate),
+				Conn: allowPath.Conn}, hints)
 		}
 	}
 	if !denyPath.Conn.IsAll() { // Connection of deny path is not tautology
-		resAllowPaths = append(resAllowPaths, &SymbolicPath{Src: allowPath.Src, Dst: allowPath.Dst,
-			Conn: allowPath.Conn.Subtract(denyPath.Conn)})
+		resAllowPaths = resAllowPaths.add(&SymbolicPath{Src: allowPath.Src, Dst: allowPath.Dst,
+			Conn: allowPath.Conn.Subtract(denyPath.Conn)}, hints)
 	}
 	// removes empty SymblicPaths; of non-empty paths removed redundant terms
-	return resAllowPaths.removeEmpty(hints).removeRedundant(hints)
+	return resAllowPaths.removeRedundant(hints)
 }
 
 // ConvertFWRuleToSymbolicPaths given a rule, converts its src, dst and Conn to SymbolicPaths

pkg/synthesis/synthesis_test.go

@@ -68,12 +68,12 @@ var allTests = []synthesisTest{
 	{
 		name:   "ExampleHogwartsNoDumbledore",
 		exData: tests.ExampleHogwartsNoDumbledore,
-		noHint: false,
+		noHint: true,
 	},
 	{
 		name:   "ExampleHogwarts",
 		exData: tests.ExampleHogwarts,
-		noHint: false,
+		noHint: true,
 	},
 }
 

pkg/synthesis/tests_expected_output/ExampleHogwartsNoDumbledore_ConvertToAbstractNoHint.txt

@@ -0,0 +1,22 @@
+Allow Only Rules
+~~~~~~~~~~~~~~~~~
+inbound rules
+	All Connections from (group  = Gryffindor) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Hufflepuff) to (group  = Web and group  = Hufflepuff)
+	All Connections from (group  = Slytherin) to (group  = Web and group  = Slytherin)
+	All Connections from (group  = Web and group  = Gryffindor) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Hufflepuff) to (group  = App and group  = Hufflepuff)
+	All Connections from (group  = Web and group  = Slytherin) to (group  = App and group  = Slytherin)
+	All Connections from (group  = App and group  = Gryffindor) to (group  = DB and group  = Gryffindor)
+	All Connections from (group  = App and group  = Hufflepuff) to (group  = DB and group  = Hufflepuff)
+	All Connections from (group  = App and group  = Slytherin) to (group  = DB and group  = Slytherin)
+outbound rules
+	All Connections from (group  = Gryffindor) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Hufflepuff) to (group  = Web and group  = Hufflepuff)
+	All Connections from (group  = Slytherin) to (group  = Web and group  = Slytherin)
+	All Connections from (group  = Web and group  = Gryffindor) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Hufflepuff) to (group  = App and group  = Hufflepuff)
+	All Connections from (group  = Web and group  = Slytherin) to (group  = App and group  = Slytherin)
+	All Connections from (group  = App and group  = Gryffindor) to (group  = DB and group  = Gryffindor)
+	All Connections from (group  = App and group  = Hufflepuff) to (group  = DB and group  = Hufflepuff)
+	All Connections from (group  = App and group  = Slytherin) to (group  = DB and group  = Slytherin)

pkg/synthesis/tests_expected_output/ExampleHogwarts_ConvertToAbstractNoHint.txt

@@ -0,0 +1,28 @@
+Allow Only Rules
+~~~~~~~~~~~~~~~~~
+inbound rules
+	All Connections from (group  = Gryffindor) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Hufflepuff) to (group  = Web and group  = Hufflepuff)
+	All Connections from (group  = Slytherin) to (group  = Web and group  = Slytherin)
+	All Connections from (group  = Dumbledore) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Gryffindor) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Hufflepuff) to (group  = App and group  = Hufflepuff)
+	All Connections from (group  = Web and group  = Slytherin) to (group  = App and group  = Slytherin)
+	All Connections from (group  = Web and group  = Dumbledore) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = App and group  = Gryffindor) to (group  = DB and group  = Gryffindor)
+	All Connections from (group  = App and group  = Hufflepuff) to (group  = DB and group  = Hufflepuff)
+	All Connections from (group  = App and group  = Slytherin) to (group  = DB and group  = Slytherin)
+	All Connections from (group  = App and group  = Dumbledore) to (group  = DB and group  = Gryffindor)
+outbound rules
+	All Connections from (group  = Gryffindor) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Hufflepuff) to (group  = Web and group  = Hufflepuff)
+	All Connections from (group  = Slytherin) to (group  = Web and group  = Slytherin)
+	All Connections from (group  = Dumbledore) to (group  = Web and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Gryffindor) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = Web and group  = Hufflepuff) to (group  = App and group  = Hufflepuff)
+	All Connections from (group  = Web and group  = Slytherin) to (group  = App and group  = Slytherin)
+	All Connections from (group  = Web and group  = Dumbledore) to (group  = App and group  = Gryffindor)
+	All Connections from (group  = App and group  = Gryffindor) to (group  = DB and group  = Gryffindor)
+	All Connections from (group  = App and group  = Hufflepuff) to (group  = DB and group  = Hufflepuff)
+	All Connections from (group  = App and group  = Slytherin) to (group  = DB and group  = Slytherin)
+	All Connections from (group  = App and group  = Dumbledore) to (group  = DB and group  = Gryffindor)