From bed47535533014efee145065ad9d82e6b485dd6e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 4 Dec 2012 17:56:30 +0100
Subject: [PATCH] Further improve speed of Cegis
---
.../scala/leon/synthesis/rules/Cegis.scala | 26 +++++++++----------
1 file changed, 12 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 80171e36d..1580e81b7 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -161,7 +161,10 @@ case object CEGIS extends Rule("CEGIS", 150) {
var continue = !clauses.isEmpty
+ //println("Unrolling #"+unrolings+" bss size: "+bss.size)
+
while (result.isEmpty && continue) {
+ //println("Looking for CE...")
//println("-"*80)
//println(basePhi)
@@ -214,25 +217,20 @@ case object CEGIS extends Rule("CEGIS", 150) {
solver1.pop()
- 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 counterexemple = substAll(freshCss ++ ceIn, And(Seq(unrolling.program, unrolling.phi)))
-
- //println("#"*80)
- //println(currentF.phi)
- //println(substAll(freshCss ++ ceIn, currentF.phi))
-
- // Found as such as the xs break, refine predicates
- solver1.assertCnstr(counterexemple)
- solver2.assertCnstr(counterexemple)
-
if (unsatCore.isEmpty) {
continue = false
} 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 counterexemple = substAll(freshCss ++ ceIn, And(Seq(unrolling.program, unrolling.phi)))
+
+ solver1.assertCnstr(counterexemple)
+ solver2.assertCnstr(counterexemple)
+
//predicates = Not(And(unsatCore.toSeq)) +: counterexemple +: predicates
solver1.assertCnstr(Not(And(unsatCore.toSeq)))
+ solver2.assertCnstr(Not(And(unsatCore.toSeq)))
}
case Some(false) =>
--
GitLab