Put SSL rules for sequences behind a flag and test suite file

Author: abhishekc-sharma

src/main/scala/org/tygus/suslik/synthesis/SynConfig.scala

@@ -29,6 +29,7 @@ case class SynConfig(
                       memoization: Boolean = true,
                       delegatePure: Boolean = false,
                       extendedPure: Boolean = false,
+                      sequenceRules: Boolean = false,
                       // Timeout and logging
                       interactive: Boolean = false,
                       printStats: Boolean = false,

src/main/scala/org/tygus/suslik/synthesis/SynthesisRunner.scala

@@ -176,6 +176,10 @@ object SynthesisRunner extends SynthesisRunnerUtil {
       conf => conf.copy(extendedPure = b, delegatePure = b || conf.delegatePure)
     }).text("use extended search space for pure synthesis with CVC4; default: false")
 
+    opt[Boolean](name = "sequenceRules").action(cfg { b =>
+      _.copy(sequenceRules = b)
+    }).text("use some additional heuristics for synthesis with sequences; default: false")
+
     opt[Boolean]('i', "interactive").action(cfg { b =>
       _.copy(interactive = b)
     }).text("interactive mode; default: false")

src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala

@@ -78,8 +78,8 @@ object BranchRules extends PureLogicUtils with SepLogicUtils with RuleUtils {
 
     def atomCandidates(goal: Goal): Seq[Expr] =
       for {
-        lhs <- goal.programVars.filter(v => goal.post.phi.vars.contains(v) && goal.getType(v) == IntType) ++ List(IntConst(0))
-        rhs <- goal.programVars.filter(v => goal.post.phi.vars.contains(v) && goal.getType(v) == IntType) ++ List(IntConst(0))
+        lhs <- goal.programVars.filter(v => goal.post.phi.vars.contains(v) && goal.getType(v) == IntType) ++ (if (goal.env.config.sequenceRules) List(IntConst(0)) else List())
+        rhs <- goal.programVars.filter(v => goal.post.phi.vars.contains(v) && goal.getType(v) == IntType) ++ (if (goal.env.config.sequenceRules) List(IntConst(0)) else List())
         if lhs != rhs
       } yield lhs |<=| rhs
 

src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala

@@ -51,10 +51,9 @@ object FailRules extends PureLogicUtils with SepLogicUtils with RuleUtils {
     def apply(goal: Goal): Seq[RuleResult] = {
       val (uniPost, exPost) = goal.splitPost
       // If precondition does not contain predicates, we can't get new facts from anywhere
-      if (!SMTSolving.valid(goal.pre.phi ==> uniPost)) {
+      if (!SMTSolving.valid(goal.pre.phi ==> uniPost))
       // universal post not implied by pre
         List(RuleResult(List(goal.unsolvableChild), IdProducer, this, goal))
-      }
       else filterOutValidPost(goal, exPost, uniPost)
     }
   }

src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala

@@ -52,7 +52,8 @@ object OperationalRules extends SepLogicUtils with RuleUtils {
 
 
       // When do two heaplets match
-      def isMatch(hl: Heaplet, hr: Heaplet) = sameLhs(hl)(hr) && !sameRhs(hl)(hr) && noGhosts(hr) && noForbiddenExprs(hr)
+      def isMatch(hl: Heaplet, hr: Heaplet) = sameLhs(hl)(hr) && !sameRhs(hl)(hr) && noGhosts(hr) &&
+                                              (!goal.env.config.sequenceRules || noForbiddenExprs(hr))
 
       findMatchingHeaplets(_ => true, isMatch, goal.pre.sigma, goal.post.sigma) match {
         case None => Nil

src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala

@@ -115,7 +115,6 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
     Γ ; {φ ; P} ; {ψ ∧ X = l; Q} ---> S
   */
   object SubstRight extends SynthesisRule with InvertibleRule {
-  //object SubstRight extends SynthesisRule {
     override def toString: String = "SubstExist"
 
     def apply(goal: Goal): Seq[RuleResult] = {
@@ -129,8 +128,8 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
           goal.isExistential(x) &&
           // if it's a program-level existential, then all vars in d must be program-level
           (!goal.isProgramLevelExistential(x) || d.vars.subsetOf(goal.programVars.toSet)) &&
-          // no forbidden expressions
-          noForbiddenExprs(d)
+          // no forbidden expressions if sequenceRules enabled
+          (!goal.env.config.sequenceRules || noForbiddenExprs(d))
         case _ => false
       }
 
@@ -184,7 +183,8 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
     override def toString: String = "PickExist"
 
     def apply(goal: Goal): Seq[RuleResult] = {
-      val constants = List(IntConst(0), IntConst(-1), SetLiteral(List()), SequenceLiteral(List()), eTrue, eFalse)
+      val constants = if (goal.env.config.sequenceRules) List(IntConst(0), IntConst(-1), SetLiteral(List()), SequenceLiteral(List()), eTrue, eFalse)
+                      else List(IntConst(0), SetLiteral(List()), SequenceLiteral(List()), eTrue, eFalse)
 
       val exCandidates = // goal.existentials
        if (goal.post.sigma.isEmp) goal.existentials else goal.existentials.intersect(goal.post.sigma.vars)
@@ -205,7 +205,8 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
       for {
         ex <- least(exCandidates) // since all existentials must go, no point trying them in different order
         val uni = toSorted(uniCandidates(ex))
-        v <- uni ++ constants ++ uni.flatMap(x => inductiveCandidates(x, x.getType(goal.gamma).get))
+        v <- if (goal.env.config.sequenceRules) uni ++ constants ++ uni.flatMap(x => inductiveCandidates(x, x.getType(goal.gamma).get))
+             else uni ++ constants
 
         if goal.getType(ex) == v.getType(goal.gamma).get
         sigma = Map(ex -> v)

src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn

@@ -1,4 +1,4 @@
-# -c 1 -o 1 -b true
+# -c 1 -o 1 -b true --sequenceRules true
 
 #####
 

src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn

@@ -1,4 +1,4 @@
-# -c 1 -o 1
+# -c 1 -o 1 --sequenceRules true
 
 #####
 

src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn

@@ -1,4 +1,4 @@
-# -c 2 -o 2 -b true
+# -c 2 -o 2 -b true --sequenceRules true
 
 #####
 

src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn

@@ -1,4 +1,4 @@
-# -c 1 -o 1 -b true
+# -c 1 -o 1 -b true --sequenceRules true
 
 #####