Implement variable-eliminating simplifications under a flag (metalift#65)

Author: shadaj

actors/synthesis.py

@@ -171,7 +171,8 @@ def __call__(
         uid: int = 0,
         noVerify: bool = False,
         unboundedInts: bool = False,
-        listBound: int = 1,
+        optimize_vc_equality: bool = False,
+        listBound: int = 2,
     ) -> typing.List[Expr]:
         ...
 

synthesize_cvc5.py

@@ -210,13 +210,35 @@ def synthesize(
     uid: int = 0,
     noVerify: bool = False,  # currently ignored
     unboundedInts: bool = False,  # currently ignored
+    optimize_vc_equality: bool = False,
     listBound: int = 2,  # currently ignored
 ) -> typing.List[Expr]:
     synthDir = "./synthesisLogs/"
     if not os.path.exists(synthDir):
         os.mkdir(synthDir)
     sygusFile = synthDir + basename + f"_{uid}" + ".sl"
 
+    if optimize_vc_equality:
+        prev_vc = vc.toSMT()
+        new_vars: typing.Set[Expr] = set()
+        while True:
+            expr_count: Dict[str, int] = {}
+            vc.countVariableUses(expr_count)
+
+            vc = vc.optimizeUselessEquality(expr_count, new_vars)
+
+            if vc.toSMT() == prev_vc:
+                break  # run to fixpoint
+            else:
+                prev_vc = vc.toSMT()
+
+        vars = vars.union(new_vars)
+        for var in list(vars):
+            if var.args[0] not in expr_count:
+                vars.remove(var)
+    else:
+        vc = vc.simplify()
+
     # Generate sygus file for synthesis
     toSMT(
         targetLang,

synthesize_rosette.py

@@ -303,6 +303,7 @@ def synthesize(
     uid: int = 0,
     noVerify: bool = False,
     unboundedInts: bool = False,
+    optimize_vc_equality: bool = False,
     listBound: int = 2,
 ) -> typing.List[Expr]:
     invGuess: typing.List[Any] = []
@@ -312,23 +313,27 @@ def synthesize(
 
     while True:
         synthFile = synthDir + basename + f"_{uid}" + ".rkt"
-        # prev_vc = vc.toSMT()
-        # new_vars: typing.Set[Expr] = set()
-        # while True:
-        #     expr_count: Dict[str, int] = {}
-        #     vc.countVariableUses(expr_count)
-
-        #     vc = vc.optimizeUselessEquality(expr_count, new_vars)
-
-        #     if vc.toSMT() == prev_vc:
-        #         break  # run to fixpoint
-        #     else:
-        #         prev_vc = vc.toSMT()
-
-        # vars = vars.union(new_vars)
-        # for var in list(vars):
-        #     if var.args[0] not in expr_count:
-        #         vars.remove(var)
+
+        if optimize_vc_equality:
+            prev_vc = vc.toSMT()
+            new_vars: typing.Set[Expr] = set()
+            while True:
+                expr_count: Dict[str, int] = {}
+                vc.countVariableUses(expr_count)
+
+                vc = vc.optimizeUselessEquality(expr_count, new_vars)
+
+                if vc.toSMT() == prev_vc:
+                    break  # run to fixpoint
+                else:
+                    prev_vc = vc.toSMT()
+
+            vars = vars.union(new_vars)
+            for var in list(vars):
+                if var.args[0] not in expr_count:
+                    vars.remove(var)
+        else:
+            vc = vc.simplify()
 
         ##### synthesis procedure #####
         choices: Dict[str, Dict[str, Expr]] = {}