Skip to content
Snippets Groups Projects
Commit e6e0ddce authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Bag encoder tests (and fixes)

parent 8b18f681
No related branches found
No related tags found
No related merge requests found
/* Copyright 2009-2016 EPFL, Lausanne */
package inox
trait DatastructureUtils {
import trees._
import dsl._
val listID = FreshIdentifier("List")
val consID = FreshIdentifier("Cons")
val nilID = FreshIdentifier("Nil")
val head = FreshIdentifier("head")
val tail = FreshIdentifier("tail")
val List = mkSort(listID)("A")(Seq(consID, nilID))
val Nil = mkConstructor(nilID)("A")(Some(listID))(_ => Seq.empty)
val Cons = mkConstructor(consID)("A")(Some(listID)) {
case Seq(aT) => Seq(ValDef(head, aT), ValDef(tail, List(aT)))
}
val optionID = FreshIdentifier("Option")
val someID = FreshIdentifier("Some")
val noneID = FreshIdentifier("None")
val v = FreshIdentifier("value")
val option = mkSort(optionID)("A")(Seq(someID, noneID))
val none = mkConstructor(noneID)("A")(Some(optionID))(_ => Seq.empty)
val some = mkConstructor(someID)("A")(Some(optionID)) {
case Seq(aT) => Seq(ValDef(v, aT))
}
val baseSymbols = NoSymbols.withADTs(Seq(List, Nil, Cons, option, none, some))
}
/* Copyright 2009-2016 EPFL, Lausanne */
package inox
package solvers
package unrolling
class BagSuite extends SolvingTestSuite with DatastructureUtils {
import trees._
import dsl._
override val configurations = for {
solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
feelingLucky <- Seq(false, true)
} yield Seq(
optSelectedSolvers(Set(solverName)),
optCheckModels(true),
optFeelingLucky(feelingLucky),
optTimeout(300),
ast.optPrintUniqueIds(true)
)
override def optionsString(options: Options): String = {
"solvr=" + options.findOptionOrDefault(optSelectedSolvers).head + " " +
"lucky=" + options.findOptionOrDefault(optFeelingLucky)
}
val bagID = FreshIdentifier("bag")
val bag = mkFunDef(bagID)("A") { case Seq(aT) => (
Seq("l" :: List(aT)), BagType(aT), { case Seq(l) =>
if_ (l.isInstOf(Cons(aT))) {
let("c" :: Cons(aT), l.asInstOf(Cons(aT))) { c =>
BagAdd(E(bagID)(aT)(c.getField(tail)), c.getField(head))
}
} else_ {
FiniteBag(Seq.empty, aT)
}
})
}
val splitID = FreshIdentifier("split")
val split = mkFunDef(splitID)("A") { case Seq(aT) => (
Seq("l" :: List(aT)), T(List(aT), List(aT)), { case Seq(l) =>
let(
"res" :: T(List(aT), List(aT)),
if_ (l.isInstOf(Cons(aT)) && l.asInstOf(Cons(aT)).getField(tail).isInstOf(Cons(aT))) {
let(
"tuple" :: T(List(aT), List(aT)),
E(splitID)(aT)(l.asInstOf(Cons(aT)).getField(tail).asInstOf(Cons(aT)).getField(tail))
) { tuple => E(
Cons(aT)(l.asInstOf(Cons(aT)).getField(head), tuple._1),
Cons(aT)(l.asInstOf(Cons(aT)).getField(tail).asInstOf(Cons(aT)).getField(head), tuple._2)
)}
} else_ {
E(l, Nil(aT)())
}
) { res => Assume(bag(aT)(l) === BagUnion(bag(aT)(res._1), bag(aT)(res._2)), res) }
})
}
val symbols = baseSymbols.withFunctions(Seq(bag, split))
test("Finite model finding 1") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = TypeParameter.fresh("A")
val b = ("bag" :: BagType(aT)).toVariable
val clause = Not(Equals(b, FiniteBag(Seq.empty, aT)))
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
test("Finite model finding 2") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = TypeParameter.fresh("A")
val b = ("bag" :: BagType(aT)).toVariable
val elem = ("elem" :: aT).toVariable
val clause = Not(Equals(b, FiniteBag(Seq(elem -> IntegerLiteral(1)), aT)))
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
test("Finite model finding 3") { ctx =>
val program = InoxProgram(ctx, symbols)
val aT = TypeParameter.fresh("A")
val b = ("bag" :: BagType(aT)).toVariable
val Seq(e1, v1, e2, v2) = Seq("e1" :: aT, "v1" :: IntegerType, "e2" :: aT, "v2" :: IntegerType).map(_.toVariable)
val clause = And(Seq(
Not(Equals(b, FiniteBag(Seq(e1 -> v1, e2 -> v2), aT))),
Not(Equals(MultiplicityInBag(e1, b), IntegerLiteral(0))),
Not(Equals(MultiplicityInBag(e2, b), IntegerLiteral(0)))
))
assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(clause).isSAT)
}
test("split preserves content") { ctx =>
val program = InoxProgram(ctx, symbols)
val Let(vd, body, Assume(pred, _)) = split.fullBody
val clause = Let(vd, body, pred)
assert(SimpleSolverAPI(SolverFactory.default(program)).solveVALID(clause) contains true)
}
}
......@@ -4,22 +4,10 @@ package inox
package solvers
package unrolling
class FunctionEqualitySuite extends SolvingTestSuite {
class FunctionEqualitySuite extends SolvingTestSuite with DatastructureUtils {
import inox.trees._
import dsl._
val v = FreshIdentifier("value")
val optionID = FreshIdentifier("Option")
val someID = FreshIdentifier("Some")
val noneID = FreshIdentifier("None")
val option = mkSort(optionID)("A")(Seq(someID, noneID))
val none = mkConstructor(noneID)("A")(Some(optionID))(_ => Seq.empty)
val some = mkConstructor(someID)("A")(Some(optionID)) {
case Seq(aT) => Seq(ValDef(v, aT))
}
val f = FreshIdentifier("f")
val mmapID = FreshIdentifier("MMap")
val mmap = mkConstructor(mmapID)("A","B")(None) {
......@@ -33,10 +21,9 @@ class FunctionEqualitySuite extends SolvingTestSuite {
})
}
val symbols = new Symbols(
Map(containsID -> contains),
Map(optionID -> option, someID -> some, noneID -> none, mmapID -> mmap)
)
val symbols = baseSymbols
.withFunctions(Seq(contains))
.withADTs(Seq(mmap))
test("simple theorem") { ctx =>
val program = InoxProgram(ctx, symbols)
......
......@@ -4,23 +4,10 @@ package inox
package solvers
package unrolling
class InductiveUnrollingSuite extends SolvingTestSuite {
class InductiveUnrollingSuite extends SolvingTestSuite with DatastructureUtils {
import trees._
import dsl._
val listID = FreshIdentifier("List")
val consID = FreshIdentifier("Cons")
val nilID = FreshIdentifier("Nil")
val head = FreshIdentifier("head")
val tail = FreshIdentifier("tail")
val List = mkSort(listID)("A")(Seq(consID, nilID))
val Nil = mkConstructor(nilID)("A")(Some(listID))(_ => Seq.empty)
val Cons = mkConstructor(consID)("A")(Some(listID)) {
case Seq(aT) => Seq(ValDef(head, aT), ValDef(tail, T(listID)(aT)))
}
val sizeID = FreshIdentifier("size")
val appendID = FreshIdentifier("append")
val flatMapID = FreshIdentifier("flatMap")
......@@ -164,11 +151,8 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
})
}
val symbols = new Symbols(
Map(sizeID -> sizeFd, appendID -> append, flatMapID -> flatMap, assocID -> associative,
forallID -> forall, contentID -> content, partitionID -> partition, sortID -> sort),
Map(listID -> List, consID -> Cons, nilID -> Nil)
)
val symbols = baseSymbols
.withFunctions(Seq(sizeFd, append, flatMap, associative, forall, content, partition, sort))
test("size(x) == 0 is satisfiable") { ctx =>
val program = InoxProgram(ctx, symbols)
......
......@@ -195,6 +195,10 @@ trait DSL {
def apply(tps: Type*) = ADTType(id, tps.toSeq)
}
implicit class ADTTypeBuilder(adt: ADTDefinition) {
def apply(tps: Type*) = ADTType(adt.id, tps.toSeq)
}
implicit class FunctionTypeBuilder(to: Type) {
def =>: (from: Type) =
FunctionType(Seq(from), to)
......
......@@ -85,8 +85,8 @@ trait BagEncoder extends TheoryEncoder {
Seq("b1" :: Bag(aT), "b2" :: Bag(aT)),
BooleanType, { case Seq(b1, b2) =>
forall("x" :: aT) { x =>
let("f1x" :: aT, b1.getField(f)(x)) { f1x =>
let("f2x" :: aT, b2.getField(f)(x)) { f2x =>
let("f1x" :: IntegerType, b1.getField(f)(x)) { f1x =>
let("f2x" :: IntegerType, b2.getField(f)(x)) { f2x =>
f1x === f2x ||
(!(b1.getField(keys) contains x) && f2x === E(BigInt(0))) ||
(f1x === E(BigInt(0)) && !(b2.getField(keys) contains x)) ||
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment