Commit ab11e6e4 authored by sroussel's avatar sroussel
Browse files

Corrected cnf computation : the id of the anonymous variable that was added to...

Corrected cnf computation : the id of the anonymous variable that was added to the cnf list was not the good one. I used a cachedVar in order to solver the issue.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1687 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent bdf7f0ad
......@@ -61,9 +61,10 @@ object Logic {
isAlreadyInCnf(this) match {
case (true, Some(x)) => x
case _ => {
val next = nextAnonymousVar
val translated = tseitinListSimple(this, List())._2
assert(!(_createdVars isEmpty))
List(_createdVars.last) :: translated
List(next) :: translated
}
}
}
......@@ -151,11 +152,17 @@ object Logic {
private var _createdVars = List[AnonymousVariable]()
/** create new propositional variables for translation into CNF */
private def newVar = {
private def newVar = if(_cachedVar != null) {val tmp = _cachedVar; _cachedVar = null; tmp} else uncachedNewVar
def uncachedNewVar = {
val v = new AnonymousVariable
_createdVars = v :: _createdVars
v
}
private def nextAnonymousVar = if(_cachedVar == null) {_cachedVar = uncachedNewVar; _cachedVar} else _cachedVar;
var _cachedVar = uncachedNewVar
/** n-ary conjunction. */
def and(l: BoolExp*): BoolExp = and(l.toList)
......
......@@ -8,66 +8,138 @@ object testLogic {
val f = True //> f : org.sat4j.scala.Logic.True.type = True
val f2 = 'y & 'x //> f2 : org.sat4j.scala.Logic.And = And(Ident(y),Ident(x))
val f3 = f2 | 'y //> f3 : org.sat4j.scala.Logic.Or = Or(And(Ident(y),Ident(x)),Ident(y))
val f4 = 'x & 'y | ('z -> 'd) //> f4 : org.sat4j.scala.Logic.Or = Or(And(Ident(x),Ident(y)),Or(Not(Ident(z)),
//| Ident(d)))
val f5 = (f3 & True) | 'y //> f5 : org.sat4j.scala.Logic.Or = Or(And(Or(And(Ident(y),Ident(x)),Ident(y)),
//| True),Ident(y))
val cnf = (True & 'x) toCnfList //> cnf : List[List[org.sat4j.scala.Logic.BoolExp]] = List(List(Ident(_nv0)), L
//| ist(Not(True), Not(Ident(x)), Ident(_nv0)), List(True, Not(Ident(_nv0))), Li
//| st(Ident(x), Not(Ident(_nv0))))
PrettyPrint(cnf) //> res0: String = "
//| _nv0
//| ~True ~x _nv0
//| True ~_nv0
//| x ~_nv0"
PrettyPrint(simplifyCnf(cnf)) //> res1: String = "
//| _nv0
//| ~x _nv0
//| x ~_nv0"
val f2 = 'y & 'x(1,2,3) //> f2 : org.sat4j.scala.Logic.And = And(Ident('y),IndexedIdent('x,List(1, 2, 3
//| )))
val f3 = f2 | 'y //> f3 : org.sat4j.scala.Logic.Or = Or(And(Ident('y),IndexedIdent('x,List(1, 2,
//| 3))),Ident('y))
val f4 = 'x & 'y | ('z implies 'd) //> f4 : org.sat4j.scala.Logic.Or = Or(And(Ident('x),Ident('y)),Implies(Ident('
//| z),Ident('d)))
val f5 = (f3 & True) | 'y //> f5 : org.sat4j.scala.Logic.Or = Or(And(Or(And(Ident('y),IndexedIdent('x,Lis
//| t(1, 2, 3))),Ident('y)),True),Ident('y))
val c1 = f + f2 + f3 === 4 //> c1 : org.sat4j.scala.Logic.CardEQ = CardEQ(List(True, And(Ident('y),Indexed
//| Ident('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),I
//| dent('y))),4)
val c2 = f + f2 + f3 < 10 //> c2 : org.sat4j.scala.Logic.CardLT = CardLT(List(True, And(Ident('y),Indexed
//| Ident('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),I
//| dent('y))),10)
val c3 = f + f2 + f3 > 11 //> c3 : org.sat4j.scala.Logic.CardGT = CardGT(List(True, And(Ident('y),Indexed
//| Ident('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),I
//| dent('y))),11)
val c4 = f + f2 + f3 <= 42 //> c4 : org.sat4j.scala.Logic.CardLE = CardLE(List(True, And(Ident('y),Indexed
//| Ident('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),I
//| dent('y))),42)
val c5 = f + f2 + f3 >= 666 //> c5 : org.sat4j.scala.Logic.CardGE = CardGE(List(True, And(Ident('y),Indexed
//| Ident('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),I
//| dent('y))),666)
val x32 = c5 implies c1 //> x32 : org.sat4j.scala.Logic.Implies = Implies(CardGE(List(True, And(Ident('
//| y),IndexedIdent('x,List(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1,
//| 2, 3))),Ident('y))),666),CardEQ(List(True, And(Ident('y),IndexedIdent('x,Li
//| st(1, 2, 3))), Or(And(Ident('y),IndexedIdent('x,List(1, 2, 3))),Ident('y))),
//| 4))
// TODO : doit-on permettre cela?
val x35 = 'x > 0 //> x35 : org.sat4j.scala.Logic.CardGT = CardGT(List(Ident('x)),0)
println(PrettyPrint(f4)) //> (('x & 'y) | ('z implies 'd))
println(PrettyPrint(f5)) //> (((('y & 'x(1,2,3)) | 'y) & True) | 'y)
println(PrettyPrint(c1)) //> (True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) === 4)
println(PrettyPrint(c2)) //> (True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) < 10)
println(PrettyPrint(c3)) //> (True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) > 11)
println(PrettyPrint(c4)) //> (True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) <= 42)
println(PrettyPrint(c5)) //> (True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) >= 666)
println(PrettyPrint(x32)) //> ((True + ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) >= 666) implies (True +
//| ('y & 'x(1,2,3)) + (('y & 'x(1,2,3)) | 'y) === 4))
isSat(f4) //> res0: (Boolean, Option[Map[Nothing,Boolean]]) = (true,Some(Map('x -> true, '
//| y -> true, 'z -> false, 'd -> false)))
val cnf = (True & 'x) toCnfList //> cnf : List[List[org.sat4j.scala.Logic.BoolExp]] = List(List(True), List(Ide
//| nt('x)))
PrettyPrint(cnf) //> res1: String = "
//| True
//| 'x"
PrettyPrint(simplifyCnf(cnf)) //> res2: String = "
//| 'x"
encode(simplifyCnf(cnf)) //> res2: (List[List[Int]], Map[String,Int]) = (List(List(1), List(-2, 1), List(
//| 2, -1)),Map(_nv0 -> 1, x -> 2))
encode(simplifyCnf(cnf)) //> res3: (List[List[Int]], Map[org.sat4j.scala.Logic.BoolExp,Int]) = (List(List
//| (1)),Map(Ident('x) -> 1))
encode(f5) //> res3: (List[List[Int]], Map[String,Int]) = (List(List(1), List(2, 3, -1), Li
//| st(-2, 1), List(-3, 1), List(-4, 2), List(4, -2), List(5, 3, -4), List(-5, 4
//| ), List(-3, 4), List(-3, -6, 5), List(3, -5), List(6, -5)),Map(x -> 6, _nv1
//| -> 2, y -> 3, _nv2 -> 4, _nv3 -> 5, _nv0 -> 1))
encode(f5) //> res4: (List[List[Int]], Map[org.sat4j.scala.Logic.BoolExp,Int]) = (List(List
//| (1), List(2, 3, -1), List(-2, 1), List(-3, 1), List(-4, 2), List(4, -2), Lis
//| t(5, 3, -4), List(-5, 4), List(-3, 4), List(-3, -6, 5), List(3, -5), List(6,
//| -5)),Map(Ident('y) -> 3, _nv#1 -> 1, _nv#2 -> 2, _nv#3 -> 4, IndexedIdent('
//| x,List(1, 2, 3)) -> 6, _nv#4 -> 5))
encode (f4) //> res4: (List[List[Int]], Map[String,Int]) = (List(List(1), List(2, 2, -1), Li
//| st(-2, 1), List(-2, 1), List(-3, -4, 2), List(3, -2), List(4, -2), List(5, 6
//| , -2), List(-5, 2), List(-6, 2), List(-7, -5), List(7, 5)),Map(x -> 3, _nv1
//| -> 2, y -> 4, _nv2 -> 5, _nv0 -> 1, z -> 7, d -> 6))
encode (f4) //> res5: (List[List[Int]], Map[org.sat4j.scala.Logic.BoolExp,Int]) = (List(List
//| (1), List(2, 3, -1), List(-2, 1), List(-3, 1), List(-4, -5, 2), List(4, -2),
//| List(5, -2), List(-6, 7, -3), List(6, 3), List(-7, 3)),Map(Ident('x) -> 4,
//| Ident('y) -> 5, _nv#1 -> 1, Ident('d) -> 7, _nv#2 -> 2, _nv#3 -> 3, Ident('z
//| ) -> 6))
encode ('a | 'b) //> res6: (List[List[Int]], Map[org.sat4j.scala.Logic.BoolExp,Int]) = (List(List
//| (1, 2)),Map(Ident('a) -> 1, Ident('b) -> 2))
encode ('a | 'b) //> res5: (List[List[Int]], Map[String,Int]) = (List(List(1), List(2, 3, -1), Li
//| st(-2, 1), List(-3, 1)),Map(_nv0 -> 1, a -> 2, b -> 3))
isSat ('x & ~'x) //> res7: (Boolean, Option[Map[Nothing,Boolean]]) = (false,None)
isSat ('x & ~'x) //> res6: (Boolean, Option[List[String]]) = (false,None)
isSat ('a | 'b) //> res7: (Boolean, Option[List[String]]) = (true,Some(List(a, ~b)))
isSat ('a | 'b) //> res8: (Boolean, Option[Map[Nothing,Boolean]]) = (true,Some(Map('a -> false,
//| 'b -> true)))
isValid ('a | 'b) //> res8: (Boolean, Option[List[String]]) = (false,Some(List(~a, ~b)))
isValid ('a | 'b) //> res9: (Boolean, Option[Map[Nothing,Boolean]]) = (false,Some(Map('a -> false,
//| 'b -> false)))
isValid( 'a | ~'a) //> res9: (Boolean, Option[List[String]]) = (true,None)
isValid( 'a | ~'a) //> res10: (Boolean, Option[Map[Nothing,Boolean]]) = (true,None)
val l = 'a & 'b //> l : org.sat4j.scala.Logic.And = And(Ident('a),Ident('b))
PrettyPrint(l) //> res11: String = ('a & 'b)
isSat (l & ~l) //> res12: (Boolean, Option[Map[Nothing,Boolean]]) = (false,None)
val x = 'x //> x : Symbol = 'x
isValid (l) //> res13: (Boolean, Option[Map[Nothing,Boolean]]) = (false,Some(Map('a -> fals
//| e, 'b -> false)))
isSat ('a implies 'a) //> res14: (Boolean, Option[Map[Nothing,Boolean]]) = (true,Some(Map('a -> false
//| )))
val liste = List('a -> 'b, 'c iff 'd) //> liste : List[Product with Serializable] = List(('a,'b), Iff(Ident('c),Iden
//| t('d)))
('a & 'b iff 'a | 'b) toCnfList //> res15: List[List[org.sat4j.scala.Logic.BoolExp]] = List(List(_nv#2), List(N
//| ot(_nv#3), _nv#4, Not(_nv#2)), List(_nv#3, Not(_nv#4), Not(_nv#2)), List(_n
//| v#3, _nv#4, _nv#2), List(Not(_nv#3), Not(_nv#4), _nv#2), List(Not(Ident('a)
//| ), Not(Ident('b)), _nv#3), List(Ident('a), Not(_nv#3)), List(Ident('b), Not
//| (_nv#3)), List(Ident('a), Ident('b), Not(_nv#4)), List(Not(Ident('a)), _nv#
//| 4), List(Not(Ident('b)), _nv#4))
PrettyPrint (~('a & 'b) toCnfList) //> res16: String = "
//| _nv#5
//| ~_nv#6 ~_nv#5
//| _nv#6 _nv#5
//| ~'a ~'b _nv#6
//| 'a ~_nv#6
//| 'b ~_nv#6"
}
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment