From 2bb0f8d8d93d2bc0a88089e0f070cb95d8120284 Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Sat, 19 Feb 2022 17:09:22 -0800
Subject: [PATCH 01/10] Adding a version of sequences using List ADT

---
 .../tygus/suslik/language/Expressions.scala   | 51 +++++++++++++-
 .../org/tygus/suslik/language/Types.scala     |  4 ++
 .../tygus/suslik/logic/PureLogicUtils.scala   | 19 +++++
 .../tygus/suslik/logic/smt/SMTSolving.scala   | 70 ++++++++++++++++++-
 .../org/tygus/suslik/parsing/SSLLexical.scala |  6 +-
 .../org/tygus/suslik/parsing/SSLParser.scala  | 11 ++-
 .../suslik/synthesis/rules/LogicalRules.scala |  1 +
 .../synthesis/rules/UnificationRules.scala    |  3 +-
 .../sequences/llist/llist-create.syn          | 14 ++++
 .../sequences/llist/llist_append.syn          |  9 +++
 .../synthesis/sequences/llist/llist_copy.syn  |  9 +++
 .../synthesis/sequences/llist/llist_empty.syn | 12 ++++
 .../sequences/llist/llist_insert_head.syn     |  9 +++
 .../sequences/llist/llist_insert_tail.syn     |  9 +++
 .../synthesis/sequences/llist/llist_skip.syn  | 12 ++++
 .../synthesis/sequences/llist/lseg.def        |  4 ++
 .../synthesis/sequences/pure/unify1.syn       | 12 ++++
 .../synthesis/sequences/pure/unify2.syn       | 13 ++++
 .../synthesis/sequences/pure/unify3.syn       | 13 ++++
 19 files changed, 271 insertions(+), 10 deletions(-)
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist-create.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_append.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_copy.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_empty.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_skip.syn
 create mode 100644 src/test/resources/synthesis/sequences/llist/lseg.def
 create mode 100644 src/test/resources/synthesis/sequences/pure/unify1.syn
 create mode 100644 src/test/resources/synthesis/sequences/pure/unify2.syn
 create mode 100644 src/test/resources/synthesis/sequences/pure/unify3.syn

diff --git a/src/main/scala/org/tygus/suslik/language/Expressions.scala b/src/main/scala/org/tygus/suslik/language/Expressions.scala
index 58ed7f9b6..8158120a0 100644
--- a/src/main/scala/org/tygus/suslik/language/Expressions.scala
+++ b/src/main/scala/org/tygus/suslik/language/Expressions.scala
@@ -75,6 +75,7 @@ object Expressions {
       (IntSetType, IntSetType) -> OpSetEq,
       (IntervalType, IntervalType) -> OpIntervalEq,
       (BoolType, BoolType) -> OpBoolEq,
+      (IntSequenceType, IntSequenceType) -> OpSequenceEq
     )
 
     override def default: BinOp = OpEq
@@ -132,6 +133,7 @@ object Expressions {
       (IntType, IntType) -> OpPlus,
       (IntSetType, IntSetType) -> OpUnion,
       (IntervalType, IntervalType) -> OpIntervalUnion,
+      (IntSequenceType, IntSequenceType) -> OpSequenceAppend
     )
 
     override def default: BinOp = OpPlus
@@ -298,7 +300,36 @@ object Expressions {
     def lType: SSLType = IntervalType
     def rType: SSLType = IntervalType
   }
-
+  object OpSequenceEq extends RelOp with SymmetricOp {
+    def level: Int = 3
+    override def pp: String = "=="
+    def lType: SSLType = IntSequenceType
+    def rType: SSLType = IntSequenceType
+  }
+  object OpSequenceCons extends BinOp {
+    def level: Int = 4
+    override def pp: String = "::"
+    def lType: SSLType = IntType
+    def rType: SSLType = IntSequenceType
+    def resType: SSLType = IntSequenceType
+  }
+  object OpSequenceAppend extends BinOp with AssociativeOp {
+    def level: Int = 4
+    override def pp: String = "++"
+    def lType: SSLType = IntSequenceType
+    def rType: SSLType = IntSequenceType
+    def resType: SSLType = IntSequenceType
+  }
+  object OpSequenceHead extends UnOp {
+    override def pp: String = "head"
+    override def inputType: SSLType = IntSequenceType
+    override def outputType: SSLType = IntType
+  }
+  object OpSequenceTail extends UnOp {
+    override def pp: String = "tail"
+    override def inputType: SSLType = IntSequenceType
+    override def outputType: SSLType = IntSequenceType
+  }
 
   sealed abstract class Expr extends PrettyPrinting with HasExpressions[Expr] with Ordered[Expr] {
 
@@ -326,6 +357,9 @@ object Expressions {
         case s@SetLiteral(elems) =>
           val acc1 = if (p(s)) acc + s.asInstanceOf[R] else acc
           elems.foldLeft(acc1)((a,e) => collector(a)(e))
+        case s@SequenceLiteral(elems) =>
+          val acc1 = if (p(s)) acc + s.asInstanceOf[R] else acc
+          elems.foldLeft(acc1)((a, e) => collector(a)(e))
         case i@IfThenElse(cond, l, r) =>
           val acc1 = if (p(i)) acc + i.asInstanceOf[R] else acc
           val acc2 = collector(acc1)(cond)
@@ -425,6 +459,13 @@ object Expressions {
             case Some(g) => e.resolve(g, Some(IntType))
           })
         } else None
+      case SequenceLiteral(elems) =>
+        if (IntSequenceType.conformsTo(target)) {
+          elems.foldLeft[Option[Gamma]](Some(gamma))((go, e) => go match {
+            case None => None
+            case Some(g) => e.resolve(g, Some(IntType))
+          })
+        } else None
       case IfThenElse(c, t, e) =>
         for {
           gamma1 <- c.resolve(gamma, Some(BoolType))
@@ -449,6 +490,7 @@ object Expressions {
       case OverloadedBinaryExpr(_, l, r) => 1 + l.size + r.size
       case UnaryExpr(_, arg) => 1 + arg.size
       case SetLiteral(elems) => 1 + elems.map(_.size).sum
+      case SequenceLiteral(elems) => 1 + elems.map(_.size).sum
       case IfThenElse(cond, l, r) => 1 + cond.size + l.size + r.size
       case _ => 1
     }
@@ -478,6 +520,7 @@ object Expressions {
       case IfThenElse(c, t, e) =>IfThenElse(c.resolveOverloading(gamma),
                                             t.resolveOverloading(gamma),
                                             e.resolveOverloading(gamma))
+      case SequenceLiteral(elems) => SequenceLiteral(elems.map(_.resolveOverloading(gamma)))
 
     }
   }
@@ -610,6 +653,12 @@ object Expressions {
     def getType(gamma: Gamma): Option[SSLType] = left.getType(gamma)
   }
 
