diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala index 9e3c20a9e3997f1f65d874e6761aff54935f9761..f544092f97d3ca0a4e4d660d8a3254d59c2b2942 100644 --- a/src/main/scala/leon/solvers/ADTManager.scala +++ b/src/main/scala/leon/solvers/ADTManager.scala @@ -127,20 +127,6 @@ class ADTManager(ctx: LeonContext) { discovered += (t -> DataType(freshId("Unit"), Seq(Constructor(freshId("Unit"), t, Nil)))) } - case at @ ArrayType(base) => - if (!(discovered contains t) && !(defined contains t)) { - val sym = freshId("array") - - val c = Constructor(freshId(sym.name), at, List( - (freshId("size"), Int32Type), - (freshId("content"), RawArrayType(Int32Type, base)) - )) - - discovered += (at -> DataType(sym, Seq(c))) - - findDependencies(base) - } - case tp @ TypeParameter(id) => if (!(discovered contains t) && !(defined contains t)) { val sym = freshId(id.name) diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala index bb576468c591b0a738f6d30f8c74b3a133f543ae..34328af602a7ff3c448dfa9fdef4ddfd1e5c4c68 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala @@ -432,37 +432,10 @@ trait SMTLIBTarget extends Interruptible { val selector = selectors.toB((tpe, i - 1)) FunctionApplication(selector, Seq(toSMT(t))) - case al @ ArrayLength(a) => - val tpe = normalizeType(a.getType) - val selector = selectors.toB((tpe, 0)) - - FunctionApplication(selector, Seq(toSMT(a))) - case al @ RawArraySelect(a, i) => ArraysEx.Select(toSMT(a), toSMT(i)) case al @ RawArrayUpdated(a, i, e) => ArraysEx.Store(toSMT(a), toSMT(i), toSMT(e)) - - case al @ ArraySelect(a, i) => - val tpe = normalizeType(a.getType) - - val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(toSMT(a))) - - ArraysEx.Select(scontent, toSMT(i)) - - - case al @ ArrayUpdated(a, i, e) => - val tpe = normalizeType(a.getType) - - val sa = toSMT(a) - val ssize = FunctionApplication(selectors.toB((tpe, 0)), Seq(sa)) - val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(sa)) - - val newcontent = ArraysEx.Store(scontent, toSMT(i), toSMT(e)) - - val constructor = constructors.toB(tpe) - FunctionApplication(constructor, Seq(ssize, newcontent)) - case ra @ RawArrayValue(keyTpe, elems, default) => val s = declareSort(ra.getType) @@ -475,18 +448,6 @@ trait SMTLIBTarget extends Interruptible { res - case a @ FiniteArray(elems, oDef, size) => - val tpe @ ArrayType(to) = normalizeType(a.getType) - declareSort(tpe) - - val default: Expr = oDef.getOrElse(simplestValue(to)) - - val arr = toSMT(RawArrayValue(Int32Type, elems.map { - case (k, v) => IntLiteral(k) -> v - }, default)) - - FunctionApplication(constructors.toB(tpe), List(toSMT(size), arr)) - /** * ===== Map operations ===== */ diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala index 15b654e7f5fdc26e900c5de36bd766e07498f331..06a2c18b338c6711fac77547d879a80a1a2cff37 100644 --- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala @@ -417,49 +417,6 @@ trait AbstractZ3Solver extends Z3Solver { val tester = testers.toB(cct) tester(rec(e)) - case al @ RawArraySelect(a, i) => - z3.mkSelect(rec(a), rec(i)) - case al @ RawArrayUpdated(a, i, e) => - z3.mkStore(rec(a), rec(i), rec(e)) - - case al @ ArraySelect(a, i) => - val tpe = normalizeType(a.getType) - - val sa = rec(a) - val content = selectors.toB((tpe, 1))(sa) - - z3.mkSelect(content, rec(i)) - - case al @ ArrayUpdated(a, i, e) => - val tpe = normalizeType(a.getType) - - val sa = rec(a) - val ssize = selectors.toB((tpe, 0))(sa) - val scontent = selectors.toB((tpe, 1))(sa) - - val newcontent = z3.mkStore(scontent, rec(i), rec(e)) - - val constructor = constructors.toB(tpe) - - constructor(ssize, newcontent) - - case al @ ArrayLength(a) => - val tpe = normalizeType(a.getType) - val sa = rec(a) - selectors.toB((tpe, 0))(sa) - - case arr @ FiniteArray(elems, oDefault, length) => - val at @ ArrayType(base) = normalizeType(arr.getType) - typeToSort(at) - - val default = oDefault.getOrElse(simplestValue(base)) - - val ar = rec(RawArrayValue(Int32Type, elems.map { - case (i, e) => IntLiteral(i) -> e - }, default)) - - constructors.toB(at)(rec(length), ar) - case f @ FunctionInvocation(tfd, args) => z3.mkApp(functionDefToDecl(tfd), args.map(rec): _*) @@ -510,6 +467,10 @@ trait AbstractZ3Solver extends Z3Solver { val withNeg = z3.mkArrayMap(minus, rec(b1), rec(b2)) z3.mkArrayMap(div, z3.mkArrayMap(plus, withNeg, z3.mkArrayMap(abs, withNeg)), all2) + case al @ RawArraySelect(a, i) => + z3.mkSelect(rec(a), rec(i)) + case al @ RawArrayUpdated(a, i, e) => + z3.mkStore(rec(a), rec(i), rec(e)) case RawArrayValue(keyTpe, elems, default) => val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))