From 857317fc4b19601ad07a6551eb2874cebb7e81b7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 24 Oct 2012 16:47:09 +0200
Subject: [PATCH] Make sure model is complete, simplify rule
---
src/main/scala/leon/synthesis/Rules.scala | 55 +++++++++++------------
1 file changed, 25 insertions(+), 30 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 1765c44f3..d5151cfca 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -38,41 +38,36 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
val p = task.problem
- p.phi match {
- case TopLevelAnds(exprs) =>
- val candidates = exprs.collect {
- case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
- (x, e, eq)
- case eq @ Equals(e, Variable(x)) if (p.xs contains x) && !(variablesOf(e) contains x) =>
- (x, e, eq)
- }
-
- if (!candidates.isEmpty) {
- val (x, e, eq) = candidates.head
+ val TopLevelAnds(exprs) = p.phi
- val others = exprs.filter(_ != eq)
- val oxs = p.xs.filter(_ != x)
+ val candidates = exprs.collect {
+ case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ (x, e, eq)
+ case eq @ Equals(e, Variable(x)) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ (x, e, eq)
+ }
- val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs)
+ if (!candidates.isEmpty) {
+ val (x, e, eq) = candidates.head
- val onSuccess: List[Solution] => Solution = {
- case List(Solution(pre, term, sc)) =>
- if (oxs.isEmpty) {
- Solution(pre, Tuple(e :: Nil), sc)
- } else {
- Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))), sc)
- }
- case _ => Solution.none
- }
+ val others = exprs.filter(_ != eq)
+ val oxs = p.xs.filter(_ != x)
- List(task.decompose(this, List(newProblem), onSuccess, 100))
- } else {
- Nil
- }
+ val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs)
+ val onSuccess: List[Solution] => Solution = {
+ case List(Solution(pre, term, sc)) =>
+ if (oxs.isEmpty) {
+ Solution(pre, Tuple(e :: Nil), sc)
+ } else {
+ Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))), sc)
+ }
+ case _ => Solution.none
+ }
- case _ =>
- Nil
+ List(task.decompose(this, List(newProblem), onSuccess, 100))
+ } else {
+ Nil
}
}
}
@@ -87,7 +82,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
synth.solveSAT(p.phi) match {
case (Some(true), model) =>
- List(task.solveUsing(this, Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200), 200))
+ List(task.solveUsing(this, Solution(BooleanLiteral(true), Tuple(p.xs.map(id => model.getOrElse(id, simplestValue(Variable(id))))).setType(tpe), 200), 200))
case (Some(false), model) =>
List(task.solveUsing(this, Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200), 200))
case _ =>
--
GitLab