diff --git a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
index a45d1b63addd8897e30196e426a05cf8e54ed665..d1b0622b7cea9b3fb0e0269043bea3fabbba5984 100755
--- a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
@@ -376,8 +376,8 @@ class SynthesizerForRuleExamples(
}
def interactivePause = {
- System.out.println("Press Any Key To Continue...");
- new java.util.Scanner(System.in).nextLine();
+// System.out.println("Press Any Key To Continue...");
+// new java.util.Scanner(System.in).nextLine();
}
def getNewExampleQueue = PriorityQueue[(Expr, Int)]()(
@@ -420,9 +420,12 @@ class SynthesizerForRuleExamples(
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
- variableRefiner =
- new VariableRefiner(loader.directSubclassesMap,
- loader.variableDeclarations, loader.classMap, reporter)
+ variableRefiner = new VariableRefinerCompose add
+ // refiner on structure
+ new VariableRefinerStructure(loader.directSubclassesMap,
+ loader.variableDeclarations, loader.classMap, reporter) add
+ // refiner that uses execution
+ new VariableRefinerExecution(loader.variableDeclarations, loader.classMap)
// new VariableSolverRefiner(loader.directSubclassesMap,
// loader.variableDeclarations, loader.classMap, mainSolver, reporter)
@@ -510,24 +513,49 @@ class SynthesizerForRuleExamples(
) {
fine("boolean snippet is: " + innerSnippetTree)
info("Trying: " + innerSnippetTree + " as a condition.")
- val (innerFound, innerPrec) = tryToSynthesizeBooleanCondition(
+ val innerPrecFound = tryToSynthesizeBooleanCondition(
snippetTree, innerSnippetTree,
// counter examples represent those for which candidate fails
(failedExamples.map(_.map) ++ maps), succeededExamples.map(_.map)
)
- // if precondition found
- if (innerFound) {
- info("Precondition " + innerPrec + " found for " + snippetTree)
-
- innerPrec match {
- case s @ Some(_) =>
- // new precondition (restore in finally)
- preconditionToRestore = s
- case _ =>
+ info("tryToSynthesizeBooleanCondition returned " + innerPrecFound + " for " + snippetTree)
+ if ( innerPrecFound ) {
+ // update accumulating expression
+ val oldAccumulatingExpression = accumulatingExpression
+ val newAccumulatingExpression =
+ (finalExpr: Expr) =>
+ oldAccumulatingExpression({
+ val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
+ innerIf.setType(snippetTree.getType)
+ innerIf
+ })
+
+ accumulatingExpression = newAccumulatingExpression
+
+ // update accumulating precondition
+ fine("updating accumulatingPrecondition")
+ accumulatingCondition = And(Seq(accumulatingCondition, Not(innerSnippetTree)))
+ fine("updating hole fun precondition and body (to be hole)")
+ // new precondition (restore in finally)
+ preconditionToRestore = Some(accumulatingCondition)
+
+ val currentBranchCondition = And(Seq(accumulatingCondition, innerSnippetTree))
+ val variableRefinementResult = variableRefiner.refine(innerSnippetTree,
+ currentBranchCondition, allDeclarations, exampleRunner.getEvaluator)
+
+ if (variableRefinementResult._1) {
+ info("Variable is refined.")
+ allDeclarations = variableRefinementResult._2
+
+ // the reason for two flags is for easier management of re-syntheses only if needed
+ variableRefinedBranch = true
+ variableRefinedCondition = true
}
+
return true
}
+
} // iterating over all boolean solutions
info("No precondition found for branch expression: " + snippetTree)
@@ -545,8 +573,17 @@ class SynthesizerForRuleExamples(
}
}
+ /**
+ * tries to abduce a new branch
+ * @param snippetTree expression candidate
+ * @param innerSnippetTree condition candidate
+ * @param counterExamples failed examples
+ * @param succExamples successful examples
+ * @return whether branch condition is found
+ */
def tryToSynthesizeBooleanCondition(snippetTree: Expr, innerSnippetTree: Expr,
- counterExamples: Seq[Map[Identifier, Expr]], succExamples: Seq[Map[Identifier, Expr]]): (Boolean, Option[Expr]) = {
+ counterExamples: Seq[Map[Identifier, Expr]], succExamples: Seq[Map[Identifier, Expr]]):
+ Boolean = {
// new condition together with existing precondition
val newPrecondition = And(Seq(initialPrecondition, accumulatingCondition, innerSnippetTree))
val newPathCondition = And(Seq(problem.pc, accumulatingCondition, innerSnippetTree))
@@ -719,56 +756,24 @@ class SynthesizerForRuleExamples(
if (valid) {
// we found a branch
info("We found a branch, for expression %s, with condition %s.".format(snippetTree, innerSnippetTree))
-
- // update accumulating expression
- val oldAccumulatingExpression = accumulatingExpression
- val newAccumulatingExpression =
- (finalExpr: Expr) =>
- oldAccumulatingExpression({
- val innerIf = IfExpr(innerSnippetTree, snippetTree, finalExpr)
- innerIf.setType(snippetTree.getType)
- innerIf
- })
-
- accumulatingExpression = newAccumulatingExpression
- val currentBranchCondition = And(Seq(accumulatingCondition, innerSnippetTree))
-
- // update accumulating precondition
- fine("updating accumulatingPrecondition")
- accumulatingCondition = And(Seq(accumulatingCondition, Not(innerSnippetTree)))
- fine("updating hole fun precondition and body (to be hole)")
-
- // set to set new precondition
- val preconditionToRestore = Some(accumulatingCondition)
-
- val variableRefinementResult = variableRefiner.checkRefinements(innerSnippetTree, currentBranchCondition, allDeclarations)
- if (variableRefinementResult._1) {
- info("Variable is refined.")
- allDeclarations = variableRefinementResult._2
-
- // the reason for two flags is for easier management of re-syntheses only if needed
- variableRefinedBranch = true
- variableRefinedCondition = true
- }
-
+
// found a boolean snippet, break
- (true, preconditionToRestore)
+ true
} else {
// collect (add) counterexamples from leon
if (collectCounterExamplesFromLeon && !map.isEmpty)
gatheredExamples ++= (map :: Nil).map(Example(_))
// reset funDef and continue with next boolean snippet
- val preconditionToRestore = Some(accumulatingCondition)
- (false, preconditionToRestore)
+ false
}
} else {
fine("Solver filtered out the precondition (does not imply counterexamples)")
- (false, None)
+ false
}
} else {// if (!isItAContradiction)
fine("Solver filtered out the precondition (is not sound)")
- (false, None)
+ false
}
}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
index 07c9ed8db774fd0c8154c67bd01268d1f61fdb0b..08c08d34f1c4913f1a1bf13315d6bd8a077bc907 100755
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
@@ -1,94 +1,67 @@
package leon.synthesis.condabd
package refinement
-import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
-
-import leon._
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
import leon.purescala.Definitions._
import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.evaluators._
-import insynth.leon.loader._
import insynth.leon.{ LeonDeclaration => Declaration, _ }
import _root_.insynth.util.logging.HasLogger
-// each variable of super type can actually have a subtype
-// get sine declaration maps to be able to refine them
-class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[Declaration],
- classMap: Map[Identifier, ClassType], reporter: Reporter) extends HasLogger {
-
- // map from identifier into a set of possible subclasses
- protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
- for (varDec <- variableDeclarations) {
- varDec match {
- case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
- variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
- case _ =>
- }
- }
-
- def getPossibleTypes(id: Identifier) = variableRefinements(id)
-
- def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[Declaration]) =
- // check for refinements
- getIdAndClassDef(expr) match {
- case Some(refinementPair @ (id, classType)) if variableRefinements(id).size > 1 =>
- fine("And now we have refinement type: " + refinementPair)
- fine("variableRefinements(id) before" + variableRefinements(id))
- variableRefinements(id) -= classMap(classType.id)
- fine("variableRefinements(id) after" + variableRefinements(id))
-
- // if we have a single subclass possible to refine
- if (variableRefinements(id).size == 1) {
- reporter.info("We do variable refinement for " + id)
-
- val newType = variableRefinements(id).head
- fine("new type is: " + newType)
-
- // update declarations
- val newDeclarations =
- refinedDeclarations(id, newType, allDeclarations)
-
- (true, newDeclarations.flatten)
- } else {
- fine("we cannot do variable refinement :(")
- (false, allDeclarations)
- }
- case _ =>
- (false, allDeclarations)
- }
+// TODO a *provider* for maps from id to possible types (so that not all classes need to maintain a map)
+trait VariableRefiner extends HasLogger {
+
+ type Type = ClassType
+
+ def getPossibleTypes(id: Identifier): Set[Type]
+
+ def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])])
- // inspect the expression if some refinements can be done
- def getIdAndClassDef(expr: Expr) = expr match {
- case CaseClassInstanceOf(classDef, Variable(id)) =>
- Some((id, classDef))
- case _ =>
- None
+ /**
+ * refine given declarations according to given expression and current partition condition
+ * @param expr
+ * @param condition
+ * @param declarations
+ * @return new declarations with refined ones
+ */
+ def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null): List[(Identifier, Set[ClassType])]
+
+ def refine(expr: Expr, condition: Expr, declarations: List[Declaration], evaluator: Evaluator = null) = {
+ checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator) match {
+ case Nil => (false, declarations)
+ case list =>
+ ((false, declarations) /: list) {
+ case ((flag, refined), (id, newTypes)) =>
+ fine(((flag, refined), (id, newTypes)).toString)
+ if (newTypes.size == 1)
+ (true, refineDeclarations(id, newTypes.head, refined))
+ else
+ (flag, refined)
+ }
+ }
}
-
- def refinedDeclarations(id: Identifier, newType: ClassType, allDeclarations: List[Declaration]) =
- for (dec <- allDeclarations)
+
+ def refineDeclarations(id: Identifier, newType: ClassType, allDeclarations: List[Declaration]) =
+ (for (dec <- allDeclarations)
yield dec match {
- case Declaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>
- ((
- newType.classDef match {
- case newTypeCaseClassDef@CaseClassDef(_, parent, fields) =>
- fine("matched case class def for refinement " + newTypeCaseClassDef)
- for (field <- fields)
- yield Declaration(
- ImmediateExpression(id.name + "." + field.id.name,
- CaseClassSelector(newTypeCaseClassDef, imex.expr, field.id) ),
- TypeTransformer(field.id.getType), field.id.getType
- )
- case _ =>
- Seq.empty
- }
- ): Seq[Declaration]) :+ Declaration(imex, TypeTransformer(newType), newType)
- case _ =>
- Seq(dec)
- }
-
+ case Declaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>
+ ((
+ newType.classDef match {
+ case newTypeCaseClassDef @ CaseClassDef(_, parent, fields) =>
+ fine("matched case class def for refinement " + newTypeCaseClassDef)
+ for (field <- fields)
+ yield Declaration(
+ ImmediateExpression(id.name + "." + field.id.name,
+ CaseClassSelector(newTypeCaseClassDef, imex.expr, field.id)),
+ TypeTransformer(field.id.getType), field.id.getType)
+ case _ =>
+ Seq.empty
+ }): Seq[Declaration]) :+ Declaration(imex, TypeTransformer(newType), newType)
+ case _ =>
+ Seq(dec)
+ }).flatten
+
}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala
new file mode 100755
index 0000000000000000000000000000000000000000..44077031754372090c3aa554a93a4044e7fef8cc
--- /dev/null
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerCompose.scala
@@ -0,0 +1,48 @@
+package leon.synthesis.condabd
+package refinement
+
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.evaluators._
+
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
+
+// TODO update other refiners with results of this one
+class VariableRefinerCompose extends VariableRefiner {
+
+ private var refiners = Array[VariableRefiner]()
+
+ def add(refiner: VariableRefiner) = {
+ refiners :+= refiner
+ // refiner.refinePossibleTypes(id, types)
+ this
+ }
+
+ override def getPossibleTypes(id: Identifier) =
+ refiners.head.getPossibleTypes(id)
+
+ override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
+ for (refiner <- refiners)
+ refiner.refinePossibleTypes(refinements)
+
+ override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
+ val refineMap =
+ ((Map[Identifier, Set[ClassType]]()) /: refiners) {
+ case (refineMap, refiner) =>
+ ( refineMap /: refiner.checkRefinements(expr, condition)(evaluator) ) {
+ case (map, (id, newTypes)) =>
+ if (map contains id)
+ map + (id -> map(id).intersect(newTypes))
+ else
+ map + (id -> newTypes)
+ }
+ }
+
+ for (refiner <- refiners)
+ refiner.refinePossibleTypes(refineMap.toList)
+
+ refineMap.toList
+ }
+
+}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala
new file mode 100755
index 0000000000000000000000000000000000000000..989fd3ccfa890189732abdf90ca2659a634b8cec
--- /dev/null
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerExecution.scala
@@ -0,0 +1,104 @@
+package leon
+package synthesis.condabd
+package refinement
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
+
+import leon.purescala.Extractors._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.evaluators._
+import EvaluationResults._
+
+import insynth.leon.loader._
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
+
+import _root_.insynth.util.logging.HasLogger
+
+class VariableRefinerExecution(variableDeclarations: Seq[Declaration],
+ classMap: Map[Identifier, ClassType]) extends VariableRefiner with HasLogger {
+
+ // map from identifier into a set of possible subclasses
+ // currently only classes with no fields
+ protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
+
+ // TODO use cd.knownDescendents?
+ for (varDec <- variableDeclarations) {
+ varDec match {
+ case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, IsTyped(Variable(id), AbstractClassType(cd)))) =>
+ variableRefinements += (id -> MutableSet(cd.knownDescendents.map(classDefToClassType _): _*))
+ case _ =>
+ }
+ }
+
+ override def getPossibleTypes(id: Identifier) = variableRefinements(id).toSet
+
+ override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
+ val variables = variablesOf(expr)
+
+ // TODO can be extended with more variables (fix SOME values for other ones)
+ if (variables.size == 1) {
+ val variable = variables.head
+ variable match {
+ case oldId @ IsTyped(id, AbstractClassType(cd)) // do not try to refine if we already know a single type is possible
+ if variableRefinements(id).size > 1 =>
+
+ assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
+
+ val optCases =
+ for (dcd <- variableRefinements(id).map(_.classDef)) yield dcd match {
+ case ccd: CaseClassDef if ccd.fields.isEmpty =>
+
+ val testValue = CaseClass(ccd, Nil)
+ val conditionToEvaluate = And(Not(expr), condition)
+ fine("Execute condition " + conditionToEvaluate + " on variable " + id + " as " + testValue)
+
+ evaluator.eval(conditionToEvaluate, Map(id -> testValue)) match {
+ case Successful(BooleanLiteral(false)) =>
+ fine("EvaluationSuccessful(false)")
+ fine("Refining variableRefinements(id): " + variableRefinements(id))
+ variableRefinements(id) -= classDefToClassType(ccd)
+ fine("Refined variableRefinements(id): " + variableRefinements(id))
+ Some(ccd)
+ case Successful(BooleanLiteral(true)) =>
+ fine("EvaluationSuccessful(true)")
+ None
+ case m =>
+ warning("Eval failed: " + m)
+ None
+ }
+
+ case _ =>
+ None
+ }
+
+ if (optCases.flatten.isEmpty)
+ Nil
+ else {
+ finest("Returning: " + List((id, variableRefinements(id).toSet)))
+ List((id, variableRefinements(id).toSet))
+ }
+ case _ =>
+ fine("did not match for refinement " + variable)
+ Nil
+ }
+ } else Nil
+ }
+
+ // inspect the expression if some refinements can be done
+ def getIdAndClassDef(expr: Expr) = expr match {
+ case CaseClassInstanceOf(classDef, Variable(id)) =>
+ Some((id, classDef))
+ case _ =>
+ None
+ }
+
+ override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
+ for ((id, types) <- refinements)
+ variableRefinements(id) &~= types
+
+}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala
new file mode 100755
index 0000000000000000000000000000000000000000..a76c8e9cfc73c19fafbfa734c4e66aa28e5df99f
--- /dev/null
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefinerStructure.scala
@@ -0,0 +1,62 @@
+package leon.synthesis.condabd
+package refinement
+
+import scala.collection.mutable.{Map => MutableMap}
+import scala.collection.mutable.{Set => MutableSet}
+
+import leon._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+import leon.purescala.Definitions._
+import leon.purescala.Common.{ Identifier, FreshIdentifier }
+import leon.evaluators._
+
+import insynth.leon.loader._
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
+
+import _root_.insynth.util.logging.HasLogger
+
+// each variable of super type can actually have a subtype
+// get sine declaration maps to be able to refine them
+class VariableRefinerStructure(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[Declaration],
+ classMap: Map[Identifier, ClassType], reporter: Reporter) extends VariableRefiner with HasLogger {
+
+ // map from identifier into a set of possible subclasses
+ protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
+ for (varDec <- variableDeclarations) {
+ varDec match {
+ case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
+ variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
+ case _ =>
+ }
+ }
+
+ override def getPossibleTypes(id: Identifier) = variableRefinements(id).toSet
+
+ override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) =
+ // check for refinements
+ getIdAndClassDef(expr) match {
+ case Some(refinementPair @ (id, classType)) if variableRefinements(id).size > 1 =>
+ fine("And now we have refinement type: " + refinementPair)
+ fine("variableRefinements(id) before" + variableRefinements(id))
+ variableRefinements(id) -= classMap(classType.id)
+ fine("variableRefinements(id) after" + variableRefinements(id))
+
+ List((id, variableRefinements(id).toSet))
+ case _ =>
+ Nil
+ }
+
+ // inspect the expression if some refinements can be done
+ def getIdAndClassDef(expr: Expr) = expr match {
+ case CaseClassInstanceOf(classDef, Variable(id)) =>
+ Some((id, classDef))
+ case _ =>
+ None
+ }
+
+ override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) =
+ for ((id, types) <- refinements)
+ variableRefinements(id) &~= types
+
+}
diff --git a/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
index 45adc6a242ddd3484871d60761eb65ea12fe2721..262d4528a76a3ef84abb78dd1bf778a7bb6dda2a 100755
--- a/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
@@ -2,8 +2,8 @@ package leon
package synthesis.condabd
package refinement
-import scala.collection.mutable.{Map => MutableMap}
-import scala.collection.mutable.{Set => MutableSet}
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet }
import purescala.Extractors._
import purescala.TypeTrees._
@@ -13,93 +13,78 @@ import purescala.Definitions._
import purescala.Common.{ Identifier, FreshIdentifier }
import solvers._
import synthesis.Problem
+import leon.evaluators._
import insynth.leon.loader._
import insynth.leon._
import _root_.insynth.util.logging.HasLogger
-// each variable of super type can actually have a subtype
-// get sine declaration maps to be able to refine them
class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
classMap: Map[Identifier, ClassType], solverf: SolverFactory[Solver], reporter: Reporter)
- extends VariableRefiner(directSubclassMap, variableDeclarations, classMap, reporter) with HasLogger {
+ extends VariableRefinerStructure(directSubclassMap, variableDeclarations, classMap, reporter) with HasLogger {
val solver = SimpleSolverAPI(solverf)
-
- override def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[LeonDeclaration]) = {
- val superResult = super.checkRefinements(expr, condition, allDeclarations)
- if (superResult._1 == false) {
- val variables = variablesOf(expr)
- if (variables.size == 1) {
- val variable = variables.head
- variable match {
- case oldId@IsTyped(id, AbstractClassType(cd)) if variableRefinements(id).size > 1 =>
-
- assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
- //val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
- val optCases = for (dcd <- variableRefinements(id).map(_.classDef)) yield dcd match {
- case ccd : CaseClassDef =>
- fine("testing variable " + id + " with condition " + condition)
- val toSat = And(condition, CaseClassInstanceOf(ccd, Variable(id)))
-
- fine("checking satisfiability of: " + toSat)
- solver.solveSAT(toSat) match {
- case (Some(false), _) =>
- fine("variable cannot be of type " + ccd)
- None
- case _ =>
- fine("variable can be of type " + ccd)
- Some(ccd)
- }
- case _ =>
- None
- }
-
- val cases = optCases.flatten
- variableRefinements(id) = variableRefinements(id) & cases.map(CaseClassType(_)).toSet
- assert(variableRefinements(id).size == cases.size)
-
- if (cases.size == 1) {
- // update declarations
- val newDeclarations =
- refinedDeclarations(id, CaseClassType(cases.head), allDeclarations)
-
- (true, newDeclarations.flatten)
- } else {
- fine("cases.size != 1")
- superResult
- }
-
- case id => {
- fine("no id found for refinement that has potential refinements > 1")
- superResult
- }
- }
- } else {
- fine("more than one variable")
- superResult
- }
+
+ override def checkRefinements(expr: Expr, condition: Expr)(evaluator: Evaluator = null) = {
+ val variables = variablesOf(expr)
+ if (variables.size == 1) {
+ val variable = variables.head
+ variable match {
+ case oldId@IsTyped(id, AbstractClassType(cd)) if variableRefinements(id).size > 1 =>
+
+ assert(variableRefinements(id).map(_.classDef) subsetOf cd.knownDescendents.toSet)
+ //val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
+ val optCases = for (dcd <- variableRefinements(id).map(_.classDef)) yield dcd match {
+ case ccd : CaseClassDef =>
+ fine("testing variable " + id + " with condition " + condition)
+ val toSat = And(condition, CaseClassInstanceOf(ccd, Variable(id)))
+
+ fine("checking satisfiability of: " + toSat)
+ solver.solveSAT(toSat) match {
+ case (Some(false), _) =>
+ fine("variable cannot be of type " + ccd)
+ None
+ case _ =>
+ fine("variable can be of type " + ccd)
+ Some(ccd)
+ }
+ case _ =>
+ None
+ }
+
+ val cases = optCases.flatten
+ variableRefinements(id) = variableRefinements(id) & cases.map(CaseClassType(_)).toSet
+ assert(variableRefinements(id).size == cases.size)
+
+ List((id, variableRefinements(id).toSet))
+
+ case id =>
+ fine("no id found for refinement that has potential refinements > 1")
+ Nil
+ }
+ } else {
+ fine("VariableSolverRefiner will not refine: more than one variable")
+ Nil
}
- else superResult
- }
-
+ }
+
def refineProblem(p: Problem) = {
val newAs = p.as.map {
- case oldId@IsTyped(id, AbstractClassType(cd)) =>
+ case oldId @ IsTyped(id, AbstractClassType(cd)) =>
val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
- case ccd : CaseClassDef =>
+ case ccd: CaseClassDef =>
val toSat = And(p.pc, CaseClassInstanceOf(ccd, Variable(id)))
-
+
val isImplied = solver.solveSAT(toSat) match {
case (Some(false), _) => true
case _ => false
}
-
+
println(isImplied)
-
+
if (!isImplied) {
Some(ccd)
} else {
@@ -110,20 +95,21 @@ class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], v
}
val cases = optCases.flatten
-
+
println(id)
println(cases)
-
+
if (cases.size == 1) {
-// id.setType(CaseClassType(cases.head))
+ // id.setType(CaseClassType(cases.head))
FreshIdentifier(oldId.name).setType(CaseClassType(cases.head))
} else oldId
-
+
case id => id
}
-
+
p.copy(as = newAs)
}
-
+ override def refinePossibleTypes(refinements: List[(Identifier, Set[ClassType])]) = Unit
+
}
diff --git a/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
index fff9381c3565dc059ba8486fc39c7247fc3d58e8..7881846ae98f6915db2cc9baf85ad7db57d643cf 100644
--- a/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
+++ b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
@@ -92,11 +92,11 @@ class EnumeratorTest extends JUnitSuite {
val listVal = funDef.args.head.toVariable
val variableRefiner =
- new VariableRefiner(loader.directSubclassesMap,
+ new VariableRefinerStructure(loader.directSubclassesMap,
loader.variableDeclarations, loader.classMap, reporter)
val (refined, newDeclarations) =
- variableRefiner.checkRefinements(
+ variableRefiner.refine(
CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
assertTrue(refined)
assert(allDeclarations.size + 2 == newDeclarations.size)
diff --git a/src/test/scala/leon/test/condabd/FilterTest.scala b/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
similarity index 98%
rename from src/test/scala/leon/test/condabd/FilterTest.scala
rename to src/test/scala/leon/test/condabd/refinement/FilterTest.scala
index d439df5363654401581941189d07c6af91b36d76..fc18cb9bae82f27430b8d333aa29dfa8f52fbd47 100644
--- a/src/test/scala/leon/test/condabd/FilterTest.scala
+++ b/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
@@ -1,4 +1,5 @@
package leon.test.condabd
+package refinement
import scala.util.Random
@@ -51,7 +52,7 @@ class FilterTest extends JUnitSuite {
val loader = new LeonLoader(prog, problem.as, true)
- variableRefiner = new VariableRefiner(loader.directSubclassesMap, loader.variableDeclarations,
+ variableRefiner = new VariableRefinerStructure(loader.directSubclassesMap, loader.variableDeclarations,
loader.classMap, sctx.reporter)
tail =
diff --git a/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala b/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d7fe41fdbced37129e9c574c52cc7a19eee2cad3
--- /dev/null
+++ b/src/test/scala/leon/test/condabd/refinement/RefinementExamples.scala
@@ -0,0 +1,72 @@
+package leon.test.condabd.refinement
+
+import scala.util.Random
+
+import org.scalatest.FunSpec
+import org.scalatest.GivenWhenThen
+
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.refinement._
+
+object RefinementExamples {
+
+ val listClassId = FreshIdentifier("List")
+ val listAbstractClassDef = new AbstractClassDef(listClassId)
+ val listAbstractClass = new AbstractClassType(listAbstractClassDef)
+
+ val nilClassId = FreshIdentifier("Nil")
+ val nilAbstractClassDef = new CaseClassDef(nilClassId).setParent(listAbstractClassDef)
+ val nilAbstractClass = new CaseClassType(nilAbstractClassDef)
+
+ val consClassId = FreshIdentifier("Cons")
+ val consAbstractClassDef = new CaseClassDef(consClassId).setParent(listAbstractClassDef)
+ val headId = FreshIdentifier("head").setType(Int32Type)
+ consAbstractClassDef.fields = Seq(VarDecl(headId, Int32Type))
+ val consAbstractClass = new CaseClassType(consAbstractClassDef)
+
+ val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
+ listAbstractClass -> Set(nilAbstractClass, consAbstractClass)
+ )
+
+ val listVal = Variable(FreshIdentifier("tempVar"))
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ val classMap: Map[Identifier, ClassType] = Map(
+ listClassId -> listAbstractClass,
+ nilClassId -> nilAbstractClass,
+ consClassId -> consAbstractClass
+ )
+
+ def buildClassMap(program: Program) = {
+ val listAbstractClassDef = program.definedClasses.find(_.id.name == "List").
+ get.asInstanceOf[AbstractClassDef]
+
+ val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+ get.asInstanceOf[CaseClassDef]
+
+ val consAbstractClassDef = program.definedClasses.find(_.id.name == "Cons").
+ get.asInstanceOf[CaseClassDef]
+
+ val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
+ AbstractClassType(listAbstractClassDef) ->
+ Set(CaseClassType(nilAbstractClassDef), CaseClassType(consAbstractClassDef))
+ )
+
+ val classMap: Map[Identifier, ClassType] = Map(
+ listAbstractClassDef.id -> AbstractClassType(listAbstractClassDef),
+ nilAbstractClassDef.id -> CaseClassType(nilAbstractClassDef),
+ consAbstractClassDef.id -> CaseClassType(consAbstractClassDef)
+ )
+
+ (directSubclassMap, AbstractClassType(listAbstractClassDef), classMap)
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..833206dcbd48c6bcb84bec8bd99aab1c14b436c4
--- /dev/null
+++ b/src/test/scala/leon/test/condabd/refinement/VariableRefinerComposeTest.scala
@@ -0,0 +1,150 @@
+package leon.test.condabd
+package refinement
+
+import scala.util.Random
+
+import org.scalatest.FunSpec
+import org.scalatest.GivenWhenThen
+
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+import leon.evaluators._
+
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.refinement._
+
+import util.Scaffold
+
+class VariableRefinerComposeTest extends FunSpec with GivenWhenThen {
+
+ import Scaffold._
+ import RefinementExamples._
+
+ val lesynthTestDir = "testcases/condabd/test/lesynth/"
+
+ describe("A variable compose(structure, exec) refiner with list ADT") {
+
+ it("should refine if condition is isSorted()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isSorted =
+ program.definedFunctions.find {
+ _.id.name == "isSorted"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isSorted"); null
+ }
+
+ val listVal = funDef.args.find(_.id.name == "l").get.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerCompose")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerCompose add
+ new VariableRefinerStructure(
+ directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
+ ) add
+ new VariableRefinerExecution(
+ declarations, classMap
+ )
+
+ val res = variableRefiner.refine(
+ isSorted(listVal),
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should be updated accordingly")
+ expectResult((true, declarations.size + 2)) {
+ (res._1, res._2.size)
+ }
+
+ withClue(declarations.toString) {
+ assert {
+ res._2.exists(_.leonType.toString contains "Cons")
+ }
+ }
+
+ And("after 2nd consequtive call, nothing should happen")
+ expectResult((false, res._2)) {
+ val res2 = variableRefiner.refine(
+ isSorted(listVal),
+ BooleanLiteral(true),
+ res._2,
+ codeGenEval
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ }
+
+ describe("A variable compose(structure) refiner with list ADT") {
+
+ it("should not refine if condition is isSorted()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isSorted =
+ program.definedFunctions.find {
+ _.id.name == "isSorted"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isSorted"); null
+ }
+
+ val listVal = funDef.args.find(_.id.name == "l").get.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerCompose")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerCompose add
+ new VariableRefinerStructure(
+ directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
+ )
+
+ val res = variableRefiner.refine(
+ isSorted(listVal),
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should stay the same")
+ expectResult((false, declarations.size)) {
+ (res._1, res._2.size)
+ }
+ }
+ }
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..202072a3da0c7be930b5395132f10cfe9b83a43a
--- /dev/null
+++ b/src/test/scala/leon/test/condabd/refinement/VariableRefinerExecutionTest.scala
@@ -0,0 +1,298 @@
+package leon.test.condabd
+package refinement
+
+import scala.util.Random
+
+import org.scalatest.FunSpec
+import org.scalatest.GivenWhenThen
+
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+import leon.evaluators._
+
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.refinement._
+
+import util.Scaffold
+
+class VariableRefinerExecutionTest extends FunSpec with GivenWhenThen {
+
+ import Scaffold._
+ import RefinementExamples._
+
+ val lesynthTestDir = "testcases/condabd/test/lesynth/"
+
+ describe("A variable execution refiner with list ADT on insertion sort") {
+
+ it("should refine if condition is isSorted()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/InsertionSortInsert.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isSorted =
+ program.definedFunctions.find {
+ _.id.name == "isSorted"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isSorted"); null
+ }
+
+ val listVal = funDef.args.find(_.id.name == "l").get.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerExecution")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerExecution(
+ declarations, classMap
+ )
+
+ val res = variableRefiner.refine(
+ isSorted(listVal),
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should be updated accordingly")
+ expectResult((true, declarations.size + 2)) {
+ (res._1, res._2.size)
+ }
+
+ withClue(declarations.toString) {
+ assert {
+ res._2.exists(_.leonType.toString contains "Cons")
+ }
+ }
+
+ And("after 2nd consequtive call, nothing should happen")
+ expectResult((false, res._2)) {
+ val res2 = variableRefiner.refine(
+ isSorted(listVal),
+ BooleanLiteral(true),
+ res._2,
+ codeGenEval
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+ }
+
+ describe("A variable execution refiner with list ADT on lists") {
+
+ it("should refine if condition is isEmpty()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isEmpty =
+ program.definedFunctions.find {
+ _.id.name == "isEmpty"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val isEmptyBad =
+ program.definedFunctions.find {
+ _.id.name == "isEmptyBad"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerExecution")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerExecution(
+ declarations, classMap
+ )
+
+ val res = variableRefiner.refine(
+ isEmpty(listVal),
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should be updated accordingly")
+ expectResult((true, declarations.size + 2)) {
+ (res._1, res._2.size)
+ }
+
+ withClue(declarations.toString) {
+ assert {
+ res._2.exists(_.leonType.toString contains "Cons")
+ }
+ }
+
+ And("after 2nd consequtive call, nothing should happen")
+ expectResult((false, res._2)) {
+ val res2 = variableRefiner.refine(
+ isEmpty(listVal),
+ BooleanLiteral(true),
+ res._2,
+ codeGenEval
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ it("should refine list to Cons if condition is hasContent()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+// val inSynth = new InSynth(loader, true)
+// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val hasContent =
+ program.definedFunctions.find {
+ _.id.name == "hasContent"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract hasContent"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerExecution")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerExecution(
+ declarations, classMap
+ )
+
+ val condition = Not(hasContent(listVal))
+
+ val res = variableRefiner.refine(
+ condition,
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should be updated accordingly")
+ expectResult((true, declarations.size + 2)) {
+ (res._1, res._2.size)
+ }
+
+ withClue(declarations.toString) {
+ assert {
+ res._2.exists(_.leonType.toString contains "Cons")
+ }
+ }
+
+ And("after 2nd consequtive call, nothing should happen")
+ expectResult((false, res._2)) {
+ val res2 = variableRefiner.refine(
+ condition,
+ BooleanLiteral(true),
+ res._2,
+ codeGenEval
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ it("should not refine if condition is isEmptyBad()") {
+
+ for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
+ val program = sctx.program
+ val solver = sctx.solverFactory
+ val reporter = sctx.reporter
+ val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
+
+ val loader = new LeonLoader(program, problem.as, false)
+ val allDeclarations = loader.load
+// val inSynth = new InSynth(loader, true)
+// val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+ val (directSubclassMap, listAbstractClass, classMap) = buildClassMap(program)
+
+ val isEmpty =
+ program.definedFunctions.find {
+ _.id.name == "isEmpty"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val isEmptyBad =
+ program.definedFunctions.find {
+ _.id.name == "isEmptyBad"
+ } match {
+ case Some(found) => (x: Expr) => FunctionInvocation(found, Seq(x))
+ case _ => fail("could not extract isEmpty"); null
+ }
+
+ val listVal = funDef.args.head.toVariable
+ val listLeonDeclaration = LeonDeclaration(
+ ImmediateExpression( "tempVar", listVal ),
+ TypeTransformer(listAbstractClass), listAbstractClass
+ )
+
+ Given("a VariableRefinerExecution")
+ val declarations = List(listLeonDeclaration)
+ val variableRefiner = new VariableRefinerExecution(
+ declarations, classMap
+ )
+
+ val res = variableRefiner.refine(
+ isEmptyBad(listVal),
+ BooleanLiteral(true),
+ declarations,
+ codeGenEval
+ )
+
+ Then("declarations should not be updated")
+ expectResult((false, res._2)) {
+ val res2 = variableRefiner.refine(
+ isEmptyBad(listVal),
+ BooleanLiteral(true),
+ res._2,
+ codeGenEval
+ )
+ (res2._1, res2._2)
+ }
+ }
+ }
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/test/condabd/VariableRefinerTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
similarity index 52%
rename from src/test/scala/leon/test/condabd/VariableRefinerTest.scala
rename to src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
index c6b9f43ad76c9c693090ea69b67af02631098bd0..18d266db7be482ac495940876be8cadda7931b22 100644
--- a/src/test/scala/leon/test/condabd/VariableRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/refinement/VariableRefinerStructureTest.scala
@@ -1,4 +1,5 @@
package leon.test.condabd
+package refinement
import scala.util.Random
@@ -15,44 +16,16 @@ import leon.synthesis.condabd.refinement._
import util.Scaffold._
-class VariableRefinerTest extends FunSpec with GivenWhenThen {
+class VariableRefinerTest extends FunSpec with GivenWhenThen {
- val listClassId = FreshIdentifier("List")
- val listAbstractClassDef = new AbstractClassDef(listClassId)
- val listAbstractClass = new AbstractClassType(listAbstractClassDef)
-
- val nilClassId = FreshIdentifier("Nil")
- val nilAbstractClassDef = new CaseClassDef(nilClassId).setParent(listAbstractClassDef)
- val nilAbstractClass = new CaseClassType(nilAbstractClassDef)
-
- val consClassId = FreshIdentifier("Cons")
- val consAbstractClassDef = new CaseClassDef(consClassId).setParent(listAbstractClassDef)
- val headId = FreshIdentifier("head").setType(Int32Type)
- consAbstractClassDef.fields = Seq(VarDecl(headId, Int32Type))
- val consAbstractClass = new CaseClassType(consAbstractClassDef)
-
- val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
- listAbstractClass -> Set(nilAbstractClass, consAbstractClass)
- )
-
- val listVal = Variable(FreshIdentifier("tempVar"))
- val listLeonDeclaration = LeonDeclaration(
- ImmediateExpression( "tempVar", listVal ),
- TypeTransformer(listAbstractClass), listAbstractClass
- )
-
- val classMap: Map[Identifier, ClassType] = Map(
- listClassId -> listAbstractClass,
- nilClassId -> nilAbstractClass,
- consClassId -> consAbstractClass
- )
+ import RefinementExamples._
describe("A variable refiner with list ADT") {
it("should refine if variable is not Nil") {
- Given("a VariableRefiner")
- val variableRefiner = new VariableRefiner(
+ Given("a VariableRefiner based on structure")
+ val variableRefiner = new VariableRefinerStructure(
directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
)
@@ -77,7 +50,7 @@ class VariableRefinerTest extends FunSpec with GivenWhenThen {
listLeonDeclaration.expression, TypeTransformer(consAbstractClass), consAbstractClass
) :: Nil
)) {
- variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
+ variableRefiner.refine(CaseClassInstanceOf(nilAbstractClassDef, listVal),
BooleanLiteral(true),
allDeclarations
)
@@ -85,7 +58,7 @@ class VariableRefinerTest extends FunSpec with GivenWhenThen {
And("after 2nd consequtive call, nothing should happen")
expectResult((false, allDeclarations)) {
- variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
+ variableRefiner.refine(CaseClassInstanceOf(nilAbstractClassDef, listVal),
BooleanLiteral(true),
allDeclarations)
}
diff --git a/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala b/src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
similarity index 83%
rename from src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
rename to src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
index 5fe37005b69230ef3dd3a03d09be6f34a35367c6..c6e63bab0beff80a73487183fca725f8e09321da 100644
--- a/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/refinement/VariableSolverRefinerTest.scala
@@ -1,4 +1,5 @@
package leon.test.condabd
+package refinement
import scala.util.Random
@@ -20,6 +21,7 @@ import util._
class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
import Scaffold._
+ import RefinementExamples._
val lesynthTestDir = "testcases/condabd/test/lesynth/"
@@ -66,7 +68,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
directSubclassMap, declarations, classMap, solver, reporter
)
- val res = variableRefiner.checkRefinements(
+ val res = variableRefiner.refine(
isEmpty(listVal),
isEmpty(listVal),
declarations
@@ -79,7 +81,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
And("after 2nd consequtive call, nothing should happen")
expectResult((false, res._2)) {
- val res2 = variableRefiner.checkRefinements(
+ val res2 = variableRefiner.refine(
isEmpty(listVal),
isEmpty(listVal),
res._2
@@ -122,7 +124,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
directSubclassMap, declarations, classMap, solver, reporter
)
- val res = variableRefiner.checkRefinements(
+ val res = variableRefiner.refine(
hasContent(listVal),
hasContent(listVal),
declarations
@@ -135,7 +137,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
And("after 2nd consequtive call, nothing should happen")
expectResult((false, res._2)) {
- val res2 = variableRefiner.checkRefinements(
+ val res2 = variableRefiner.refine(
hasContent(listVal),
hasContent(listVal),
res._2
@@ -186,7 +188,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
directSubclassMap, declarations, classMap, solver, reporter
)
- val res = variableRefiner.checkRefinements(
+ val res = variableRefiner.refine(
isEmptyBad(listVal),
isEmptyBad(listVal),
declarations
@@ -194,7 +196,7 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
Then("declarations should not be updated")
expectResult((false, res._2)) {
- val res2 = variableRefiner.checkRefinements(
+ val res2 = variableRefiner.refine(
isEmptyBad(listVal),
isEmptyBad(listVal),
res._2
@@ -206,28 +208,4 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
}
- private def buildClassMap(program: Program) = {
- val listAbstractClassDef = program.definedClasses.find(_.id.name == "List").
- get.asInstanceOf[AbstractClassDef]
-
- val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
- get.asInstanceOf[CaseClassDef]
-
- val consAbstractClassDef = program.definedClasses.find(_.id.name == "Cons").
- get.asInstanceOf[CaseClassDef]
-
- val directSubclassMap: Map[ClassType, Set[ClassType]] = Map(
- AbstractClassType(listAbstractClassDef) ->
- Set(CaseClassType(nilAbstractClassDef), CaseClassType(consAbstractClassDef))
- )
-
- val classMap: Map[Identifier, ClassType] = Map(
- listAbstractClassDef.id -> AbstractClassType(listAbstractClassDef),
- nilAbstractClassDef.id -> CaseClassType(nilAbstractClassDef),
- consAbstractClassDef.id -> CaseClassType(consAbstractClassDef)
- )
-
- (directSubclassMap, AbstractClassType(listAbstractClassDef), classMap)
- }
-
}