+  case class SequenceLiteral(elems: List[Expr]) extends Expr {
+    override def pp: String = s"[${elems.map(_.pp).mkString(",")}]"
+    override def subst(sigma: Subst): SequenceLiteral = SequenceLiteral(elems.map(_.subst(sigma)))
+    def getType(gamma: Gamma): Option[SSLType] = Some(IntSequenceType)
+  }
+
   /**
     * Unknown predicate (to be replaced by a term)
     * @param name Predicate name
diff --git a/src/main/scala/org/tygus/suslik/language/Types.scala b/src/main/scala/org/tygus/suslik/language/Types.scala
index c0e69fdce..6478c5ff1 100644
--- a/src/main/scala/org/tygus/suslik/language/Types.scala
+++ b/src/main/scala/org/tygus/suslik/language/Types.scala
@@ -95,3 +95,7 @@ case object CardType extends SSLType {
     case _ => None
   }
 }
+
+case object IntSequenceType extends SSLType {
+  override def pp: String = "intseq"
+}
diff --git a/src/main/scala/org/tygus/suslik/logic/PureLogicUtils.scala b/src/main/scala/org/tygus/suslik/logic/PureLogicUtils.scala
index 60580246e..b55a6ad8f 100644
--- a/src/main/scala/org/tygus/suslik/logic/PureLogicUtils.scala
+++ b/src/main/scala/org/tygus/suslik/logic/PureLogicUtils.scala
@@ -44,6 +44,7 @@ trait PureLogicUtils {
     case _:Var => e
     case IfThenElse(e1,e2,e3) => IfThenElse(propagate_not(e1),propagate_not(e2), propagate_not(e3))
     case SetLiteral(args) => SetLiteral(args.map(propagate_not))
+    case SequenceLiteral(args) => SequenceLiteral(args.map(propagate_not))
     case e => throw SynthesisException(s"Not supported: ${e.pp} (${e.getClass.getName})")
   }
 
@@ -67,6 +68,7 @@ trait PureLogicUtils {
     case _:Var => e
     case IfThenElse(e1,e2,e3) => IfThenElse(desugar(e1),desugar(e2), desugar(e3))
     case SetLiteral(args) => SetLiteral(args.map(desugar))
+    case SequenceLiteral(args) => SequenceLiteral(args.map(desugar))
     case e => throw SynthesisException(s"Not supported: ${e.pp} (${e.getClass.getName})")
   }
 
@@ -120,6 +122,23 @@ trait PureLogicUtils {
 //    case BinaryExpr(OpBoolEq, v1@Var(n1), v2@Var(n2)) => // sort arguments lexicographically
 //      if (n1 <= n2) BinaryExpr(OpBoolEq, v1, v2) else BinaryExpr(OpBoolEq, v2, v1)
 //    case BinaryExpr(OpBoolEq, e, v@Var(_)) if !e.isInstanceOf[Var] => BinaryExpr(OpBoolEq, v, simplify(e))
+    
+    // Sequence Operations
+    
+    // Sequence Equality
+    case BinaryExpr(OpSequenceEq, Var(n1), Var(n2)) if n1 == n2 => // remove trivial equality
+      BoolConst(true)
+    case BinaryExpr(OpSequenceEq, v1@Var(n1), v2@Var(n2)) =>  // sort arguments lexicographically
+      if (n1 <= n2) BinaryExpr(OpSequenceEq, v1, v2) else BinaryExpr(OpSequenceEq, v2, v1)
+    case BinaryExpr(OpSequenceEq, e, v@Var(_)) if !e.isInstanceOf[Var] => BinaryExpr(OpSequenceEq, v, simplify(e))
+
+    // Sequence Append
+    case BinaryExpr(OpSequenceAppend, left, SequenceLiteral(s)) if s.isEmpty => simplify(left)
+    case BinaryExpr(OpSequenceAppend, SequenceLiteral(s), right) if s.isEmpty => simplify(right)
+
+    // Sequence Cons
+    //case BinaryExpr(OpSequenceCons, left, SequenceLiteral(s)) if s.isEmpty => SequenceLiteral([simplify(left)])
+
 
     case BinaryExpr(OpPlus, left, IntConst(i)) if i.toInt == 0 => simplify(left)
     case BinaryExpr(OpPlus, IntConst(i), right) if i.toInt == 0 => simplify(right)
diff --git a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
index 828c118c7..7333be57d 100644
--- a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
+++ b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
@@ -54,11 +54,13 @@ object SMTSolving extends Core
 
   trait SetTerm
   trait IntervalTerm
+  trait SequenceTerm
 
   type SMTBoolTerm = TypedTerm[BoolTerm, Term]
   type SMTIntTerm = TypedTerm[IntTerm, Term]
   type SMTSetTerm = TypedTerm[SetTerm, Term]
   type SMTIntervalTerm = TypedTerm[IntervalTerm, Term]
+  type SMTSequenceTerm = TypedTerm[SequenceTerm, Term]
 
   def setSort: Sort = SortId(SymbolId(SSymbol("SetInt")))
 
@@ -107,6 +109,23 @@ object SMTSolving extends Core
     "(define-fun iunion ((s1 Interval) (s2 Interval)) Interval (ite (iempty s1) s2 (iinsert (lower s1) (iinsert (upper s1) s2))))",
   )
 
+  def sequenceSort: Sort = SortId(SymbolId(SSymbol("SequenceInt")))
+
+  def emptySequenceSymbol = SimpleQId(SymbolId(SSymbol("sempty")))
+
+  def sequenceConsSymbol = SimpleQId(SymbolId(SSymbol("scons")))
+
+  def sequenceAppendSymbol = SimpleQId(SymbolId(SSymbol("sappend")))
+
+  def emptySequenceTerm: Term = QIdTerm(emptySequenceSymbol)
+
+  def sequencePrelude: List[String] = List(
+    "(define-sort SequenceInt () (List Int))",
+    "(define-fun sempty () SequenceInt (as nil SequenceInt))",
+    "(define-fun scons ((x Int) (xs SequenceInt)) SequenceInt (insert x xs))",
+    "(define-fun-rec sappend ((xs SequenceInt) (ys SequenceInt)) SequenceInt (match xs ((nil ys) ((insert x xsn) (insert x (sappend xsn ys))))))"
+  )
+
   // Commands to be executed before solving starts
   def prelude = if (defaultSolver == "CVC4") {
     List(
@@ -127,7 +146,7 @@ object SMTSolving extends Core
       "(assert (forall ((b1 Bool) (b2 Bool)) (= (andNot b1 b2) (and b1 (not b2)))))",
       "(define-fun difference ((s1 SetInt) (s2 SetInt)) SetInt ((_ map andNot) s1 s2))",
       "(declare-datatypes () ((Interval (interval (lower Int) (upper Int)))))"
-    ) ++ intervalPrelude
+    ) ++ sequencePrelude ++ intervalPrelude
   } else if (defaultSolver == "Z3 <= 4.7.x") {
     // In Z3 4.7.x and below, difference is built in and intersection is called intersect
     List(
@@ -136,7 +155,7 @@ object SMTSolving extends Core
       "(define-fun member ((x Int) (s SetInt)) Bool (select s x))",
       "(define-fun insert ((x Int) (s SetInt)) SetInt (store s x true))",
       "(declare-datatypes () ((Interval (interval (lower Int) (upper Int)))))"
-    ) ++ intervalPrelude
+    ) ++ sequencePrelude ++ intervalPrelude
   } else throw SolverUnsupportedExpr(defaultSolver)
 
   private def checkSat(term: SMTBoolTerm): Boolean =
@@ -238,6 +257,47 @@ object SMTSolving extends Core
     case _ => throw SMTUnsupportedExpr(e)
   }
 
+  private def convertSequenceExpr(e: Expr): SMTSequenceTerm = e match {
+    case Var(name) => new VarTerm[SequenceTerm](name, sequenceSort)
+    case SequenceLiteral(elems) => {
+      val emptyTerm = new TypedTerm[SequenceTerm, Term](Set.empty, emptySequenceTerm)
+      makeSequenceCons(emptyTerm, elems)
+    }
+    case BinaryExpr(OpSequenceCons, left, right) => {
+      val l = convertIntExpr(left)
+      val r = convertSequenceExpr(right)
+
+      new TypedTerm[SequenceTerm, Term](l.typeDefs ++ r.typeDefs,
+        QIdAndTermsTerm(sequenceConsSymbol, List(l.termDef, r.termDef)))      
+    }
+
+    case BinaryExpr(OpSequenceAppend, left, right) => {
+      val l = convertSequenceExpr(left)
+      val r = convertSequenceExpr(right)
+
+      new TypedTerm[SequenceTerm, Term](l.typeDefs ++ r.typeDefs,
+        QIdAndTermsTerm(sequenceAppendSymbol, List(l.termDef, r.termDef)))      
+    }
+    case _ => throw SMTUnsupportedExpr(e)
+  }
+
+  private def makeSequenceCons(sequenceTerm: SMTSequenceTerm, elems: List[Expr]): SMTSequenceTerm = {
+    if (elems.isEmpty) {
+      sequenceTerm
+    } else {
+      val eTerms: List[SMTIntTerm] = elems.map(convertIntExpr)
+      if (defaultSolver == "CVC4") {
+        throw SolverUnsupportedExpr(defaultSolver)
+      } else if (defaultSolver == "Z3" || defaultSolver == "Z3 <= 4.7.x") {
+        def makeInsertOne(eTerm: SMTIntTerm, sequenceTerm: SMTSequenceTerm): SMTSequenceTerm =
+          new TypedTerm[SequenceTerm, Term](sequenceTerm.typeDefs ++ eTerm.typeDefs,
+            QIdAndTermsTerm(sequenceConsSymbol, List(eTerm.termDef, sequenceTerm.termDef)))
+
+        eTerms.foldRight(sequenceTerm)(makeInsertOne)
+      } else throw SolverUnsupportedExpr(defaultSolver)
+    }
+  }
+
   private def convertBoolExpr(e: Expr): SMTBoolTerm = e match {
     case Var(name) => Bools(name)
     case BoolConst(true) => True()
@@ -314,6 +374,12 @@ object SMTSolving extends Core
       val r = convertBoolExpr(right)
       c.ite(l, r)
     }
+    case BinaryExpr(OpSequenceEq, left, right) => {
+      val l = convertSequenceExpr(left)
+      val r = convertSequenceExpr(right)
+
+      l === r
+    }
     case Unknown(_, _, _) => True() // Treat unknown predicates as true
     case _ => throw SMTUnsupportedExpr(e)
   }
diff --git a/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala b/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
index ca792274b..4a879c9ba 100644
--- a/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
+++ b/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
@@ -8,15 +8,15 @@ import scala.util.parsing.combinator.lexical.StdLexical
 class SSLLexical extends StdLexical {
 
   // Add keywords
-  reserved += ("if", "then", "else", "true", "false", "emp", "not", "return", "predicate", "in", "lower", "upper")
+  reserved += ("if", "then", "else", "true", "false", "emp", "not", "return", "predicate", "in", "lower", "upper", "head", "tail")
   reserved += ("error","magic","malloc", "free", "let", "assume")
   reserved += ("null")
 
   // Types
-  reserved += ("int", "bool", "loc", "set", "void", "interval")
+  reserved += ("int", "bool", "loc", "set", "void", "interval", "seq")
 
   delimiters += ("(", ")", "=", ";", "**", "*", ":->", "=i", "<=i", "++", "--", "..",
-      "{", "}", "/\\", "&&", "\\/", "||", "\n", "\r", "=>", "?", ":",
+      "{", "}", "/\\", "&&", "\\/", "||", "\n", "\r", "=>", "?", ":", "::",
       "<", ">", ",", "/",   "+", "-", "==", "!=", "==>", "<=", ">=", "[", "]", "|", "??"
   )
 
diff --git a/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala b/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
index 22ceabd33..f386e3488 100644
--- a/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
+++ b/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
@@ -38,7 +38,8 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
       | "loc" ^^^ LocType
       | "set" ^^^ IntSetType
       | "interval" ^^^ IntervalType
-      | "void" ^^^ VoidType)
+      | "void" ^^^ VoidType
+      | "seq" ^^^ IntSequenceType)
 
   def formal: Parser[(Var, SSLType)] = typeParser ~ ident ^^ { case a ~ b => (Var(b), a) }
 
@@ -63,10 +64,13 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
     "[" ~> intervalInternal <~ "]"
   }
 
+  def sequenceLiteral: Parser[Expr] =
+    "<" ~> repsep(expr, ",") <~ ">" ^^ SequenceLiteral
+
   def varParser: Parser[Var] = ident ^^ Var
 
   def unOpParser: Parser[UnOp] =
-    ("not" ^^^ OpNot ||| "-" ^^^ OpUnaryMinus ||| "lower" ^^^ OpLower ||| "upper" ^^^ OpUpper)
+    ("not" ^^^ OpNot ||| "-" ^^^ OpUnaryMinus ||| "lower" ^^^ OpLower ||| "upper" ^^^ OpUpper ||| "head" ^^^ OpSequenceHead ||| "tail" ^^^ OpSequenceTail)
 
   // TODO: remove legacy ++, --, =i, /\, \/, <=i
   def termOpParser: Parser[OverloadedBinOp] = "*" ^^^ OpOverloadedStar
@@ -75,6 +79,7 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
   def addOpParser: Parser[OverloadedBinOp] = (
     ("++" ||| "+") ^^^ OpOverloadedPlus
       ||| ("--" ||| "-") ^^^ OpOverloadedMinus
+      ||| "::" ^^^ OpSequenceCons
     )
 
   def relOpParser: Parser[OverloadedBinOp] = (
@@ -100,7 +105,7 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
   def atom: Parser[Expr] = (
     unOpParser ~ atom ^^ { case op ~ a => UnaryExpr(op, a) }
       | "(" ~> expr <~ ")"
-      | intLiteral | boolLiteral | setLiteral | locLiteral | intervalLiteral
+      | intLiteral | boolLiteral | setLiteral | locLiteral | intervalLiteral | sequenceLiteral
       | varParser
     )
 
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/LogicalRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/LogicalRules.scala
index 1d124eceb..e450deabd 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/LogicalRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/LogicalRules.scala
@@ -256,6 +256,7 @@ object LogicalRules extends PureLogicUtils with SepLogicUtils with RuleUtils {
         case BinaryExpr(OpBoolEq, l, r) => extractSides(l, r)
         case BinaryExpr(OpSetEq, l, r) => extractSides(l, r)
         case BinaryExpr(OpIntervalEq, l, r) => extractSides(l, r)
+        case BinaryExpr(OpSequenceEq, l, r) => extractSides(l, r)
         case _ => None
       }, p1) match {
         case Some(((x, e), rest1)) => {
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
index 8e34846e4..89bbc4fb1 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
@@ -141,6 +141,7 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
         case BinaryExpr(OpBoolEq, l, r) => extractSides(l,r)
         case BinaryExpr(OpSetEq, l, r) => extractSides(l,r)
         case BinaryExpr(OpIntervalEq, l, r) => extractSides(l,r)
+        case BinaryExpr(OpSequenceEq, l, r) => extractSides(l, r)
         case _ => None
       }, p2) match {
         case Some(((x, e), rest2)) => {
@@ -167,7 +168,7 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
     override def toString: String = "PickExist"
 
     def apply(goal: Goal): Seq[RuleResult] = {
-      val constants = List(IntConst(0), SetLiteral(List()), eTrue, eFalse)
+      val constants = 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)
diff --git a/src/test/resources/synthesis/sequences/llist/llist-create.syn b/src/test/resources/synthesis/sequences/llist/llist-create.syn
new file mode 100644
index 000000000..2364ca70f
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist-create.syn
@@ -0,0 +1,14 @@
+should be able to allocate a linked list
+###
+
+{ true;  r :-> 0 }
+  void llist_create(loc z, loc r)
+{ true ; r :-> x ** x :-> 0 ** [x, 1] ** lseg(z, z, S) }
+
+###
+
+void llist_create (loc z, loc r) {
+  let x = malloc(1);
+  *r = x;
+  *x = 0;
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/llist_append.syn b/src/test/resources/synthesis/sequences/llist/llist_append.syn
new file mode 100644
index 000000000..b45662abe
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_append.syn
@@ -0,0 +1,9 @@
+should be able to append two linked lists
+
+#####
+
+{ true ; r :-> x ** lseg(x, 0, Sx) ** lseg(y, 0, Sy)}
+void llist_append(loc r, loc y)
+{ S == Sx ++ Sy ; r :-> z ** lseg(z, 0, S)}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/llist_copy.syn b/src/test/resources/synthesis/sequences/llist/llist_copy.syn
new file mode 100644
index 000000000..d6438a732
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_copy.syn
@@ -0,0 +1,9 @@
+should be able to copy one linked list to another
+
+#####
+
+{true ; r :-> x ** lseg(x, 0, s)<a>}
+void sll_copy(loc r)
+{true ; r :-> y ** lseg(x, 0, s)<a> ** lseg(y, 0, s)<b> }
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/llist_empty.syn b/src/test/resources/synthesis/sequences/llist/llist_empty.syn
new file mode 100644
index 000000000..7882f3a1d
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_empty.syn
@@ -0,0 +1,12 @@
+Step 1: x-list is Nil, nothing to do here
+
+#####
+
+{(x == 0) /\ S == <> ; r :-> x}
+void llist_empty(loc r)
+{true ; r :-> y ** lseg(y, 0, S) }
+
+#####
+
+void list_copy (loc r) {
+}
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
new file mode 100644
index 000000000..27e641409
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
@@ -0,0 +1,9 @@
+should insert an item at the beginning of a list
+
+#####
+
+{true; r :-> x ** lseg(x, 0, S)}
+void llist_insert_head(loc r, int item)
+{S1 == item:S; r:-> z ** lseg(z, 0, S1)}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
new file mode 100644
index 000000000..201e5efbb
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
@@ -0,0 +1,9 @@
+should insert an item at the beginning of a list
+
+#####
+
+{true; r :-> x ** lseg(x, 0, S)}
+void llist_insert_tail(loc r, int item)
+{S1 == <item>; r:-> z ** lseg(z, y, S) ** lseg(y, 0, S1)}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/llist_skip.syn b/src/test/resources/synthesis/sequences/llist/llist_skip.syn
new file mode 100644
index 000000000..2845c60a0
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_skip.syn
@@ -0,0 +1,12 @@
+should be able to synthesize programs with non-trivial lists
+
+#####
+
+{true ; r :-> x ** lseg(x, 0, S)}
+  void llist_skip(loc x, loc r)
+{true ; r :-> x ** lseg(x, 0, S) }
+
+###
+
+void llist_skip (loc x, loc r) {
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/lseg.def b/src/test/resources/synthesis/sequences/llist/lseg.def
new file mode 100644
index 000000000..24ebdd087
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/lseg.def
@@ -0,0 +1,4 @@
+predicate lseg(loc x, loc y, seq s) {
+|  x == y        => { s == <> ; emp }
+|  not (x == y)  => { s == v:s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/pure/unify1.syn b/src/test/resources/synthesis/sequences/pure/unify1.syn
new file mode 100644
index 000000000..127a84145
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/pure/unify1.syn
@@ -0,0 +1,12 @@
+Should solve the unification with empty sequences
+
+#####
+
+{ S == <v2> ++ S1 /\ S1 == <> ; emp}
+void foo (int v)
+{ S == <v2> ++ S11  /\  S11 == <> ; emp}
+
+#####
+
+void foo (int v) {
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/pure/unify2.syn b/src/test/resources/synthesis/sequences/pure/unify2.syn
new file mode 100644
index 000000000..069c19312
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/pure/unify2.syn
@@ -0,0 +1,13 @@
+Should solve the unification with empty sequences - 2
+
+#####
+
+{ S == <v> ++ S1 /\ S2 == <>; x :-> a}
+void elemInSet (loc x, int v)
+{  <v1> ++ S1 == S ++ S2; x :-> v1}
+
+#####
+
+void elemInSet (loc x, int v) {
+  *x = v;
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/pure/unify3.syn b/src/test/resources/synthesis/sequences/pure/unify3.syn
new file mode 100644
index 000000000..96f6dcdb7
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/pure/unify3.syn
@@ -0,0 +1,13 @@
+Should solve the unification with empty sequences - 3
+
+#####
+
+{ S == v:S1 /\ S2 == <>; x :-> a}
+void elemInSet (loc x, int v)
+{  v1:S1 == S ++ S2; x :-> v1}
+
+#####
+
+void elemInSet (loc x, int v) {
+  *x = v;
+}
\ No newline at end of file

From 93bec3a4869daa1e83d61813946a1068fa86ee9f Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Mon, 21 Feb 2022 00:40:03 -0800
Subject: [PATCH 02/10] Switching to SMT Seq based encoding for Suslik
 sequences

---
 .../tygus/suslik/language/Expressions.scala   |  2 +-
 .../tygus/suslik/logic/smt/SMTSolving.scala   | 12 +++++-
 .../logic/unification/PureUnification.scala   |  3 ++
 .../paper-benchmarks/dll/definitions.def      | 10 +++++
 .../paper-benchmarks/dll/dll-append.syn       | 29 +++++++++++++
 .../paper-benchmarks/dll/dll-copy.syn         | 41 ++++++++++++++++++
 .../paper-benchmarks/dll/dll-delete-all.syn   | 42 +++++++++++++++++++
 .../paper-benchmarks/dll/dll-dupleton.syn     | 17 ++++++++
 .../paper-benchmarks/dll/dll-singleton.syn    | 18 ++++++++
 .../paper-benchmarks/dll/from-sll.syn         | 41 ++++++++++++++++++
 10 files changed, 213 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/definitions.def
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-append.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-copy.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-dupleton.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-singleton.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/dll/from-sll.syn

diff --git a/src/main/scala/org/tygus/suslik/language/Expressions.scala b/src/main/scala/org/tygus/suslik/language/Expressions.scala
index 8158120a0..377d6fd04 100644
--- a/src/main/scala/org/tygus/suslik/language/Expressions.scala
+++ b/src/main/scala/org/tygus/suslik/language/Expressions.scala
@@ -654,7 +654,7 @@ object Expressions {
   }
 
   case class SequenceLiteral(elems: List[Expr]) extends Expr {
-    override def pp: String = s"[${elems.map(_.pp).mkString(",")}]"
+    override def pp: String = s"<${elems.map(_.pp).mkString(",")}>"
     override def subst(sigma: Subst): SequenceLiteral = SequenceLiteral(elems.map(_.subst(sigma)))
     def getType(gamma: Gamma): Option[SSLType] = Some(IntSequenceType)
   }
diff --git a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
index 7333be57d..1d4d4018b 100644
--- a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
+++ b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
@@ -119,11 +119,18 @@ object SMTSolving extends Core
 
   def emptySequenceTerm: Term = QIdTerm(emptySequenceSymbol)
 
-  def sequencePrelude: List[String] = List(
+  /*def sequencePrelude: List[String] = List(
     "(define-sort SequenceInt () (List Int))",
     "(define-fun sempty () SequenceInt (as nil SequenceInt))",
     "(define-fun scons ((x Int) (xs SequenceInt)) SequenceInt (insert x xs))",
     "(define-fun-rec sappend ((xs SequenceInt) (ys SequenceInt)) SequenceInt (match xs ((nil ys) ((insert x xsn) (insert x (sappend xsn ys))))))"
+  )*/
+
+  def sequencePrelude: List[String] = List(
+    "(define-sort SequenceInt () (Seq Int))",
+    "(define-fun sempty () SequenceInt (as seq.empty SequenceInt))",
+    "(define-fun scons ((x Int) (xs SequenceInt)) SequenceInt (seq.++ (seq.unit x) xs))",
+    "(define-fun sappend ((xs SequenceInt) (ys SequenceInt)) SequenceInt (seq.++ xs ys))"
   )
 
   // Commands to be executed before solving starts
@@ -162,6 +169,7 @@ object SMTSolving extends Core
     this.synchronized {
       timed {
         push(1)
+        //System.out.println("HERE !! " + term);
         val res = isSat(term)
         pop(1)
         res != Success(UnSat()) // Unknown counts as SAT
@@ -431,11 +439,13 @@ object SMTSolving extends Core
 
   // Check if phi is satisfiable; all vars are implicitly existentially quantified
   def sat(phi: Expr): Boolean = {
+    //System.out.println("EXPR:  " + phi.pp);
     cache.getOrElseUpdate(phi, checkSat(convertBoolExpr(phi)))
   }
 
   // Check if phi is valid; all vars are implicitly universally quantified
   def valid(phi: Expr): Boolean = {
+    //System.out.println("EXPR:  " + phi.not.pp)
     !sat(phi.not)
   }
 
diff --git a/src/main/scala/org/tygus/suslik/logic/unification/PureUnification.scala b/src/main/scala/org/tygus/suslik/logic/unification/PureUnification.scala
index ea6b79132..60d23e067 100644
--- a/src/main/scala/org/tygus/suslik/logic/unification/PureUnification.scala
+++ b/src/main/scala/org/tygus/suslik/logic/unification/PureUnification.scala
@@ -31,6 +31,9 @@ object PureUnification extends PureLogicUtils {
       case (SetLiteral(Nil), SetLiteral(Nil)) => List(Map.empty)
       case (SetLiteral(es :: ess), SetLiteral(et :: ets)) =>
         unifyPairs( et, SetLiteral(ets), es, SetLiteral(ess), freeVars)
+      case (SequenceLiteral(Nil), SequenceLiteral(Nil)) => List(Map.empty)
+      case (SequenceLiteral(es :: ess), SequenceLiteral(et :: ets)) =>
+        unifyPairs( et, SequenceLiteral(ets), es, SequenceLiteral(ess), freeVars)
       case _ => if (source == target) List(Map.empty) else Nil
     }
   }
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/definitions.def b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/definitions.def
new file mode 100644
index 000000000..066a99e45
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/definitions.def
@@ -0,0 +1,10 @@
+predicate dll(loc x, loc z, seq s) {
+|  x == 0 => { s == <> ; emp }
+|  not (x == 0) =>
+   { s == v :: s1 ; [x, 3] ** x :-> v ** (x + 1) :-> w ** (x + 2) :-> z ** dll(w, x, s1) }
+}
+
+predicate sll(loc x, seq s) {
+|  x == 0        => { s == <> ; emp }
+|  not (x == 0)  => { s == v :: s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
+}
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-append.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-append.syn
new file mode 100644
index 000000000..7cff0e941
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-append.syn
@@ -0,0 +1,29 @@
+# -c 2 -f 1
+
+doubly-linked list: append
+
+#####
+
+{true ; dll(x1, a, s1) ** dll(x2, b, s2) ** ret :-> x2}
+void dll_append (loc x1, loc ret)
+{s == s1 ++ s2 ; dll(y, c, s) ** ret :-> y }
+
+#####
+
+void dll_append (loc x1, loc ret) {
+  if (x1 == 0) {
+  } else {
+    let w = *(x1 + 1);
+    dll_append(w, ret);
+    let y = *ret;
+    if (y == 0) {
+      *(x1 + 1) = 0;
+      *ret = x1;
+    } else {
+      *(y + 2) = x1;
+      *(x1 + 1) = y;
+      *ret = x1;
+    }
+  }
+}
+
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-copy.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-copy.syn
new file mode 100644
index 000000000..8a7688d1e
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-copy.syn
@@ -0,0 +1,41 @@
+# -c 2 -f 1
+
+should be able to synthesize list copy
+
+#####
+
+{true ; r :-> x ** dll(x, a, s)}
+void dll_copy(loc r)
+{true ; r :-> y ** dll(x, a, s) ** dll(y, b, s) }
+
+#####
+
+void dll_copy (loc r) {
+  let x = *r;
+  if (x == 0) {
+    *r = 0;
+  } else {
+    let vx = *x;
+    let w = *(x + 1);
+    *r = w;
+    dll_copy(r);
+    let y1 = *r;
+    if (y1 == 0) {
+      let y = malloc(3);
+      *r = y;
+      *(y + 1) = 0;
+      *y = vx;
+      *(y + 2) = 0;
+    } else {
+      let v = *y1;
+      let y = malloc(3);
+      *(y1 + 2) = y;
+      *r = y;
+      *(y + 1) = y1;
+      *y1 = vx;
+      *y = v;
+      *(y + 2) = 0;
+    }
+  }
+}
+
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
new file mode 100644
index 000000000..cc83611fa
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
@@ -0,0 +1,42 @@
+# -b true -c 2 -f 1
+doubly-linked list: delete all occurrences of x
+
+#####
+
+{true ; dll(x, b, s) ** ret :-> a}
+void dll_delete_all (loc x, loc ret)
+{s1 =i s -- {a} ; dll(y, c, s1) ** ret :-> y }
+
+#####
+
+void dll_delete_all (loc x, loc ret) {
+  let a = *ret;
+  if (x == 0) {
+    *ret = 0;
+  } else {
+    let vx = *x;
+    if (a <= vx && vx <= a) {
+      let w = *(x + 1);
+      dll_delete_all(w, ret);
+      free(x);
+    } else {
+      let w = *(x + 1);
+      dll_delete_all(w, ret);
+      let y = *ret;
+      if (y == 0) {
+        *(x + 1) = 0;
+        *ret = x;
+      } else {
+        let v = *y;
+        if (vx <= v && v <= vx) {
+          free(x);
+        } else {
+          *(y + 2) = x;
+          *(x + 1) = y;
+          *ret = x;
+        }
+      }
+    }
+  }
+}
+
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-dupleton.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-dupleton.syn
new file mode 100644
index 000000000..0ee585212
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-dupleton.syn
@@ -0,0 +1,17 @@
+# -c 3
+singly-linked list: construct a list with two elements
+
+#####
+
+{ ret :-> a }
+void dll_dupleton (int x, int y, loc ret)
+{ elems == <x, y> ; ret :-> z ** dll(z, 0, elems) }
+
+#####
+
+void sll_dupleton (int x, loc ret) {
+  let y2 = malloc(2);
+  *y2 = x;
+  *(y2 + 1) = 0;
+  *ret = y2;
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-singleton.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-singleton.syn
new file mode 100644
index 000000000..530f46b3c
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-singleton.syn
@@ -0,0 +1,18 @@
+#. -c 2
+singly-linked list: construct a list with one element
+
+#####
+
+{ ret :-> a }
+void dll_singleton (int x, loc ret)
+{ elems == <x> ; ret :-> y ** dll(y, 0, elems) }
+
+#####
+
+void dll_singleton (int x, loc ret) {
+  let y = malloc(3);
+  *ret = y;
+  *(y + 1) = 0;
+  *(y + 2) = 0;
+  *y = x;
+}
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/from-sll.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/from-sll.syn
new file mode 100644
index 000000000..7e017cfc2
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/from-sll.syn
@@ -0,0 +1,41 @@
+# -c 2
+
+should be able to convert a singly-linked list to a double-linked list
+
+#######
+
+{ f :-> x ** sll(x, s)}
+void sll_to_dll(loc f)
+{ f :-> i ** dll(i, 0, s)}
+
+#######
+
+void sll_to_dll (loc f) {
+  let x = *f;
+  if (x == 0) {
+    *f = 0;
+  } else {
+    let v = *x;
+    let n = *(x + 1);
+    *f = n;
+    sll_to_dll(f);
+    let i1 = *f;
+    if (i1 == 0) {
+      let i = malloc(3);
+      free(x);
+      *f = i;
+      *(i + 1) = 0;
+      *i = v;
+      *(i + 2) = 0;
+    } else {
+      let i = malloc(3);
+      free(x);
+      *(i1 + 2) = i;
+      *f = i;
+      *(i + 1) = i1;
+      *i = v;
+      *(i + 2) = 0;
+    }
+  }
+}
+

From 0aa3133b992b50fdebd921f3dc02fdc8a95b180e Mon Sep 17 00:00:00 2001
From: aidandenlinger <47428697+aidandenlinger@users.noreply.github.com>
Date: Mon, 21 Feb 2022 17:52:50 -0800
Subject: [PATCH 03/10] Port paper-benchmarks/sll tests to sequences (#1)

* ported common.def to use sequences, sll-singleton works

* ported dupleton, added README to clarify where these tests come from

* sll-free works without modification

* updated README

* sll-copy works

* sll-append works

* update README and tests that are currently failing
---
 .../sll/FAILS_sll-delete-all.syn              | 30 +++++++++++++++++++
 .../paper-benchmarks/sll/FAILS_sll-init.syn   | 19 ++++++++++++
 .../sequences/paper-benchmarks/sll/README.md  | 18 +++++++++++
 .../sequences/paper-benchmarks/sll/common.def |  4 +++
 .../paper-benchmarks/sll/sll-append.syn       | 20 +++++++++++++
 .../paper-benchmarks/sll/sll-copy.syn         | 25 ++++++++++++++++
 .../paper-benchmarks/sll/sll-dupleton.syn     | 20 +++++++++++++
 .../paper-benchmarks/sll/sll-free.syn         | 17 +++++++++++
 .../paper-benchmarks/sll/sll-singleton.syn    | 18 +++++++++++
 9 files changed, 171 insertions(+)
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-delete-all.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-init.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/README.md
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-append.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-copy.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-dupleton.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-free.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-singleton.syn

diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-delete-all.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-delete-all.syn
new file mode 100644
index 000000000..332ecb9a1
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-delete-all.syn
@@ -0,0 +1,30 @@
+# -b true
+singly-linked list: delete all occurrences of x
+
+#####
+
+{true ; sll(x, s) ** ret :-> a}
+void sll_delete_all (loc x, loc ret)
+{s1 == s -- {a} ; sll(y, s1) ** ret :-> y }
+
+#####
+
+void sll_delete_all (loc x, loc ret) {
+  let a2 = *ret;
+  if (x == 0) {
+    *ret = 0;
+  } else {
+    let v2 = *x;
+    if (true && v2 <= a2 && a2 <= v2) {
+      let nxt2 = *(x + 1);
+      sll_delete_all(nxt2, ret);
+      free(x);
+    } else {
+      let nxt2 = *(x + 1);
+      sll_delete_all(nxt2, ret);
+      let y12 = *ret;
+      *(x + 1) = y12;
+      *ret = x;
+    }
+  }
+}
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-init.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-init.syn
new file mode 100644
index 000000000..d37eb6a4c
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-init.syn
@@ -0,0 +1,19 @@
+should be able to initialize a linked list (implemented with sequences)
+
+NEED TO RESOLVE HOW/IF THE SUBSET INTERVAL SHOULD BE DEFINED ON SEQUENCES
+###
+
+{ sll(x, s) }
+  void sll_init(loc x, int v)
+{ s1 <= <v> ; sll(x, s1) }
+
+###
+
+void sll_init (loc x, int v) {
+  if (x == 0) {
+  } else {
+    let n = *(x + 1);
+    sll_init(n, v);
+    *x = v;
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/README.md b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/README.md
new file mode 100644
index 000000000..e88f48f75
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/README.md
@@ -0,0 +1,18 @@
+# Paper-Benchmarks/SLL
+Port of singly-linked list tests from
+`src/test/resources/synthesis/paper-benchmarks/sll` to use sequences instead
+
+## Works
+| Name         | Any Notes                                              |
+|--------------|--------------------------------------------------------|
+|ssl-singleton |                                                        |
+|ssl-dupleton  |                                                        |
+|ssl-free      |                                                        |
+|ssl-copy      |                                                        |
+|ssl-append    |                                                        |
+
+## Doesn't work
+| Name         | Reason                                      |
+|--------------|---------------------------------------------|
+| ssl-init     | Haven't defined `<=` (subset) for sequences (OpSubinterval) |
+| ssl-delete-all | Haven't defined `--` (difference) on sequences (OpDiff) |
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
new file mode 100644
index 000000000..a7ef6df07
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
@@ -0,0 +1,4 @@
+predicate sll(loc x, seq s) {
+|  x == 0        => { s == <> ; emp }
+|  not (x == 0)  => { s == <v> ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-append.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-append.syn
new file mode 100644
index 000000000..7ffb1386f
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-append.syn
@@ -0,0 +1,20 @@
+singly-linked list: append
+
+#####
+
+{true ; sll(x1, s1) ** sll(x2, s2) ** ret :-> x2}
+void sll_append (loc x1, loc ret)
+{s == s1 ++ s2 ; sll(y, s) ** ret :-> y }
+
+#####
+
+void sll_append (loc x1, loc ret) {
+  if (x1 == 0) {
+  } else {
+    let n = *(x1 + 1);
+    sll_append(n, ret);
+    let y = *ret;
+    *ret = x1;
+    *(x1 + 1) = y;
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-copy.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-copy.syn
new file mode 100644
index 000000000..671969e85
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-copy.syn
@@ -0,0 +1,25 @@
+should be able to synthesize list copy (implemented with sequences)
+
+#####
+
+{true ; r :-> x ** sll(x, s)<a>}
+void sll_copy(loc r)
+{true ; r :-> y ** sll(x, s)<a> ** sll(y, s)<b> }
+
+#####
+
+void sll_copy (loc r) {
+  let x = *r;
+  if (x == 0) {
+  } else {
+    let v = *x;
+    let n = *(x + 1);
+    *r = n;
+    sll_copy(r);
+    let y1 = *r;
+    let y = malloc(2);
+    *r = y;
+    *(y + 1) = y1;
+    *y = v;
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-dupleton.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-dupleton.syn
new file mode 100644
index 000000000..54b318338
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-dupleton.syn
@@ -0,0 +1,20 @@
+# -c 3
+singly-linked list (as sequence): construct a list with two elements
+
+#####
+
+{ true ; ret :-> a }
+void sll_dupleton (int x, int y, loc ret)
+{ elems == <x, y> ; ret :-> z ** sll(z, elems) }
+
+#####
+
+void sll_dupleton (int x, int y, loc ret) {
+  let z = malloc(2);
+  let n = malloc(2);
+  *ret = z;
+  *(z + 1) = n;
+  *(n + 1) = 0;
+  *n = y;
+  *z = x;
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-free.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-free.syn
new file mode 100644
index 000000000..60d095fe9
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-free.syn
@@ -0,0 +1,17 @@
+should be able to deallocate a linked list (implemented with sequences)
+###
+
+{ true; sll(x, s) }
+  void sll_free(loc x)
+{ true ; emp }
+
+###
+
+void sll_free (loc x) {
+  if (x == 0) {
+  } else {
+    let n = *(x + 1);
+    sll_free(n);
+    free(x);
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-singleton.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-singleton.syn
new file mode 100644
index 000000000..f0bd65831
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-singleton.syn
@@ -0,0 +1,18 @@
+#. -c 2
+singly-linked list (as sequence): construct a list with one element
+changed specification to use a sequence, same outputted code
+
+#####
+
+{ true ; ret :-> a }
+void sll_singleton (int x, loc ret)
+{ elems == <x> ; ret :-> y ** sll(y, elems) }
+
+#####
+
+void sll_singleton (int x, loc ret) {
+  let y = malloc(2);
+  *ret = y;
+  *(y + 1) = 0;
+  *y = x;
+}
\ No newline at end of file

From ba9090b0cc7f0436de28e7647b9870dc27c7ccb2 Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Sat, 12 Mar 2022 15:06:09 -0800
Subject: [PATCH 04/10] Adding additional sequence operations

* Binary sequence remove (--) operations that removes the
  first occurance of a particular item.
* Unary length (slen) operation to get the length of a sequence.
* Binary indexing (@) operation to get a one element sequence at a
  particular index.
* Binary indexOf (!!) operation to find the index of the first occurence
  of an item from a seqquence.
---
 .../tygus/suslik/language/Expressions.scala   | 29 +++++++++
 .../tygus/suslik/logic/smt/SMTSolving.scala   | 65 ++++++++++++++++---
 .../org/tygus/suslik/parsing/SSLLexical.scala |  4 +-
 .../org/tygus/suslik/parsing/SSLParser.scala  |  4 +-
 4 files changed, 90 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/org/tygus/suslik/language/Expressions.scala b/src/main/scala/org/tygus/suslik/language/Expressions.scala
index 377d6fd04..dff0a28db 100644
--- a/src/main/scala/org/tygus/suslik/language/Expressions.scala
+++ b/src/main/scala/org/tygus/suslik/language/Expressions.scala
@@ -145,6 +145,7 @@ object Expressions {
     override def opFromTypes: Map[(SSLType, SSLType), BinOp] = Map(
       (IntType, IntType) -> OpMinus,
       (IntSetType, IntSetType) -> OpDiff,
+      (IntSequenceType, IntType) -> OpSequenceRemove,
     )
 
     override def default: BinOp = OpMinus
@@ -320,6 +321,20 @@ object Expressions {
     def rType: SSLType = IntSequenceType
     def resType: SSLType = IntSequenceType
   }
+  object OpSequenceRemove extends BinOp {
+    def level: Int = 4
+    override def pp: String = "--"
+    def lType: SSLType = IntSequenceType
+    def rType: SSLType = IntType
+    def resType: SSLType = IntSequenceType
+  }
+  object OpSequenceAt extends BinOp {
+    def level: Int = 4
+    override def pp: String = "@"
+    def lType: SSLType = IntSequenceType
+    def rType: SSLType = IntType
+    def resType: SSLType = IntSequenceType
+  }
   object OpSequenceHead extends UnOp {
     override def pp: String = "head"
     override def inputType: SSLType = IntSequenceType
@@ -331,6 +346,20 @@ object Expressions {
     override def outputType: SSLType = IntSequenceType
   }
 
+  object OpSequenceLen extends UnOp {
+    override def pp: String = "len"
+    override def inputType: SSLType = IntSequenceType
+    override def outputType: SSLType = IntType
+  }
+
+  object OpSequenceIndexof extends BinOp {
+    def level: Int = 4
+    override def pp: String = "!!"
+    def lType: SSLType = IntSequenceType
+    def rType: SSLType = IntType
+    def resType: SSLType = IntType
+  }
+
   sealed abstract class Expr extends PrettyPrinting with HasExpressions[Expr] with Ordered[Expr] {
 
     def compare(that: Expr): Int = this.pp.compare(that.pp)
diff --git a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
index 1d4d4018b..0ac65d943 100644
--- a/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
+++ b/src/main/scala/org/tygus/suslik/logic/smt/SMTSolving.scala
@@ -117,6 +117,14 @@ object SMTSolving extends Core
 
   def sequenceAppendSymbol = SimpleQId(SymbolId(SSymbol("sappend")))
 
+  def sequenceRemoveSymbol = SimpleQId(SymbolId(SSymbol("sremove")))
+
+  def sequenceIndexofSymbol = SimpleQId(SymbolId(SSymbol("sindexof")))
+
+  def sequenceLenSymbol = SimpleQId(SymbolId(SSymbol("slen")))
+
+  def sequenceAtSymbol = SimpleQId(SymbolId(SSymbol("seat")))
+
   def emptySequenceTerm: Term = QIdTerm(emptySequenceSymbol)
 
   /*def sequencePrelude: List[String] = List(
@@ -130,7 +138,11 @@ object SMTSolving extends Core
     "(define-sort SequenceInt () (Seq Int))",
     "(define-fun sempty () SequenceInt (as seq.empty SequenceInt))",
     "(define-fun scons ((x Int) (xs SequenceInt)) SequenceInt (seq.++ (seq.unit x) xs))",
-    "(define-fun sappend ((xs SequenceInt) (ys SequenceInt)) SequenceInt (seq.++ xs ys))"
+    "(define-fun sappend ((xs SequenceInt) (ys SequenceInt)) SequenceInt (seq.++ xs ys))",
+    "(define-fun sremove ((xs SequenceInt) (y Int)) SequenceInt (seq.replace xs (seq.unit y) sempty))",
+    "(define-fun sindexof ((xs SequenceInt) (y Int)) Int (seq.indexof xs (seq.unit y)))",
+    "(define-fun slen ((xs SequenceInt)) Int (seq.len xs))",
+    "(define-fun seat ((xs SequenceInt) (y Int)) SequenceInt (seq.at xs y))"
   )
 
   // Commands to be executed before solving starts
@@ -169,7 +181,6 @@ object SMTSolving extends Core
     this.synchronized {
       timed {
         push(1)
-        //System.out.println("HERE !! " + term);
         val res = isSat(term)
         pop(1)
         res != Success(UnSat()) // Unknown counts as SAT
@@ -286,6 +297,25 @@ object SMTSolving extends Core
       new TypedTerm[SequenceTerm, Term](l.typeDefs ++ r.typeDefs,
         QIdAndTermsTerm(sequenceAppendSymbol, List(l.termDef, r.termDef)))      
     }
+
+    case BinaryExpr(OpSequenceRemove, left, right) => {
+      var l = convertSequenceExpr(left)
+      var r = convertIntExpr(right)
+
+      new TypedTerm[SequenceTerm, Term](l.typeDefs ++ r.typeDefs,
+        QIdAndTermsTerm(sequenceRemoveSymbol, List(l.termDef, r.termDef)))
+    }
+    case BinaryExpr(OpSequenceAt, left, right) => {
+          val l = convertSequenceExpr(left)
+          var r = convertIntExpr(right)
+          new TypedTerm[SequenceTerm, Term](l.typeDefs ++ r.typeDefs, QIdAndTermsTerm(sequenceAtSymbol, List(l.termDef, r.termDef)))
+    }
+    case IfThenElse(cond, left, right) => {
+      val c = convertBoolExpr(cond)
+      val l = convertSequenceExpr(left)
+      val r = convertSequenceExpr(right)
+      c.ite(l, r)
+    }
     case _ => throw SMTUnsupportedExpr(e)
   }
 
@@ -404,13 +434,32 @@ object SMTSolving extends Core
       val s = convertIntervalExpr(e)
       new TypedTerm[IntTerm, Term](s.typeDefs, QIdAndTermsTerm(intervalUpperSymbol, List(s.termDef)))
     }
+    case UnaryExpr(OpSequenceLen, e) => {
+      val s = convertSequenceExpr(e)
+      new TypedTerm[IntTerm, Term](s.typeDefs, QIdAndTermsTerm(sequenceLenSymbol, List(s.termDef)))
+    }
     case BinaryExpr(op, left, right) => {
-      val l = convertIntExpr(left)
-      val r = convertIntExpr(right)
       op match {
-        case OpPlus => l + r
-        case OpMinus => l - r
-        case OpMultiply => l * r
+        case OpPlus => {
+          val l = convertIntExpr(left)
+          val r = convertIntExpr(right)
+          l + r
+        }
+        case OpMinus => {
+          val l = convertIntExpr(left)
+          val r = convertIntExpr(right)
+          l - r
+        }
+        case OpMultiply => {
+          val l = convertIntExpr(left)
+          val r = convertIntExpr(right)
+          l * r
+        }
+        case OpSequenceIndexof => {
+          val l = convertSequenceExpr(left)
+          val r = convertIntExpr(right)
+          new TypedTerm[IntTerm, Term](l.typeDefs ++ r.typeDefs, QIdAndTermsTerm(sequenceIndexofSymbol, List(l.termDef, r.termDef)))
+        }
         case _ => throw SMTUnsupportedExpr(e)
       }
     }
@@ -439,13 +488,11 @@ object SMTSolving extends Core
 
   // Check if phi is satisfiable; all vars are implicitly existentially quantified
   def sat(phi: Expr): Boolean = {
-    //System.out.println("EXPR:  " + phi.pp);
     cache.getOrElseUpdate(phi, checkSat(convertBoolExpr(phi)))
   }
 
   // Check if phi is valid; all vars are implicitly universally quantified
   def valid(phi: Expr): Boolean = {
-    //System.out.println("EXPR:  " + phi.not.pp)
     !sat(phi.not)
   }
 
diff --git a/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala b/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
index 4a879c9ba..3bbd4169f 100644
--- a/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
+++ b/src/main/scala/org/tygus/suslik/parsing/SSLLexical.scala
@@ -8,7 +8,7 @@ import scala.util.parsing.combinator.lexical.StdLexical
 class SSLLexical extends StdLexical {
 
   // Add keywords
-  reserved += ("if", "then", "else", "true", "false", "emp", "not", "return", "predicate", "in", "lower", "upper", "head", "tail")
+  reserved += ("if", "then", "else", "true", "false", "emp", "not", "return", "predicate", "in", "lower", "upper", "head", "tail", "slen")
   reserved += ("error","magic","malloc", "free", "let", "assume")
   reserved += ("null")
 
@@ -17,7 +17,7 @@ class SSLLexical extends StdLexical {
 
   delimiters += ("(", ")", "=", ";", "**", "*", ":->", "=i", "<=i", "++", "--", "..",
       "{", "}", "/\\", "&&", "\\/", "||", "\n", "\r", "=>", "?", ":", "::",
-      "<", ">", ",", "/",   "+", "-", "==", "!=", "==>", "<=", ">=", "[", "]", "|", "??"
+      "<", ">", ",", "/",   "+", "-", "==", "!=", "==>", "<=", ">=", "[", "]", "|", "!!", "@"
   )
 
 }
diff --git a/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala b/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
index f386e3488..21844b669 100644
--- a/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
+++ b/src/main/scala/org/tygus/suslik/parsing/SSLParser.scala
@@ -70,7 +70,7 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
   def varParser: Parser[Var] = ident ^^ Var
 
   def unOpParser: Parser[UnOp] =
-    ("not" ^^^ OpNot ||| "-" ^^^ OpUnaryMinus ||| "lower" ^^^ OpLower ||| "upper" ^^^ OpUpper ||| "head" ^^^ OpSequenceHead ||| "tail" ^^^ OpSequenceTail)
+    ("not" ^^^ OpNot ||| "-" ^^^ OpUnaryMinus ||| "lower" ^^^ OpLower ||| "upper" ^^^ OpUpper ||| "slen" ^^^ OpSequenceLen)
 
   // TODO: remove legacy ++, --, =i, /\, \/, <=i
   def termOpParser: Parser[OverloadedBinOp] = "*" ^^^ OpOverloadedStar
@@ -80,6 +80,8 @@ class SSLParser extends StandardTokenParsers with SepLogicUtils {
     ("++" ||| "+") ^^^ OpOverloadedPlus
       ||| ("--" ||| "-") ^^^ OpOverloadedMinus
       ||| "::" ^^^ OpSequenceCons
+      ||| "!!" ^^^ OpSequenceIndexof
+      ||| "@" ^^^ OpSequenceAt
     )
 
   def relOpParser: Parser[OverloadedBinOp] = (

From 0624123a91549cfb8183296e657aa86367b59d69 Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Sat, 12 Mar 2022 15:49:35 -0800
Subject: [PATCH 05/10] Adding singly-linked-list push/pop operations

---
 .../sequences/paper-benchmarks/sll/common.def          |  9 +++++++--
 .../sequences/paper-benchmarks/sll/sll-pop-back.syn    | 10 ++++++++++
 .../sequences/paper-benchmarks/sll/sll-pop-front.syn   |  9 +++++++++
 .../sequences/paper-benchmarks/sll/sll-push-back.syn   | 10 ++++++++++
 .../sequences/paper-benchmarks/sll/sll-push-front.syn  |  9 +++++++++
 5 files changed, 45 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-front.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-back.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-front.syn

diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
index a7ef6df07..f16e22390 100644
--- a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/common.def
@@ -1,4 +1,9 @@
 predicate sll(loc x, seq s) {
-|  x == 0        => { s == <> ; emp }
-|  not (x == 0)  => { s == <v> ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
+|  x == 0        => { s == <>; emp }
+|  not (x == 0)  => { s == <v> ++ s1; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
+}
+
+predicate sll_len(loc x, seq s, int len) {
+| x == 0 => {len == 0 /\ s == <>; emp}
+| not (x == 0) => { s == <v> ++ s1 /\ len == (1 + len1) /\ (len1 >= 0); [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll_len(nxt, s1, len1) }
 }
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn
new file mode 100644
index 000000000..a738bc644
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn
@@ -0,0 +1,10 @@
+#. -c 2 -o 2 -b true
+singly-linked list: pop back
+
+#####
+
+{true; res :-> 0 ** list :-> x1 ** sll(x1, s1)}
+void sll_pop_back (loc list, loc res, int def)
+{(s1 == <> /\ result == def) \/ (s1 == s ++ <item> /\ result == item); sll(y, s) ** list :-> y ** res :-> item }
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-front.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-front.syn
new file mode 100644
index 000000000..4a04ea7b8
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-front.syn
@@ -0,0 +1,9 @@
+singly-linked list: pop front
+
+#####
+
+{true; res :-> 0 ** list :-> x1 ** sll(x1, s1)}
+void sll_pop_front (loc list, loc res, int def)
+{ (s1 == <> /\ result == def) \/ (s1 == <item> ++ s /\ result == item); sll(y, s) ** list :-> y ** res :-> result }
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-back.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-back.syn
new file mode 100644
index 000000000..29876ebd5
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-back.syn
@@ -0,0 +1,10 @@
+#. -c 2
+singly-linked list: push back
+
+#####
+
+{true ; ret :-> x1 ** sll(x1, s1)}
+void sll_push_back (loc ret, int item)
+{(s == s1 ++ <item>) ; sll(y, s) ** ret :-> y }
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-front.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-front.syn
new file mode 100644
index 000000000..ab27c93eb
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-push-front.syn
@@ -0,0 +1,9 @@
+singly-linked list: push front
+
+#####
+
+{true ; ret :-> x1 ** sll(x1, s1)}
+void sll_push_front (loc ret, int item)
+{s == <item> ++ s1 ; sll(y, s) ** ret :-> y }
+
+#####
\ No newline at end of file

From 790edc7f53e7612503544190d0c979799859beb3 Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Sat, 12 Mar 2022 15:53:28 -0800
Subject: [PATCH 06/10] Augment SSL rules to work with Sequence operations

* Branch Abduction - use the Integer Constant 0 as a candidate for
  branch conditions.
* Write - prevent writing sequence literals into program variables.
  Currently only Ghost Variables are filtered but not literals.
* SubstExist - prevent substituting variables assigned to expressions
  with sequence operations from being substituted in the post-condition.
  We prefer that these variables are given values using Unification or
  the Pick Exist rule.
* PickExist - consider the Integer Constant -1 and also the expressions
  <var> + 1 and <var> - 1 as candidates when instantiating existentials
  as these are common constants for "inductive" properties.
---
 .../suslik/synthesis/rules/BranchRules.scala  |  7 ++---
 .../suslik/synthesis/rules/FailRules.scala    |  3 +-
 .../synthesis/rules/OperationalRules.scala    | 13 +++++++-
 .../synthesis/rules/UnificationRules.scala    | 31 +++++++++++++++++--
 4 files changed, 45 insertions(+), 9 deletions(-)

diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala
index fba612cff..ee439cddd 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala
@@ -1,6 +1,6 @@
 package org.tygus.suslik.synthesis.rules
 
-import org.tygus.suslik.language.Expressions.{Expr, Unknown, Var}
+import org.tygus.suslik.language.Expressions.{Expr, Unknown, Var, IntConst}
 import org.tygus.suslik.language.Statements.Guarded
 import org.tygus.suslik.language.{Expressions, IntType}
 import org.tygus.suslik.logic.Specifications._
@@ -78,10 +78,9 @@ object BranchRules extends PureLogicUtils with SepLogicUtils with RuleUtils {
 
     def atomCandidates(goal: Goal): Seq[Expr] =
       for {
-        lhs <- goal.programVars.filter(goal.post.phi.vars.contains)
-        rhs <- goal.programVars.filter(goal.post.phi.vars.contains)
+        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))
         if lhs != rhs
-        if goal.getType(lhs) == IntType && goal.getType(rhs) == IntType
       } yield lhs |<=| rhs
 
     def condCandidates(goal: Goal): Seq[Expr] = {
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala
index 84d52366e..758791d7d 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala
@@ -51,9 +51,10 @@ 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)
     }
   }
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala
index 833b433ca..d4611131a 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala
@@ -40,8 +40,19 @@ object OperationalRules extends SepLogicUtils with RuleUtils {
         case _ => false
       }
 
+      def isForbiddenExpr: Expr => Boolean = {
+        case SequenceLiteral(_) => true
+        case _ => false
+      }
+
+      def noForbiddenExprs: Heaplet => Boolean = {
+        case PointsTo(x@Var(_), _, e) => e.collect(isForbiddenExpr).isEmpty
+        case _ => false
+      }
+
+
       // When do two heaplets match
-      def isMatch(hl: Heaplet, hr: Heaplet) = sameLhs(hl)(hr) && !sameRhs(hl)(hr) && noGhosts(hr)
+      def isMatch(hl: Heaplet, hr: Heaplet) = sameLhs(hl)(hr) && !sameRhs(hl)(hr) && noGhosts(hr) && noForbiddenExprs(hr)
 
       findMatchingHeaplets(_ => true, isMatch, goal.pre.sigma, goal.post.sigma) match {
         case None => Nil
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
index 89bbc4fb1..be004c4d8 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
+++ b/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
@@ -1,6 +1,8 @@
 package org.tygus.suslik.synthesis.rules
 
 import org.tygus.suslik.language.CardType
+import org.tygus.suslik.language.SSLType
+import org.tygus.suslik.language.IntType
 import org.tygus.suslik.language.Expressions._
 import org.tygus.suslik.logic.Specifications._
 import org.tygus.suslik.logic._
@@ -113,6 +115,7 @@ 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] = {
@@ -125,10 +128,23 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
           // e must be an existential var:
           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))
+          (!goal.isProgramLevelExistential(x) || d.vars.subsetOf(goal.programVars.toSet)) &&
+          // no forbidden expressions
+          noForbiddenExprs(d)
         case _ => false
       }
 
+      def isForbiddenExpr(e: Expr): Boolean = e match {
+        case UnaryExpr(OpSequenceLen, _) => true
+        case BinaryExpr(OpSequenceAt, _, _) => true
+        case BinaryExpr(OpSequenceIndexof, _, _) => true
+        case _ => false
+      }
+
+      def noForbiddenExprs(d: Expr): Boolean = {
+        d.collect(isForbiddenExpr).isEmpty
+      }
+
       def extractSides(l: Expr, r: Expr): Option[(Var, Expr)] =
         if (l.vars.intersect(r.vars).isEmpty) {
           if (canSubst(l, r)) Some(l.asInstanceOf[Var], r)
@@ -168,7 +184,7 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
     override def toString: String = "PickExist"
 
     def apply(goal: Goal): Seq[RuleResult] = {
-      val constants = List(IntConst(0), SetLiteral(List()), SequenceLiteral(List()), eTrue, eFalse)
+      val constants = List(IntConst(0), IntConst(-1), 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)
@@ -179,9 +195,18 @@ object UnificationRules extends PureLogicUtils with SepLogicUtils with RuleUtils
 //        goal.allUniversals.intersect(goal.pre.vars ++ goal.post.vars)
       }
 
+      def inductiveCandidates(ex: Expr, ty: SSLType): List[Expr] = {
+        ty match {
+          case IntType => List(BinaryExpr(OpPlus, ex, IntConst(1)), BinaryExpr(OpMinus, ex, IntConst(1)))
+          case _ => List()
+        }
+      }
+
       for {
         ex <- least(exCandidates) // since all existentials must go, no point trying them in different order
-        v <- toSorted(uniCandidates(ex)) ++ constants
+        val uni = toSorted(uniCandidates(ex))
+        v <- uni ++ constants ++ uni.flatMap(x => inductiveCandidates(x, x.getType(goal.gamma).get))
+
         if goal.getType(ex) == v.getType(goal.gamma).get
         sigma = Map(ex -> v)
         newPost = goal.post.subst(sigma)

From 598b31150c967918dad4b8dfad2ffea9cfc24aa7 Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Sat, 12 Mar 2022 18:55:18 -0800
Subject: [PATCH 07/10] Benchmarks using new Sequence Operations

* src/test/resources/synthesis/sequences/llist/llist_ith.syn - returns a
  pointer to the ith node in a linked list known to have at least i nodes
* src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn
  - returns the length of an arbitrary linked list
* src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn -
  the value at the ith node in a linked list known to have sufficient
  nodes
---
 .../resources/synthesis/sequences/llist/llist_ith.syn  | 10 ++++++++++
 .../sequences/paper-benchmarks/sll/sll-ith.syn         |  9 +++++++++
 .../sequences/paper-benchmarks/sll/sll-length.syn      |  9 +++++++++
 3 files changed, 28 insertions(+)
 create mode 100644 src/test/resources/synthesis/sequences/llist/llist_ith.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn
 create mode 100644 src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn

diff --git a/src/test/resources/synthesis/sequences/llist/llist_ith.syn b/src/test/resources/synthesis/sequences/llist/llist_ith.syn
new file mode 100644
index 000000000..e3f0e23a9
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/llist/llist_ith.syn
@@ -0,0 +1,10 @@
+# -c 2 -o 2 -b true
+
+#####
+
+{i >= 0 /\ i < slen s; r :-> x ** lseg(x, 0, s)}
+void llist_ith(loc r, int i)
+{s == s1 ++ s2 /\ slen s1 == i; r :-> y ** lseg(x, y, s1) ** lseg(y, 0, s2) }
+
+#####
+
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn
new file mode 100644
index 000000000..31dcfba45
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn
@@ -0,0 +1,9 @@
+# -c 1 -o 1 -b true
+
+#####
+
+{i >= 0 /\ i < slen s; sll(x, s) ** ret :-> i}
+void sll_ith(loc x, loc ret)
+{<item> == s@i; sll(x, s) ** ret :-> item}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn
new file mode 100644
index 000000000..5ad79d4b7
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn
@@ -0,0 +1,9 @@
+# -c 1 -o 1
+
+#####
+
+{true; sll(x, s) ** res :-> a}
+void sll_length(loc x, loc res)
+{len == slen s; sll(x, s) ** res :-> len}
+
+#####
\ No newline at end of file

From d85e649da9197b16199fef39c5554fb9305f601a Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Mon, 14 Mar 2022 17:42:24 -0700
Subject: [PATCH 08/10] Added a folder with project benchmarks

---
 .../scala/org/tygus/suslik/language/Expressions.scala  |  8 ++++++--
 .../sequences/project-benchmarks/llist_ith.syn         | 10 ++++++++++
 .../sequences/project-benchmarks/predicates.def        |  9 +++++++++
 .../synthesis/sequences/project-benchmarks/sll-ith.syn |  9 +++++++++
 .../sequences/project-benchmarks/sll-length.syn        |  9 +++++++++
 .../sequences/project-benchmarks/sll-pop-front.syn     |  9 +++++++++
 .../sequences/project-benchmarks/sll-push-back.syn     | 10 ++++++++++
 7 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/predicates.def
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/sll-pop-front.syn
 create mode 100644 src/test/resources/synthesis/sequences/project-benchmarks/sll-push-back.syn

diff --git a/src/main/scala/org/tygus/suslik/language/Expressions.scala b/src/main/scala/org/tygus/suslik/language/Expressions.scala
index dff0a28db..642f98387 100644
--- a/src/main/scala/org/tygus/suslik/language/Expressions.scala
+++ b/src/main/scala/org/tygus/suslik/language/Expressions.scala
@@ -664,7 +664,11 @@ object Expressions {
     def subst(sigma: Subst): Expr = UnaryExpr(op, arg.subst(sigma))
     override def substUnknown(sigma: UnknownSubst): Expr = UnaryExpr(op, arg.substUnknown(sigma))
     override def level = 5
-    override def pp: String = s"${op.pp} ${arg.printInContext(this)}"
+    override def pp: String = op match {
+      case OpSequenceLen => s"|${arg.printInContext(this)}|"
+      case _ => s"${op.pp} ${arg.printInContext(this)}"
+    }
+      
     def getType(gamma: Gamma): Option[SSLType] = Some(op.outputType)
   }
 
@@ -683,7 +687,7 @@ object Expressions {
   }
 
   case class SequenceLiteral(elems: List[Expr]) extends Expr {
-    override def pp: String = s"<${elems.map(_.pp).mkString(",")}>"
+    override def pp: String = s"<<${elems.map(_.pp).mkString(",")}>>"
     override def subst(sigma: Subst): SequenceLiteral = SequenceLiteral(elems.map(_.subst(sigma)))
     def getType(gamma: Gamma): Option[SSLType] = Some(IntSequenceType)
   }
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn b/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn
new file mode 100644
index 000000000..e3f0e23a9
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn
@@ -0,0 +1,10 @@
+# -c 2 -o 2 -b true
+
+#####
+
+{i >= 0 /\ i < slen s; r :-> x ** lseg(x, 0, s)}
+void llist_ith(loc r, int i)
+{s == s1 ++ s2 /\ slen s1 == i; r :-> y ** lseg(x, y, s1) ** lseg(y, 0, s2) }
+
+#####
+
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/predicates.def b/src/test/resources/synthesis/sequences/project-benchmarks/predicates.def
new file mode 100644
index 000000000..f177ed98b
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/predicates.def
@@ -0,0 +1,9 @@
+predicate sll(loc x, seq s) {
+|  x == 0        => { s == <>; emp }
+|  not (x == 0)  => { s == <v> ++ s1; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** sll(nxt, s1) }
+}
+
+predicate lseg(loc x, loc y, seq s) {
+|  x == y        => { s == <> ; emp }
+|  not (x == y)  => { s == <v> ++ s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
+}
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn
new file mode 100644
index 000000000..31dcfba45
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn
@@ -0,0 +1,9 @@
+# -c 1 -o 1 -b true
+
+#####
+
+{i >= 0 /\ i < slen s; sll(x, s) ** ret :-> i}
+void sll_ith(loc x, loc ret)
+{<item> == s@i; sll(x, s) ** ret :-> item}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
new file mode 100644
index 000000000..5ad79d4b7
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
@@ -0,0 +1,9 @@
+# -c 1 -o 1
+
+#####
+
+{true; sll(x, s) ** res :-> a}
+void sll_length(loc x, loc res)
+{len == slen s; sll(x, s) ** res :-> len}
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-pop-front.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-pop-front.syn
new file mode 100644
index 000000000..4a04ea7b8
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/sll-pop-front.syn
@@ -0,0 +1,9 @@
+singly-linked list: pop front
+
+#####
+
+{true; res :-> 0 ** list :-> x1 ** sll(x1, s1)}
+void sll_pop_front (loc list, loc res, int def)
+{ (s1 == <> /\ result == def) \/ (s1 == <item> ++ s /\ result == item); sll(y, s) ** list :-> y ** res :-> result }
+
+#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-push-back.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-push-back.syn
new file mode 100644
index 000000000..29876ebd5
--- /dev/null
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/sll-push-back.syn
@@ -0,0 +1,10 @@
+#. -c 2
+singly-linked list: push back
+
+#####
+
+{true ; ret :-> x1 ** sll(x1, s1)}
+void sll_push_back (loc ret, int item)
+{(s == s1 ++ <item>) ; sll(y, s) ** ret :-> y }
+
+#####
\ No newline at end of file

From 85bf08043f1293f44bc3b58c677646f8b4f934aa Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Fri, 22 Apr 2022 00:45:07 -0700
Subject: [PATCH 09/10] Marking/removing some failing test cases

---
 .../synthesis/sequences/llist/llist_insert_head.syn      | 4 ++--
 .../synthesis/sequences/llist/llist_insert_tail.syn      | 9 ---------
 src/test/resources/synthesis/sequences/llist/lseg.def    | 4 ++--
 .../dll/{dll-delete-all.syn => FAIL_dll-delete-all.syn}  | 2 +-
 .../sll/{sll-pop-back.syn => FAILS_sll-pop-back.syn}     | 0
 src/test/resources/synthesis/sequences/pure/unify3.syn   | 6 +++---
 6 files changed, 8 insertions(+), 17 deletions(-)
 delete mode 100644 src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
 rename src/test/resources/synthesis/sequences/paper-benchmarks/dll/{dll-delete-all.syn => FAIL_dll-delete-all.syn} (93%)
 rename src/test/resources/synthesis/sequences/paper-benchmarks/sll/{sll-pop-back.syn => FAILS_sll-pop-back.syn} (100%)

diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
index 27e641409..eae537bf6 100644
--- a/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
+++ b/src/test/resources/synthesis/sequences/llist/llist_insert_head.syn
@@ -4,6 +4,6 @@ should insert an item at the beginning of a list
 
 {true; r :-> x ** lseg(x, 0, S)}
 void llist_insert_head(loc r, int item)
-{S1 == item:S; r:-> z ** lseg(z, 0, S1)}
+{S1 == item::S; r:-> z ** lseg(z, 0, S1)}
 
-#####
\ No newline at end of file
+#####
diff --git a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn b/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
deleted file mode 100644
index 201e5efbb..000000000
--- a/src/test/resources/synthesis/sequences/llist/llist_insert_tail.syn
+++ /dev/null
@@ -1,9 +0,0 @@
-should insert an item at the beginning of a list
-
-#####
-
-{true; r :-> x ** lseg(x, 0, S)}
-void llist_insert_tail(loc r, int item)
-{S1 == <item>; r:-> z ** lseg(z, y, S) ** lseg(y, 0, S1)}
-
-#####
\ No newline at end of file
diff --git a/src/test/resources/synthesis/sequences/llist/lseg.def b/src/test/resources/synthesis/sequences/llist/lseg.def
index 24ebdd087..858723c8d 100644
--- a/src/test/resources/synthesis/sequences/llist/lseg.def
+++ b/src/test/resources/synthesis/sequences/llist/lseg.def
@@ -1,4 +1,4 @@
 predicate lseg(loc x, loc y, seq s) {
 |  x == y        => { s == <> ; emp }
-|  not (x == y)  => { s == v:s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
-}
\ No newline at end of file
+|  not (x == y)  => { s == v::s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }
+}
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/FAIL_dll-delete-all.syn
similarity index 93%
rename from src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
rename to src/test/resources/synthesis/sequences/paper-benchmarks/dll/FAIL_dll-delete-all.syn
index cc83611fa..e578ffdf4 100644
--- a/src/test/resources/synthesis/sequences/paper-benchmarks/dll/dll-delete-all.syn
+++ b/src/test/resources/synthesis/sequences/paper-benchmarks/dll/FAIL_dll-delete-all.syn
@@ -5,7 +5,7 @@ doubly-linked list: delete all occurrences of x
 
 {true ; dll(x, b, s) ** ret :-> a}
 void dll_delete_all (loc x, loc ret)
-{s1 =i s -- {a} ; dll(y, c, s1) ** ret :-> y }
+{s1 == s -- <a> ; dll(y, c, s1) ** ret :-> y }
 
 #####
 
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-pop-back.syn
similarity index 100%
rename from src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-pop-back.syn
rename to src/test/resources/synthesis/sequences/paper-benchmarks/sll/FAILS_sll-pop-back.syn
diff --git a/src/test/resources/synthesis/sequences/pure/unify3.syn b/src/test/resources/synthesis/sequences/pure/unify3.syn
index 96f6dcdb7..bbd7c9b5d 100644
--- a/src/test/resources/synthesis/sequences/pure/unify3.syn
+++ b/src/test/resources/synthesis/sequences/pure/unify3.syn
@@ -2,12 +2,12 @@ Should solve the unification with empty sequences - 3
 
 #####
 
-{ S == v:S1 /\ S2 == <>; x :-> a}
+{ S == v::S1 /\ S2 == <>; x :-> a}
 void elemInSet (loc x, int v)
-{  v1:S1 == S ++ S2; x :-> v1}
+{  v1::S1 == S ++ S2; x :-> v1}
 
 #####
 
 void elemInSet (loc x, int v) {
   *x = v;
-}
\ No newline at end of file
+}

From 96248641f3c81d872874e21e099507d3e7fe0c3b Mon Sep 17 00:00:00 2001
From: Abhishek Chandramouli Sharma <abhishekcs@protonmail.com>
Date: Wed, 27 Apr 2022 17:05:32 -0700
Subject: [PATCH 10/10] Put SSL rules for sequences behind a flag and test
 suite file

---
 .../tygus/suslik/synthesis/SynConfig.scala    |  1 +
 .../suslik/synthesis/SynthesisRunner.scala    |  4 +++
 .../suslik/synthesis/rules/BranchRules.scala  |  4 +--
 .../suslik/synthesis/rules/FailRules.scala    |  3 +-
 .../synthesis/rules/OperationalRules.scala    |  3 +-
 .../synthesis/rules/UnificationRules.scala    | 11 +++---
 .../paper-benchmarks/sll/sll-ith.syn          |  2 +-
 .../paper-benchmarks/sll/sll-length.syn       |  2 +-
 .../project-benchmarks/llist_ith.syn          |  2 +-
 .../sequences/project-benchmarks/sll-ith.syn  |  2 +-
 .../project-benchmarks/sll-length.syn         |  2 +-
 .../suslik/synthesis/SequencesTests.scala     | 34 +++++++++++++++++++
 12 files changed, 55 insertions(+), 15 deletions(-)
 create mode 100644 src/test/scala/org/tygus/suslik/synthesis/SequencesTests.scala

diff --git a/src/main/scala/org/tygus/suslik/synthesis/SynConfig.scala b/src/main/scala/org/tygus/suslik/synthesis/SynConfig.scala
index e7455e4d1..4144538a8 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/SynConfig.scala
+++ b/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,
diff --git a/src/main/scala/org/tygus/suslik/synthesis/SynthesisRunner.scala b/src/main/scala/org/tygus/suslik/synthesis/SynthesisRunner.scala
index 318425fae..8f6592f2a 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/SynthesisRunner.scala
+++ b/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")
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala
index ee439cddd..f6815fc3d 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/BranchRules.scala
+++ b/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
 
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala
index 758791d7d..84d52366e 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/FailRules.scala
+++ b/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)
     }
   }
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala
index d4611131a..91b23ca49 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/OperationalRules.scala
+++ b/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
diff --git a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala b/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
index be004c4d8..c5c84f71b 100644
--- a/src/main/scala/org/tygus/suslik/synthesis/rules/UnificationRules.scala
+++ b/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)
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn
index 31dcfba45..737d72d24 100644
--- a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-ith.syn
+++ b/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
 
 #####
 
diff --git a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn b/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn
index 5ad79d4b7..7e68aa964 100644
--- a/src/test/resources/synthesis/sequences/paper-benchmarks/sll/sll-length.syn
+++ b/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
 
 #####
 
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn b/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn
index e3f0e23a9..a58e38ae7 100644
--- a/src/test/resources/synthesis/sequences/project-benchmarks/llist_ith.syn
+++ b/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
 
 #####
 
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn
index 31dcfba45..737d72d24 100644
--- a/src/test/resources/synthesis/sequences/project-benchmarks/sll-ith.syn
+++ b/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
 
 #####
 
diff --git a/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn b/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
index 5ad79d4b7..7e68aa964 100644
--- a/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
+++ b/src/test/resources/synthesis/sequences/project-benchmarks/sll-length.syn
@@ -1,4 +1,4 @@
-# -c 1 -o 1
+# -c 1 -o 1 --sequenceRules true
 
 #####
 
diff --git a/src/test/scala/org/tygus/suslik/synthesis/SequencesTests.scala b/src/test/scala/org/tygus/suslik/synthesis/SequencesTests.scala
new file mode 100644
index 000000000..16ee23066
--- /dev/null
+++ b/src/test/scala/org/tygus/suslik/synthesis/SequencesTests.scala
@@ -0,0 +1,34 @@
+package org.tygus.suslik.synthesis
+
+import org.scalatest.{FunSpec, Matchers}
+
+/**
+  * @author Abhishek Sharma, Aidan Denlinger
+  */
+
+class SequencesTests extends FunSpec with Matchers with SynthesisRunnerUtil {
+
+  override def doRun(testName: String, desc: String, in: String, out: String, params: SynConfig = defaultConfig): Unit = {
+    super.doRun(testName, desc, in, out, params)
+    it(desc) {
+      synthesizeFromSpec(testName, in, out, params)
+    }
+  }
+
+  describe("Pure synthesis with sequences") {
+    runAllTestsFromDir("sequences/pure")
+  }
+
+  describe("Linked lists with sequences") {
+    runAllTestsFromDir("sequences/llist")
+  }
+
+  describe("Doubly-linked list with sequence of elements") {
+    runAllTestsFromDir("sequences/paper-benchmarks/dll")
+  }
+
+  describe("Singly-linked list with sequence of elements") {
+    runAllTestsFromDir("sequences/paper-benchmarks/sll")
+  }
+
+}
\ No newline at end of file