Add path condition into problems, unused for now

src/main/scala/leon/synthesis/Heuristics.scala

@@ -97,9 +97,9 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
         val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi)
         val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
 
-        val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.phi), p.xs)
-        val subGT   = Problem(inductOn :: postXs, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs)
-        val subLT   = Problem(inductOn :: postXs, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs)
+        val subBase = Problem(List(), p.c, subst(origId -> IntLiteral(0), p.phi), p.xs)
+        val subGT   = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs)
+        val subLT   = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs)
 
         val onSuccess: List[Solution] => Solution = {
           case List(base, gt, lt) =>

src/main/scala/leon/synthesis/Problem.scala

@@ -5,9 +5,9 @@ import leon.purescala.Trees._
 import leon.purescala.Common._
 
 // Defines a synthesis triple of the form:
-// ⟦ as ⟨ phi ⟩ xs ⟧
-case class Problem(as: List[Identifier], phi: Expr, xs: List[Identifier]) {
-  override def toString = "⟦ "+as.mkString(";")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+// ⟦ as ⟨ C | phi ⟩ xs ⟧
+case class Problem(as: List[Identifier], c: Expr, phi: Expr, xs: List[Identifier]) {
+  override def toString = "⟦ "+as.mkString(";")+" ⟨ "+c+" | "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
 
   val complexity: ProblemComplexity = ProblemComplexity(this)
 }

src/main/scala/leon/synthesis/Rules.scala

@@ -62,7 +62,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
       val others = exprs.filter(_ != eq)
       val oxs    = p.xs.filter(_ != x)
 
-      val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs)
+      val newProblem = Problem(p.as, p.c, subst(x -> e, And(others)), oxs)
 
       val onSuccess: List[Solution] => Solution = { 
         case List(Solution(pre, term)) =>
@@ -108,8 +108,8 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
     val p = task.problem
     p.phi match {
       case Or(Seq(o1, o2)) =>
-        val sub1 = Problem(p.as, o1, p.xs)
-        val sub2 = Problem(p.as, o2, p.xs)
+        val sub1 = Problem(p.as, p.c, o1, p.xs)
+        val sub2 = Problem(p.as, p.c, o2, p.xs)
 
         val onSuccess: List[Solution] => Solution = { 
           case List(Solution(p1, t1), Solution(p2, t2)) => Solution(Or(p1, p2), IfExpr(p1, t1, t2))
@@ -183,7 +183,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
       val sub = p.copy(xs = p.xs.filterNot(unconstr))
 
       val onSuccess: List[Solution] => Solution = { 
-        case List(s) => 
+        case List(s) =>
           Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id)))))
         case _ =>
           Solution.none

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -88,7 +88,7 @@ class Synthesizer(val r: Reporter,
         val as = (variablesOf(pred)--xs).toList
         val phi = pred
 
-        val sol = synthesize(Problem(as, phi, xs), rules)
+        val sol = synthesize(Problem(as, BooleanLiteral(true), phi, xs), rules)
 
         solutions = (ch -> sol) :: solutions