Skip to content
Snippets Groups Projects
Commit 43c45c32 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Fix bug in CEGIS

parent 796f08ed
No related branches found
No related tags found
No related merge requests found
...@@ -448,14 +448,15 @@ abstract class CEGISLike(name: String) extends Rule(name) { ...@@ -448,14 +448,15 @@ abstract class CEGISLike(name: String) extends Rule(name) {
} }
val innerSol = outerExprToInnerExpr(outerSol) val innerSol = outerExprToInnerExpr(outerSol)
val cnstr = letTuple(p.xs, innerSol, innerPhi) val cnstr = letTuple(p.xs, innerSol, innerPhi)
cTreeFd.fullBody = innerSol
timers.testForProgram.start()
def withBindings(e: Expr) = p.pc.bindings.foldRight(e){ def withBindings(e: Expr) = p.pc.bindings.foldRight(e){
case ((id, v), bd) => let(id, outerExprToInnerExpr(v), bd) case ((id, v), bd) => let(id, outerExprToInnerExpr(v), bd)
} }
cTreeFd.fullBody = withBindings(innerSol) // FIXME! This shouldnt be needed... Solution around should be somehow used
timers.testForProgram.start()
val boundCnstr = withBindings(cnstr) val boundCnstr = withBindings(cnstr)
val res = ex match { val res = ex match {
...@@ -482,6 +483,8 @@ abstract class CEGISLike(name: String) extends Rule(name) { ...@@ -482,6 +483,8 @@ abstract class CEGISLike(name: String) extends Rule(name) {
case EvaluationResults.EvaluatorError(err) => case EvaluationResults.EvaluatorError(err) =>
debug("Error testing CE: "+err) debug("Error testing CE: "+err)
//println(s"InnerSol: $innerSol")
//println(s"Constr : $boundCnstr")
None None
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment