From 77a1990461865ca81ebb0b9748e3b9eeaf7c8271 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sat, 15 Dec 2012 03:01:03 +0100
Subject: [PATCH] It might be that the counter example does not specify some
input variables if they are not used in the formula.
---
src/main/scala/leon/synthesis/rules/Cegis.scala | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 6dd2b83b6..cfa39a2d6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -191,7 +191,9 @@ case object CEGIS extends Rule("CEGIS", 150) {
//println("#"*80)
val invalidModel = solver2.getModel
- val fixedAss = And(ass.map(a => Equals(Variable(a), invalidModel(a))).toSeq)
+ val fixedAss = And(ass.collect {
+ case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
+ }.toSeq)
solver1.push()
solver1.assertCnstr(fixedAss)
@@ -222,7 +224,10 @@ case object CEGIS extends Rule("CEGIS", 150) {
} else {
val freshCss = unrolling.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
- val ceIn = ass.map(id => id -> invalidModel(id))
+ val ceIn = ass.collect {
+ case id if invalidModel contains id => id -> invalidModel(id)
+ }
+
val counterexemple = substAll(freshCss ++ ceIn, And(Seq(unrolling.program, unrolling.phi)))
solver1.assertCnstr(counterexemple)
--
GitLab