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

Fix non-bijective sorts in AbstractZ3Solver

parent eb93ed8a
No related branches found
No related tags found
No related merge requests found
...@@ -92,13 +92,14 @@ trait AbstractZ3Solver extends Solver { ...@@ -92,13 +92,14 @@ trait AbstractZ3Solver extends Solver {
// Bijections between Leon Types/Functions/Ids to Z3 Sorts/Decls/ASTs // Bijections between Leon Types/Functions/Ids to Z3 Sorts/Decls/ASTs
protected val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]() protected val functions = new IncrementalBijection[TypedFunDef, Z3FuncDecl]()
protected val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]() protected val lambdas = new IncrementalBijection[FunctionType, Z3FuncDecl]()
protected val sorts = new IncrementalBijection[TypeTree, Z3Sort]()
protected val variables = new IncrementalBijection[Expr, Z3AST]() protected val variables = new IncrementalBijection[Expr, Z3AST]()
protected val constructors = new IncrementalBijection[TypeTree, Z3FuncDecl]() protected val constructors = new IncrementalBijection[TypeTree, Z3FuncDecl]()
protected val selectors = new IncrementalBijection[(TypeTree, Int), Z3FuncDecl]() protected val selectors = new IncrementalBijection[(TypeTree, Int), Z3FuncDecl]()
protected val testers = new IncrementalBijection[TypeTree, Z3FuncDecl]() protected val testers = new IncrementalBijection[TypeTree, Z3FuncDecl]()
protected val sorts = new IncrementalMap[TypeTree, Z3Sort]()
var isInitialized = false var isInitialized = false
protected[leon] def initZ3(): Unit = { protected[leon] def initZ3(): Unit = {
if (!isInitialized) { if (!isInitialized) {
...@@ -108,11 +109,11 @@ trait AbstractZ3Solver extends Solver { ...@@ -108,11 +109,11 @@ trait AbstractZ3Solver extends Solver {
functions.clear() functions.clear()
lambdas.clear() lambdas.clear()
sorts.clear()
variables.clear() variables.clear()
constructors.clear() constructors.clear()
selectors.clear() selectors.clear()
testers.clear() testers.clear()
sorts.reset()
prepareSorts() prepareSorts()
...@@ -136,7 +137,7 @@ trait AbstractZ3Solver extends Solver { ...@@ -136,7 +137,7 @@ trait AbstractZ3Solver extends Solver {
adtManager.defineADT(t) match { adtManager.defineADT(t) match {
case Left(adts) => case Left(adts) =>
declareDatatypes(adts.toSeq) declareDatatypes(adts.toSeq)
sorts.toB(normalizeType(t)) sorts(normalizeType(t))
case Right(conflicts) => case Right(conflicts) =>
conflicts.foreach { declareStructuralSort } conflicts.foreach { declareStructuralSort }
...@@ -217,15 +218,15 @@ trait AbstractZ3Solver extends Solver { ...@@ -217,15 +218,15 @@ trait AbstractZ3Solver extends Solver {
// assumes prepareSorts has been called.... // assumes prepareSorts has been called....
protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match { protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match {
case Int32Type | BooleanType | IntegerType | RealType | CharType => case Int32Type | BooleanType | IntegerType | RealType | CharType =>
sorts.toB(oldtt) sorts(oldtt)
case tpe @ (_: ClassType | _: ArrayType | _: TupleType | _: TypeParameter | UnitType) => case tpe @ (_: ClassType | _: ArrayType | _: TupleType | _: TypeParameter | UnitType) =>
sorts.cachedB(tpe) { sorts.cached(tpe) {
declareStructuralSort(tpe) declareStructuralSort(tpe)
} }
case tt @ SetType(base) => case tt @ SetType(base) =>
sorts.cachedB(tt) { sorts.cached(tt) {
z3.mkSetSort(typeToSort(base)) z3.mkSetSort(typeToSort(base))
} }
...@@ -233,7 +234,7 @@ trait AbstractZ3Solver extends Solver { ...@@ -233,7 +234,7 @@ trait AbstractZ3Solver extends Solver {
typeToSort(RawArrayType(fromType, library.optionType(toType))) typeToSort(RawArrayType(fromType, library.optionType(toType)))
case rat @ RawArrayType(from, to) => case rat @ RawArrayType(from, to) =>
sorts.cachedB(rat) { sorts.cached(rat) {
val fromSort = typeToSort(from) val fromSort = typeToSort(from)
val toSort = typeToSort(to) val toSort = typeToSort(to)
...@@ -241,7 +242,7 @@ trait AbstractZ3Solver extends Solver { ...@@ -241,7 +242,7 @@ trait AbstractZ3Solver extends Solver {
} }
case ft @ FunctionType(from, to) => case ft @ FunctionType(from, to) =>
sorts.cachedB(ft) { sorts.cached(ft) {
val symbol = z3.mkFreshStringSymbol(ft.toString) val symbol = z3.mkFreshStringSymbol(ft.toString)
z3.mkUninterpretedSort(symbol) z3.mkUninterpretedSort(symbol)
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment