diff --git a/project/Sbt.scala b/project/Sbt.scala index 3fb03a64a..c434c5098 100644 --- a/project/Sbt.scala +++ b/project/Sbt.scala @@ -74,7 +74,7 @@ object Sbt extends Build // cross versioning lazy val crossSub = baseProject(utilPath / "cross", "Cross") settings(inConfig(Compile)(Transform.crossGenSettings): _*) // A logic with restricted negation as failure for a unique, stable model - lazy val logicSub = baseProject(utilPath / "logic", "Logic").dependsOn(collectionSub, relationSub) + lazy val logicSub = testedBaseProject(utilPath / "logic", "Logic").dependsOn(collectionSub, relationSub) /* **** Intermediate-level Modules **** */ diff --git a/util/logic/src/test/scala/sbt/logic/Test.scala b/util/logic/src/test/scala/sbt/logic/Test.scala index 49836998a..cf50ef9fd 100644 --- a/util/logic/src/test/scala/sbt/logic/Test.scala +++ b/util/logic/src/test/scala/sbt/logic/Test.scala @@ -1,7 +1,40 @@ package sbt package logic -object Test { + import org.scalacheck._ + import Prop.secure + import Logic.{LogicException, Matched} + +object LogicTest extends Properties("Logic") +{ + import TestClauses._ + + property("Handles trivial resolution.") = secure( expect(trivial, Set(A) ) ) + property("Handles less trivial resolution.") = secure( expect(lessTrivial, Set(B,A,D)) ) + property("Handles cycles without negation") = secure( expect(cycles, Set(F,A,B)) ) + property("Handles basic exclusion.") = secure( expect(excludedPos, Set()) ) + property("Handles exclusion of head proved by negation.") = secure( expect(excludedNeg, Set()) ) + // TODO: actually check ordering, probably as part of a check that dependencies are satisifed + property("Properly orders results.") = secure( expect(ordering, Set(B,A,C,E,F))) + property("Detects cyclic negation") = secure( + Logic.reduceAll(badClauses, Set()) match { + case Right(res) => false + case Left(err: Logic.CyclicNegation) => true + case Left(err) => error(s"Expected cyclic error, got: $err") + } + ) + + def expect(result: Either[LogicException, Matched], expected: Set[Atom]) = result match { + case Left(err) => false + case Right(res) => + val actual = res.provenSet + (actual == expected) || error(s"Expected to prove $expected, but actually proved $actual") + } +} + +object TestClauses +{ + val A = Atom("A") val B = Atom("B") val C = Atom("C")