Skip to content
Snippets Groups Projects
Commit 8205d924 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Optimistic ground now uses path condition, IntInduction pushes case to path...

Optimistic ground now uses path condition, IntInduction pushes case to path condition instead of formula
parent 08543021
No related branches found
No related tags found
No related merge requests found
...@@ -26,8 +26,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50) ...@@ -26,8 +26,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50)
val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi) val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
val subBase = Problem(List(), p.c, subst(origId -> IntLiteral(0), p.phi), 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 subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.c)), newPhi, p.xs)
val subLT = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs) val subLT = Problem(inductOn :: postXs, And(Seq(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, p.c)), newPhi, p.xs)
val onSuccess: List[Solution] => Solution = { val onSuccess: List[Solution] => Solution = {
case List(base, gt, lt) => case List(base, gt, lt) =>
......
...@@ -22,7 +22,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn ...@@ -22,7 +22,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
var predicates: Seq[Expr] = Seq() var predicates: Seq[Expr] = Seq()
while (result.isEmpty && i < maxTries) { while (result.isEmpty && i < maxTries) {
val phi = And(p.phi +: predicates) val phi = And(p.c +: p.phi +: predicates)
//println("SOLVING " + phi + " ...") //println("SOLVING " + phi + " ...")
synth.solver.solveSAT(phi) match { synth.solver.solveSAT(phi) match {
case (Some(true), satModel) => case (Some(true), satModel) =>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment