From 8205d9245e3ecfe9d0995616c2d2c91d7bb0a71e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 22 Nov 2012 18:50:35 +0100
Subject: [PATCH] Optimistic ground now uses path condition, IntInduction
pushes case to path condition instead of formula
---
src/main/scala/leon/synthesis/heuristics/IntInduction.scala | 4 ++--
src/main/scala/leon/synthesis/rules/OptimisticGround.scala | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index f75e44e6d..28cb94845 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -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 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 subGT = Problem(inductOn :: postXs, And(Seq(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, p.c)), newPhi, 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 = {
case List(base, gt, lt) =>
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index ac005a380..8225c7b6c 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -22,7 +22,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
var predicates: Seq[Expr] = Seq()
while (result.isEmpty && i < maxTries) {
- val phi = And(p.phi +: predicates)
+ val phi = And(p.c +: p.phi +: predicates)
//println("SOLVING " + phi + " ...")
synth.solver.solveSAT(phi) match {
case (Some(true), satModel) =>
--
GitLab