diff --git a/src/it/scala/inox/DatastructureUtils.scala b/src/it/scala/inox/DatastructureUtils.scala new file mode 100644 index 0000000000000000000000000000000000000000..67a7d8a1ae9336aa7fcfb141593e4822e8037e6c --- /dev/null +++ b/src/it/scala/inox/DatastructureUtils.scala @@ -0,0 +1,36 @@ +/* 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)) +} diff --git a/src/it/scala/inox/solvers/unrolling/BagSuite.scala b/src/it/scala/inox/solvers/unrolling/BagSuite.scala new file mode 100644 index 0000000000000000000000000000000000000000..77db57dbbe0d7050437eb7ae132fe14467fb6854 --- /dev/null +++ b/src/it/scala/inox/solvers/unrolling/BagSuite.scala @@ -0,0 +1,105 @@ +/* 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) + } +} diff --git a/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala b/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala index e231792e228d99d32b8f58bb53735c449a23ffa7..93247b65c205bf4a9a935fbd2c1756d97c2356ea 100644 --- a/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala +++ b/src/it/scala/inox/solvers/unrolling/FunctionEqualitySuite.scala @@ -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) diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala index 70fcc7b3a385aa673cf7551c2c7df7db3876358f..fbf3c29ad4fe8e699d46dba038c4eeaf4d56c8c2 100644 --- a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala +++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala @@ -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) diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala index 1981602bce539fab266c2bd06729f8fbc405fcdc..c7dcf1f3721439dd3e85f69fe649ca2327c3a9d2 100644 --- a/src/main/scala/inox/ast/DSL.scala +++ b/src/main/scala/inox/ast/DSL.scala @@ -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) diff --git a/src/main/scala/inox/solvers/theories/BagEncoder.scala b/src/main/scala/inox/solvers/theories/BagEncoder.scala index 86e527993f70e590b617598a6be5533df6b491d2..61b19be6d5c5ff85569ac98194cdda560ffc63bd 100644 --- a/src/main/scala/inox/solvers/theories/BagEncoder.scala +++ b/src/main/scala/inox/solvers/theories/BagEncoder.scala @@ -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)) ||