diff --git a/testcases/SatFun.scala b/testcases/SatFun.scala
index 8dc7995c17f63c141052ec630c79b19b2d5b7997..6bc9ed4e259e0acbc478d989cee163423f6eb910 100644
--- a/testcases/SatFun.scala
+++ b/testcases/SatFun.scala
@@ -8,7 +8,7 @@ object SatFun {
case class Not(f: Formula) extends Formula
case class Var(i: Int) extends Formula
- //vars are numbered from 1 to n, and Not(Var(n)) is represented as -n
+ //vars are numbered from 2 to n+1, and Not(Var(n)) is represented as -n. 1 is true and -1 is false
sealed abstract class VarList
case class VarCons(head: Int, tail: VarList) extends VarList
case class VarNil() extends VarList
@@ -47,44 +47,40 @@ object SatFun {
case VarLit(b) => b
}
- def vars(formula: Formula): Set[Int] = formula match {
- case Var(n) => Set(n)
- case Not(f) => vars(f)
- case And(f1, f2) => vars(f1) ++ vars(f2)
- case Or(f1, f2) => vars(f1) ++ vars(f2)
- }
-
def concatClauses(cll1: ClauseList, cll2: ClauseList): ClauseList = cll1 match {
case ClauseCons(cl, tail) => ClauseCons(cl, concatClauses(tail, cll2))
case ClauseNil() => cll2
- case cl@ClauseLit(_) => ClauseCons(cl, clls)
+ case ClauseLit(b) => ClauseCons(VarLit(b), cll2)
}
def concatVars(l1: VarList, l2: VarList): VarList = l1 match {
case VarCons(v, vs) => VarCons(v, concatVars(vs, l2))
case VarNil() => l2
- case v@VarLit(_) => VarCons(v, vs)
+ case VarLit(b) => if(b) VarCons(1, l2) else VarCons(-1, l2)
}
def distributeClause(cl: VarList, cll: ClauseList): ClauseList = cll match {
case ClauseCons(cl2, cl2s) => ClauseCons(concatVars(cl, cl2), distributeClause(cl, cl2s))
case ClauseNil() => ClauseNil()
- case cl@ClauseLit(b) => ClauseCons(cl, clls)
+ case ClauseLit(b) => if(b) ClauseCons(VarCons(1, cl), ClauseNil()) else ClauseCons(VarCons(-1, cl), ClauseNil())
}
def distribute(cll1: ClauseList, cll2: ClauseList): ClauseList = cll1 match {
case ClauseCons(cl, cls) => concatClauses(distributeClause(cl, cll2), distribute(cls, cll2))
case ClauseNil() => cll2
+ case ClauseLit(b) => distributeClause(VarLit(b), cll2)
}
def negateClauses(cll: ClauseList): ClauseList = cll match {
case ClauseCons(cl, cls) => ClauseCons(negateVars(cl), negateClauses(cls))
case ClauseNil() => ClauseNil()
+ case ClauseLit(b) => ClauseLit(!b)
}
def negateVars(lst: VarList): VarList = lst match {
case VarCons(v, vs) => VarCons(-v, negateVars(vs))
case VarNil() => VarNil()
+ case VarLit(b) => VarLit(!b)
}
def cnfNaive(formula: Formula): ClauseList = formula match {
@@ -104,7 +100,6 @@ object SatFun {
case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
}
-
def dnfNaive(formula: Formula): ClauseList = formula match {
case And(f1, f2) => {
val dnf1 = dnfNaive(f1)
@@ -122,47 +117,80 @@ object SatFun {
case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
}
+ def property1(formula: Formula, assignment: Map[Int, Boolean]): Boolean = {
+ val dnfFormula = dnfNaive(formula)
+ eval(formula, assignment) == evalDnf(dnfFormula, assignment)
+ } ensuring(_ == true)
+
+ def vars(formula: Formula): Set[Int] = formula match {
+ case Var(n) => Set(n)
+ case Not(f) => vars(f)
+ case And(f1, f2) => vars(f1) ++ vars(f2)
+ case Or(f1, f2) => vars(f1) ++ vars(f2)
+ }
def isContradictory(clause: VarList, vars: Set[Int]): Boolean = clause match {
- case VarCons(v, vs) => vars.contains(-v) || isContradictory(vs, vars ++ Set(v))
+ case VarCons(v, vs) => vars.contains(-v) || vars.contains(-1) || isContradictory(vs, vars ++ Set(v))
case VarNil() => false
+ case VarLit(b) => !b
}
-
def isSatDnf(clauses: ClauseList): Boolean = clauses match {
case ClauseCons(cl, cls) => !isContradictory(cl, Set.empty) || isSatDnf(cls)
case ClauseNil() => false
+ case ClauseLit(b) => b
}
-
+ //for substitute we assume we are dealing with a cnf formula
def substitute(formula: ClauseList, variable: Int, value: Boolean): ClauseList = formula match {
case ClauseNil() => ClauseNil()
- case ClauseCons(cl, cls) =>
+ case ClauseCons(cl, cls) => ClauseCons(substitute(cl, variable, value), substitute(cls, variable, value))
+ case ClauseLit(b) => ClauseLit(b)
}
def substitute(vars: VarList, variable: Int, value: Boolean): VarList = vars match {
case VarNil() => VarNil()
- case VarCons(v, vs) => if(v == variable)
- }
-
- def choose(formula: ClauseList): Int = {
- formula.head.head
+ case VarLit(b) => VarLit(b)
+ case VarCons(v, vs) =>
+ if (v == variable && value) VarLit(true)
+ else if(v == variable && !value) substitute(vs, variable, value)
+ else if(v == -variable && value) substitute(vs, variable, value)
+ else if(v == -variable && !value) VarLit(true)
+ else VarCons(v, substitute(vs, variable, value))
+ }
+
+ def choose(formula: ClauseList): Int = formula match {
+ case ClauseCons(varList, cls) => varList match {
+ case VarCons(head, vs) => head
+ case VarNil() => 0
+ case VarLit(b) => 0
+ }
+ case ClauseNil() => 0
+ case ClauseLit(b) => 0
}
- def dpll(formula: ClauseList): Boolean = {
-
+ def dpll(formula: ClauseList): Boolean = formula match {
+ case ClauseNil() => true
+ case ClauseLit(b) => b
+ case _ => {
+ val chosenVar = choose(formula)
+ val lhs = dpll(substitute(formula, chosenVar, true))
+ val rhs = dpll(substitute(formula, chosenVar, false))
+ lhs || rhs
+ }
}
- def main(args: Array[String]) {
- val f1 = And(Var(1), Or(Var(1), Not(Var(2)), Var(3)), Var(2), Not(Var(3)))
- val dnff1 = clauses2list(dnfNaive(f1))
- val vars1 = vars(f1)
- vars.foreach(v => {
-
- })
- println(f1 + " translated in dnf as:\n\t" + dnff1.mkString("\n\t"))
- }
+// def main(args: Array[String]) {
+// val f1 = And(Var(1), Or(Var(1), Not(Var(2)), Var(3)), Var(2), Not(Var(3)))
+// val dnff1 = clauses2list(dnfNaive(f1))
+// val vars1 = vars(f1)
+// vars.foreach(v => {
+//
+//
+// })
+// println(f1 + " translated in dnf as:\n\t" + dnff1.mkString("\n\t"))
+// }
//some non-leon functions to test the program with scala
object False {
@@ -188,9 +216,11 @@ object SatFun {
def clause2list(cl: VarList): List[Int] = cl match {
case VarCons(v, vs) => v :: clause2list(vs)
case VarNil() => Nil
+ case VarLit(b) => if(b) List(1) else List(-1)
}
def clauses2list(cll: ClauseList): List[List[Int]] = cll match {
case ClauseCons(cl, cls) => clause2list(cl) :: clauses2list(cls)
case ClauseNil() => Nil
+ case ClauseLit(b) => if(b) List(List(1)) else List(List(-1))
}
}