From c7105dbd0c66ea2c0a44412ca3599611ce1333b4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 12 Nov 2012 18:41:45 +0100
Subject: [PATCH] CEGIS
---
.../scala/leon/synthesis/Heuristics.scala | 55 +++++++++++++++++--
1 file changed, 50 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index ce34ab79c..3f9f54859 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -273,11 +273,56 @@ class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 5
def closedFormula = And(f :: recTerms.keySet.map(id => Not(Variable(id))).toList)
}
- println("Formula is: "+p.phi)
- val initF = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x))) // Set to expand on xs
- println("unroll 1: "+initF.unroll.closedFormula)
- println("unroll 2: "+initF.unroll.unroll.closedFormula)
+ var result: Option[RuleResult] = None
- RuleInapplicable
+ var ass = p.as.toSet
+
+ var lastF = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x)))
+ var currentF = lastF.unroll
+ var unrolings = 0
+ do {
+ println("Was: "+lastF.closedFormula)
+ println("Now Trying : "+currentF.closedFormula)
+
+ val tpe = TupleType(p.xs.map(_.getType))
+
+ var i = 0;
+ var maxTries = 10;
+
+ var predicates: Seq[Expr] = Seq()
+
+ while (result.isEmpty && i < maxTries) {
+ val phi = And(currentF.closedFormula +: predicates)
+ synth.solver.solveSAT(phi) match {
+ case (Some(true), satModel) =>
+ val notAss = satModel.keySet.filterNot(ass)
+ val satXsModel = satModel.filterKeys(notAss)
+
+ val newPhi = valuateWithModelIn(phi, notAss, satModel)
+
+ synth.solver.solveSAT(Not(newPhi)) match {
+ case (Some(true), invalidModel) =>
+ // Found as such as the xs break, refine predicates
+ predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
+
+ case (Some(false), _) =>
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+
+ case _ =>
+ }
+
+ case (Some(false), _) =>
+ case _ =>
+ }
+
+ i += 1
+ }
+
+ lastF = currentF
+ currentF = lastF.unroll
+ unrolings += 1
+ } while(unrolings < 5 && lastF != currentF && result.isEmpty)
+
+ result.getOrElse(RuleInapplicable)
}
}
--
GitLab