Skip to content
Snippets Groups Projects
Commit a330dede authored by Manos Koukoutos's avatar Manos Koukoutos Committed by Etienne Kneuss
Browse files

Some SMTLib tweaking

parent a3216570
No related branches found
No related tags found
No related merge requests found
...@@ -64,17 +64,17 @@ trait SMTLIBTarget { ...@@ -64,17 +64,17 @@ trait SMTLIBTarget {
// Corresponds to a smt map, not a leon/scala array // Corresponds to a smt map, not a leon/scala array
// Should NEVER escape past SMT-world // Should NEVER escape past SMT-world
case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree private[smtlib] case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
// Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array) // Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
// Should NEVER escape past SMT-world // Should NEVER escape past SMT-world
case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr { private[smtlib] case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr {
val getType = RawArrayType(keyTpe, default.getType) val getType = RawArrayType(keyTpe, default.getType)
} }
def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match { def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
case SetType(base) => case SetType(base) =>
assert(r.default == BooleanLiteral(false) && r.keyTpe == base) require(r.default == BooleanLiteral(false) && r.keyTpe == base)
finiteSet(r.elems.keySet, base) finiteSet(r.elems.keySet, base)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment