From 953a1799ba7a9517df8221fb0478bba9d4d6afe5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Tue, 10 May 2011 15:58:38 +0000
Subject: [PATCH] trust Z3 that it will return distinct models when asked.
---
cp-demo/SortedList.scala | 17 ++++++++++++++++-
src/cp/Terms.scala | 6 ++++--
2 files changed, 20 insertions(+), 3 deletions(-)
diff --git a/cp-demo/SortedList.scala b/cp-demo/SortedList.scala
index 87e93798d..7fcd0d73e 100644
--- a/cp-demo/SortedList.scala
+++ b/cp-demo/SortedList.scala
@@ -1,4 +1,5 @@
import cp.Definitions._
+import cp.Terms._
@spec object Lists {
sealed abstract class List
@@ -15,6 +16,13 @@ import cp.Definitions._
case Cons(x, Nil()) => true
case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
}
+ // def isSorted(l : List) : Boolean = l match {
+ // case Nil() => true
+ // case Cons(x, xs) => xs match {
+ // case Nil() => true
+ // case Cons(y, _) => x <= y && isSorted(xs)
+ // }
+ // }
def valuesWithin(l: List, lower: Int, upper: Int) : Boolean = l match {
case Nil() => true
@@ -29,7 +37,14 @@ object SortedList {
val len = if (args.isEmpty) 3 else args(0).toInt
val set = scala.collection.mutable.Set[List]()
- for (list <- ((l : List) => isSorted(l) && valuesWithin(l, 0, len) && size(l) == len).findAll)
+ val c1 : Constraint1[List] = (l : List) => isSorted(l)
+ val c2 : Constraint1[List] = (l : List) => valuesWithin(l, 0, len)
+ val c3 : Constraint1[List] = (l : List) => size(l) == len
+
+ val combined = c1 && c2 && c3
+
+ // for (list <- ((l : List) => isSorted(l) && valuesWithin(l, 0, len) && size(l) == len).findAll)
+ for (list <- combined.findAll)
set += list
println("size : " + set.size)
diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala
index e87074319..3891786a4 100644
--- a/src/cp/Terms.scala
+++ b/src/cp/Terms.scala
@@ -1555,7 +1555,8 @@ object Terms {
nextModel = Some(Some(completeModel))
val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))))
toCheck = negate(newModelEqualities)
- toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall{ case (k,v) => completeModel.get(k) == Some(v) }))
+ // accumulate negations of models in evaluator
+ // toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall{ case (k,v) => completeModel.get(k) == Some(v) }))
true
case Some(true) =>
// there are definitely no more solutions
@@ -1593,7 +1594,8 @@ object Terms {
val newModelEqualities = And(outputVariables.map(ov => Equals(Variable(ov), completeModel(ov))))
toCheck = negate(newModelEqualities)
- toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall{ case (k,v) => completeModel.get(k) == Some(v) }))
+ // accumulate negations of models in evaluator
+ // toUseAsEvaluator = toUseAsEvaluator.map(e => ((m : Map[Identifier,Expr]) => e(m) && !m.forall(p => completeModel.get(p._1) == Some(p._2))))
completeModel
case Some(true) =>
// Definitely no more solutions
--
GitLab