From 5d1c0022c871ffaa822d48c8149b35ffe01d9117 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 20 Feb 2023 02:31:23 +0100 Subject: [PATCH 01/15] Starting an attempt to do a conditional flyweight pattern without annotations --- src/main/scala/Config.scala | 2 + src/main/scala/decider/Decider.scala | 6 +- src/main/scala/decider/PathConditions.scala | 4 +- .../decider/TermToSMTLib2Converter.scala | 6 +- .../scala/decider/TermToZ3APIConverter.scala | 6 +- src/main/scala/reporting/Converter.scala | 4 +- src/main/scala/reporting/Formatters.scala | 4 +- .../scala/resources/PropertyInterpreter.scala | 20 +- .../QuantifiedPropertyInterpreter.scala | 2 +- src/main/scala/rules/Evaluator.scala | 30 ++- src/main/scala/rules/Executor.scala | 2 +- src/main/scala/rules/MagicWandSupporter.scala | 4 +- .../scala/rules/QuantifiedChunkSupport.scala | 18 +- src/main/scala/rules/StateConsolidator.scala | 4 +- .../FunctionPreconditionTransformer.scala | 4 +- src/main/scala/state/Terms.scala | 234 ++++++++++++------ .../supporters/ExpressionTranslator.scala | 6 +- ...pAccessReplacingExpressionTranslator.scala | 4 +- 18 files changed, 224 insertions(+), 136 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 754e61d0b..76b173803 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -550,6 +550,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))} .getOrElse(0) + lazy val useFlyweight: Boolean = false + val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth", descr = "Maximal number of nested heuristics applications (default: 3)", default = Some(3), diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 6b389d49b..ef0c64552 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -270,10 +270,10 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => } private def isKnownToBeTrue(t: Term) = t match { - case True() => true + case True => true // case eq: BuiltinEquals => eq.p0 == eq.p1 /* WARNING: Blocking trivial equalities might hinder axiom triggering. */ case _ if pcs.assumptions contains t => true - case q: Quantification if q.body == True() => true + case q: Quantification if q.body == True => true case _ => false } @@ -379,7 +379,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def statistics(): Map[String, String] = prover.statistics() - override def generateModel(): Unit = proverAssert(False(), None) + override def generateModel(): Unit = proverAssert(False, None) override def getModel(): Model = prover.getModel() diff --git a/src/main/scala/decider/PathConditions.scala b/src/main/scala/decider/PathConditions.scala index fef19cf65..3f09e0a17 100644 --- a/src/main/scala/decider/PathConditions.scala +++ b/src/main/scala/decider/PathConditions.scala @@ -142,7 +142,7 @@ private trait LayeredPathConditionStackLike { protected def conditionalized(layers: Stack[PathConditionStackLayer]): Seq[Term] = { var unconditionalTerms = Vector.empty[Term] var conditionalTerms = Vector.empty[Term] - var implicationLHS: Term = True() + var implicationLHS: Term = True for (layer <- layers.reverseIterator) { unconditionalTerms ++= layer.globalAssumptions @@ -181,7 +181,7 @@ private trait LayeredPathConditionStackLike { Quantification( quantifier, qvars, - Implies(layer.branchCondition.getOrElse(True()), And(layer.nonGlobalAssumptions -- ignores)), + Implies(layer.branchCondition.getOrElse(True), And(layer.nonGlobalAssumptions -- ignores)), triggers, name, isGlobal) diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala index 5449b90f9..32b0c1b9e 100644 --- a/src/main/scala/decider/TermToSMTLib2Converter.scala +++ b/src/main/scala/decider/TermToSMTLib2Converter.scala @@ -370,9 +370,9 @@ class TermToSMTLib2Converter else parens(text("- 0") <+> value(-n)) case Unit => "$Snap.unit" - case True() => "true" - case False() => "false" - case Null() => "$Ref.null" + case True => "true" + case False => "false" + case Null => "$Ref.null" case _: SeqNil => renderApp("Seq_empty", Seq(), literal.sort) case _: EmptySet => renderApp("Set_empty", Seq(), literal.sort) case _: EmptyMultiset => renderApp("Multiset_empty", Seq(), literal.sort) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 0560a5dd6..f1ba4da0c 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -212,9 +212,9 @@ class TermToZ3APIConverter else ctx.mkUnaryMinus(ctx.mkInt((-n).toString())) } - case True() => ctx.mkTrue() - case False() => ctx.mkFalse() - case Null() => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref")) + case True => ctx.mkTrue() + case False => ctx.mkFalse() + case Null => ctx.mkConst("$Ref.null", ctx.mkUninterpretedSort("$Ref")) case Unit => ctx.mkConst(getUnitConstructor) case _: SeqNil => createApp("Seq_empty", Seq(), l.sort) case _: EmptySet => createApp("Set_empty", Seq(), l.sort) diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index c41f6edef..3d310fe71 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -151,7 +151,7 @@ object Converter { lazy val symbolConverter: SymbolConverter = new DefaultSymbolConverter //some tokens used for naming model entries in a more maintainable way lazy val snapUnitId: String = termconverter.convert(Unit) - lazy val nullRefId: String = termconverter.convert(Null()) + lazy val nullRefId: String = termconverter.convert(Null) def getFunctionValue(model: Model, fname: String, @@ -254,7 +254,7 @@ object Converter { case Unit => UnprocessedModelEntry(ConstantEntry(snapUnitId)) case IntLiteral(x) => LitIntEntry(x) case t: BooleanLiteral => LitBoolEntry(t.value) - case Null() => VarEntry(model.entries(nullRefId).toString, sorts.Ref) + case Null => VarEntry(model.entries(nullRefId).toString, sorts.Ref) case Var(_, sort) => val key: String = term.toString val entry: Option[ModelEntry] = model.entries.get(key) diff --git a/src/main/scala/reporting/Formatters.scala b/src/main/scala/reporting/Formatters.scala index a8cd164e1..f7248fe49 100644 --- a/src/main/scala/reporting/Formatters.scala +++ b/src/main/scala/reporting/Formatters.scala @@ -58,7 +58,7 @@ class DefaultStateFormatter extends StateFormatter { case c: BuiltinEquals if c.p0.isInstanceOf[Combine] || c.p1.isInstanceOf[Combine] => true - case Not(BuiltinEquals(_, Null())) => true + case Not(BuiltinEquals(_, Null)) => true case _ => false }.mkString("(", ", ", ")") } @@ -92,7 +92,7 @@ class DefaultStateFormatter extends StateFormatter { val filteredPcs = pcs.filterNot { case c: BuiltinEquals if c.p0.isInstanceOf[Combine] || c.p1.isInstanceOf[Combine] => true - case Not(BuiltinEquals(_, Null())) => true + case Not(BuiltinEquals(_, Null)) => true case _ => false } if (filteredPcs.isEmpty) "[]" else filteredPcs.mkString("[\"", "\",\"", "\"]") diff --git a/src/main/scala/resources/PropertyInterpreter.scala b/src/main/scala/resources/PropertyInterpreter.scala index 7d86dbc3b..596a3a64d 100644 --- a/src/main/scala/resources/PropertyInterpreter.scala +++ b/src/main/scala/resources/PropertyInterpreter.scala @@ -14,10 +14,10 @@ abstract class PropertyInterpreter { protected def buildPathCondition[K <: Kind](expression: PropertyExpression[K], info: Info): Term = expression match { // Literals - case True() => terms.True() - case False() => terms.False() + case True() => terms.True + case False() => terms.False case PermissionLiteral(numerator, denominator) => buildPermissionLiteral(numerator, denominator) - case Null() => terms.Null() + case Null() => terms.Null // Boolean operators case Not(expr) => terms.Not(buildPathCondition(expr, info)) @@ -62,7 +62,7 @@ abstract class PropertyInterpreter { the right-hand side is not evaluated. */ protected def buildAnd(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = { buildPathCondition(left, info) match { - case leftTerm: terms.False => leftTerm + case f@terms.False => f case leftTerm => terms.And(leftTerm, buildPathCondition(right, info)) } } @@ -71,7 +71,7 @@ abstract class PropertyInterpreter { the right-hand side is not evaluated. */ protected def buildOr(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = { buildPathCondition(left, info) match { - case leftTerm: terms.True => leftTerm + case t@terms.True => t case leftTerm => terms.Or(leftTerm, buildPathCondition(right, info)) } } @@ -80,26 +80,26 @@ abstract class PropertyInterpreter { the right-hand side is not evaluated. */ protected def buildImplies(left: PropertyExpression[kinds.Boolean], right: PropertyExpression[kinds.Boolean], info: Info) = { buildPathCondition(left, info) match { - case terms.False() => terms.True() + case terms.False => terms.True case leftTerm => terms.Implies(leftTerm, buildPathCondition(right, info)) } } protected def buildEquals[K <: EquatableKind](left: PropertyExpression[K], right: PropertyExpression[K], info: Info) = { (left, right) match { - case (Null(), Null()) => terms.True() + case (Null(), Null()) => terms.True case (ArgumentAccess(cv1), ArgumentAccess(cv2)) => val args1 = extractArguments(cv1, info) val args2 = extractArguments(cv2, info) if (args1 == args2) { // if all arguments are the same, they are definitely equal - terms.True() + terms.True } else { // else return argument-wise equal terms.And(args1.zip(args2).map{ case (t1, t2) => t1 === t2 }) } - case (ArgumentAccess(cv), Null()) => terms.And(extractArguments(cv, info).map(_ === terms.Null())) - case (Null(), ArgumentAccess(cv)) => terms.And(extractArguments(cv, info).map(_ === terms.Null())) + case (ArgumentAccess(cv), Null()) => terms.And(extractArguments(cv, info).map(_ === terms.Null)) + case (Null(), ArgumentAccess(cv)) => terms.And(extractArguments(cv, info).map(_ === terms.Null)) case _ => terms.Equals(buildPathCondition(left, info), buildPathCondition(right, info)) } } diff --git a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala index 2f0ebfcce..3a72ee4dd 100644 --- a/src/main/scala/resources/QuantifiedPropertyInterpreter.scala +++ b/src/main/scala/resources/QuantifiedPropertyInterpreter.scala @@ -27,7 +27,7 @@ class QuantifiedPropertyInterpreter extends PropertyInterpreter { : Term = { val body = buildPathCondition(property.expression, Info(chunk, args, perms)).replace(chunk.quantifiedVars, args) val description = s"$qidPrefix-${property.name}" - val cond = if (argsUsed) condition else terms.True() + val cond = if (argsUsed) condition else terms.True argsUsed = false terms.Forall(qvars, terms.Implies(cond, body), triggers, description) } diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 27121c349..05450df76 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -149,10 +149,10 @@ object evaluator extends EvaluationRules { : VerificationResult = { val resultTerm = e match { - case _: ast.TrueLit => Q(s, True(), v) - case _: ast.FalseLit => Q(s, False(), v) + case _: ast.TrueLit => Q(s, True, v) + case _: ast.FalseLit => Q(s, False, v) - case _: ast.NullLit => Q(s, Null(), v) + case _: ast.NullLit => Q(s, Null, v) case ast.IntLit(bigval) => Q(s, IntLiteral(bigval), v) case ast.EqCmp(e0, e1) => evalBinOp(s, e0, e1, Equals, pve, v)(Q) @@ -241,7 +241,7 @@ object evaluator extends EvaluationRules { } val permCheck = if (s1.triggerExp) { - True() + True } else { val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr) IsPositive(totalPermissions) @@ -555,7 +555,7 @@ object evaluator extends EvaluationRules { val zippedArgs = argsWithIndex map (ai => (ai._1, ch.args(ai._2))) val argsPairWiseEqual = And(zippedArgs map {case (a1, a2) => a1 === a2}) - evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False()), None,body, false, pve, v1) ((s4, tImplies, v2) => + evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False), None,body, false, pve, v1) ((s4, tImplies, v2) => bindRcvrsAndEvalBody(s4, chs.tail, args, tImplies +: ts, v2)((s5, ts1, v3) => { v3.symbExLog.closeScope(uidImplies) Q(s5, ts1, v3) @@ -1073,11 +1073,11 @@ object evaluator extends EvaluationRules { joiner.join[Term, Term](s, v)((s1, v1, QB) => brancher.branch(s1, tLhs, eLhs, v1, fromShortCircuitingAnd)( (s2, v2) => eval(s2, eRhs, pve, v2)(QB), - (s2, v2) => QB(s2, True(), v2)) + (s2, v2) => QB(s2, True, v2)) )(entries => { assert(entries.length <= 2) val s1 = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s)) - val t = Implies(tLhs, entries.headOption.map(_.data).getOrElse(True())) + val t = Implies(tLhs, entries.headOption.map(_.data).getOrElse(True)) (s1, t) })(Q) } @@ -1134,6 +1134,18 @@ object evaluator extends EvaluationRules { } } + private def evalBinOp[T <: Term](s: State, + e0: ast.Exp, + e1: ast.Exp, + termOp: ((Term, Term)) => T, + pve: PartialVerificationError, + v: Verifier) + (Q: (State, T, Verifier) => VerificationResult) + : VerificationResult = { + + evalBinOp(s, e0, e1, (t0, t1) => termOp((t0, t1)), pve, v)(Q) + } + private def evalBinOp[T <: Term] (s: State, e0: ast.Exp, @@ -1522,8 +1534,8 @@ object evaluator extends EvaluationRules { // TODO: Find out and document why swapIfAnd is needed val (stop, swapIfAnd) = - if(constructor == Or) (True(), (a: brFun, b: brFun) => (a, b)) - else (False(), (a: brFun, b: brFun) => (b, a)) + if(constructor == Or) (True, (a: brFun, b: brFun) => (a, b)) + else (False, (a: brFun, b: brFun) => (b, a)) eval(s, exps.head, pve, v)((s1, t0, v1) => { t0 match { diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 88d796627..dbcb11139 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -367,7 +367,7 @@ object executor extends ExecutionRules { case ast.NewStmt(x, fields) => val tRcvr = v.decider.fresh(x) - v.decider.assume(tRcvr !== Null()) + v.decider.assume(tRcvr !== Null) val newChunks = fields map (field => { val p = FullPerm() val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ)) diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 5e0bbf3d3..771d077f4 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -155,10 +155,10 @@ object magicWandSupporter extends SymbolicExecutionRules { * and thus be unsound. Since fractional wands do not exist it is not necessary to equate their * snapshots. Also have a look at the comments in the packageWand and applyWand methods. */ - case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True() + case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True case (Some(ch1: NonQuantifiedChunk), Some(ch2: NonQuantifiedChunk)) => ch1.snap === ch2.snap case (Some(ch1: QuantifiedBasicChunk), Some(ch2: QuantifiedBasicChunk)) => ch1.snapshotMap === ch2.snapshotMap - case _ => True() + case _ => True } v.decider.assume(tEq) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 3e6c7b003..00ffa7fdc 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -424,7 +424,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val additionalFvfArgs = s.functionRecorderQuantifiedVariables() val sm = freshSnapshotMap(s, field, additionalFvfArgs, v) - val smDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(True()) + val smDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(True) val codomainQVarsInDomainOfSummarisingSm = SetIn(codomainQVar, Domain(field.name, sm)) val valueDefinitions = @@ -520,7 +520,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val effectiveCondition = And( - transformedOptSmDomainDefinitionCondition.getOrElse(True()), /* Alternatively: qvarInDomainOfSummarisingSm */ + transformedOptSmDomainDefinitionCondition.getOrElse(True), /* Alternatively: qvarInDomainOfSummarisingSm */ IsPositive(chunk.perm).replace(snapToCodomainTermsSubstitution)) Forall( @@ -877,7 +877,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { qidPrefix = qid, program = s.program) } else { - True() + True } v.decider.prover.comment("Check receiver injectivity") v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program)) @@ -1261,7 +1261,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { codomainQVars, relevantChunks, v1, - optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True()) else None, + optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True) else None, optQVarsInstantiations = Some(arguments)) val permsTaken = result match { case Complete() => rPerm @@ -1305,7 +1305,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { resource = resource, codomainQVars = codomainQVars, relevantChunks = relevantChunks, - optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True()) else None, + optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True) else None, optQVarsInstantiations = Some(arguments), v = v) val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1), @@ -1474,7 +1474,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { quantifiedDepletedCheck) } - (permissionConstraint.getOrElse(True()), depletedCheck) + (permissionConstraint.getOrElse(True), depletedCheck) } /* Misc */ @@ -1550,7 +1550,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val argsEqual: Term = if (args1.isEmpty) - True() + True else (args1 zip args2) .map(argsRenamed => argsRenamed._1 === argsRenamed._2) @@ -1627,8 +1627,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { imagesOfCodomains(idx) = img(codomainQVars) } else { // imageFunctions(idx) remains null, will be filtered out later. - imagesOfFcts(idx) = True() - imagesOfCodomains(idx) = True() + imagesOfFcts(idx) = True + imagesOfCodomains(idx) = True } } diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 373076b8a..c52882f28 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -207,8 +207,8 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol */ private def combineSnapshots(fr: FunctionRecorder, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = { (IsPositive(p1), IsPositive(p2)) match { - case (True(), b2) => (fr, t1, Implies(b2, t1 === t2)) - case (b1, True()) => (fr, t2, Implies(b1, t2 === t1)) + case (True, b2) => (fr, t1, Implies(b2, t1 === t2)) + case (b1, True) => (fr, t2, Implies(b1, t2 === t1)) case (b1, b2) => /* * Since it is not definitely known whether p1 and p2 are positive, diff --git a/src/main/scala/state/FunctionPreconditionTransformer.scala b/src/main/scala/state/FunctionPreconditionTransformer.scala index c21d23dfa..515d917b3 100644 --- a/src/main/scala/state/FunctionPreconditionTransformer.scala +++ b/src/main/scala/state/FunctionPreconditionTransformer.scala @@ -23,7 +23,7 @@ import viper.silver.ast object FunctionPreconditionTransformer { def transform(t: Term, p: ast.Program): Term = { val res = t match { - case _:Literal => True() + case _:Literal => True case And(ts) => And(transform(ts.head, p), Implies(ts.head, transform(And(ts.tail), p))) case Or(ts) => And(transform(ts.head, p), Implies(Not(ts.head), transform(Or(ts.tail), p))) case Implies(t0, t1) => And(transform(t0, p), Implies(t0, transform(t1, p))) @@ -32,7 +32,7 @@ object FunctionPreconditionTransformer { And(And(bindings.map(b => transform(b._2, p))), Let(bindings, transform(body, p))) case Quantification(_, vars, body, triggers, name, isGlobal, weight) => val tBody = transform(body, p) - if (tBody == True()) { + if (tBody == True) { tBody } else { // We assume well-definedness for *all* possible values even for existential quantifiers diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index e4b511b64..82caf52c4 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -7,13 +7,13 @@ package viper.silicon.state.terms import java.util.concurrent.atomic.AtomicInteger - import scala.annotation.tailrec import scala.reflect.ClassTag import viper.silver.ast import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.{Map, Stack, state, toMap} import viper.silicon.state.{Identifier, MagicWandChunk, MagicWandIdentifier, SortBasedIdentifier} +import viper.silicon.verifier.Verifier sealed trait Node { def toString: String @@ -376,6 +376,14 @@ trait BinaryOp[E] { override lazy val toString = s"$p0 $op $p1" } +trait ConditionalFlyweightBinaryOp[T] extends BinaryOp[Term] with ConditionalFlyweight[(Term, Term), T] with Term { + override val equalityDefiningMembers = (p0, p1) +} + +trait ConditionalFlyweightUnaryOp extends UnaryOp[Term] with ConditionalFlyweight[Term, ConditionalFlyweightUnaryOp] with Term { + override val equalityDefiningMembers = p +} + trait StructuralEqualityUnaryOp[E] extends UnaryOp[E] { override def equals(other: Any) = this.eq(other.asInstanceOf[AnyRef]) || (other match { @@ -415,6 +423,61 @@ trait StructuralEquality { self: AnyRef => })) } +trait ConditionalFlyweight[T, V] extends Term { self: AnyRef => + val equalityDefiningMembers: T + + override lazy val hashCode = if (Verifier.config.useFlyweight) + System.identityHashCode(this) + else + viper.silver.utility.Common.generateHashCode(equalityDefiningMembers) + + override def equals(other: Any): Boolean = { + if (Verifier.config.useFlyweight) { + this.eq(other.asInstanceOf[AnyRef]) + } else { + ( + this.eq(other.asInstanceOf[AnyRef]) + || (other match { + case se: ConditionalFlyweight[T, V] if this.getClass.eq(se.getClass) => + equalityDefiningMembers == se.equalityDefiningMembers + case _ => false + })) + } + } +} + + +trait ConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V]] extends GeneralConditionalFlyweightFactory[T, Term, V] + +trait GeneralConditionalFlyweightFactory[T, U <: Term, V <: U with ConditionalFlyweight[T, V]] extends AGeneralConditionalFlyweightFactory[T, T, U, V] { + def apply(v1: T): U = createIfNonExistent(v1) + +} + +trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U <: Term, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { + + import scala.collection.concurrent.TrieMap + + var pool = new TrieMap[T, V]() + + def createIfNonExistent(args: T): V = { + pool.get(args) match { + case Some(v) => v + case None => + val newInstance = actualCreate(args) + pool.addOne(args, newInstance) + newInstance + } + } + + def unapply(v: V): Option[T] = Some(v.equalityDefiningMembers) + + def actualCreate(args: T): V +} + + + + /* Literals */ sealed trait Literal extends Term @@ -431,7 +494,7 @@ case class IntLiteral(n: BigInt) extends ArithmeticTerm with Literal { override lazy val toString = n.toString() } -case class Null() extends Term with Literal { +case object Null extends Term with Literal { val sort = sorts.Ref override lazy val toString = "Null" } @@ -442,15 +505,15 @@ sealed trait BooleanLiteral extends BooleanTerm with Literal { } object BooleanLiteral extends (Boolean => BooleanLiteral) { - def apply(b: Boolean): BooleanLiteral = if (b) True() else False() + def apply(b: Boolean): BooleanLiteral = if (b) True else False } -case class True() extends BooleanLiteral { +case object True extends BooleanLiteral { val value = true override lazy val toString = "True" } -case class False() extends BooleanLiteral { +case object False extends BooleanLiteral { val value = false override lazy val toString = "False" } @@ -608,7 +671,7 @@ object Quantification */ new Quantification(q, vars, tBody, triggers, name, isGlobal, weight) // tBody match { -// case True() | False() => tBody +// case True | False => tBody // case _ => new Quantification(q, vars, tBody, triggers) // } } @@ -627,82 +690,91 @@ sealed abstract class ArithmeticTerm extends Term { } class Plus(val p0: Term, val p1: Term) extends ArithmeticTerm - with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Plus] { override val op = "+" } -object Plus extends ((Term, Term) => Term) { +object Plus extends ConditionalFlyweightFactory[(Term, Term), Plus] { import predef.Zero - def apply(e0: Term, e1: Term) = (e0, e1) match { + override def apply(v0: (Term, Term)) = v0 match { case (t0, Zero) => t0 case (Zero, t1) => t1 case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 + n1) - case _ => new Plus(e0, e1) + case (e0, e1) => createIfNonExistent(e0, e1) } - def unapply(t: Plus) = Some((t.p0, t.p1)) + override def actualCreate(args: (Term, Term)): Plus = new Plus(args._1, args._2) } class Minus(val p0: Term, val p1: Term) extends ArithmeticTerm - with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Minus] { override val op = "-" } -object Minus extends ((Term, Term) => Term) { +object Minus extends ConditionalFlyweightFactory[(Term, Term), Minus] { import predef.Zero - def apply(e0: Term, e1: Term) = (e0, e1) match { + override def apply(v1: (Term, Term)) = v1 match { case (t0, Zero) => t0 case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 - n1) case (t0, t1) if t0 == t1 => Zero - case _ => new Minus(e0, e1) + case (e0, e1) => createIfNonExistent(e0, e1) } - def unapply(t: Minus) = Some((t.p0, t.p1)) + override def actualCreate(args: (Term, Term)): Minus = new Minus(args._1, args._2) } class Times(val p0: Term, val p1: Term) extends ArithmeticTerm - with BinaryOp[Term] with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Times] { override val op = "*" } -object Times extends ((Term, Term) => Term) { +object Times extends ConditionalFlyweightFactory[(Term, Term), Times] { import predef.{Zero, One} - def apply(e0: Term, e1: Term) = (e0, e1) match { + override def apply(v0: (Term, Term)) =v0 match { case (_, Zero) => Zero case (Zero, _) => Zero case (t0, One) => t0 case (One, t1) => t1 case (IntLiteral(n0), IntLiteral(n1)) => IntLiteral(n0 * n1) - case _ => new Times(e0, e1) + case (e0, e1) => createIfNonExistent(e0, e1) } - def unapply(t: Times) = Some((t.p0, t.p1)) + override def actualCreate(args: (Term, Term)): Times = new Times(args._1, args._2) } -case class Div(p0: Term, p1: Term) extends ArithmeticTerm - with BinaryOp[Term] { +class Div(val p0: Term, val p1: Term) extends ArithmeticTerm + with ConditionalFlyweightBinaryOp[Div] { override val op = "/" } -case class Mod(p0: Term, p1: Term) extends ArithmeticTerm - with BinaryOp[Term] { +object Div extends GeneralConditionalFlyweightFactory[(Term, Term), Div, Div] { + override def actualCreate(args: (Term, Term)): Div = new Div(args._1, args._2) +} + +class Mod(val p0: Term, val p1: Term) extends ArithmeticTerm + with ConditionalFlyweightBinaryOp[Mod] { override val op = "%" } +object Mod extends GeneralConditionalFlyweightFactory[(Term, Term), Mod, Mod] { + override def actualCreate(args: (Term, Term)): Mod = new Mod(args._1, args._2) +} + + /* Boolean expression terms */ sealed trait BooleanTerm extends Term { override val sort = sorts.Bool } class Not(val p: Term) extends BooleanTerm - with StructuralEqualityUnaryOp[Term] { + with ConditionalFlyweightUnaryOp { override val op = "!" @@ -712,19 +784,19 @@ class Not(val p: Term) extends BooleanTerm } } -object Not extends (Term => Term) { - def apply(e0: Term) = e0 match { +object Not extends ConditionalFlyweightFactory[Term, ConditionalFlyweightUnaryOp] { + + override def apply(e0: Term) = e0 match { case Not(e1) => e1 - case True() => False() - case False() => True() - case _ => new Not(e0) + case True => False + case False => True + case _ => createIfNonExistent(e0) } - - def unapply(e: Not) = Some(e.p) + override def actualCreate(args: Term): Not = new Not(args) } class Or(val ts: Seq[Term]) extends BooleanTerm - with StructuralEquality { + with ConditionalFlyweight[Seq[Term], Or] { assert(ts.nonEmpty, "Expected at least one term, but found none") @@ -739,14 +811,16 @@ class Or(val ts: Seq[Term]) extends BooleanTerm * that conflicts with using extractor objects to simplify terms, * since extractor objects can't be type-parametrised. */ -object Or extends (Iterable[Term] => Term) { +object Or extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], Term, Or] { def apply(ts: Term*) = createOr(ts) def apply(ts: Iterable[Term]) = createOr(ts.toSeq) + + // def apply(e0: Term, e1: Term) = (e0, e1) match { - // case (True(), _) | (_, True()) => True() - // case (False(), _) => e1 - // case (_, False()) => e0 + // case (True, _) | (_, True) => True + // case (False, _) => e1 + // case (_, False) => e0 // case _ if e0 == e1 => e0 // case _ => new Or(e0, e1) // } @@ -754,18 +828,18 @@ object Or extends (Iterable[Term] => Term) { @inline def createOr(_ts: Seq[Term]): Term = { var ts = _ts.flatMap { case Or(ts1) => ts1; case other => other :: Nil} - ts = _ts.filterNot(_ == False()) + ts = _ts.filterNot(_ == False) ts = ts.distinct ts match { - case Seq() => False() + case Seq() => False case Seq(t) => t - case _ if ts.contains(True()) => True() - case _ => new Or(ts) + case _ if ts.contains(True) => True + case _ => createIfNonExistent(ts) } } - def unapply(e: Or) = Some(e.ts) + override def actualCreate(args: Seq[Term]): Or = new Or(args) } class And(val ts: Seq[Term]) extends BooleanTerm @@ -785,13 +859,13 @@ object And extends (Iterable[Term] => Term) { @inline def createAnd(_ts: Seq[Term]): Term = { var ts = _ts.flatMap { case And(ts1) => ts1; case other => other :: Nil} - ts = _ts.filterNot(_ == True()) + ts = _ts.filterNot(_ == True) ts = ts.distinct ts match { - case Seq() => True() + case Seq() => True case Seq(t) => t - case _ if ts.contains(False()) => False() + case _ if ts.contains(False) => False case _ => new And(ts) } } @@ -808,11 +882,11 @@ class Implies(val p0: Term, val p1: Term) extends BooleanTerm object Implies extends ((Term, Term) => Term) { @tailrec def apply(e0: Term, e1: Term): Term = (e0, e1) match { - case (True(), _) => e1 - case (False(), _) => True() - case (_, True()) => True() + case (True, _) => e1 + case (False, _) => True + case (_, True) => True case (_, Implies(e10, e11)) => Implies(And(e0, e10), e11) - case _ if e0 == e1 => True() + case _ if e0 == e1 => True case _ => new Implies(e0, e1) } @@ -827,9 +901,9 @@ class Iff(val p0: Term, val p1: Term) extends BooleanTerm object Iff extends ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (True(), _) => e1 - case (_, True()) => e0 - case _ if e0 == e1 => True() + case (True, _) => e1 + case (_, True) => e0 + case _ if e0 == e1 => True case _ => new Iff(e0, e1) } @@ -850,10 +924,10 @@ class Ite(val t0: Term, val t1: Term, val t2: Term) object Ite extends ((Term, Term, Term) => Term) { def apply(e0: Term, e1: Term, e2: Term) = (e0, e1, e2) match { case _ if e1 == e2 => e1 - case (True(), _, _) => e1 - case (False(), _, _) => e2 - case (_, True(), False()) => e0 - case (_, False(), True()) => Not(e0) + case (True, _, _) => e1 + case (False, _, _) => e2 + case (_, True, False) => e0 + case (_, False, True) => Not(e0) case _ => new Ite(e0, e1, e2) } @@ -874,7 +948,7 @@ object Equals extends ((Term, Term) => BooleanTerm) { // Note that the syntactic simplifications (first two cases) can interfere with triggering // if they eliminate potential trigger terms. (e0, e1) match { - case (`e0`, `e0`) => True() + case (`e0`, `e0`) => True case (l1: Literal, l2: Literal) => BooleanLiteral(l1 == l2) case _ => e0.sort match { @@ -914,9 +988,9 @@ class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends Equals object BuiltinEquals extends ((Term, Term) => BooleanTerm) { def apply(t1: Term, t2: Term) = (t1, t2) match { case (p0: PermLiteral, p1: PermLiteral) => - // NOTE: The else-case (False()) is only justified because permission literals are stored in a normal form + // NOTE: The else-case (False) is only justified because permission literals are stored in a normal form // such that two literals are semantically equivalent iff they are syntactically equivalent. - if (p0.literal == p1.literal) True() else False() + if (p0.literal == p1.literal) True else False case _ => new BuiltinEquals(t1, t2) } @@ -946,9 +1020,9 @@ class Less(val p0: Term, val p1: Term) extends ComparisonTerm object Less extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True() else False() - case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True() else False() - case (t0, t1) if t0 == t1 => False() + case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True else False + case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True else False + case (t0, t1) if t0 == t1 => False case _ => new Less(e0, e1) } @@ -963,9 +1037,9 @@ class AtMost(val p0: Term, val p1: Term) extends ComparisonTerm object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True() else False() - case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True() else False() - case (t0, t1) if t0 == t1 => True() + case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True else False + case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True else False + case (t0, t1) if t0 == t1 => True case _ => new AtMost(e0, e1) } @@ -980,9 +1054,9 @@ class Greater(val p0: Term, val p1: Term) extends ComparisonTerm object Greater extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True() else False() - case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True() else False() - case (t0, t1) if t0 == t1 => False() + case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True else False + case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True else False + case (t0, t1) if t0 == t1 => False case _ => new Greater(e0, e1) } @@ -997,9 +1071,9 @@ class AtLeast(val p0: Term, val p1: Term) extends ComparisonTerm object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True() else False() - case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True() else False() - case (t0, t1) if t0 == t1 => True() + case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True else False + case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True else False + case (t0, t1) if t0 == t1 => True case _ => new AtLeast(e0, e1) } @@ -1257,8 +1331,8 @@ class PermLess(val p0: Term, val p1: Term) object PermLess extends ((Term, Term) => Term) { def apply(t0: Term, t1: Term): Term = { (t0, t1) match { - case _ if t0 == t1 => False() - case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal < p1.literal) True() else False() + case _ if t0 == t1 => False + case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal < p1.literal) True else False case (`t0`, Ite(tCond, tIf, tElse)) => /* The pattern p0 < b ? p1 : p2 arises very often in the context of quantified permissions. @@ -1281,8 +1355,8 @@ class PermAtMost(val p0: Term, val p1: Term) extends ComparisonTerm object PermAtMost extends ((Term, Term) => Term) { def apply(e0: Term, e1: Term) = (e0, e1) match { - case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True() else False() - case (t0, t1) if t0 == t1 => True() + case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True else False + case (t0, t1) if t0 == t1 => True case _ => new PermAtMost(e0, e1) } @@ -2126,7 +2200,7 @@ class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with StructuralEquali object Distinct extends (Set[DomainFun] => Term) { def apply(ts: Set[DomainFun]): Term = if (ts.size >= 2) new Distinct(ts) - else True() + else True def unapply(d: Distinct) = Some(d.ts) } @@ -2172,12 +2246,12 @@ object perms { */ def IsPositive(p: Term): Term = p match { - case p: PermLiteral => if (p.literal > Rational.zero) True() else False() + case p: PermLiteral => if (p.literal > Rational.zero) True else False case _ => PermLess(NoPerm(), p) } def IsNonPositive(p: Term): Term = p match { - case p: PermLiteral => if (p.literal <= Rational.zero) True() else False() + case p: PermLiteral => if (p.literal <= Rational.zero) True else False case _ => Or(p === NoPerm(), PermLess(p, NoPerm())) } @@ -2254,5 +2328,5 @@ object implicits { import scala.language.implicitConversions implicit def intToTerm(i: Int): IntLiteral = IntLiteral(i) - implicit def boolToTerm(b: Boolean): BooleanLiteral = if (b) True() else False() + implicit def boolToTerm(b: Boolean): BooleanLiteral = if (b) True else False } diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 10bf5c580..ca029a862 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -102,8 +102,8 @@ trait ExpressionTranslator { false, weight) - case _: ast.TrueLit => True() - case _: ast.FalseLit => False() + case _: ast.TrueLit => True + case _: ast.FalseLit => False case ast.Not(e0) => Not(f(e0)) case ast.And(e0, e1) => And(f(e0), f(e1)) case ast.Or(e0, e1) => Or(f(e0), f(e1)) @@ -126,7 +126,7 @@ trait ExpressionTranslator { case ast.LeCmp(e0, e1) => AtMost(f(e0), f(e1)) case ast.LtCmp(e0, e1) => Less(f(e0), f(e1)) - case _: ast.NullLit => Null() + case _: ast.NullLit => Null case v: ast.AbstractLocalVar => Var(Identifier(v.name), toSort(v.typ)) diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala index c1cdbce9d..81aa923a1 100644 --- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala +++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala @@ -87,8 +87,8 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter, : Term = e match { - case _: ast.AccessPredicate | _: ast.MagicWand if ignoreAccessPredicates => True() - case q: ast.Forall if !q.isPure && ignoreAccessPredicates => True() + case _: ast.AccessPredicate | _: ast.MagicWand if ignoreAccessPredicates => True + case q: ast.Forall if !q.isPure && ignoreAccessPredicates => True case _: ast.Result => data.formalResult From a4fec68034c3be6391739fbd1eae4ab7eee9b8e1 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 20 Feb 2023 02:36:31 +0100 Subject: [PATCH 02/15] Actually using config flag to turn pool usage on/off --- src/main/scala/Config.scala | 2 +- src/main/scala/state/Terms.scala | 17 +++++++++++------ 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 76b173803..7110e509a 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -550,7 +550,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))} .getOrElse(0) - lazy val useFlyweight: Boolean = false + lazy val useFlyweight: Boolean = true val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth", descr = "Maximal number of nested heuristics applications (default: 3)", diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 82caf52c4..8c6f39bfe 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -461,12 +461,17 @@ trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U <: Term, V <: U with Co var pool = new TrieMap[T, V]() def createIfNonExistent(args: T): V = { - pool.get(args) match { - case Some(v) => v - case None => - val newInstance = actualCreate(args) - pool.addOne(args, newInstance) - newInstance + if (Verifier.config.useFlyweight) { + pool.get(args) match { + case Some(v) => + v + case None => + val newInstance = actualCreate(args) + pool.addOne(args, newInstance) + newInstance + } + } else { + actualCreate(args) } } From 614bf2769cfe6fe903e33df0b4e9b8bcb5e0071b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 20 Feb 2023 12:08:11 +0100 Subject: [PATCH 03/15] Fixed tests --- src/test/scala/SimpleArithmeticTermSolverTests.scala | 9 ++++++++- src/test/scala/TriggerRewriterTests.scala | 8 ++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/test/scala/SimpleArithmeticTermSolverTests.scala b/src/test/scala/SimpleArithmeticTermSolverTests.scala index eee936d23..77e623906 100644 --- a/src/test/scala/SimpleArithmeticTermSolverTests.scala +++ b/src/test/scala/SimpleArithmeticTermSolverTests.scala @@ -9,12 +9,19 @@ package viper.silicon.tests import org.scalatest.matchers.should.Matchers import viper.silicon.state.Identifier import DSL._ +import org.scalatest.BeforeAndAfter import org.scalatest.funsuite.AnyFunSuite +import viper.silicon.Config import viper.silicon.state.terms._ +import viper.silicon.verifier.Verifier -class SimpleArithmeticTermSolverTests extends AnyFunSuite with Matchers { +class SimpleArithmeticTermSolverTests extends AnyFunSuite with Matchers with BeforeAndAfter { import SimpleArithmeticSolver.{solve, SolverResult, SolvingSuccess, SolvingFailure} + before { + Verifier.config = new Config(Seq()) + } + test("Pre-solving errors") { assert(solve(b, y, y).isInstanceOf[SolverResult]) assert(solve(x, b, y).isInstanceOf[SolverResult]) diff --git a/src/test/scala/TriggerRewriterTests.scala b/src/test/scala/TriggerRewriterTests.scala index 7f5df140b..c7b29a3d2 100644 --- a/src/test/scala/TriggerRewriterTests.scala +++ b/src/test/scala/TriggerRewriterTests.scala @@ -40,7 +40,7 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers { import rewriter.rewrite test("No-ops") { - val forall1 = Forall(x, True(), Trigger(f(x)), "forall1") + val forall1 = Forall(x, True, Trigger(f(x)), "forall1") val forall2 = Forall(x, f(x), Trigger(f(x)), "forall2") val forall3 = Forall(Seq(x, y, b), f(x), Trigger(f(x)), "forall3") @@ -86,15 +86,15 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers { test("Failures") { rewrite( - Forall(x, True(), Trigger(f(x * n))) + Forall(x, True, Trigger(f(x * n))) ) should be (None) /* Multiplication is currently not handled */ rewrite( - Forall(x, True(), Trigger(f(x / n))) + Forall(x, True, Trigger(f(x / n))) ) should be (None) /* Division is currently not handled */ rewrite( - Forall(Seq(x, y), True(), Trigger(f(x + y))) + Forall(Seq(x, y), True, Trigger(f(x + y))) ) should be (None) /* Invalid triggers that mention more than one quantified variable are currently not handled */ } } From 8b78b4a1b3f089365da3fe5155df20ef0a5d0c3d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 20 Feb 2023 16:18:04 +0100 Subject: [PATCH 04/15] Progress on making terms and decls conditionally flyweight --- src/main/scala/state/Terms.scala | 288 +++++++++++++++++-------------- 1 file changed, 160 insertions(+), 128 deletions(-) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 8c6f39bfe..851e1396f 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -94,19 +94,40 @@ sealed trait Decl extends Node { def id: Identifier } -case class SortDecl(sort: Sort) extends Decl { +class SortDecl(val sort: Sort) extends Decl with ConditionalFlyweight[Sort, SortDecl] { val id: Identifier = sort.id + override val equalityDefiningMembers: Sort = sort } -case class FunctionDecl(func: Function) extends Decl { +object SortDecl extends GeneralConditionalFlyweightFactory[Sort, SortDecl, SortDecl] { + override def actualCreate(args: Sort): SortDecl = new SortDecl(args) +} + +class FunctionDecl(val func: Function) extends Decl with ConditionalFlyweight[Function, FunctionDecl] { val id: Identifier = func.id + override val equalityDefiningMembers: Function = func +} + +object FunctionDecl extends GeneralConditionalFlyweightFactory[Function, FunctionDecl, FunctionDecl] { + override def actualCreate(args: Function): FunctionDecl = new FunctionDecl(args) } -case class SortWrapperDecl(from: Sort, to: Sort) extends Decl { +class SortWrapperDecl(val from: Sort, val to: Sort) extends Decl with ConditionalFlyweight[(Sort, Sort), SortWrapperDecl] { val id: Identifier = SortWrapperId(from, to) + override val equalityDefiningMembers: (Sort, Sort) = (from, to) +} + +object SortWrapperDecl extends GeneralConditionalFlyweightFactory[(Sort, Sort), SortWrapperDecl, SortWrapperDecl] { + override def actualCreate(args: (Sort, Sort)): SortWrapperDecl = new SortWrapperDecl(args._1, args._2) +} + +class MacroDecl(val id: Identifier, val args: Seq[Var], val body: Term) extends Decl with ConditionalFlyweight[(Identifier, Seq[Var], Term), MacroDecl] { + override val equalityDefiningMembers: (Identifier, Seq[Var], Term) = (id, args, body) } -case class MacroDecl(id: Identifier, args: Seq[Var], body: Term) extends Decl +object MacroDecl extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Var], Term), MacroDecl, MacroDecl] { + override def actualCreate(args: (Identifier, Seq[Var], Term)): MacroDecl = new MacroDecl(args._1, args._2, args._3) +} object ConstDecl extends (Var => Decl) { /* TODO: Inconsistent naming - Const vs Var */ def apply(v: Var) = FunctionDecl(v) @@ -142,8 +163,8 @@ object Function { * (i.e. field) that indicates the kind of */ -trait GenericFunction[F <: Function] extends Function with StructuralEquality { - val equalityDefiningMembers = id +: argSorts :+ resultSort +trait GenericFunction[F <: Function] extends Function { + val equalityDefiningMembers = (id, argSorts, resultSort) def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort): F @@ -157,20 +178,19 @@ trait GenericFunctionCompanion[F <: Function] { def apply(id: Identifier, argSort: Sort, resultSort: Sort): F = apply(id, Seq(argSort), resultSort) - - def unapply(fun: F): Some[(Identifier, Seq[Sort], Sort)] = - Some((fun.id, fun.argSorts, fun.resultSort)) } class Fun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[Fun] { + extends GenericFunction[Fun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Fun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = Fun(id, argSorts, resultSort) } -object Fun extends ((Identifier, Seq[Sort], Sort) => Fun) with GenericFunctionCompanion[Fun] { - def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new Fun(id, argSorts, resultSort) +object Fun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), Fun, Fun] with GenericFunctionCompanion[Fun] { + def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) + + override def actualCreate(args: (Identifier, Seq[Sort], Sort)): Fun = new Fun(args._1, args._2, args._3) } /* TODO: [18-12-2015 Malte] Since heap-dependent functions are represented by a separate class, @@ -179,58 +199,78 @@ object Fun extends ((Identifier, Seq[Sort], Sort) => Fun) with GenericFunctionCo * object. */ class HeapDepFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[HeapDepFun] { + extends GenericFunction[HeapDepFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), HeapDepFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = HeapDepFun(id, argSorts, resultSort) } -object HeapDepFun extends ((Identifier, Seq[Sort], Sort) => HeapDepFun) with GenericFunctionCompanion[HeapDepFun] { - def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new HeapDepFun(id, argSorts, resultSort) +object HeapDepFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), HeapDepFun, HeapDepFun] with GenericFunctionCompanion[HeapDepFun] { + def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) + + override def actualCreate(args: (Identifier, Seq[Sort], Sort)): HeapDepFun = new HeapDepFun(args._1, args._2, args._3) } class DomainFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[DomainFun] { + extends GenericFunction[DomainFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), DomainFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = DomainFun(id, argSorts, resultSort) } -object DomainFun extends ((Identifier, Seq[Sort], Sort) => DomainFun) with GenericFunctionCompanion[DomainFun] { - def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new DomainFun(id, argSorts, resultSort) +object DomainFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), DomainFun, DomainFun] with GenericFunctionCompanion[DomainFun] { + def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) + + override def actualCreate(args: (Identifier, Seq[Sort], Sort)): DomainFun = new DomainFun(args._1, args._2, args._3) } class SMTFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[SMTFun] { + extends GenericFunction[SMTFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), SMTFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = SMTFun(id, argSorts, resultSort) } -object SMTFun extends ((Identifier, Seq[Sort], Sort) => SMTFun) with GenericFunctionCompanion[SMTFun] { - def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = new SMTFun(id, argSorts, resultSort) +object SMTFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), SMTFun, SMTFun] with GenericFunctionCompanion[SMTFun] { + def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) + + override def actualCreate(args: (Identifier, Seq[Sort], Sort)): SMTFun = new SMTFun(args._1, args._2, args._3) +} + +class Macro(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) extends Applicable + with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Macro] { + override val equalityDefiningMembers: (Identifier, Seq[Sort], Sort) = (id, argSorts, resultSort) } -case class Macro(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) extends Applicable +object Macro extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), Macro, Macro] { + override def actualCreate(args: (Identifier, Stack[Sort], Sort)): Macro = new Macro(args._1, args._2, args._3) +} -case class Var(id: Identifier, sort: Sort) extends Function with Application[Var] { +class Var(val id: Identifier, val sort: Sort) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort), Var] { + override val equalityDefiningMembers: (Identifier, Sort) = (id, sort) val applicable: Var = this val args: Seq[Term] = Seq.empty val argSorts: Seq[Sort] = Seq(sorts.Unit) val resultSort: Sort = sort override lazy val toString = id.toString + + def copy(id: Identifier = id, sort: Sort = sort) = Var(id, sort) +} + +object Var extends GeneralConditionalFlyweightFactory[(Identifier, Sort), Var, Var] { + override def actualCreate(args: (Identifier, Sort)): Var = new Var(args._1, args._2) } class App(val applicable: Applicable, val args: Seq[Term]) extends Application[Applicable] - with StructuralEquality { + with ConditionalFlyweight[(Applicable, Seq[Term]), App] { /*with PossibleTrigger*/ utils.assertExpectedSorts(applicable, args) val sort: Sort = applicable.resultSort - val equalityDefiningMembers = applicable +: args + val equalityDefiningMembers = (applicable, args) def copy(applicable: Applicable = applicable, args: Seq[Term] = args) = App(applicable, args) override lazy val toString = @@ -238,10 +278,11 @@ class App(val applicable: Applicable, val args: Seq[Term]) else s"${applicable.id}${args.mkString("(", ", ", ")")}" } -object App extends ((Applicable, Seq[Term]) => App) { - def apply(applicable: Applicable, args: Seq[Term]) = new App(applicable, args) - def apply(applicable: Applicable, arg: Term) = new App(applicable, Seq(arg)) - def unapply(app: App) = Some((app.applicable, app.args)) +object App extends ConditionalFlyweightFactory[(Applicable, Seq[Term]), App] { + def apply(applicable: Applicable, args: Seq[Term]) = createIfNonExistent((applicable, args)) + def apply(applicable: Applicable, arg: Term) = createIfNonExistent((applicable, Seq(arg))) + + override def actualCreate(args: (Applicable, Seq[Term])): App = new App(args._1, args._2) } /* @@ -423,7 +464,7 @@ trait StructuralEquality { self: AnyRef => })) } -trait ConditionalFlyweight[T, V] extends Term { self: AnyRef => +trait ConditionalFlyweight[T, V] { self: AnyRef => val equalityDefiningMembers: T override lazy val hashCode = if (Verifier.config.useFlyweight) @@ -447,14 +488,14 @@ trait ConditionalFlyweight[T, V] extends Term { self: AnyRef => } -trait ConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V]] extends GeneralConditionalFlyweightFactory[T, Term, V] +trait ConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends GeneralConditionalFlyweightFactory[T, Term, V] -trait GeneralConditionalFlyweightFactory[T, U <: Term, V <: U with ConditionalFlyweight[T, V]] extends AGeneralConditionalFlyweightFactory[T, T, U, V] { +trait GeneralConditionalFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends AGeneralConditionalFlyweightFactory[T, T, U, V] { def apply(v1: T): U = createIfNonExistent(v1) } -trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U <: Term, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { +trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { import scala.collection.concurrent.TrieMap @@ -462,14 +503,7 @@ trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U <: Term, V <: U with Co def createIfNonExistent(args: T): V = { if (Verifier.config.useFlyweight) { - pool.get(args) match { - case Some(v) => - v - case None => - val newInstance = actualCreate(args) - pool.addOne(args, newInstance) - newInstance - } + pool.getOrElseUpdate(args, actualCreate(args)) } else { actualCreate(args) } @@ -491,12 +525,16 @@ case object Unit extends SnapshotTerm with Literal { override lazy val toString = "_" } -case class IntLiteral(n: BigInt) extends ArithmeticTerm with Literal { +class IntLiteral(val n: BigInt) extends ArithmeticTerm with Literal with ConditionalFlyweight[BigInt, IntLiteral] { def +(m: Int) = IntLiteral(n + m) def -(m: Int) = IntLiteral(n - m) def *(m: Int) = IntLiteral(n * m) def /(m: Int) = Div(this, IntLiteral(m)) override lazy val toString = n.toString() + override val equalityDefiningMembers: BigInt = n +} +object IntLiteral extends GeneralConditionalFlyweightFactory[BigInt, IntLiteral, IntLiteral] { + override def actualCreate(args: BigInt): IntLiteral = new IntLiteral(args) } case object Null extends Term with Literal { @@ -596,9 +634,9 @@ class Quantification private[terms] (val q: Quantifier, /* TODO: Rename */ val isGlobal: Boolean, val weight: Option[Int]) extends BooleanTerm - with StructuralEquality { + with ConditionalFlyweight[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] { - val equalityDefiningMembers = q :: vars :: body :: triggers :: weight :: Nil + val equalityDefiningMembers = (q, vars, body, triggers, name, isGlobal, weight) def copy(q: Quantifier = q, vars: Seq[Var] = vars, @@ -629,7 +667,7 @@ class Quantification private[terms] (val q: Quantifier, /* TODO: Rename */ } object Quantification - extends ((Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]) => Quantification) { + extends ConditionalFlyweightFactory[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] { private val qidCounter = new AtomicInteger() @@ -674,17 +712,15 @@ object Quantification /* TODO: If we optimise away a quantifier, we cannot, for example, access * autoTrigger on the returned object. */ - new Quantification(q, vars, tBody, triggers, name, isGlobal, weight) + createIfNonExistent(q, vars, tBody, triggers, name, isGlobal, weight) // tBody match { // case True | False => tBody // case _ => new Quantification(q, vars, tBody, triggers) // } } - def unapply(q: Quantification) - : Some[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int])] = { - - Some((q.q, q.vars, q.body, q.triggers, q.name, q.isGlobal, q.weight)) + override def actualCreate(args: (Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int])): Quantification = { + new Quantification(args._1, args._2, args._3, args._4, args._5, args._6, args._7) } } @@ -848,7 +884,7 @@ object Or extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], } class And(val ts: Seq[Term]) extends BooleanTerm - with StructuralEquality { + with ConditionalFlyweight[Seq[Term], And] { assert(ts.nonEmpty, "Expected at least one term, but found none") @@ -857,7 +893,7 @@ class And(val ts: Seq[Term]) extends BooleanTerm override lazy val toString = ts.mkString(" && ") } -object And extends (Iterable[Term] => Term) { +object And extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], Term, And] { def apply(ts: Term*) = createAnd(ts) def apply(ts: Iterable[Term]) = createAnd(ts.toSeq) @@ -871,72 +907,72 @@ object And extends (Iterable[Term] => Term) { case Seq() => True case Seq(t) => t case _ if ts.contains(False) => False - case _ => new And(ts) + case _ => createIfNonExistent(ts) } } - def unapply(e: And) = Some(e.ts) + override def actualCreate(args: Seq[Term]): And = new And(args) } class Implies(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Implies] { override val op = "==>" } -object Implies extends ((Term, Term) => Term) { +object Implies extends ConditionalFlyweightFactory[(Term, Term), Implies] { @tailrec - def apply(e0: Term, e1: Term): Term = (e0, e1) match { - case (True, _) => e1 + override def apply(v0: (Term, Term)): Term = v0 match { + case (True, e1) => e1 case (False, _) => True case (_, True) => True - case (_, Implies(e10, e11)) => Implies(And(e0, e10), e11) - case _ if e0 == e1 => True - case _ => new Implies(e0, e1) + case (e0, Implies(e10, e11)) => Implies(And(e0, e10), e11) + case (e0, e1) if e0 == e1 => True + case (e0, e1) => createIfNonExistent(e0, e1) } - def unapply(e: Implies) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): Implies = new Implies(args._1, args._2) } class Iff(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Iff] { override val op = "<==>" } -object Iff extends ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { - case (True, _) => e1 - case (_, True) => e0 - case _ if e0 == e1 => True - case _ => new Iff(e0, e1) +object Iff extends ConditionalFlyweightFactory[(Term, Term), Iff] { + override def apply(v0: (Term, Term)) = v0 match { + case (True, e1) => e1 + case (e0, True) => e0 + case (e0, e1) if e0 == e1 => True + case (e0, e1) => createIfNonExistent(e0, e1) } - def unapply(e: Iff) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): Iff = new Iff(args._1, args._2) } class Ite(val t0: Term, val t1: Term, val t2: Term) - extends Term with StructuralEquality { + extends Term with ConditionalFlyweight[(Term, Term, Term), Ite] { assert(t0.sort == sorts.Bool && t1.sort == t2.sort, /* @elidable */ s"Ite term Ite($t0, $t1, $t2) is not well-sorted: ${t0.sort}, ${t1.sort}, ${t2.sort}") - val equalityDefiningMembers = t0 :: t1 :: t2 :: Nil + val equalityDefiningMembers = (t0, t1, t2) val sort = t1.sort override lazy val toString = s"($t0 ? $t1 : $t2)" } -object Ite extends ((Term, Term, Term) => Term) { - def apply(e0: Term, e1: Term, e2: Term) = (e0, e1, e2) match { - case _ if e1 == e2 => e1 - case (True, _, _) => e1 - case (False, _, _) => e2 - case (_, True, False) => e0 - case (_, False, True) => Not(e0) - case _ => new Ite(e0, e1, e2) +object Ite extends ConditionalFlyweightFactory[(Term, Term, Term), Ite] { + override def apply(v0: (Term, Term, Term)) = v0 match { + case (_, e1, e2) if e1 == e2 => e1 + case (True, e1, _) => e1 + case (False, _, e2) => e2 + case (e0, True, False) => e0 + case (e0, False, True) => Not(e0) + case _ => createIfNonExistent(v0) } - def unapply(e: Ite) = Some((e.t0, e.t1, e.t2)) + override def actualCreate(args: (Term, Term, Term)): Ite = new Ite(args._1, args._2, args._3) } /* Comparison expression terms */ @@ -975,10 +1011,10 @@ object Equals extends ((Term, Term) => BooleanTerm) { case _ => /* Ok */ } - new BuiltinEquals(e0, e1) + BuiltinEquals(e0, e1) - case _: sorts.Seq | _: sorts.Set | _: sorts.Multiset | _: sorts.Map => new CustomEquals(e0, e1) - case _ => new BuiltinEquals(e0, e1) + case _: sorts.Seq | _: sorts.Set | _: sorts.Multiset | _: sorts.Map => CustomEquals(e0, e1) + case _ => BuiltinEquals(e0, e1) } } } @@ -988,34 +1024,33 @@ object Equals extends ((Term, Term) => BooleanTerm) { /* Represents built-in equality, e.g., '=' in SMT-LIB */ class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends Equals - with StructuralEqualityBinaryOp[Term] + with ConditionalFlyweightBinaryOp[BuiltinEquals] -object BuiltinEquals extends ((Term, Term) => BooleanTerm) { - def apply(t1: Term, t2: Term) = (t1, t2) match { +object BuiltinEquals extends GeneralConditionalFlyweightFactory[(Term, Term), BooleanTerm, BuiltinEquals] { + override def apply(v0: (Term, Term)) = v0 match { case (p0: PermLiteral, p1: PermLiteral) => // NOTE: The else-case (False) is only justified because permission literals are stored in a normal form // such that two literals are semantically equivalent iff they are syntactically equivalent. if (p0.literal == p1.literal) True else False - case _ => new BuiltinEquals(t1, t2) + case _ => createIfNonExistent(v0) } - def unapply(e: BuiltinEquals) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): BuiltinEquals = new BuiltinEquals(args._1, args._2) } /* Custom equality that (potentially) needs to be axiomatised. */ class CustomEquals private[terms] (val p0: Term, val p1: Term) extends Equals - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[CustomEquals] { override val op = "===" } -object CustomEquals extends ((Term, Term) => BooleanTerm) { - def apply(t1: Term, t2: Term) = new CustomEquals(t1, t2) - def unapply(e: CustomEquals) = Some((e.p0, e.p1)) +object CustomEquals extends GeneralConditionalFlyweightFactory[(Term, Term), BooleanTerm, CustomEquals] { + override def actualCreate(args: (Term, Term)): CustomEquals = new CustomEquals(args._1, args._2) } class Less(val p0: Term, val p1: Term) extends ComparisonTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Less] { assert(p0.sort == p1.sort, s"Expected both operands to be of the same sort, but found ${p0.sort} ($p0) and ${p1.sort} ($p1).") @@ -1023,66 +1058,66 @@ class Less(val p0: Term, val p1: Term) extends ComparisonTerm override val op = "<" } -object Less extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object Less extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), Less] { + override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True else False case (t0, t1) if t0 == t1 => False - case _ => new Less(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: Less) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): Less = new Less(args._1, args._2) } class AtMost(val p0: Term, val p1: Term) extends ComparisonTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[AtMost] { override val op = "<=" } -object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), AtMost] { + override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True else False case (t0, t1) if t0 == t1 => True - case _ => new AtMost(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: AtMost) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): AtMost = new AtMost(args._1, args._2) } class Greater(val p0: Term, val p1: Term) extends ComparisonTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Greater] { override val op = ">" } -object Greater extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object Greater extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), Greater] { + override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True else False case (t0, t1) if t0 == t1 => False - case _ => new Greater(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: Greater) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): Greater = new Greater(args._1, args._2) } class AtLeast(val p0: Term, val p1: Term) extends ComparisonTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[AtLeast] { override val op = ">=" } -object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), AtLeast] { + override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True else False case (t0, t1) if t0 == t1 => True - case _ => new AtLeast(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: AtLeast) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): AtLeast = new AtLeast(args._1, args._2) } /* @@ -1141,39 +1176,36 @@ sealed abstract class PermLiteral(val literal: Rational) extends Permissions case class NoPerm() extends PermLiteral(Rational.zero) { override lazy val toString = "Z" } case class FullPerm() extends PermLiteral(Rational.one) { override lazy val toString = "W" } -class FractionPermLiteral(r: Rational) extends PermLiteral(r) { - override def equals(obj: Any) = obj match { - case p: FractionPermLiteral => literal == p.literal - case _ => false - } +class FractionPermLiteral(r: Rational) extends PermLiteral(r) with ConditionalFlyweight[Rational, FractionPermLiteral] { + override val equalityDefiningMembers: Rational = r override lazy val toString = literal.toString } -object FractionPermLiteral extends (Rational => Permissions) { - def apply(r: Rational) = r match { +object FractionPermLiteral extends GeneralConditionalFlyweightFactory[Rational, Permissions, FractionPermLiteral] { + override def apply(r: Rational) = r match { case Rational(n, _) if n == 0 => NoPerm() case Rational(n, d) if n == d => FullPerm() - case _ => new FractionPermLiteral(r) + case _ => createIfNonExistent(r) } - def unapply(t: FractionPermLiteral) = Some(t.literal) + override def actualCreate(args: Rational): FractionPermLiteral = new FractionPermLiteral(args) } class FractionPerm(val n: Term, val d: Term) extends Permissions - with StructuralEquality { + with ConditionalFlyweight[(Term, Term), FractionPerm] { - val equalityDefiningMembers = n :: d :: Nil + val equalityDefiningMembers = (n, d) override lazy val toString = s"$n/$d" } -object FractionPerm extends ((Term, Term) => Permissions) { - def apply(n: Term, d: Term) = (n, d) match { +object FractionPerm extends GeneralConditionalFlyweightFactory[(Term, Term), Permissions, FractionPerm] { + override def apply(v: (Term, Term)) = v match { case (IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => FractionPermLiteral(Rational(i1, i2)) - case _ => new FractionPerm(n, d) + case _ => createIfNonExistent(v) } - def unapply(fp: FractionPerm) = Some((fp.n, fp.d)) + override def actualCreate(args: (Term, Term)): FractionPerm = new FractionPerm(args._1, args._2) } case class IsValidPermVar(v: Var) extends BooleanTerm { From 919bed3f62689b27f72bc6ff446afc3cfb837517 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 20 Feb 2023 21:09:30 +0100 Subject: [PATCH 05/15] Handling most commonly used terms, fixed unary ops, term caching in Z3 API converter --- src/main/scala/Config.scala | 2 +- .../scala/decider/TermToZ3APIConverter.scala | 5 + .../scala/resources/PropertyInterpreter.scala | 11 +- src/main/scala/state/Terms.scala | 295 +++++++++++------- 4 files changed, 202 insertions(+), 111 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 7110e509a..b1ecca455 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -550,7 +550,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))} .getOrElse(0) - lazy val useFlyweight: Boolean = true + lazy val useFlyweight: Boolean = true // prover() == "Z3-API" val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth", descr = "Maximal number of nested heuristics applications (default: 3)", diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index f1ba4da0c..7d947dc81 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -30,6 +30,7 @@ class TermToZ3APIConverter val sortCache = mutable.HashMap[Sort, Z3Sort]() val funcDeclCache = mutable.HashMap[(String, Seq[Sort], Sort), Z3FuncDecl]() + val termCache = mutable.HashMap[Term, Z3Expr]() def convert(s: Sort): Z3Sort = convertSort(s) @@ -203,6 +204,9 @@ class TermToZ3APIConverter def convertTerm(term: Term): Z3Expr = { + val cached = termCache.get(term) + if (cached.isDefined) + return cached.get val res = term match { case l: Literal => { l match { @@ -441,6 +445,7 @@ class TermToZ3APIConverter | _: Quantification => sys.error(s"Unexpected term $term cannot be translated to SMTLib code") } + termCache.put(term, res) res } diff --git a/src/main/scala/resources/PropertyInterpreter.scala b/src/main/scala/resources/PropertyInterpreter.scala index 596a3a64d..02490d3fb 100644 --- a/src/main/scala/resources/PropertyInterpreter.scala +++ b/src/main/scala/resources/PropertyInterpreter.scala @@ -115,11 +115,20 @@ abstract class PropertyInterpreter { } } + protected def buildBinary[K <: Kind] + (builder: ((Term, Term)) => Term, + left: PropertyExpression[K], + right: PropertyExpression[K], + pm: Info): Term = { + def wrapper(t0: Term, t1: Term): Term = builder((t0, t1)) + buildBinary(wrapper _, left, right, pm) + } + protected def buildBinary[K <: Kind] (builder: (Term, Term) => Term, left: PropertyExpression[K], right: PropertyExpression[K], - pm: Info) = { + pm: Info): Term = { val leftTerm = buildPathCondition(left, pm) val rightTerm = buildPathCondition(right, pm) builder(leftTerm, rightTerm) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 851e1396f..55c6cdb79 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -421,7 +421,7 @@ trait ConditionalFlyweightBinaryOp[T] extends BinaryOp[Term] with ConditionalFly override val equalityDefiningMembers = (p0, p1) } -trait ConditionalFlyweightUnaryOp extends UnaryOp[Term] with ConditionalFlyweight[Term, ConditionalFlyweightUnaryOp] with Term { +trait ConditionalFlyweightUnaryOp[T] extends UnaryOp[Term] with ConditionalFlyweight[Term, T] with Term { override val equalityDefiningMembers = p } @@ -490,6 +490,9 @@ trait ConditionalFlyweight[T, V] { self: AnyRef => trait ConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends GeneralConditionalFlyweightFactory[T, Term, V] +trait PreciseConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends GeneralConditionalFlyweightFactory[T, V, V] + + trait GeneralConditionalFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends AGeneralConditionalFlyweightFactory[T, T, U, V] { def apply(v1: T): U = createIfNonExistent(v1) @@ -815,8 +818,8 @@ object Mod extends GeneralConditionalFlyweightFactory[(Term, Term), Mod, Mod] { sealed trait BooleanTerm extends Term { override val sort = sorts.Bool } class Not(val p: Term) extends BooleanTerm - with ConditionalFlyweightUnaryOp { - + with ConditionalFlyweightUnaryOp[Not] { + assert(p.sort == sorts.Bool) override val op = "!" override lazy val toString = p match { @@ -825,7 +828,7 @@ class Not(val p: Term) extends BooleanTerm } } -object Not extends ConditionalFlyweightFactory[Term, ConditionalFlyweightUnaryOp] { +object Not extends ConditionalFlyweightFactory[Term, Not] { override def apply(e0: Term) = e0 match { case Not(e1) => e1 @@ -1208,95 +1211,101 @@ object FractionPerm extends GeneralConditionalFlyweightFactory[(Term, Term), Per override def actualCreate(args: (Term, Term)): FractionPerm = new FractionPerm(args._1, args._2) } -case class IsValidPermVar(v: Var) extends BooleanTerm { +class IsValidPermVar(val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsValidPermVar] { + override val equalityDefiningMembers: Var = v override lazy val toString = s"PVar($v)" } -case class IsReadPermVar(v: Var) extends BooleanTerm { +object IsValidPermVar extends ConditionalFlyweightFactory[Var, IsValidPermVar] { + override def actualCreate(args: Var): IsValidPermVar = new IsValidPermVar((args)) +} + +class IsReadPermVar(val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsReadPermVar] { + override val equalityDefiningMembers: Var = v override lazy val toString = s"RdVar($v)" } +object IsReadPermVar extends ConditionalFlyweightFactory[Var, IsReadPermVar] { + override def actualCreate(args: Var): IsReadPermVar = new IsReadPermVar((args)) +} + class PermTimes(val p0: Term, val p1: Term) extends Permissions - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermTimes] { override val op = "*" } -object PermTimes extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) = (t0, t1) match { +object PermTimes extends ConditionalFlyweightFactory[(Term, Term), PermTimes] { + override def apply(v0: (Term, Term)) = v0 match { case (FullPerm(), t) => t case (t, FullPerm()) => t case (NoPerm(), _) => NoPerm() case (_, NoPerm()) => NoPerm() case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal * p1.literal) - case (_, _) => new PermTimes(t0, t1) + case (_, _) => createIfNonExistent(v0) } - def unapply(pt: PermTimes) = Some((pt.p0, pt.p1)) + override def actualCreate(args: (Term, Term)): PermTimes = new PermTimes(args._1, args._2) } class IntPermTimes(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[IntPermTimes] { override val op = "*" } -object IntPermTimes extends ((Term, Term) => Term) { +object IntPermTimes extends ConditionalFlyweightFactory[(Term, Term), IntPermTimes] { import predef.{Zero, One} - def apply(t0: Term, t1: Term) = (t0, t1) match { + override def apply(v0: (Term, Term)) = v0 match { case (Zero, _) => NoPerm() case (One, t) => t case (_, NoPerm()) => NoPerm() case (IntLiteral(i), p: PermLiteral) => FractionPermLiteral(Rational(i, 1) * p.literal) - case (_, _) => new IntPermTimes(t0, t1) + case (_, _) => createIfNonExistent(v0) } - def unapply(pt: IntPermTimes) = Some((pt.p0, pt.p1)) + override def actualCreate(args: (Term, Term)): IntPermTimes = new IntPermTimes(args._1, args._2) } class PermIntDiv(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermIntDiv] { utils.assertSort(p1, "Second term", sorts.Int) override val op = "/" } -object PermIntDiv extends ((Term, Term) => Term) { +object PermIntDiv extends ConditionalFlyweightFactory[(Term, Term), PermIntDiv] { import predef.One - def apply(t0: Term, t1: Term) = (t0, t1) match { + override def apply(v0: (Term, Term)) = v0 match { case (t, One) => t case (p: PermLiteral, IntLiteral(i)) if i != 0 => FractionPermLiteral(p.literal / Rational(i, 1)) - case (_, _) => new PermIntDiv(t0, t1) + case (_, _) => createIfNonExistent(v0) } - def unapply(t: PermIntDiv) = Some((t.p0, t.p1)) + override def actualCreate(args: (Term, Term)): PermIntDiv = new PermIntDiv(args._1, args._2) } class PermPermDiv(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermPermDiv] { utils.assertSort(p1, "Second term", sorts.Perm) override val op = "/" } -object PermPermDiv extends ((Term, Term) => Term) { +object PermPermDiv extends ConditionalFlyweightFactory[(Term, Term), PermPermDiv] { - def apply(t0: Term, t1: Term) = (t0, t1) match { - case (_, _) => new PermPermDiv(t0, t1) - } - - def unapply(t: PermPermDiv) = Some((t.p0, t.p1)) + override def actualCreate(args: (Term, Term)): PermPermDiv = new PermPermDiv(args._1, args._2) } object PermDiv extends ((Term, Term) => Term) { @@ -1308,30 +1317,30 @@ object PermDiv extends ((Term, Term) => Term) { class PermPlus(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermPlus] { override val op = "+" } -object PermPlus extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) = (t0, t1) match { - case (NoPerm(), _) => t1 - case (_, NoPerm()) => t0 +object PermPlus extends ConditionalFlyweightFactory[(Term, Term), PermPlus] { + override def apply(v0: (Term, Term)) = v0 match { + case (NoPerm(), t1) => t1 + case (t0, NoPerm()) => t0 case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal + p1.literal) case (FractionPerm(n1, d1), FractionPerm(n2, d2)) if d1 == d2 => FractionPerm(Plus(n1, n2), d1) - case (PermMinus(t00, t01), _) if t01 == t1 => t00 - case (_, PermMinus(t10, t11)) if t11 == t0 => t10 + case (PermMinus(t00, t01), t1) if t01 == t1 => t00 + case (t0, PermMinus(t10, t11)) if t11 == t0 => t10 - case (_, _) => new PermPlus(t0, t1) + case (_, _) => createIfNonExistent(v0) } - def unapply(pp: PermPlus) = Some((pp.p0, pp.p1)) + override def actualCreate(args: (Term, Term)): PermPlus = new PermPlus(args._1, args._2) } class PermMinus(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermMinus] { override val op = "-" @@ -1341,68 +1350,68 @@ class PermMinus(val p0: Term, val p1: Term) } } -object PermMinus extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) = (t0, t1) match { - case (_, NoPerm()) => t0 +object PermMinus extends ConditionalFlyweightFactory[(Term, Term), PermMinus] { + override def apply(v0: (Term, Term)) = v0 match { + case (t0, NoPerm()) => t0 case (p0, p1) if p0 == p1 => NoPerm() case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal - p1.literal) case (p0, PermMinus(p1, p2)) if p0 == p1 => p2 case (PermPlus(p0, p1), p2) if p0 == p2 => p1 case (PermPlus(p0, p1), p2) if p1 == p2 => p0 - case (_, _) => new PermMinus(t0, t1) + case (_, _) => createIfNonExistent(v0) } - def unapply(pm: PermMinus) = Some((pm.p0, pm.p1)) + override def actualCreate(args: (Term, Term)): PermMinus = new PermMinus(args._1, args._2) } class PermLess(val p0: Term, val p1: Term) extends BooleanTerm with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermLess] { override lazy val toString = s"($p0) < ($p1)" override val op = "<" } -object PermLess extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term): Term = { - (t0, t1) match { - case _ if t0 == t1 => False +object PermLess extends ConditionalFlyweightFactory[(Term, Term), PermLess] { + override def apply(v0: (Term, Term)): Term = { + v0 match { + case (t0, t1) if t0 == t1 => False case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal < p1.literal) True else False - case (`t0`, Ite(tCond, tIf, tElse)) => + case (t0, Ite(tCond, tIf, tElse)) => /* The pattern p0 < b ? p1 : p2 arises very often in the context of quantified permissions. * Pushing the comparisons into the ite allows further simplifications. */ Ite(tCond, PermLess(t0, tIf), PermLess(t0, tElse)) - case _ => new PermLess(t0, t1) + case _ => createIfNonExistent(v0) } } - def unapply(pl: PermLess) = Some((pl.p0, pl.p1)) + override def actualCreate(args: (Term, Term)): PermLess = new PermLess(args._1, args._2) } class PermAtMost(val p0: Term, val p1: Term) extends ComparisonTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermAtMost] { override val op = "<=" } -object PermAtMost extends ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object PermAtMost extends ConditionalFlyweightFactory[(Term, Term), PermAtMost] { + override def apply(v0: (Term, Term)) = v0 match { case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True else False case (t0, t1) if t0 == t1 => True - case _ => new PermAtMost(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: PermAtMost) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): PermAtMost = new PermAtMost(args._1, args._2) } class PermMin(val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[PermMin] { utils.assertSort(p0, "Permission 1st", sorts.Perm) utils.assertSort(p1, "Permission 2nd", sorts.Perm) @@ -1410,14 +1419,14 @@ class PermMin(val p0: Term, val p1: Term) extends Permissions override lazy val toString = s"min ($p0, $p1)" } -object PermMin extends ((Term, Term) => Term) { - def apply(e0: Term, e1: Term) = (e0, e1) match { +object PermMin extends ConditionalFlyweightFactory[(Term, Term), PermMin] { + override def apply(v0: (Term, Term)) = v0 match { case (t0, t1) if t0 == t1 => t0 case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal > p1.literal) p1 else p0 - case _ => new PermMin(e0, e1) + case _ => createIfNonExistent(v0) } - def unapply(e: PermMin) = Some((e.p0, e.p1)) + override def actualCreate(args: (Term, Term)): PermMin = new PermMin(args._1, args._2) } /* Sequences */ @@ -1953,7 +1962,7 @@ object MapRange extends (Term => SetTerm) { sealed trait SnapshotTerm extends Term { val sort = sorts.Snap } class Combine(val p0: Term, val p1: Term) extends SnapshotTerm - with StructuralEqualityBinaryOp[Term] { + with ConditionalFlyweightBinaryOp[Combine] { utils.assertSort(p0, "first operand", sorts.Snap) utils.assertSort(p1, "second operand", sorts.Snap) @@ -1961,103 +1970,143 @@ class Combine(val p0: Term, val p1: Term) extends SnapshotTerm override lazy val toString = s"($p0, $p1)" } -object Combine extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) = new Combine(t0.convert(sorts.Snap), t1.convert(sorts.Snap)) +object Combine extends ConditionalFlyweightFactory[(Term, Term), Combine] { + override def apply(v0: (Term, Term)) = createIfNonExistent(v0._1.convert(sorts.Snap), v0._2.convert(sorts.Snap)) - def unapply(c: Combine) = Some((c.p0, c.p1)) + override def actualCreate(args: (Term, Term)): Combine = new Combine(args._1, args._2) } class First(val p: Term) extends SnapshotTerm - with StructuralEqualityUnaryOp[Term] + with ConditionalFlyweightUnaryOp[First] /*with PossibleTrigger*/ { utils.assertSort(p, "term", sorts.Snap) } -object First extends (Term => Term) { - def apply(t: Term) = t match { +object First extends ConditionalFlyweightFactory[Term, First] { + override def apply(t: Term) = t match { case Combine(t1, _) => t1 - case _ => new First(t) + case _ => createIfNonExistent(t) } - def unapply(f: First) = Some(f.p) + override def actualCreate(args: Term): First = new First(args) } class Second(val p: Term) extends SnapshotTerm - with StructuralEqualityUnaryOp[Term] + with ConditionalFlyweightUnaryOp[Second] /*with PossibleTrigger*/ { utils.assertSort(p, "term", sorts.Snap) } -object Second extends (Term => Term) { - def apply(t: Term) = t match { +object Second extends ConditionalFlyweightFactory[Term, Second] { + override def apply(t: Term) = t match { case Combine(_, t2) => t2 - case _ => new Second(t) + case _ => createIfNonExistent(t) } - def unapply(s: Second) = Some(s.p) + override def actualCreate(args: Term): Second = new Second(args) } /* Quantified permissions */ -case class Lookup(field: String, fvf: Term, at: Term) extends Term { +class Lookup(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), Lookup] { utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction]) utils.assertSort(at, "receiver", sorts.Ref) + override val equalityDefiningMembers: (String, Term, Term) = (field, fvf, at) val sort = fvf.sort.asInstanceOf[sorts.FieldValueFunction].codomainSort } -case class PermLookup(field: String, pm: Term, at: Term) extends Term { +object Lookup extends PreciseConditionalFlyweightFactory[(String, Term, Term), Lookup] { + override def actualCreate(args: (String, Term, Term)): Lookup = new Lookup(args._1, args._2, args._3) +} + +class PermLookup(val field: String, val pm: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), PermLookup] { utils.assertSort(pm, "field perm function", "FieldPermFunction", _.isInstanceOf[sorts.FieldPermFunction]) utils.assertSort(at, "receiver", sorts.Ref) + override val equalityDefiningMembers: (String, Term, Term) = (field, pm, at) val sort = sorts.Perm } -case class Domain(field: String, fvf: Term) extends SetTerm /*with PossibleTrigger*/ { +object PermLookup extends PreciseConditionalFlyweightFactory[(String, Term, Term), PermLookup] { + override def actualCreate(args: (String, Term, Term)): PermLookup = new PermLookup(args._1, args._2, args._3) +} + +class Domain(val field: String, val fvf: Term) extends SetTerm /*with PossibleTrigger*/ with ConditionalFlyweight[(String, Term), Domain] { utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction]) val elementsSort = sorts.Ref val sort = sorts.Set(elementsSort) + override val equalityDefiningMembers: (String, Term) = (field, fvf) +} + +object Domain extends ConditionalFlyweightFactory[(String, Term), Domain] { + override def actualCreate(args: (String, Term)): Domain = new Domain(args._1, args._2) } -case class FieldTrigger(field: String, fvf: Term, at: Term) extends Term { +class FieldTrigger(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), FieldTrigger] { utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction]) utils.assertSort(at, "receiver", sorts.Ref) val sort = sorts.Bool + override val equalityDefiningMembers: (String, Term, Term) = (field, fvf, at) +} + +object FieldTrigger extends PreciseConditionalFlyweightFactory[(String, Term, Term), FieldTrigger] { + override def actualCreate(args: (String, Term, Term)): FieldTrigger = new FieldTrigger(args._1, args._2, args._3) } /* Quantified predicates */ -case class PredicateLookup(predname: String, psf: Term, args: Seq[Term]) extends Term { +class PredicateLookup(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateLookup] { utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction]) val sort = psf.sort.asInstanceOf[sorts.PredicateSnapFunction].codomainSort + override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, psf, args) +} + +object PredicateLookup extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicateLookup] { + override def actualCreate(args: (String, Term, Seq[Term])): PredicateLookup = new PredicateLookup(args._1, args._2, args._3) } -case class PredicatePermLookup(predname: String, pm: Term, args: Seq[Term]) extends Term { +class PredicatePermLookup(val predname: String, val pm: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicatePermLookup] { utils.assertSort(pm, "predicate perm function", "PredicatePermFunction", _.isInstanceOf[sorts.PredicatePermFunction]) val sort = sorts.Perm + override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, pm, args) } -case class PredicateDomain(predname: String, psf: Term) extends SetTerm /*with PossibleTrigger*/ { +object PredicatePermLookup extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicatePermLookup] { + override def actualCreate(args: (String, Term, Seq[Term])): PredicatePermLookup = new PredicatePermLookup(args._1, args._2, args._3) +} + +class PredicateDomain(val predname: String, val psf: Term) extends SetTerm /*with PossibleTrigger*/ with ConditionalFlyweight[(String, Term), PredicateDomain] { utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction]) val elementsSort = sorts.Snap val sort = sorts.Set(elementsSort) + override val equalityDefiningMembers: (String, Term) = (predname, psf) +} + +object PredicateDomain extends ConditionalFlyweightFactory[(String, Term), PredicateDomain] { + override def actualCreate(args: (String, Term)): PredicateDomain = new PredicateDomain(args._1, args._2) } -case class PredicateTrigger(predname: String, psf: Term, args: Seq[Term]) extends Term { +class PredicateTrigger(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateTrigger] { utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction]) val sort = sorts.Bool + override val equalityDefiningMembers: (String, Term, Stack[Term]) = (predname, psf, args) +} + +object PredicateTrigger extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicateTrigger] { + override def actualCreate(args: (String, Term, Seq[Term])): PredicateTrigger = new PredicateTrigger(args._1, args._2, args._3) } /* Magic wands */ -case class MagicWandSnapshot(abstractLhs: Term, rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) { +class MagicWandSnapshot(val abstractLhs: Term, val rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) { utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap) utils.assertSort(rhsSnapshot, "rhs", sorts.Snap) @@ -2073,7 +2122,7 @@ case class MagicWandSnapshot(abstractLhs: Term, rhsSnapshot: Term) extends Combi } } -object MagicWandSnapshot { +object MagicWandSnapshot { def apply(snapshot: Term): MagicWandSnapshot = { assert(snapshot.sort == sorts.Snap) snapshot match { @@ -2082,20 +2131,45 @@ object MagicWandSnapshot { MagicWandSnapshot(First(snapshot), Second(snapshot)) } } + + // Since MagicWandSnapshot subclasses Combine, we apparently cannot inherit the normal subclass, so we + // have to copy paste the code here. + import scala.collection.concurrent.TrieMap + + var pool = new TrieMap[(Term, Term), MagicWandSnapshot]() + + def createIfNonExistent(args: (Term, Term)): MagicWandSnapshot = { + if (Verifier.config.useFlyweight) { + pool.getOrElseUpdate(args, actualCreate(args)) + } else { + actualCreate(args) + } + } + + def actualCreate(tuple: (Term, Term)) = new MagicWandSnapshot(tuple._1, tuple._2) + def apply(fst: Term, snd: Term): MagicWandSnapshot = createIfNonExistent((fst, snd)) + + def unapply(mws: MagicWandSnapshot) = Some((mws.abstractLhs, mws.rhsSnapshot)) } -case class MagicWandChunkTerm(chunk: MagicWandChunk) extends Term { +class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] { override val sort = sorts.Unit /* TODO: Does this make sense? */ override lazy val toString = s"wand@${chunk.id.ghostFreeWand.pos}}" + override val equalityDefiningMembers: MagicWandChunk = chunk +} + +object MagicWandChunkTerm extends ConditionalFlyweightFactory[MagicWandChunk, MagicWandChunkTerm] { + override def actualCreate(args: MagicWandChunk): MagicWandChunkTerm = new MagicWandChunkTerm(args) } /* Factory methods for all resources */ object toSnapTree extends (Seq[Term] => Term) { + private def binaryCombine(t0: Term, t1: Term) = Combine(t0, t1) @inline def apply(args: Seq[Term]): Term = { if (args.isEmpty) Unit - else args.map(_.convert(sorts.Snap)).reduceLeft(Combine) + else args.map(_.convert(sorts.Snap)).reduceLeft(binaryCombine) } } @@ -2204,63 +2278,64 @@ object PsfTop extends (String => Identifier) { */ class SortWrapper(val t: Term, val to: Sort) extends Term - with StructuralEquality { + with ConditionalFlyweight[(Term, Sort), SortWrapper] { assert((t.sort == sorts.Snap || to == sorts.Snap) && t.sort != to, s"Unexpected sort wrapping of $t from ${t.sort} to $to") - val equalityDefiningMembers = t :: to :: Nil + val equalityDefiningMembers = (t, to) // override lazy val toString = s"SortWrapper($t, $to)" override lazy val toString = t.toString override val sort = to } -object SortWrapper { - def apply(t: Term, to: Sort) = t match { - case _ if t.sort == to => t - case sw: SortWrapper if sw.t.sort == to => sw.t - case _ => new SortWrapper(t, to) +object SortWrapper extends ConditionalFlyweightFactory[(Term, Sort), SortWrapper] { + override def apply(v0: (Term, Sort)) = v0 match { + case (t, to) if t.sort == to => t + case (sw: SortWrapper, to) if sw.t.sort == to => sw.t + case _ => createIfNonExistent(v0) } - def unapply(sw: SortWrapper) = Some((sw.t, sw.to)) + override def actualCreate(args: (Term, Sort)): SortWrapper = new SortWrapper(args._1, args._2) } /* Other terms */ -class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with StructuralEquality { +class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with ConditionalFlyweight[Set[DomainFun], Distinct] { assert(ts.size >= 2, "Distinct requires at least two terms") - val equalityDefiningMembers = ts :: Nil + val equalityDefiningMembers = ts override lazy val toString = s"Distinct($ts)" } -object Distinct extends (Set[DomainFun] => Term) { - def apply(ts: Set[DomainFun]): Term = - if (ts.size >= 2) new Distinct(ts) +object Distinct extends ConditionalFlyweightFactory[Set[DomainFun], Distinct] { + override def apply(ts: Set[DomainFun]): Term = + if (ts.size >= 2) createIfNonExistent(ts) else True - def unapply(d: Distinct) = Some(d.ts) + override def actualCreate(args: Set[DomainFun]): Distinct = new Distinct(args) } -class Let(val bindings: Map[Var, Term], val body: Term) extends Term with StructuralEquality { +class Let(val bindings: Map[Var, Term], val body: Term) extends Term with ConditionalFlyweight[(Map[Var, Term], Term), Let] { assert(bindings.nonEmpty, "Let needs to bind at least one variable") val sort = body.sort - val equalityDefiningMembers = Seq(body) ++ bindings.flatMap(_.productIterator) + val equalityDefiningMembers = (bindings, body) override lazy val toString = s"let ${bindings.map(p => s"${p._1} = ${p._2}")} in $body" } -object Let extends ((Map[Var, Term], Term) => Term) { +object Let extends ConditionalFlyweightFactory[(Map[Var, Term], Term), Let] { def apply(v: Var, t: Term, body: Term): Term = apply(Map(v -> t), body) def apply(vs: Seq[Var], ts: Seq[Term], body: Term): Term = apply(toMap(vs zip ts), body) - def apply(bindings: Map[Var, Term], body: Term) = { + override def apply(v0: (Map[Var, Term], Term)) = { + val (bindings, body) = v0 if (bindings.isEmpty) body - else new Let(bindings, body) + else createIfNonExistent(v0) } - def unapply(l: Let) = Some((l.bindings, l.body)) + override def actualCreate(args: (Map[Var, Term], Term)): Let = new Let(args._1, args._2) } /* Predefined terms */ @@ -2292,8 +2367,10 @@ object perms { case _ => Or(p === NoPerm(), PermLess(p, NoPerm())) } - def BigPermSum(it: Iterable[Term], f: Term => Term = t => t): Term = - viper.silicon.utils.mapReduceLeft(it, f, PermPlus, NoPerm()) + def BigPermSum(it: Iterable[Term], f: Term => Term = t => t): Term = { + def binaryPermPlus(t0: Term, t1: Term) = PermPlus(t0, t1) + viper.silicon.utils.mapReduceLeft(it, f, binaryPermPlus, NoPerm()) + } } /* Utility functions */ From fdc401ea55b118a42a435be01535193672919669 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 23 Feb 2023 16:45:49 +0100 Subject: [PATCH 06/15] Finished conditional flyweight modulo cleanup --- .../decider/TermToSMTLib2Converter.scala | 4 +- .../scala/decider/TermToZ3APIConverter.scala | 5 +- src/main/scala/reporting/Converter.scala | 4 +- .../scala/resources/PropertyInterpreter.scala | 4 +- src/main/scala/rules/ChunkSupporter.scala | 10 +- src/main/scala/rules/Consumer.scala | 6 +- src/main/scala/rules/Evaluator.scala | 12 +- src/main/scala/rules/Executor.scala | 10 +- src/main/scala/rules/HavocSupporter.scala | 2 +- src/main/scala/rules/MagicWandSupporter.scala | 4 +- .../rules/MoreCompleteExhaleSupporter.scala | 40 +- src/main/scala/rules/Producer.scala | 4 +- .../scala/rules/QuantifiedChunkSupport.scala | 16 +- src/main/scala/rules/StateConsolidator.scala | 6 +- src/main/scala/state/State.scala | 2 +- src/main/scala/state/Terms.scala | 550 ++++++++++-------- .../supporters/ExpressionTranslator.scala | 19 +- src/test/scala/TriggerGeneratorTests.scala | 9 +- src/test/scala/TriggerRewriterTests.scala | 43 +- 19 files changed, 421 insertions(+), 329 deletions(-) diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala index 32b0c1b9e..7bad3a6ed 100644 --- a/src/main/scala/decider/TermToSMTLib2Converter.scala +++ b/src/main/scala/decider/TermToSMTLib2Converter.scala @@ -197,8 +197,8 @@ class TermToSMTLib2Converter /* Permissions */ - case FullPerm() => "$Perm.Write" - case NoPerm() => "$Perm.No" + case FullPerm => "$Perm.Write" + case NoPerm => "$Perm.No" case FractionPermLiteral(r) => renderBinaryOp("/", renderAsReal(IntLiteral(r.numerator)), renderAsReal(IntLiteral(r.denominator))) case FractionPerm(n, d) => renderBinaryOp("/", renderAsReal(n), renderAsReal(d)) case PermLess(t0, t1) => renderBinaryOp("<", render(t0), render(t1)) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 7d947dc81..e6c9f04ab 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -314,8 +314,8 @@ class TermToZ3APIConverter /* Permissions */ - case FullPerm() => ctx.mkReal(1) - case NoPerm() => ctx.mkReal(0) + case FullPerm => ctx.mkReal(1) + case NoPerm => ctx.mkReal(0) case FractionPermLiteral(r) => ctx.mkDiv(convertToReal(IntLiteral(r.numerator)), convertToReal(IntLiteral(r.denominator))) case FractionPerm(n, d) => ctx.mkDiv(convertToReal(n), convertToReal(d)) case PermLess(t0, t1) => ctx.mkLt(convertTerm(t0).asInstanceOf[ArithExpr], convertTerm(t1).asInstanceOf[ArithExpr]) @@ -521,6 +521,7 @@ class TermToZ3APIConverter macros.clear() funcDeclCache.clear() sortCache.clear() + termCache.clear() unitConstructor = null combineConstructor = null firstFunc = null diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index 3d310fe71..6ac77ce62 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -416,8 +416,8 @@ object Converter { case _ => None } case App(_, _) => None - case NoPerm() => Some(Rational.zero) - case FullPerm() => Some(Rational.one) + case NoPerm => Some(Rational.zero) + case FullPerm => Some(Rational.one) case FractionPermLiteral(r) => Some(r) case _: FractionPerm => None case IsValidPermVar(_) => None diff --git a/src/main/scala/resources/PropertyInterpreter.scala b/src/main/scala/resources/PropertyInterpreter.scala index 02490d3fb..ebaa2d9c0 100644 --- a/src/main/scala/resources/PropertyInterpreter.scala +++ b/src/main/scala/resources/PropertyInterpreter.scala @@ -109,8 +109,8 @@ abstract class PropertyInterpreter { protected def buildPermissionLiteral(numerator: BigInt, denominator: BigInt): Term = { require(denominator != 0, "Denominator of permission literal must not be 0") (numerator, denominator) match { - case (n, _) if n == 0 => terms.NoPerm() - case (n, d) if n == d => terms.FullPerm() + case (n, _) if n == 0 => terms.NoPerm + case (n, d) if n == d => terms.FullPerm case (n, d) => terms.FractionPerm(terms.IntLiteral(n), terms.IntLiteral(d)) } } diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 5f4a5b1a8..2f41894a6 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -119,10 +119,10 @@ object chunkSupporter extends ChunkSupportRules { val snap = optCh2 match { case None => None case Some(ch) => - if (v1.decider.check(Greater(perms, NoPerm()), Verifier.config.checkTimeout())) { + if (v1.decider.check(Greater(perms, NoPerm), Verifier.config.checkTimeout())) { Some(ch.snap) } else { - Some(Ite(Greater(perms, NoPerm()), ch.snap.convert(sorts.Snap), Unit)) + Some(Ite(Greater(perms, NoPerm), ch.snap.convert(sorts.Snap), Unit)) } } QS(s2.copy(h = s.h), h2, snap, v1) @@ -159,13 +159,13 @@ object chunkSupporter extends ChunkSupportRules { val newChunk = ch.withPerm(PermMinus(ch.perm, toTake)) val takenChunk = Some(ch.withPerm(toTake)) var newHeap = h - ch - if (!v.decider.check(newChunk.perm === NoPerm(), Verifier.config.checkTimeout())) { + if (!v.decider.check(newChunk.perm === NoPerm, Verifier.config.checkTimeout())) { newHeap = newHeap + newChunk assumeProperties(newChunk, newHeap) } (ConsumptionResult(PermMinus(perms, toTake), v, 0), s, newHeap, takenChunk) } else { - if (v.decider.check(ch.perm !== NoPerm(), Verifier.config.checkTimeout())) { + if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) { v.decider.assume(PermLess(perms, ch.perm)) val newChunk = ch.withPerm(PermMinus(ch.perm, perms)) val takenChunk = ch.withPerm(perms) @@ -177,7 +177,7 @@ object chunkSupporter extends ChunkSupportRules { } } case None => - if (consumeExact && s.retrying && v.decider.check(perms === NoPerm(), Verifier.config.checkTimeout())) { + if (consumeExact && s.retrying && v.decider.check(perms === NoPerm, Verifier.config.checkTimeout())) { (Complete(), s, h, None) } else { (Incomplete(perms), s, h, None) diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index d337f572c..ac1a95edc 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -290,7 +290,7 @@ object consumer extends ConsumptionRules { if (forall.triggers.isEmpty) None else Some(forall.triggers) val ePerm = ast.FullPerm()() - val tPerm = FullPerm() + val tPerm = FullPerm evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) { case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) => quantifiedChunkSupporter.consume( @@ -421,7 +421,7 @@ object consumer extends ConsumptionRules { } else { s1 } - val loss = PermTimes(FullPerm(), s1.permissionScalingFactor) + val loss = PermTimes(FullPerm, s1.permissionScalingFactor) quantifiedChunkSupporter.consumeSingleLocation( s1p, h, @@ -441,7 +441,7 @@ object consumer extends ConsumptionRules { magicWandSupporter.evaluateWandArguments(s, wand, pve, v)((s1, tArgs, v1) => { val ve = pve dueTo MagicWandChunkNotFound(wand) val description = s"consume wand $wand" - chunkSupporter.consume(s1, h, wand, tArgs, FullPerm(), ve, v1, description)(Q) + chunkSupporter.consume(s1, h, wand, tArgs, FullPerm, ve, v1, description)(Q) }) case _ => diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 05450df76..f229cea55 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -160,8 +160,8 @@ object evaluator extends EvaluationRules { case x: ast.AbstractLocalVar => Q(s, s.g(x), v) - case _: ast.FullPerm => Q(s, FullPerm(), v) - case _: ast.NoPerm => Q(s, NoPerm(), v) + case _: ast.FullPerm => Q(s, FullPerm, v) + case _: ast.NoPerm => Q(s, NoPerm, v) case ast.FractionalPerm(e0, e1) => var t1: Term = null @@ -385,7 +385,7 @@ object evaluator extends EvaluationRules { case ast.PermMinus(e0) => eval(s, e0, pve, v)((s1, t0, v1) => - Q(s1, PermMinus(NoPerm(), t0), v1)) + Q(s1, PermMinus(NoPerm, t0), v1)) case ast.PermMul(e0, e1) => evalBinOp(s, e0, e1, PermTimes, pve, v)(Q) @@ -481,7 +481,7 @@ object evaluator extends EvaluationRules { } val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head) v1.decider.prover.comment(s"perm($resacc) ~~> assume upper permission bound") - v1.decider.assume(PermAtMost(currentPermAmount, FullPerm())) + v1.decider.assume(PermAtMost(currentPermAmount, FullPerm)) (s2, currentPermAmount) case predicate: ast.Predicate => @@ -499,9 +499,9 @@ object evaluator extends EvaluationRules { } else { val chs = chunkSupporter.findChunksWithID[NonQuantifiedChunk](h.values, identifier) val currentPermAmount = - chs.foldLeft(NoPerm(): Term)((q, ch) => { + chs.foldLeft(NoPerm: Term)((q, ch) => { val argsPairWiseEqual = And(args.zip(ch.args).map { case (a1, a2) => a1 === a2 }) - PermPlus(q, Ite(argsPairWiseEqual, ch.perm, NoPerm())) + PermPlus(q, Ite(argsPairWiseEqual, ch.perm, NoPerm)) }) /* TODO: See todo above */ // v1.decider.prover.comment(s"perm($locacc) ~~> assume upper permission bound") diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index dbcb11139..24854b86a 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -330,7 +330,7 @@ object executor extends ExecutionRules { Seq(`?r`), `?r` === tRcvr, field, - FullPerm(), + FullPerm, chunkOrderHeuristics, v2 ) @@ -340,7 +340,7 @@ object executor extends ExecutionRules { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v2) v1.decider.prover.comment("Definitional axioms for singleton-FVF's value") v1.decider.assume(smValueDef) - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm(), sm, s.program) + val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), field, Seq(tRcvr), FullPerm, sm, s.program) if (s3.heapDependentTriggers.contains(field)) v1.decider.assume(FieldTrigger(field.name, sm, tRcvr)) Q(s3.copy(h = h3 + ch), v2) @@ -355,10 +355,10 @@ object executor extends ExecutionRules { val resource = fa.res(s.program) val ve = pve dueTo InsufficientPermission(fa) val description = s"consume ${ass.pos}: $ass" - chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm(), ve, v2, description)((s3, h3, _, v3) => { + chunkSupporter.consume(s2, s2.h, resource, Seq(tRcvr), FullPerm, ve, v2, description)((s3, h3, _, v3) => { val tSnap = ssaifyRhs(tRhs, field.name, field.typ, v3) val id = BasicChunkIdentifier(field.name) - val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), tSnap, FullPerm()) + val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), tSnap, FullPerm) chunkSupporter.produce(s3, h3, newChunk, v3)((s4, h4, v4) => Q(s4.copy(h = h4), v4)) }) @@ -369,7 +369,7 @@ object executor extends ExecutionRules { val tRcvr = v.decider.fresh(x) v.decider.assume(tRcvr !== Null) val newChunks = fields map (field => { - val p = FullPerm() + val p = FullPerm val snap = v.decider.fresh(field.name, v.symbolConverter.toSort(field.typ)) if (s.qpFields.contains(field)) { val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, field, Seq(tRcvr), snap, v) diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala index 63520ae22..ec2ea7cfe 100644 --- a/src/main/scala/rules/HavocSupporter.scala +++ b/src/main/scala/rules/HavocSupporter.scala @@ -116,7 +116,7 @@ object havocSupporter extends SymbolicExecutionRules { quantifiedChunkSupporter.injectivityAxiom( qvars = tVars, condition = tCond, - perms = FullPerm(), + perms = FullPerm, arguments = tArgs, triggers = Nil, qidPrefix = qid, diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala index 771d077f4..8b509f3a6 100644 --- a/src/main/scala/rules/MagicWandSupporter.scala +++ b/src/main/scala/rules/MagicWandSupporter.scala @@ -106,7 +106,7 @@ object magicWandSupporter extends SymbolicExecutionRules { (Q: (State, MagicWandChunk, Verifier) => VerificationResult) : VerificationResult = { evaluateWandArguments(s, wand, pve, v)((s1, ts, v1) => - Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, snap, FullPerm()), v1) + Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, snap, FullPerm), v1) ) } @@ -297,7 +297,7 @@ object magicWandSupporter extends SymbolicExecutionRules { quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4) v4.decider.prover.comment("Definitional axioms for singleton-SM's value") v4.decider.assume(smValueDef) - val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program) + val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program) appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4) Success() }) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 248f0469a..b99919c60 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -59,7 +59,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val `?s` = Var(Identifier("?s"), sort) var summarisingSnapshotDefinitions: Seq[Term] = Vector.empty - var permissionSum: Term = NoPerm() + var permissionSum: Term = NoPerm relevantChunks.foreach(ch => { val argumentEqualities = @@ -69,7 +69,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { Implies(And(argumentEqualities, IsPositive(ch.perm)), `?s` === ch.snap) permissionSum = - PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm())) + PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm)) }) val taggedSummarisingSnapshot = @@ -109,7 +109,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (v.decider.check(And(chunk.args.zip(args).map { case (t1, t2) => t1 === t2 }), Verifier.config.checkTimeout())) { return Q(s, chunk.snap, Seq(), chunk.perm, v) } else { - return Q(s, chunk.snap, Seq(), NoPerm(), v) + return Q(s, chunk.snap, Seq(), NoPerm, v) } } val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v) @@ -217,7 +217,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (relevantChunks.isEmpty) { // if no permission is exhaled, return none - if (v.decider.check(perms === NoPerm(), Verifier.config.checkTimeout())) { + if (v.decider.check(perms === NoPerm, Verifier.config.checkTimeout())) { Q(s, h, None, v) } else { createFailure(ve, v, s) @@ -228,7 +228,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { Q(s1, Heap(updatedChunks ++ otherChunks), optSnap, v2)}) } else { var pNeeded = perms - var pSum: Term = NoPerm() + var pSum: Term = NoPerm val newChunks = ListBuffer[NonQuantifiedChunk]() var moreNeeded = true @@ -246,8 +246,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { relevantChunks.sortWith(sortFunction) foreach { ch => if (moreNeeded) { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) - pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm())) - val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm()) + pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm)) + val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) val pTakenArgs = additionalArgs val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody) val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort) @@ -263,7 +263,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { newChunks.append(newChunk) } - moreNeeded = !v.decider.check(pNeeded === NoPerm(), Verifier.config.splitTimeout()) + moreNeeded = !v.decider.check(pNeeded === NoPerm, Verifier.config.splitTimeout()) } else { newChunks.append(ch) } @@ -285,7 +285,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (!moreNeeded) { Q(s1, newHeap, Some(snap), v1) } else { - v1.decider.assert(pNeeded === NoPerm()) { + v1.decider.assert(pNeeded === NoPerm) { case true => Q(s1, newHeap, Some(snap), v1) case false => @@ -307,8 +307,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { assert(s.functionRecorder == NoopFunctionRecorder) - var totalPermSum: Term = NoPerm() - var totalPermTaken: Term = NoPerm() + var totalPermSum: Term = NoPerm + var totalPermTaken: Term = NoPerm val snap: Term = v.decider.fresh(sorts.Snap) val updatedChunks = @@ -316,14 +316,14 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) val permTaken = v.decider.fresh("p", sorts.Perm) - totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm())) + totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm)) totalPermTaken = PermPlus(totalPermTaken, permTaken) v.decider.assume(Seq( IsValidPermVar(permTaken), PermAtMost(permTaken, ch.perm), - Implies(Not(eq), permTaken === NoPerm()), - Implies(permTaken !== NoPerm(), snap === ch.snap.convert(sorts.Snap)) + Implies(Not(eq), permTaken === NoPerm), + Implies(permTaken !== NoPerm, snap === ch.snap.convert(sorts.Snap)) )) ch.withPerm(PermMinus(ch.perm, permTaken)) @@ -331,12 +331,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { v.decider.assume( Implies( - totalPermSum !== NoPerm(), + totalPermSum !== NoPerm, And( - PermLess(NoPerm(), totalPermTaken), + PermLess(NoPerm, totalPermTaken), PermLess(totalPermTaken, totalPermSum)))) - v.decider.assert(totalPermTaken !== NoPerm()) { + v.decider.assert(totalPermTaken !== NoPerm) { case true => v.decider.assume(perms === totalPermTaken) Q(s, updatedChunks, Some(snap), v) @@ -364,14 +364,14 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { relevantChunksPerField foreach { case (_, relevantChunks) => val permissionSum = - relevantChunks.foldLeft(NoPerm(): Term) { case (permSum, chunk) => + relevantChunks.foldLeft(NoPerm: Term) { case (permSum, chunk) => val eq = freeReceiver === chunk.args.head /* For field chunks, the receiver is the only argument */ - PermPlus(permSum, Ite(eq, chunk.perm, NoPerm())) + PermPlus(permSum, Ite(eq, chunk.perm, NoPerm)) } relevantChunks foreach (chunk => { val instantiatedPermSum = permissionSum.replace(freeReceiver, chunk.args.head) - v.decider.assume(PermAtMost(instantiatedPermSum, FullPerm())) + v.decider.assume(PermAtMost(instantiatedPermSum, FullPerm)) }) } } diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index dae269e2d..29ad88dba 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -297,7 +297,7 @@ object producer extends ProductionRules { if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail else s1.conservedPcs val ch = - quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm(), sm, s.program) + quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program) val h2 = s1.h + ch val smCache1 = if(s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))){ val (relevantChunks, _) = @@ -412,7 +412,7 @@ object producer extends ProductionRules { tCond, tArgs, tSnap, - FullPerm(), + FullPerm, pve, NegativePermission(ast.FullPerm()()), QPAssertionNotInjective(wand), diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 00ffa7fdc..def1441a1 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -225,7 +225,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { .map { case (x, a) => x === a }) val conditionalizedPermissions = - Ite(condition, permissions, NoPerm()) + Ite(condition, permissions, NoPerm) val hints = extractHints(None, arguments) @@ -274,7 +274,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { Ite( And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain)), permissions.replace(qvarsToInversesOfCodomain), - NoPerm()) + NoPerm) val hints = extractHints(Some(condition), arguments) @@ -1355,7 +1355,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val precomputedData = candidates map { ch => val permsProvided = ch.perm - val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm()) + val permsTakenBody = Ite(condition, PermMin(permsProvided, permsNeeded), NoPerm) val permsTakenArgs = codomainQVars ++ additionalArgs val permsTakenDecl = v.decider.freshMacro("pTaken", permsTakenArgs, permsTakenBody) val permsTakenMacro = Macro(permsTakenDecl.id, permsTakenDecl.args.map(_.sort), permsTakenDecl.body.sort) @@ -1372,7 +1372,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { v.decider.prover.comment(s"Done precomputing, updating quantified chunks") v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.beforeIteration) - var tookEnoughCheck = Forall(codomainQVars, Implies(condition, permsNeeded === NoPerm()), Nil) + var tookEnoughCheck = Forall(codomainQVars, Implies(condition, permsNeeded === NoPerm), Nil) precomputedData foreach { case (ithChunk, ithPTaken, ithPNeeded) => if (success.isComplete) @@ -1404,7 +1404,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { * the assertion to check is recorded by tookEnoughCheck. */ tookEnoughCheck = - Forall(codomainQVars, Implies(condition, ithPNeeded === NoPerm()), Nil) + Forall(codomainQVars, Implies(condition, ithPNeeded === NoPerm), Nil) v.decider.prover.comment(s"Intermediate check if already taken enough permissions") success = if (v.decider.check(tookEnoughCheck, Verifier.config.splitTimeout())) { @@ -1438,7 +1438,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { : (Term, Term) = { val conditionalizedPerms = - Ite(condition, perms, NoPerm()) // c(rs) ? p(rs) : none + Ite(condition, perms, NoPerm) // c(rs) ? p(rs) : none val quantifiedPermissionConstraint = if (!constrainPermissions) { @@ -1449,7 +1449,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { Forall( codomainQVars, Implies( - ithChunk.perm !== NoPerm(), + ithChunk.perm !== NoPerm, PermLess(conditionalizedPerms, ithChunk.perm)), Nil, s"qp.srp${v.counter(this).next()}") @@ -1462,7 +1462,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { } val quantifiedDepletedCheck = - Forall(codomainQVars, PermMinus(ithChunk.perm, ithPTaken) === NoPerm(), Nil) + Forall(codomainQVars, PermMinus(ithChunk.perm, ithPTaken) === NoPerm, Nil) val (permissionConstraint, depletedCheck) = ithChunk.singletonArguments match { diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index c52882f28..ba207cefe 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -245,7 +245,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol val currentPermAmount = PermLookup(field.name, pmDef.pm, receiver) v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}") v.decider.assume( - Forall(receiver, PermAtMost(currentPermAmount, FullPerm()), Trigger(trigger), "qp-fld-prm-bnd")) + Forall(receiver, PermAtMost(currentPermAmount, FullPerm), Trigger(trigger), "qp-fld-prm-bnd")) } else { /* If we don't use heap-dependent triggers, the trigger x.f does not work. Instead, we assume the permission @@ -255,14 +255,14 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol */ for (chunk <- fieldChunks) { if (chunk.singletonRcvr.isDefined){ - v.decider.assume(PermAtMost(PermLookup(field.name, pmDef.pm, chunk.singletonRcvr.get), FullPerm())) + v.decider.assume(PermAtMost(PermLookup(field.name, pmDef.pm, chunk.singletonRcvr.get), FullPerm)) } else { val chunkReceivers = chunk.invs.get.inverses.map(i => App(i, chunk.invs.get.additionalArguments ++ chunk.quantifiedVars)) val triggers = chunkReceivers.map(r => Trigger(r)).toSeq val currentPermAmount = PermLookup(field.name, pmDef.pm, chunk.quantifiedVars.head) v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}") v.decider.assume( - Forall(chunk.quantifiedVars, PermAtMost(currentPermAmount, FullPerm()), triggers, "qp-fld-prm-bnd")) + Forall(chunk.quantifiedVars, PermAtMost(currentPermAmount, FullPerm), triggers, "qp-fld-prm-bnd")) } } diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala index ea509358c..296a39543 100644 --- a/src/main/scala/state/State.scala +++ b/src/main/scala/state/State.scala @@ -44,7 +44,7 @@ final case class State(g: Store = Store(), triggerExp: Boolean = false, partiallyConsumedHeap: Option[Heap] = None, - permissionScalingFactor: Term = terms.FullPerm(), + permissionScalingFactor: Term = terms.FullPerm, reserveHeaps: Stack[Heap] = Nil, reserveCfgs: Stack[SilverCfg] = Stack(), diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 55c6cdb79..71b602e6f 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -94,7 +94,7 @@ sealed trait Decl extends Node { def id: Identifier } -class SortDecl(val sort: Sort) extends Decl with ConditionalFlyweight[Sort, SortDecl] { +class SortDecl private[terms] (val sort: Sort) extends Decl with ConditionalFlyweight[Sort, SortDecl] { val id: Identifier = sort.id override val equalityDefiningMembers: Sort = sort } @@ -103,7 +103,7 @@ object SortDecl extends GeneralConditionalFlyweightFactory[Sort, SortDecl, SortD override def actualCreate(args: Sort): SortDecl = new SortDecl(args) } -class FunctionDecl(val func: Function) extends Decl with ConditionalFlyweight[Function, FunctionDecl] { +class FunctionDecl private[terms] (val func: Function) extends Decl with ConditionalFlyweight[Function, FunctionDecl] { val id: Identifier = func.id override val equalityDefiningMembers: Function = func } @@ -112,7 +112,7 @@ object FunctionDecl extends GeneralConditionalFlyweightFactory[Function, Functio override def actualCreate(args: Function): FunctionDecl = new FunctionDecl(args) } -class SortWrapperDecl(val from: Sort, val to: Sort) extends Decl with ConditionalFlyweight[(Sort, Sort), SortWrapperDecl] { +class SortWrapperDecl private[terms] (val from: Sort, val to: Sort) extends Decl with ConditionalFlyweight[(Sort, Sort), SortWrapperDecl] { val id: Identifier = SortWrapperId(from, to) override val equalityDefiningMembers: (Sort, Sort) = (from, to) } @@ -121,7 +121,7 @@ object SortWrapperDecl extends GeneralConditionalFlyweightFactory[(Sort, Sort), override def actualCreate(args: (Sort, Sort)): SortWrapperDecl = new SortWrapperDecl(args._1, args._2) } -class MacroDecl(val id: Identifier, val args: Seq[Var], val body: Term) extends Decl with ConditionalFlyweight[(Identifier, Seq[Var], Term), MacroDecl] { +class MacroDecl private[terms] (val id: Identifier, val args: Seq[Var], val body: Term) extends Decl with ConditionalFlyweight[(Identifier, Seq[Var], Term), MacroDecl] { override val equalityDefiningMembers: (Identifier, Seq[Var], Term) = (id, args, body) } @@ -180,8 +180,8 @@ trait GenericFunctionCompanion[F <: Function] { apply(id, Seq(argSort), resultSort) } -class Fun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[Fun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Fun] { +class Fun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) + extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Fun] with GenericFunction[Fun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = Fun(id, argSorts, resultSort) @@ -198,8 +198,8 @@ object Fun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], So * toLimited/toStateless, and to remove the corresponding methods from the FunctionSupporter * object. */ -class HeapDepFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[HeapDepFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), HeapDepFun] { +class HeapDepFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) + extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), HeapDepFun] with GenericFunction[HeapDepFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = HeapDepFun(id, argSorts, resultSort) @@ -211,8 +211,8 @@ object HeapDepFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[So override def actualCreate(args: (Identifier, Seq[Sort], Sort)): HeapDepFun = new HeapDepFun(args._1, args._2, args._3) } -class DomainFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[DomainFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), DomainFun] { +class DomainFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) + extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), DomainFun] with GenericFunction[DomainFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = DomainFun(id, argSorts, resultSort) @@ -224,8 +224,8 @@ object DomainFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sor override def actualCreate(args: (Identifier, Seq[Sort], Sort)): DomainFun = new DomainFun(args._1, args._2, args._3) } -class SMTFun(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) - extends GenericFunction[SMTFun] with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), SMTFun] { +class SMTFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) + extends ConditionalFlyweight[(Identifier, Seq[Sort], Sort), SMTFun] with GenericFunction[SMTFun] { def copy(id: Identifier = id, argSorts: Seq[Sort] = argSorts, resultSort: Sort = resultSort) = SMTFun(id, argSorts, resultSort) @@ -237,7 +237,7 @@ object SMTFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], override def actualCreate(args: (Identifier, Seq[Sort], Sort)): SMTFun = new SMTFun(args._1, args._2, args._3) } -class Macro(val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) extends Applicable +class Macro private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resultSort: Sort) extends Applicable with ConditionalFlyweight[(Identifier, Seq[Sort], Sort), Macro] { override val equalityDefiningMembers: (Identifier, Seq[Sort], Sort) = (id, argSorts, resultSort) } @@ -246,7 +246,7 @@ object Macro extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], override def actualCreate(args: (Identifier, Stack[Sort], Sort)): Macro = new Macro(args._1, args._2, args._3) } -class Var(val id: Identifier, val sort: Sort) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort), Var] { +class Var private[terms] (val id: Identifier, val sort: Sort) extends Function with Application[Var] with ConditionalFlyweight[(Identifier, Sort), Var] { override val equalityDefiningMembers: (Identifier, Sort) = (id, sort) val applicable: Var = this val args: Seq[Term] = Seq.empty @@ -262,7 +262,7 @@ object Var extends GeneralConditionalFlyweightFactory[(Identifier, Sort), Var, V override def actualCreate(args: (Identifier, Sort)): Var = new Var(args._1, args._2) } -class App(val applicable: Applicable, val args: Seq[Term]) +class App private[terms] (val applicable: Applicable, val args: Seq[Term]) extends Application[Applicable] with ConditionalFlyweight[(Applicable, Seq[Term]), App] { /*with PossibleTrigger*/ @@ -417,11 +417,11 @@ trait BinaryOp[E] { override lazy val toString = s"$p0 $op $p1" } -trait ConditionalFlyweightBinaryOp[T] extends BinaryOp[Term] with ConditionalFlyweight[(Term, Term), T] with Term { +trait ConditionalFlyweightBinaryOp[T] extends ConditionalFlyweight[(Term, Term), T] with BinaryOp[Term] with Term { override val equalityDefiningMembers = (p0, p1) } -trait ConditionalFlyweightUnaryOp[T] extends UnaryOp[Term] with ConditionalFlyweight[Term, T] with Term { +trait ConditionalFlyweightUnaryOp[T] extends ConditionalFlyweight[Term, T] with UnaryOp[Term] with Term { override val equalityDefiningMembers = p } @@ -485,6 +485,15 @@ trait ConditionalFlyweight[T, V] { self: AnyRef => })) } } + + override def toString: String = { + val argString = equalityDefiningMembers match { + case p: Product => + p.productIterator.mkString(", ") + case trm => trm.toString + } + s"${this.getClass.getSimpleName}(${argString})" + } } @@ -528,7 +537,7 @@ case object Unit extends SnapshotTerm with Literal { override lazy val toString = "_" } -class IntLiteral(val n: BigInt) extends ArithmeticTerm with Literal with ConditionalFlyweight[BigInt, IntLiteral] { +class IntLiteral private[terms] (val n: BigInt) extends ArithmeticTerm with Literal with ConditionalFlyweight[BigInt, IntLiteral] { def +(m: Int) = IntLiteral(n + m) def -(m: Int) = IntLiteral(n - m) def *(m: Int) = IntLiteral(n * m) @@ -839,7 +848,7 @@ object Not extends ConditionalFlyweightFactory[Term, Not] { override def actualCreate(args: Term): Not = new Not(args) } -class Or(val ts: Seq[Term]) extends BooleanTerm +class Or private[terms] (val ts: Seq[Term]) extends BooleanTerm with ConditionalFlyweight[Seq[Term], Or] { assert(ts.nonEmpty, "Expected at least one term, but found none") @@ -886,7 +895,7 @@ object Or extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], override def actualCreate(args: Seq[Term]): Or = new Or(args) } -class And(val ts: Seq[Term]) extends BooleanTerm +class And private[terms](val ts: Seq[Term]) extends BooleanTerm with ConditionalFlyweight[Seq[Term], And] { assert(ts.nonEmpty, "Expected at least one term, but found none") @@ -954,7 +963,7 @@ object Iff extends ConditionalFlyweightFactory[(Term, Term), Iff] { override def actualCreate(args: (Term, Term)): Iff = new Iff(args._1, args._2) } -class Ite(val t0: Term, val t1: Term, val t2: Term) +class Ite private[terms] (val t0: Term, val t1: Term, val t2: Term) extends Term with ConditionalFlyweight[(Term, Term, Term), Ite] { assert(t0.sort == sorts.Bool && t1.sort == t2.sort, /* @elidable */ @@ -1026,8 +1035,7 @@ object Equals extends ((Term, Term) => BooleanTerm) { } /* Represents built-in equality, e.g., '=' in SMT-LIB */ -class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends Equals - with ConditionalFlyweightBinaryOp[BuiltinEquals] +class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[BuiltinEquals] with Equals object BuiltinEquals extends GeneralConditionalFlyweightFactory[(Term, Term), BooleanTerm, BuiltinEquals] { override def apply(v0: (Term, Term)) = v0 match { @@ -1042,8 +1050,7 @@ object BuiltinEquals extends GeneralConditionalFlyweightFactory[(Term, Term), Bo } /* Custom equality that (potentially) needs to be axiomatised. */ -class CustomEquals private[terms] (val p0: Term, val p1: Term) extends Equals - with ConditionalFlyweightBinaryOp[CustomEquals] { +class CustomEquals private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[CustomEquals] with Equals { override val op = "===" } @@ -1052,7 +1059,7 @@ object CustomEquals extends GeneralConditionalFlyweightFactory[(Term, Term), Boo override def actualCreate(args: (Term, Term)): CustomEquals = new CustomEquals(args._1, args._2) } -class Less(val p0: Term, val p1: Term) extends ComparisonTerm +class Less private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm with ConditionalFlyweightBinaryOp[Less] { assert(p0.sort == p1.sort, @@ -1072,7 +1079,7 @@ object Less extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFl override def actualCreate(args: (Term, Term)): Less = new Less(args._1, args._2) } -class AtMost(val p0: Term, val p1: Term) extends ComparisonTerm +class AtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm with ConditionalFlyweightBinaryOp[AtMost] { override val op = "<=" @@ -1089,7 +1096,7 @@ object AtMost extends /* OptimisingBinaryArithmeticOperation with */ Conditional override def actualCreate(args: (Term, Term)): AtMost = new AtMost(args._1, args._2) } -class Greater(val p0: Term, val p1: Term) extends ComparisonTerm +class Greater private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm with ConditionalFlyweightBinaryOp[Greater] { override val op = ">" @@ -1106,7 +1113,7 @@ object Greater extends /* OptimisingBinaryArithmeticOperation with */ Conditiona override def actualCreate(args: (Term, Term)): Greater = new Greater(args._1, args._2) } -class AtLeast(val p0: Term, val p1: Term) extends ComparisonTerm +class AtLeast private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm with ConditionalFlyweightBinaryOp[AtLeast] { override val op = ">=" @@ -1155,6 +1162,8 @@ final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] { case _ => false } + override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d) + override lazy val toString = s"$numerator/$denominator" } @@ -1176,25 +1185,25 @@ sealed trait Permissions extends Term { sealed abstract class PermLiteral(val literal: Rational) extends Permissions -case class NoPerm() extends PermLiteral(Rational.zero) { override lazy val toString = "Z" } -case class FullPerm() extends PermLiteral(Rational.one) { override lazy val toString = "W" } +case object NoPerm extends PermLiteral(Rational.zero) { override lazy val toString = "Z" } +case object FullPerm extends PermLiteral(Rational.one) { override lazy val toString = "W" } -class FractionPermLiteral(r: Rational) extends PermLiteral(r) with ConditionalFlyweight[Rational, FractionPermLiteral] { +class FractionPermLiteral private[terms] (r: Rational) extends PermLiteral(r) with ConditionalFlyweight[Rational, FractionPermLiteral] { override val equalityDefiningMembers: Rational = r override lazy val toString = literal.toString } object FractionPermLiteral extends GeneralConditionalFlyweightFactory[Rational, Permissions, FractionPermLiteral] { override def apply(r: Rational) = r match { - case Rational(n, _) if n == 0 => NoPerm() - case Rational(n, d) if n == d => FullPerm() + case Rational(n, _) if n == 0 => NoPerm + case Rational(n, d) if n == d => FullPerm case _ => createIfNonExistent(r) } override def actualCreate(args: Rational): FractionPermLiteral = new FractionPermLiteral(args) } -class FractionPerm(val n: Term, val d: Term) +class FractionPerm private[terms] (val n: Term, val d: Term) extends Permissions with ConditionalFlyweight[(Term, Term), FractionPerm] { @@ -1211,7 +1220,7 @@ object FractionPerm extends GeneralConditionalFlyweightFactory[(Term, Term), Per override def actualCreate(args: (Term, Term)): FractionPerm = new FractionPerm(args._1, args._2) } -class IsValidPermVar(val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsValidPermVar] { +class IsValidPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsValidPermVar] { override val equalityDefiningMembers: Var = v override lazy val toString = s"PVar($v)" } @@ -1220,7 +1229,7 @@ object IsValidPermVar extends ConditionalFlyweightFactory[Var, IsValidPermVar] { override def actualCreate(args: Var): IsValidPermVar = new IsValidPermVar((args)) } -class IsReadPermVar(val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsReadPermVar] { +class IsReadPermVar private[terms] (val v: Var) extends BooleanTerm with ConditionalFlyweight[Var, IsReadPermVar] { override val equalityDefiningMembers: Var = v override lazy val toString = s"RdVar($v)" } @@ -1229,7 +1238,7 @@ object IsReadPermVar extends ConditionalFlyweightFactory[Var, IsReadPermVar] { override def actualCreate(args: Var): IsReadPermVar = new IsReadPermVar((args)) } -class PermTimes(val p0: Term, val p1: Term) +class PermTimes private[terms] (val p0: Term, val p1: Term) extends Permissions with ConditionalFlyweightBinaryOp[PermTimes] { @@ -1238,10 +1247,10 @@ class PermTimes(val p0: Term, val p1: Term) object PermTimes extends ConditionalFlyweightFactory[(Term, Term), PermTimes] { override def apply(v0: (Term, Term)) = v0 match { - case (FullPerm(), t) => t - case (t, FullPerm()) => t - case (NoPerm(), _) => NoPerm() - case (_, NoPerm()) => NoPerm() + case (FullPerm, t) => t + case (t, FullPerm) => t + case (NoPerm, _) => NoPerm + case (_, NoPerm) => NoPerm case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal * p1.literal) case (_, _) => createIfNonExistent(v0) } @@ -1249,10 +1258,10 @@ object PermTimes extends ConditionalFlyweightFactory[(Term, Term), PermTimes] { override def actualCreate(args: (Term, Term)): PermTimes = new PermTimes(args._1, args._2) } -class IntPermTimes(val p0: Term, val p1: Term) - extends Permissions - with BinaryOp[Term] - with ConditionalFlyweightBinaryOp[IntPermTimes] { +class IntPermTimes private[terms] (val p0: Term, val p1: Term) + extends ConditionalFlyweightBinaryOp[IntPermTimes] + with Permissions + with BinaryOp[Term] { override val op = "*" } @@ -1261,9 +1270,9 @@ object IntPermTimes extends ConditionalFlyweightFactory[(Term, Term), IntPermTim import predef.{Zero, One} override def apply(v0: (Term, Term)) = v0 match { - case (Zero, _) => NoPerm() + case (Zero, _) => NoPerm case (One, t) => t - case (_, NoPerm()) => NoPerm() + case (_, NoPerm) => NoPerm case (IntLiteral(i), p: PermLiteral) => FractionPermLiteral(Rational(i, 1) * p.literal) case (_, _) => createIfNonExistent(v0) } @@ -1271,10 +1280,10 @@ object IntPermTimes extends ConditionalFlyweightFactory[(Term, Term), IntPermTim override def actualCreate(args: (Term, Term)): IntPermTimes = new IntPermTimes(args._1, args._2) } -class PermIntDiv(val p0: Term, val p1: Term) - extends Permissions - with BinaryOp[Term] - with ConditionalFlyweightBinaryOp[PermIntDiv] { +class PermIntDiv private[terms] (val p0: Term, val p1: Term) + extends ConditionalFlyweightBinaryOp[PermIntDiv] + with Permissions + with BinaryOp[Term] { utils.assertSort(p1, "Second term", sorts.Int) @@ -1293,10 +1302,10 @@ object PermIntDiv extends ConditionalFlyweightFactory[(Term, Term), PermIntDiv] override def actualCreate(args: (Term, Term)): PermIntDiv = new PermIntDiv(args._1, args._2) } -class PermPermDiv(val p0: Term, val p1: Term) - extends Permissions - with BinaryOp[Term] - with ConditionalFlyweightBinaryOp[PermPermDiv] { +class PermPermDiv private[terms] (val p0: Term, val p1: Term) + extends ConditionalFlyweightBinaryOp[PermPermDiv] + with Permissions + with BinaryOp[Term] { utils.assertSort(p1, "Second term", sorts.Perm) @@ -1314,18 +1323,18 @@ object PermDiv extends ((Term, Term) => Term) { def apply(t0: Term, t1: Term) = PermTimes(t0, FractionPerm(One, t1)) } -class PermPlus(val p0: Term, val p1: Term) - extends Permissions - with BinaryOp[Term] - with ConditionalFlyweightBinaryOp[PermPlus] { +class PermPlus private[terms] (val p0: Term, val p1: Term) + extends ConditionalFlyweightBinaryOp[PermPlus] + with Permissions + with BinaryOp[Term] { override val op = "+" } object PermPlus extends ConditionalFlyweightFactory[(Term, Term), PermPlus] { override def apply(v0: (Term, Term)) = v0 match { - case (NoPerm(), t1) => t1 - case (t0, NoPerm()) => t0 + case (NoPerm, t1) => t1 + case (t0, NoPerm) => t0 case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal + p1.literal) case (FractionPerm(n1, d1), FractionPerm(n2, d2)) if d1 == d2 => FractionPerm(Plus(n1, n2), d1) case (PermMinus(t00, t01), t1) if t01 == t1 => t00 @@ -1337,7 +1346,7 @@ object PermPlus extends ConditionalFlyweightFactory[(Term, Term), PermPlus] { override def actualCreate(args: (Term, Term)): PermPlus = new PermPlus(args._1, args._2) } -class PermMinus(val p0: Term, val p1: Term) +class PermMinus private[terms] (val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] with ConditionalFlyweightBinaryOp[PermMinus] { @@ -1352,8 +1361,8 @@ class PermMinus(val p0: Term, val p1: Term) object PermMinus extends ConditionalFlyweightFactory[(Term, Term), PermMinus] { override def apply(v0: (Term, Term)) = v0 match { - case (t0, NoPerm()) => t0 - case (p0, p1) if p0 == p1 => NoPerm() + case (t0, NoPerm) => t0 + case (p0, p1) if p0 == p1 => NoPerm case (p0: PermLiteral, p1: PermLiteral) => FractionPermLiteral(p0.literal - p1.literal) case (p0, PermMinus(p1, p2)) if p0 == p1 => p2 case (PermPlus(p0, p1), p2) if p0 == p2 => p1 @@ -1364,7 +1373,7 @@ object PermMinus extends ConditionalFlyweightFactory[(Term, Term), PermMinus] { override def actualCreate(args: (Term, Term)): PermMinus = new PermMinus(args._1, args._2) } -class PermLess(val p0: Term, val p1: Term) +class PermLess private[terms] (val p0: Term, val p1: Term) extends BooleanTerm with BinaryOp[Term] with ConditionalFlyweightBinaryOp[PermLess] { @@ -1393,7 +1402,7 @@ object PermLess extends ConditionalFlyweightFactory[(Term, Term), PermLess] { override def actualCreate(args: (Term, Term)): PermLess = new PermLess(args._1, args._2) } -class PermAtMost(val p0: Term, val p1: Term) extends ComparisonTerm +class PermAtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm with ConditionalFlyweightBinaryOp[PermAtMost] { override val op = "<=" @@ -1409,7 +1418,7 @@ object PermAtMost extends ConditionalFlyweightFactory[(Term, Term), PermAtMost] override def actualCreate(args: (Term, Term)): PermAtMost = new PermAtMost(args._1, args._2) } -class PermMin(val p0: Term, val p1: Term) extends Permissions +class PermMin private[terms] (val p0: Term, val p1: Term) extends Permissions with BinaryOp[Term] with ConditionalFlyweightBinaryOp[PermMin] { @@ -1436,30 +1445,47 @@ sealed trait SeqTerm extends Term { val sort: sorts.Seq } -case class SeqRanged(p0: Term, p1: Term) extends SeqTerm /* with BinaryOp[Term] */ { +class SeqRanged private[terms] (val p0: Term, val p1: Term) extends SeqTerm /* with BinaryOp[Term] */ + with ConditionalFlyweight[(Term, Term), SeqRanged] { utils.assertSort(p0, "first operand", sorts.Int) utils.assertSort(p1, "second operand", sorts.Int) val elementsSort = sorts.Int val sort = sorts.Seq(elementsSort) + override val equalityDefiningMembers: (Term, Term) = (p0, p1) + override lazy val toString = s"[$p0..$p1]" } -case class SeqNil(elementsSort: Sort) extends SeqTerm with Literal { +object SeqRanged extends ConditionalFlyweightFactory[(Term, Term), SeqRanged] { + override def actualCreate(args: (Term, Term)): SeqRanged = new SeqRanged(args._1, args._2) +} + +class SeqNil private[terms] (val elementsSort: Sort) extends SeqTerm with Literal with ConditionalFlyweight[Sort, SeqNil] { val sort = sorts.Seq(elementsSort) override lazy val toString = "Nil" + override val equalityDefiningMembers: Sort = elementsSort +} + +object SeqNil extends ConditionalFlyweightFactory[Sort, SeqNil] { + override def actualCreate(args: Sort): SeqNil = new SeqNil(args) } -case class SeqSingleton(p: Term) extends SeqTerm /* with UnaryOp[Term] */ { +class SeqSingleton private[terms] (val p: Term) extends SeqTerm /* with UnaryOp[Term] */ with ConditionalFlyweight[Term, SeqSingleton] { val elementsSort = p.sort val sort = sorts.Seq(elementsSort) + override val equalityDefiningMembers: Term = p override lazy val toString = s"[$p]" } -class SeqAppend(val p0: Term, val p1: Term) extends SeqTerm - with StructuralEqualityBinaryOp[Term] { +object SeqSingleton extends GeneralConditionalFlyweightFactory[Term, SeqTerm, SeqSingleton] { + override def actualCreate(args: Term): SeqSingleton = new SeqSingleton(args) +} + +class SeqAppend private[terms] (val p0: Term, val p1: Term) extends SeqTerm + with ConditionalFlyweightBinaryOp[SeqAppend] { val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort val sort = sorts.Seq(elementsSort) @@ -1467,17 +1493,17 @@ class SeqAppend(val p0: Term, val p1: Term) extends SeqTerm override val op = "++" } -object SeqAppend extends ((Term, Term) => SeqTerm) { - def apply(t0: Term, t1: Term) = { - utils.assertSameSorts[sorts.Seq](t0, t1) - new SeqAppend(t0, t1) +object SeqAppend extends ConditionalFlyweightFactory[(Term, Term), SeqAppend] { + override def apply(v0: (Term, Term)) = { + utils.assertSameSorts[sorts.Seq](v0._1, v0._2) + createIfNonExistent(v0) } - def unapply(sa: SeqAppend) = Some((sa.p0, sa.p1)) + override def actualCreate(args: (Term, Term)): SeqAppend = new SeqAppend(args._1, args._2) } -class SeqDrop(val p0: Term, val p1: Term) extends SeqTerm - with StructuralEqualityBinaryOp[Term] { +class SeqDrop private[terms] (val p0: Term, val p1: Term) extends SeqTerm + with ConditionalFlyweightBinaryOp[SeqDrop] { val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort val sort = sorts.Seq(elementsSort) @@ -1485,18 +1511,19 @@ class SeqDrop(val p0: Term, val p1: Term) extends SeqTerm override lazy val toString = p0.toString + "[" + p1.toString + ":]" } -object SeqDrop extends ((Term, Term) => SeqTerm) { - def apply(t0: Term, t1: Term) = { +object SeqDrop extends ConditionalFlyweightFactory[(Term, Term), SeqDrop] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) utils.assertSort(t1, "second operand", sorts.Int) - new SeqDrop(t0, t1) + createIfNonExistent(v0) } - def unapply(sd: SeqDrop) = Some((sd.p0, sd.p1)) + override def actualCreate(args: (Term, Term)): SeqDrop = new SeqDrop(args._1, args._2) } -class SeqTake(val p0: Term, val p1: Term) extends SeqTerm - with StructuralEqualityBinaryOp[Term] { +class SeqTake private[terms] (val p0: Term, val p1: Term) extends SeqTerm + with ConditionalFlyweightBinaryOp[SeqTake] { val elementsSort = p0.sort.asInstanceOf[sorts.Seq].elementsSort val sort = sorts.Seq(elementsSort) @@ -1504,86 +1531,90 @@ class SeqTake(val p0: Term, val p1: Term) extends SeqTerm override lazy val toString = p0.toString + "[:" + p1.toString + "]" } -object SeqTake extends ((Term, Term) => SeqTerm) { - def apply(t0: Term, t1: Term) = { +object SeqTake extends ConditionalFlyweightFactory[(Term, Term), SeqTake] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) utils.assertSort(t1, "second operand", sorts.Int) - new SeqTake(t0, t1) + createIfNonExistent(v0) } - def unapply(st: SeqTake) = Some((st.p0, st.p1)) + override def actualCreate(args: (Term, Term)): SeqTake = new SeqTake(args._1, args._2) } -class SeqLength(val p: Term) extends Term - with StructuralEqualityUnaryOp[Term] { +class SeqLength private[terms] (val p: Term) extends Term + with ConditionalFlyweightUnaryOp[SeqLength] { val sort = sorts.Int override lazy val toString = s"|$p|" } -object SeqLength { - def apply(t: Term) = { +object SeqLength extends ConditionalFlyweightFactory [Term, SeqLength] { + override def apply(t: Term) = { utils.assertSort(t, "term", "Seq", _.isInstanceOf[sorts.Seq]) - new SeqLength(t) + createIfNonExistent(t) } - def unapply(sl: SeqLength) = Some(sl.p) + override def actualCreate(args: Term): SeqLength = new SeqLength(args) } -class SeqAt(val p0: Term, val p1: Term) extends Term - with StructuralEqualityBinaryOp[Term] { +class SeqAt private[terms] (val p0: Term, val p1: Term) extends Term + with ConditionalFlyweightBinaryOp[SeqAt] { val sort = p0.sort.asInstanceOf[sorts.Seq].elementsSort override lazy val toString = s"$p0[$p1]" } -object SeqAt extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) = { +object SeqAt extends ConditionalFlyweightFactory[(Term, Term), SeqAt] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) utils.assertSort(t1, "second operand", sorts.Int) - new SeqAt(t0, t1) + createIfNonExistent(v0) } - def unapply(sa: SeqAt) = Some((sa.p0, sa.p1)) + override def actualCreate(args: (Term, Term)): SeqAt = new SeqAt(args._1, args._2) } -class SeqIn(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { +class SeqIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm + with ConditionalFlyweightBinaryOp[SeqIn] { override lazy val toString = s"$p1 in $p0" } -object SeqIn extends ((Term, Term) => BooleanTerm) { - def apply(t0: Term, t1: Term) = { +object SeqIn extends ConditionalFlyweightFactory[(Term, Term), SeqIn] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Seq].elementsSort) - new SeqIn(t0, t1) + createIfNonExistent(v0) } - def unapply(si: SeqIn) = Some((si.p0, si.p1)) + override def actualCreate(args: (Term, Term)): SeqIn = new SeqIn(args._1, args._2) } -class SeqUpdate(val t0: Term, val t1: Term, val t2: Term) +class SeqUpdate private[terms] (val t0: Term, val t1: Term, val t2: Term) extends SeqTerm - with StructuralEquality { + with ConditionalFlyweight[(Term, Term, Term), SeqUpdate] { val sort = t0.sort.asInstanceOf[sorts.Seq] val elementsSort = sort.elementsSort - val equalityDefiningMembers = t0 :: t1 :: t2 :: Nil + val equalityDefiningMembers = (t0, t1, t2) override lazy val toString = s"$t0[$t1] := $t2" } -object SeqUpdate extends ((Term, Term, Term) => SeqTerm) { - def apply(t0: Term, t1: Term, t2: Term) = { +object SeqUpdate extends ConditionalFlyweightFactory[(Term, Term, Term), SeqUpdate] { + override def apply(v0: (Term, Term, Term)) = { + val (t0, t1, t2) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) utils.assertSort(t1, "second operand", sorts.Int) utils.assertSort(t2, "third operand", t0.sort.asInstanceOf[sorts.Seq].elementsSort) - new SeqUpdate(t0, t1, t2) + createIfNonExistent(v0) } - def unapply(su: SeqUpdate) = Some((su.t0, su.t1, su.t2)) + override def actualCreate(args: (Term, Term, Term)): SeqUpdate = new SeqUpdate(args._1, args._2, args._3) } /* Sets */ @@ -1593,27 +1624,37 @@ sealed trait SetTerm extends Term { val sort: sorts.Set } -sealed trait BinarySetOp extends SetTerm - with StructuralEqualityBinaryOp[Term] { - +sealed trait BinarySetOp extends SetTerm { + val p0: Term + val p1: Term val elementsSort = p0.sort.asInstanceOf[sorts.Set].elementsSort val sort = sorts.Set(elementsSort) } -case class EmptySet(elementsSort: Sort) extends SetTerm with Literal { +class EmptySet private[terms] (val elementsSort: Sort) extends ConditionalFlyweight[Sort, EmptySet] with SetTerm with Literal { val sort = sorts.Set(elementsSort) override lazy val toString = "Ø" + override val equalityDefiningMembers: Sort = elementsSort } -case class SingletonSet(p: Term) extends SetTerm /* with UnaryOp[Term] */ { +object EmptySet extends ConditionalFlyweightFactory[Sort, EmptySet] { + override def actualCreate(args: Sort): EmptySet = new EmptySet(args) +} + +class SingletonSet private [terms] (val p: Term) extends ConditionalFlyweight[Term, SingletonSet] with SetTerm /* with UnaryOp[Term] */ { val elementsSort = p.sort val sort = sorts.Set(elementsSort) override lazy val toString = s"{$p}" + override val equalityDefiningMembers: Term = p +} + +object SingletonSet extends PreciseConditionalFlyweightFactory[Term, SingletonSet] { + override def actualCreate(args: Term): SingletonSet = new SingletonSet(args) } -class SetAdd(val p0: Term, val p1: Term) extends SetTerm - with StructuralEqualityBinaryOp[Term] { +class SetAdd private[terms] (val p0: Term, val p1: Term) extends SetTerm + with ConditionalFlyweightBinaryOp[SetAdd] { val elementsSort = p0.sort.asInstanceOf[sorts.Set].elementsSort val sort = sorts.Set(elementsSort) @@ -1621,115 +1662,122 @@ class SetAdd(val p0: Term, val p1: Term) extends SetTerm override val op = "+" } -object SetAdd extends ((Term, Term) => SetTerm) { - def apply(t0: Term, t1: Term) = { +object SetAdd extends ConditionalFlyweightFactory[(Term, Term), SetAdd] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Set]) utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Set].elementsSort) - new SetAdd(t0, t1) + createIfNonExistent(v0) } - def unapply(sa: SetAdd) = Some((sa.p0, sa.p1)) + override def actualCreate(args: (Term, Term)): SetAdd = new SetAdd(args._1, args._2) } -class SetUnion(val p0: Term, val p1: Term) extends BinarySetOp { +class SetUnion(val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetUnion] with BinarySetOp { override val op = "∪" } -object SetUnion extends ((Term, Term) => SetTerm) { - def apply(t0: Term, t1: Term) = { +object SetUnion extends PreciseConditionalFlyweightFactory[(Term, Term), SetUnion] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) - new SetUnion(t0, t1) + createIfNonExistent(v0) } - def unapply(su: SetUnion) = Some((su.p0, su.p1)) + override def actualCreate(args: (Term, Term)): SetUnion = new SetUnion(args._1, args._2) } -class SetIntersection(val p0: Term, val p1: Term) extends BinarySetOp { +class SetIntersection private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetIntersection] with BinarySetOp { override val op = "∩" } -object SetIntersection extends ((Term, Term) => SetTerm) { - def apply(t0: Term, t1: Term) = { +object SetIntersection extends PreciseConditionalFlyweightFactory[(Term, Term), SetIntersection] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) - new SetIntersection(t0, t1) + createIfNonExistent(v0) } - def unapply(si: SetIntersection) = Some((si.p0, si.p1)) + override def actualCreate(args: (Term, Term)): SetIntersection = new SetIntersection(args._1, args._2) } -class SetSubset(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { +class SetSubset private[terms] (val p0: Term, val p1: Term) extends BooleanTerm + with ConditionalFlyweightBinaryOp[SetSubset] { override val op = "⊂" } -object SetSubset extends ((Term, Term) => BooleanTerm) { - def apply(t0: Term, t1: Term) = { +object SetSubset extends PreciseConditionalFlyweightFactory[(Term, Term), SetSubset] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) - new SetSubset(t0, t1) + createIfNonExistent(v0) } - def unapply(ss: SetSubset) = Some((ss.p0, ss.p1)) + override def actualCreate(args: (Term, Term)): SetSubset = new SetSubset(args._1, args._2) } -class SetDisjoint(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { +class SetDisjoint private[terms] (val p0: Term, val p1: Term) extends BooleanTerm + with ConditionalFlyweightBinaryOp[SetDisjoint] { override val op = "disj" } -object SetDisjoint extends ((Term, Term) => BooleanTerm) { - def apply(t0: Term, t1: Term) = { +object SetDisjoint extends PreciseConditionalFlyweightFactory[(Term, Term), SetDisjoint] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) - new SetDisjoint(t0, t1) + createIfNonExistent(v0) } - def unapply(sd: SetDisjoint) = Some((sd.p0, sd.p1)) + override def actualCreate(args: (Term, Term)): SetDisjoint = new SetDisjoint(args._1, args._2) } -class SetDifference(val p0: Term, val p1: Term) extends BinarySetOp { +class SetDifference private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[SetDifference] with BinarySetOp { override val op = "\\" } -object SetDifference extends ((Term, Term) => SetTerm) { - def apply(t0: Term, t1: Term) = { +object SetDifference extends PreciseConditionalFlyweightFactory[(Term, Term), SetDifference] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) - new SetDifference(t0, t1) + createIfNonExistent(v0) } - def unapply(sd: SetDifference) = Some((sd.p0, sd.p1)) + override def actualCreate(args: (Term, Term)): SetDifference = new SetDifference(args._1, args._2) } -class SetIn(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { +class SetIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm + with ConditionalFlyweightBinaryOp[SetIn] { override val op = "in" } -object SetIn extends ((Term, Term) => BooleanTerm) { - def apply(t0: Term, t1: Term) = { +object SetIn extends PreciseConditionalFlyweightFactory[(Term, Term), SetIn] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t1, "second operand", "Set", _.isInstanceOf[sorts.Set]) utils.assertSort(t0, "first operand", t1.sort.asInstanceOf[sorts.Set].elementsSort) - new SetIn(t0, t1) + createIfNonExistent(v0) } - def unapply(si: SetIn) = Some((si.p0, si.p1)) + override def actualCreate(args: (Term, Term)): SetIn = new SetIn(args._1, args._2) } -class SetCardinality(val p: Term) extends Term - with StructuralEqualityUnaryOp[Term] { +class SetCardinality private[terms] (val p: Term) extends Term + with ConditionalFlyweightUnaryOp[SetCardinality] { val sort = sorts.Int override lazy val toString = s"|$p|" } -object SetCardinality extends (Term => SetCardinality) { - def apply(t: Term) = { +object SetCardinality extends PreciseConditionalFlyweightFactory[Term, SetCardinality] { + override def apply(t: Term) = { utils.assertSort(t, "term", "Set", _.isInstanceOf[sorts.Set]) - new SetCardinality(t) + createIfNonExistent(t) } - def unapply(sc: SetCardinality) = Some(sc.p) + override def actualCreate(args: Term): SetCardinality = new SetCardinality(args) } /* Multisets */ @@ -1739,130 +1787,143 @@ sealed trait MultisetTerm extends Term { val sort: sorts.Multiset } -sealed trait BinaryMultisetOp extends MultisetTerm - with StructuralEqualityBinaryOp[Term] { +sealed trait BinaryMultisetOp extends MultisetTerm { + val p0: Term val elementsSort = p0.sort.asInstanceOf[sorts.Multiset].elementsSort val sort = sorts.Multiset(elementsSort) } -case class EmptyMultiset(elementsSort: Sort) extends MultisetTerm with Literal { +class EmptyMultiset private[terms] (val elementsSort: Sort) extends MultisetTerm with Literal with ConditionalFlyweight[Sort, EmptyMultiset] { val sort = sorts.Multiset(elementsSort) override lazy val toString = "Ø" + override val equalityDefiningMembers: Sort = elementsSort } -case class SingletonMultiset(p: Term) extends MultisetTerm /* with UnaryOp[Term] */ { +object EmptyMultiset extends PreciseConditionalFlyweightFactory[Sort, EmptyMultiset] { + override def actualCreate(args: Sort): EmptyMultiset = new EmptyMultiset(args) +} + +class SingletonMultiset private[terms] (val p: Term) extends MultisetTerm /* with UnaryOp[Term] */ with ConditionalFlyweight[Term, SingletonMultiset] { val elementsSort = p.sort val sort = sorts.Multiset(elementsSort) override lazy val toString = s"{$p}" + override val equalityDefiningMembers: Term = p } -class MultisetAdd(val p0: Term, val p1: Term) extends MultisetTerm - with StructuralEqualityBinaryOp[Term] { +object SingletonMultiset extends PreciseConditionalFlyweightFactory[Term, SingletonMultiset] { + override def actualCreate(args: Term): SingletonMultiset = new SingletonMultiset((args)) +} - val elementsSort = p0.sort.asInstanceOf[sorts.Multiset].elementsSort - val sort = sorts.Multiset(elementsSort) +class MultisetAdd private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp + with ConditionalFlyweightBinaryOp[MultisetAdd] { override val op = "+" } -object MultisetAdd extends ((Term, Term) => MultisetTerm) { - def apply(t0: Term, t1: Term) = { +object MultisetAdd extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetAdd] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Multiset]) utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Multiset].elementsSort) - new MultisetAdd(t0, t1) + createIfNonExistent(v0) } - def unapply(ma: MultisetAdd) = Some((ma.p0, ma.p1)) + override def actualCreate(args: (Term, Term)): MultisetAdd = new MultisetAdd(args._1, args._2) } -class MultisetUnion(val p0: Term, val p1: Term) extends BinaryMultisetOp { +class MultisetUnion private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetUnion] { override val op = "∪" } -object MultisetUnion extends ((Term, Term) => MultisetTerm) { - def apply(t0: Term, t1: Term) = { +object MultisetUnion extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetUnion] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) - new MultisetUnion(t0, t1) + createIfNonExistent(v0) } - def unapply(mu: MultisetUnion) = Some((mu.p0, mu.p1)) + override def actualCreate(args: (Term, Term)): MultisetUnion = new MultisetUnion(args._1, args._2) } -class MultisetIntersection(val p0: Term, val p1: Term) extends BinaryMultisetOp { +class MultisetIntersection private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetIntersection] { override val op = "∩" } -object MultisetIntersection extends ((Term, Term) => MultisetTerm) { - def apply(t0: Term, t1: Term) = { +object MultisetIntersection extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetIntersection] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) - new MultisetIntersection(t0, t1) + createIfNonExistent(v0) } - def unapply(mi: MultisetIntersection) = Some((mi.p0, mi.p1)) + override def actualCreate(args: (Term, Term)): MultisetIntersection = new MultisetIntersection(args._1, args._2) } -class MultisetSubset(val p0: Term, val p1: Term) extends BooleanTerm - with StructuralEqualityBinaryOp[Term] { +class MultisetSubset private[terms] (val p0: Term, val p1: Term) extends BooleanTerm + with ConditionalFlyweightBinaryOp[MultisetSubset] { override val op = "⊂" } -object MultisetSubset extends ((Term, Term) => BooleanTerm) { - def apply(t0: Term, t1: Term) = { +object MultisetSubset extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetSubset] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) - new MultisetSubset(t0, t1) + createIfNonExistent(v0) } - def unapply(ms: MultisetSubset) = Some((ms.p0, ms.p1)) + override def actualCreate(args: (Term, Term)): MultisetSubset = new MultisetSubset(args._1, args._2) } -class MultisetDifference(val p0: Term, val p1: Term) extends BinaryMultisetOp { +class MultisetDifference private[terms] (val p0: Term, val p1: Term) extends BinaryMultisetOp with ConditionalFlyweightBinaryOp[MultisetDifference] { override val op = "\\" } -object MultisetDifference extends ((Term, Term) => MultisetTerm) { - def apply(t0: Term, t1: Term) = { +object MultisetDifference extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetDifference] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) - new MultisetDifference(t0, t1) + createIfNonExistent(v0) } - def unapply(md: MultisetDifference) = Some((md.p0, md.p1)) + override def actualCreate(args: (Term, Term)): MultisetDifference = new MultisetDifference(args._1, args._2) } -class MultisetCardinality(val p: Term) extends Term - with StructuralEqualityUnaryOp[Term] { +class MultisetCardinality private[terms] (val p: Term) extends Term + with ConditionalFlyweightUnaryOp[MultisetCardinality] { val sort = sorts.Int override lazy val toString = s"|$p|" } -object MultisetCardinality extends (Term => MultisetCardinality) { - def apply(t: Term) = { +object MultisetCardinality extends PreciseConditionalFlyweightFactory[Term, MultisetCardinality] { + override def apply(t: Term) = { utils.assertSort(t, "term", "Multiset", _.isInstanceOf[sorts.Multiset]) - new MultisetCardinality(t) + createIfNonExistent(t) } - def unapply(mc: MultisetCardinality) = Some(mc.p) + override def actualCreate(args: Term): MultisetCardinality = new MultisetCardinality(args) } -class MultisetCount(val p0: Term, val p1: Term) extends Term - with StructuralEqualityBinaryOp[Term] { +class MultisetCount private[terms] (val p0: Term, val p1: Term) extends Term + with ConditionalFlyweightBinaryOp[MultisetCount] { val sort = sorts.Int override lazy val toString = s"$p0($p1)" } -object MultisetCount extends { - def apply(ms: Term, el: Term) = { +object MultisetCount extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetCount] { + override def apply(v0: (Term, Term)) = { + val (ms, el) = v0 utils.assertSort(ms, "first operand", "Multiset", _.isInstanceOf[sorts.Multiset]) utils.assertSort(el, "second operand", ms.sort.asInstanceOf[sorts.Multiset].elementsSort) - new MultisetCount(ms, el) + createIfNonExistent(v0) } - def unapply(mc: MultisetCount) = Some((mc.p0, mc.p1)) + override def actualCreate(args: (Term, Term)): MultisetCount = new MultisetCount(args._1, args._2) } /* Maps */ @@ -1873,88 +1934,95 @@ sealed trait MapTerm extends Term { val sort: sorts.Map } -case class EmptyMap(keySort: Sort, valueSort: Sort) extends MapTerm with Literal { +class EmptyMap private[terms] (val keySort: Sort, val valueSort: Sort) extends MapTerm with Literal with ConditionalFlyweight[(Sort, Sort), EmptyMap] { val sort = sorts.Map(keySort, valueSort) override lazy val toString = "Ø" + override val equalityDefiningMembers: (Sort, Sort) = (keySort, valueSort) +} + +object EmptyMap extends PreciseConditionalFlyweightFactory[(Sort, Sort), EmptyMap] { + override def actualCreate(args: (Sort, Sort)): EmptyMap = new EmptyMap(args._1, args._2) } -class MapLookup(base: Term, key: Term) extends Term with StructuralEqualityBinaryOp[Term] { +class MapLookup private[terms] (val base: Term, val key: Term) extends Term with ConditionalFlyweightBinaryOp[MapLookup] { val sort: Sort = p0.sort.asInstanceOf[sorts.Map].valueSort override def p0: Term = base override def p1: Term = key override lazy val toString = s"$p0[$p1]" } -object MapLookup extends ((Term, Term) => Term) { - def apply(t0: Term, t1: Term) : Term = { +object MapLookup extends PreciseConditionalFlyweightFactory[(Term, Term), MapLookup] { + override def apply(v0: (Term, Term)) = { + val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map]) utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Map].keySort) - new MapLookup(t0, t1) + createIfNonExistent(v0) } - def unapply(ml: MapLookup) = Some((ml.p0, ml.p1)) + override def actualCreate(args: (Term, Term)): MapLookup = new MapLookup(args._1, args._2) } -class MapCardinality(val p: Term) extends Term with StructuralEqualityUnaryOp[Term] { +class MapCardinality private[terms] (val p: Term) extends Term with ConditionalFlyweightUnaryOp[MapCardinality] { val sort = sorts.Int override lazy val toString = s"|$p|" } -object MapCardinality extends (Term => MapCardinality) { - def apply(t: Term) : MapCardinality = { +object MapCardinality extends PreciseConditionalFlyweightFactory[Term, MapCardinality] { + override def apply(t: Term) : MapCardinality = { utils.assertSort(t, "term", "Map", _.isInstanceOf[sorts.Map]) - new MapCardinality(t) + createIfNonExistent(t) } - def unapply(mc: MapCardinality) = Some(mc.p) + override def actualCreate(args: Term): MapCardinality = new MapCardinality(args) } -class MapUpdate(val base: Term, val key: Term, val value: Term) extends MapTerm with StructuralEquality { +class MapUpdate private[terms] (val base: Term, val key: Term, val value: Term) extends MapTerm with ConditionalFlyweight[(Term, Term, Term), MapUpdate] { override val sort: sorts.Map = base.sort.asInstanceOf[sorts.Map] override val keySort: Sort = sort.keySort override val valueSort: Sort = sort.valueSort - override val equalityDefiningMembers: Seq[Any] = Seq(base, key, value) + override val equalityDefiningMembers = (base, key, value) } -object MapUpdate extends ((Term, Term, Term) => MapTerm) { - def apply(t0: Term, t1: Term, t2: Term) : MapUpdate = { +object MapUpdate extends PreciseConditionalFlyweightFactory[(Term, Term, Term), MapUpdate] { + override def apply(v0: (Term, Term, Term)) : MapUpdate = { + val (t0, t1, t2) = v0 utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map]) utils.assertSort(t1, "second operand", t0.sort.asInstanceOf[sorts.Map].keySort) utils.assertSort(t2, "third operand", t0.sort.asInstanceOf[sorts.Map].valueSort) - new MapUpdate(t0, t1, t2) + createIfNonExistent(v0) } - def unapply(mu: MapUpdate) = Some((mu.base, mu.key, mu.value)) + override def actualCreate(args: (Term, Term, Term)): MapUpdate = new MapUpdate(args._1, args._2, args._3) } -class MapDomain(val p: Term) extends SetTerm with StructuralEqualityUnaryOp[Term] { +class MapDomain private[terms] (val p: Term) extends SetTerm with ConditionalFlyweightUnaryOp[MapDomain] { override val elementsSort: Sort = p.sort.asInstanceOf[sorts.Map].keySort override val sort: sorts.Set = sorts.Set(elementsSort) override lazy val toString = s"domain($p)" } -object MapDomain extends (Term => SetTerm) { - def apply(t0: Term) : SetTerm = { +object MapDomain extends PreciseConditionalFlyweightFactory[Term, MapDomain] { + override def apply(t0: Term) = { utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map]) - new MapDomain(t0) + createIfNonExistent(t0) } - def unapply(md : MapDomain) = Some(md.p) + override def actualCreate(args: Term): MapDomain = new MapDomain(args) } -class MapRange(val p: Term) extends SetTerm with StructuralEqualityUnaryOp[Term] { +class MapRange private[terms] (val p: Term) extends SetTerm with ConditionalFlyweightUnaryOp[MapRange] { override val elementsSort: Sort = p.sort.asInstanceOf[sorts.Map].valueSort override val sort: sorts.Set = sorts.Set(elementsSort) override lazy val toString = s"range($p)" } -object MapRange extends (Term => SetTerm) { - def apply(t0: Term) : SetTerm = { +object MapRange extends PreciseConditionalFlyweightFactory[Term, MapRange] { + override def apply(t0: Term) = { utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map]) - new MapRange(t0) + createIfNonExistent(t0) } - def unapply(mr : MapRange) = Some(mr.p) + override def actualCreate(args: Term): MapRange = new MapRange(args) } /* Snapshots */ @@ -2352,24 +2420,24 @@ object predef { object perms { def IsNonNegative(p: Term): Term = - Or(p === NoPerm(), IsPositive(p)) + Or(p === NoPerm, IsPositive(p)) /* All basic static simplifications should be covered by Equals, * IsPositive and or */ def IsPositive(p: Term): Term = p match { case p: PermLiteral => if (p.literal > Rational.zero) True else False - case _ => PermLess(NoPerm(), p) + case _ => PermLess(NoPerm, p) } def IsNonPositive(p: Term): Term = p match { case p: PermLiteral => if (p.literal <= Rational.zero) True else False - case _ => Or(p === NoPerm(), PermLess(p, NoPerm())) + case _ => Or(p === NoPerm, PermLess(p, NoPerm)) } def BigPermSum(it: Iterable[Term], f: Term => Term = t => t): Term = { def binaryPermPlus(t0: Term, t1: Term) = PermPlus(t0, t1) - viper.silicon.utils.mapReduceLeft(it, f, binaryPermPlus, NoPerm()) + viper.silicon.utils.mapReduceLeft(it, f, binaryPermPlus, NoPerm) } } diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index ca029a862..132e70450 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -40,9 +40,18 @@ trait ExpressionTranslator { } def translateAnySetBinExp(exp: ast.AnySetBinExp, + setTerm: ((Term, Term)) => Term, + multisetTerm: ((Term, Term)) => Term, + anysetTypedExp: ast.Exp = exp): Term = { + def setFun(t0: Term, t1: Term): Term = setTerm((t0, t1)) + def multisetFun(t0: Term, t1: Term): Term = multisetTerm((t0, t1)) + actualTranslateAnySetBinExp(exp, setFun _, multisetFun _, anysetTypedExp) + } + + def actualTranslateAnySetBinExp(exp: ast.AnySetBinExp, setTerm: (Term, Term) => Term, multisetTerm: (Term, Term) => Term, - anysetTypedExp: ast.Exp = exp) = + anysetTypedExp: ast.Exp = exp): Term = anysetTypedExp.typ match { case _: ast.SetType => setTerm(f(exp.left), f(exp.right)) @@ -148,11 +157,11 @@ trait ExpressionTranslator { /* Permissions */ - case _: ast.FullPerm => FullPerm() - case _: ast.NoPerm => NoPerm() + case _: ast.FullPerm => FullPerm + case _: ast.NoPerm => NoPerm case ast.FractionalPerm(e0, e1) => FractionPerm(f(e0), f(e1)) - case ast.PermMinus(e0) => PermMinus(NoPerm(), f(e0)) + case ast.PermMinus(e0) => PermMinus(NoPerm, f(e0)) case ast.PermAdd(e0, e1) => PermPlus(f(e0), f(e1)) case ast.PermSub(e0, e1) => PermMinus(f(e0), f(e1)) case ast.PermMul(e0, e1) => PermTimes(f(e0), f(e1)) @@ -197,7 +206,7 @@ trait ExpressionTranslator { case as: ast.AnySetIntersection => translateAnySetBinExp(as, SetIntersection, MultisetIntersection) case as: ast.AnySetSubset => translateAnySetBinExp(as, SetSubset, MultisetSubset, as.left) case as: ast.AnySetMinus => translateAnySetBinExp(as, SetDifference, MultisetDifference) - case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, (t0, t1) => MultisetCount(t1, t0), as.right) + case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, v0 => MultisetCount(v0._2, v0._1), as.right) case as: ast.AnySetCardinality => translateAnySetUnExp(as, SetCardinality, MultisetCardinality, as.exp) /* Maps */ diff --git a/src/test/scala/TriggerGeneratorTests.scala b/src/test/scala/TriggerGeneratorTests.scala index afe163500..2a7b831b9 100644 --- a/src/test/scala/TriggerGeneratorTests.scala +++ b/src/test/scala/TriggerGeneratorTests.scala @@ -6,13 +6,20 @@ package viper.silicon.tests +import org.scalatest.BeforeAndAfter import org.scalatest.funsuite.AnyFunSuite +import viper.silicon.Config import viper.silicon.state.Identifier import viper.silicon.state.terms._ +import viper.silicon.verifier.Verifier -class TriggerGeneratorTests extends AnyFunSuite { +class TriggerGeneratorTests extends AnyFunSuite with BeforeAndAfter { val triggerGenerator = new TriggerGenerator() + before { + Verifier.config = new Config(Seq()) + } + test("Work in simple cases") { val i = Var(Identifier("i"), sorts.Int) val s = Var(Identifier("S"), sorts.Seq(sorts.Int)) diff --git a/src/test/scala/TriggerRewriterTests.scala b/src/test/scala/TriggerRewriterTests.scala index c7b29a3d2..e9ad7c5fe 100644 --- a/src/test/scala/TriggerRewriterTests.scala +++ b/src/test/scala/TriggerRewriterTests.scala @@ -7,14 +7,16 @@ package viper.silicon.tests import java.io.{PrintWriter, StringWriter} - import org.scalatest.matchers.should.Matchers import viper.silicon.state.Identifier import DSL._ +import org.scalatest.BeforeAndAfter import org.scalatest.funsuite.AnyFunSuite +import viper.silicon.Config import viper.silicon.state.terms._ +import viper.silicon.verifier.Verifier -class TriggerRewriterTests extends AnyFunSuite with Matchers { +class TriggerRewriterTests extends AnyFunSuite with Matchers with BeforeAndAfter { val dummySink = new PrintWriter(new StringWriter()) // val dummyLogger = new MultiRunLogger(dummySink, () => None) val counter = new viper.silicon.utils.Counter() @@ -32,13 +34,18 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers { } } - val x0 = Var(Identifier("x0"), sorts.Int) - val x1 = Var(Identifier("x1"), sorts.Int) - val y0 = Var(Identifier("y0"), sorts.Int) - val z0 = Var(Identifier("z0"), sorts.Int) + lazy val x0 = Var(Identifier("x0"), sorts.Int) + lazy val x1 = Var(Identifier("x1"), sorts.Int) + lazy val y0 = Var(Identifier("y0"), sorts.Int) + lazy val z0 = Var(Identifier("z0"), sorts.Int) import rewriter.rewrite + before { + Verifier.config = new Config(Seq()) + } + + test("No-ops") { val forall1 = Forall(x, True, Trigger(f(x)), "forall1") val forall2 = Forall(x, f(x), Trigger(f(x)), "forall2") @@ -51,50 +58,50 @@ class TriggerRewriterTests extends AnyFunSuite with Matchers { test("Successes") { rewrite( - Forall(x, x > `0`, Trigger(f(x + n))) + Forall(x, x > `0`, Trigger(f(x + n)), "") ) should be (Some( - Forall(x0, x0 - n > `0`, Trigger(f(x0))) + Forall(x0, x0 - n > `0`, Trigger(f(x0)), "") )) rewrite( - Forall(x, f(x, x + `1`) > x, Trigger(f(x, x + `1`))) + Forall(x, f(x, x + `1`) > x, Trigger(f(x, x + `1`)), "") ) should be (Some( Forall(Seq(x, x0), /* TODO: Make order of variables predictable (or use an ordered set) */ (x === x0 - `1`) ==> (f(x, x0) > x), - Trigger(f(x, x0))) + Trigger(f(x, x0)), "") )) rewrite( - Forall(x, f(x + `1`) === g(x - `2`) + f(x), Trigger(Seq(f(x + `1`), g(x - `2`)))) + Forall(x, f(x + `1`) === g(x - `2`) + f(x), Trigger(Seq(f(x + `1`), g(x - `2`))), "") ) should contain oneOf ( // TODO: Can we make the result deterministic? Forall(Seq(x0, x1), (x0 - `1` === x1 + `2`) ==> (f(x0) === g(x1) + f(x0 - `1`)), - Trigger(Seq(f(x0), g(x1)))) + Trigger(Seq(f(x0), g(x1))), "") , Forall(Seq(x0, x1), (x0 - `1` === x1 + `2`) ==> (f(x0) === g(x1) + f(x1 + `2`)), - Trigger(Seq(f(x0), g(x1)))) + Trigger(Seq(f(x0), g(x1))), "") ) rewrite( - Forall(Seq(x, y, z), f(x, y + `1`) > z, Trigger(g(x, y + `1`, z))) + Forall(Seq(x, y, z), f(x, y + `1`) > z, Trigger(g(x, y + `1`, z)), "") ) should be (Some( - Forall(Seq(x, z, y0), f(x, y0) > z, Trigger(g(x, y0, z))) + Forall(Seq(x, z, y0), f(x, y0) > z, Trigger(g(x, y0, z)), "") )) } test("Failures") { rewrite( - Forall(x, True, Trigger(f(x * n))) + Forall(x, True, Trigger(f(x * n)), "") ) should be (None) /* Multiplication is currently not handled */ rewrite( - Forall(x, True, Trigger(f(x / n))) + Forall(x, True, Trigger(f(x / n)), "") ) should be (None) /* Division is currently not handled */ rewrite( - Forall(Seq(x, y), True, Trigger(f(x + y))) + Forall(Seq(x, y), True, Trigger(f(x + y)), "") ) should be (None) /* Invalid triggers that mention more than one quantified variable are currently not handled */ } } From 0c98aa94b123f0efeff4a68ceabc9dfd13afcf46 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 23 Feb 2023 17:00:40 +0100 Subject: [PATCH 07/15] Turning on flyweight only for Z3 API mode --- src/main/scala/Config.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index b1ecca455..50ee0cb15 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -550,7 +550,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { proverArgs.flatMap(args => proverTimeoutArg findFirstMatchIn args map(_.group(1).toInt))} .getOrElse(0) - lazy val useFlyweight: Boolean = true // prover() == "Z3-API" + lazy val useFlyweight: Boolean = prover() == "Z3-API" val maxHeuristicsDepth: ScallopOption[Int] = opt[Int]("maxHeuristicsDepth", descr = "Maximal number of nested heuristics applications (default: 3)", From 40bc2a7c642a424cb28979b58a5c28dd6414b1f4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 28 Feb 2023 15:46:35 +0100 Subject: [PATCH 08/15] Omitting pattern simplification, filtering invalid patterns after Z3 rejects them, dropping MCE macros which lead to additional terms --- .../scala/decider/TermToZ3APIConverter.scala | 12 +++++++++--- src/main/scala/decider/Z3ProverAPI.scala | 16 +++++++++++++--- .../rules/MoreCompleteExhaleSupporter.scala | 12 ++++++------ 3 files changed, 28 insertions(+), 12 deletions(-) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index e6c9f04ab..5ed3e1b5e 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -258,11 +258,17 @@ class TermToZ3APIConverter } else{ val qvarExprs = vars.map(v => convert(v)).toArray val nonEmptyTriggers = triggers.filter(_.p.nonEmpty) - val patterns = if (nonEmptyTriggers.nonEmpty) + val patterns = if (nonEmptyTriggers.nonEmpty) { // Simplify trigger terms; Z3 does this automatically when used via stdio, and it sometimes makes // triggers valid that would otherwise be rejected. - nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm).simplify()): _*)).toArray - else null + val beforeSimplify = nonEmptyTriggers.map(t => t.p.map(trm => convertTerm(trm))) + //val afterSimplfiy = beforeSimplify.map(t => t.map(trm => trm.simplify())) + //if (beforeSimplify != afterSimplfiy){ + // println("***") + //} + beforeSimplify.map(t => ctx.mkPattern(t: _*)).toArray + //nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm).simplify()): _*)).toArray + } else null val weightValue = weight.getOrElse(1) if (quant == Forall) { ctx.mkForall(qvarExprs, convertTerm(body), weightValue, patterns, null, ctx.mkSymbol(name), null) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index ec1a2751b..dc1a95234 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -10,14 +10,14 @@ import com.typesafe.scalalogging.LazyLogging import viper.silicon.common.config.Version import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat} import viper.silicon.state.IdentifierFactory -import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Sort, SortDecl, SortWrapperDecl, Term, sorts} +import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier import viper.silver.reporter.{InternalWarningMessage, Reporter} import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel} + import java.io.PrintWriter import java.nio.file.Path - import scala.collection.mutable import com.microsoft.z3._ import viper.silicon.reporting.ExternalToolError @@ -227,7 +227,17 @@ class Z3ProverAPI(uniqueId: String, else preambleAssumes.add(termConverter.convert(term).asInstanceOf[BoolExpr]) } catch { - case e: Z3Exception => reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage)) + case e: Z3Exception => + val cleanTerm = term.transform{ + case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty => + val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{ + case i: Ite => i + case i: Implies => i + }.nonEmpty)) + q.copy(triggers = goodTriggers) + }() + prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr]) + reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage)) } } diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index b99919c60..380cc2198 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -248,13 +248,13 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm)) val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) - val pTakenArgs = additionalArgs - val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody) - val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort) - val pTaken = App(pTakenMacro, pTakenArgs) + //val pTakenArgs = additionalArgs + //val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody) + //val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort) + val pTaken = pTakenBody //App(pTakenMacro, pTakenArgs) - currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl) - v.symbExLog.addMacro(pTaken, pTakenBody) + //currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl) + //v.symbExLog.addMacro(pTaken, pTakenBody) val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken)) pNeeded = PermMinus(pNeeded, pTaken) From ef651917bd7948af979e9c843b8240eb5f9464b2 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 13 Mar 2023 22:58:29 +0100 Subject: [PATCH 09/15] Cleanup and documentation --- src/main/scala/state/Terms.scala | 286 ++++++++++++++++++------------- 1 file changed, 166 insertions(+), 120 deletions(-) diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index 71b602e6f..c1bccae34 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -99,7 +99,7 @@ class SortDecl private[terms] (val sort: Sort) extends Decl with ConditionalFlyw override val equalityDefiningMembers: Sort = sort } -object SortDecl extends GeneralConditionalFlyweightFactory[Sort, SortDecl, SortDecl] { +object SortDecl extends CondFlyweightFactory[Sort, SortDecl, SortDecl] { override def actualCreate(args: Sort): SortDecl = new SortDecl(args) } @@ -108,7 +108,7 @@ class FunctionDecl private[terms] (val func: Function) extends Decl with Conditi override val equalityDefiningMembers: Function = func } -object FunctionDecl extends GeneralConditionalFlyweightFactory[Function, FunctionDecl, FunctionDecl] { +object FunctionDecl extends CondFlyweightFactory[Function, FunctionDecl, FunctionDecl] { override def actualCreate(args: Function): FunctionDecl = new FunctionDecl(args) } @@ -117,7 +117,7 @@ class SortWrapperDecl private[terms] (val from: Sort, val to: Sort) extends Decl override val equalityDefiningMembers: (Sort, Sort) = (from, to) } -object SortWrapperDecl extends GeneralConditionalFlyweightFactory[(Sort, Sort), SortWrapperDecl, SortWrapperDecl] { +object SortWrapperDecl extends CondFlyweightFactory[(Sort, Sort), SortWrapperDecl, SortWrapperDecl] { override def actualCreate(args: (Sort, Sort)): SortWrapperDecl = new SortWrapperDecl(args._1, args._2) } @@ -125,7 +125,7 @@ class MacroDecl private[terms] (val id: Identifier, val args: Seq[Var], val body override val equalityDefiningMembers: (Identifier, Seq[Var], Term) = (id, args, body) } -object MacroDecl extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Var], Term), MacroDecl, MacroDecl] { +object MacroDecl extends CondFlyweightFactory[(Identifier, Seq[Var], Term), MacroDecl, MacroDecl] { override def actualCreate(args: (Identifier, Seq[Var], Term)): MacroDecl = new MacroDecl(args._1, args._2, args._3) } @@ -187,7 +187,7 @@ class Fun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val resul Fun(id, argSorts, resultSort) } -object Fun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), Fun, Fun] with GenericFunctionCompanion[Fun] { +object Fun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), Fun, Fun] with GenericFunctionCompanion[Fun] { def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) override def actualCreate(args: (Identifier, Seq[Sort], Sort)): Fun = new Fun(args._1, args._2, args._3) @@ -205,7 +205,7 @@ class HeapDepFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], va HeapDepFun(id, argSorts, resultSort) } -object HeapDepFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), HeapDepFun, HeapDepFun] with GenericFunctionCompanion[HeapDepFun] { +object HeapDepFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), HeapDepFun, HeapDepFun] with GenericFunctionCompanion[HeapDepFun] { def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) override def actualCreate(args: (Identifier, Seq[Sort], Sort)): HeapDepFun = new HeapDepFun(args._1, args._2, args._3) @@ -218,7 +218,7 @@ class DomainFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val DomainFun(id, argSorts, resultSort) } -object DomainFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), DomainFun, DomainFun] with GenericFunctionCompanion[DomainFun] { +object DomainFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), DomainFun, DomainFun] with GenericFunctionCompanion[DomainFun] { def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) override def actualCreate(args: (Identifier, Seq[Sort], Sort)): DomainFun = new DomainFun(args._1, args._2, args._3) @@ -231,7 +231,7 @@ class SMTFun private[terms] (val id: Identifier, val argSorts: Seq[Sort], val re SMTFun(id, argSorts, resultSort) } -object SMTFun extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), SMTFun, SMTFun] with GenericFunctionCompanion[SMTFun] { +object SMTFun extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), SMTFun, SMTFun] with GenericFunctionCompanion[SMTFun] { def apply(id: Identifier, argSorts: Seq[Sort], resultSort: Sort) = createIfNonExistent((id, argSorts, resultSort)) override def actualCreate(args: (Identifier, Seq[Sort], Sort)): SMTFun = new SMTFun(args._1, args._2, args._3) @@ -242,7 +242,7 @@ class Macro private[terms] (val id: Identifier, val argSorts: Seq[Sort], val res override val equalityDefiningMembers: (Identifier, Seq[Sort], Sort) = (id, argSorts, resultSort) } -object Macro extends GeneralConditionalFlyweightFactory[(Identifier, Seq[Sort], Sort), Macro, Macro] { +object Macro extends CondFlyweightFactory[(Identifier, Seq[Sort], Sort), Macro, Macro] { override def actualCreate(args: (Identifier, Stack[Sort], Sort)): Macro = new Macro(args._1, args._2, args._3) } @@ -258,7 +258,7 @@ class Var private[terms] (val id: Identifier, val sort: Sort) extends Function w def copy(id: Identifier = id, sort: Sort = sort) = Var(id, sort) } -object Var extends GeneralConditionalFlyweightFactory[(Identifier, Sort), Var, Var] { +object Var extends CondFlyweightFactory[(Identifier, Sort), Var, Var] { override def actualCreate(args: (Identifier, Sort)): Var = new Var(args._1, args._2) } @@ -278,7 +278,7 @@ class App private[terms] (val applicable: Applicable, val args: Seq[Term]) else s"${applicable.id}${args.mkString("(", ", ", ")")}" } -object App extends ConditionalFlyweightFactory[(Applicable, Seq[Term]), App] { +object App extends CondFlyweightTermFactory[(Applicable, Seq[Term]), App] { def apply(applicable: Applicable, args: Seq[Term]) = createIfNonExistent((applicable, args)) def apply(applicable: Applicable, arg: Term) = createIfNonExistent((applicable, Seq(arg))) @@ -417,12 +417,23 @@ trait BinaryOp[E] { override lazy val toString = s"$p0 $op $p1" } -trait ConditionalFlyweightBinaryOp[T] extends ConditionalFlyweight[(Term, Term), T] with BinaryOp[Term] with Term { - override val equalityDefiningMembers = (p0, p1) -} +/** + * Trait that implements equality and hashCode based on the equality of the equalityDefiningMembers value. + * Used to implement case class like behavior for ordinary classes. + * No longer used and superseded by the ConditionalFlyweight trait, but kept here for documentation purposes. + */ +trait StructuralEquality { self: AnyRef => + val equalityDefiningMembers: Seq[Any] -trait ConditionalFlyweightUnaryOp[T] extends ConditionalFlyweight[Term, T] with UnaryOp[Term] with Term { - override val equalityDefiningMembers = p + override val hashCode = viper.silver.utility.Common.generateHashCode(equalityDefiningMembers) + + override def equals(other: Any) = ( + this.eq(other.asInstanceOf[AnyRef]) + || (other match { + case se: StructuralEquality if this.getClass.eq(se.getClass) => + equalityDefiningMembers == se.equalityDefiningMembers + case _ => false + })) } trait StructuralEqualityUnaryOp[E] extends UnaryOp[E] { @@ -450,21 +461,23 @@ trait StructuralEqualityBinaryOp[E] extends BinaryOp[E] { override def hashCode(): Int = p0.hashCode() * p1.hashCode() } -trait StructuralEquality { self: AnyRef => - val equalityDefiningMembers: Seq[Any] - - override val hashCode = viper.silver.utility.Common.generateHashCode(equalityDefiningMembers) - - override def equals(other: Any) = ( - this.eq(other.asInstanceOf[AnyRef]) - || (other match { - case se: StructuralEquality if this.getClass.eq(se.getClass) => - equalityDefiningMembers == se.equalityDefiningMembers - case _ => false - })) -} - +/** + * A trait that defines equality and hashcode in such a way that: + * 1. if Verifier.config.useFlyweight is set, then both are computed using references + * 2. otherwise, both are computed based on equality of the equalityDefiningMembers value. + * See also trait StructuralEquality above. + * The motivation for this is to use the flyweight pattern when Z3 is used via its API, in which case it is + * advantageous to have only a single version of each Silicon term (since this enables check caching of their + * Z3 translations, and repeatedly translating the same Silicon term to a Z3 expression massively reduces performance + * for large files), but to avoid the overhead of the flyweight pattern otherwise (since it costs time to check + * for existing copies of a term, and there is no benefit to this when Z3 or some other SMT solver is used via + * StdIO. + * + * @tparam T the type of the constructor parameters of the class (i.e., a tuple or a single parameter type) + * @tparam V the type of the class implementing the trait + */ trait ConditionalFlyweight[T, V] { self: AnyRef => + // The single value or tuple of values that define equality val equalityDefiningMembers: T override lazy val hashCode = if (Verifier.config.useFlyweight) @@ -496,18 +509,53 @@ trait ConditionalFlyweight[T, V] { self: AnyRef => } } +trait ConditionalFlyweightBinaryOp[T] extends ConditionalFlyweight[(Term, Term), T] with BinaryOp[Term] with Term { + override val equalityDefiningMembers = (p0, p1) +} -trait ConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends GeneralConditionalFlyweightFactory[T, Term, V] - -trait PreciseConditionalFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends GeneralConditionalFlyweightFactory[T, V, V] - +trait ConditionalFlyweightUnaryOp[T] extends ConditionalFlyweight[Term, T] with UnaryOp[Term] with Term { + override val equalityDefiningMembers = p +} -trait GeneralConditionalFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends AGeneralConditionalFlyweightFactory[T, T, U, V] { +/** + * Version of CondFlyweightFactory where the return type of apply is Term, i.e., the apply method may return + * arbitrary terms due to simplification. + * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument) + * @tparam V class we are creating instances of + */ +trait CondFlyweightTermFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends CondFlyweightFactory[T, Term, V] + +/** + * Version of CondFlyweightFactory where the return type of apply is V, i.e., the apply method always returns an + * instance of the class whose apply method is called. + * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument) + * @tparam V class we are creating instances of + */ +trait PreciseCondFlyweightFactory[T, V <: ConditionalFlyweight[T, V] with Term] extends CondFlyweightFactory[T, V, V] + + +/** + * Default version of GeneralCondFlyweightFactory where the arguments of the apply method is the same as the + * constructor arguments of class V. + * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument) + * @tparam U return type of the apply method (i.e., either the class itself or something more general for simplifying + * apply methods) + * @tparam V class we are creating instances of + */ +trait CondFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends GeneralCondFlyweightFactory[T, T, U, V] { def apply(v1: T): U = createIfNonExistent(v1) } -trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { +/** + * Most general trait to be implemented by companion objects to create instances of ConditionalFlyweight[T, V]. + * @tparam IF parameter type of the apply method (can be different from the constructor args of the class) + * @tparam T constructor argument type of the class V (i.e., a tuple or the type of the only argument) + * @tparam U return type of the apply method (i.e., either the class itself or something more general for simplifying + * apply methods) + * @tparam V class we are creating instances of + */ +trait GeneralCondFlyweightFactory[IF, T <: IF, U, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { import scala.collection.concurrent.TrieMap @@ -527,8 +575,6 @@ trait AGeneralConditionalFlyweightFactory[IF, T <: IF, U, V <: U with Conditiona } - - /* Literals */ sealed trait Literal extends Term @@ -545,7 +591,7 @@ class IntLiteral private[terms] (val n: BigInt) extends ArithmeticTerm with Lite override lazy val toString = n.toString() override val equalityDefiningMembers: BigInt = n } -object IntLiteral extends GeneralConditionalFlyweightFactory[BigInt, IntLiteral, IntLiteral] { +object IntLiteral extends CondFlyweightFactory[BigInt, IntLiteral, IntLiteral] { override def actualCreate(args: BigInt): IntLiteral = new IntLiteral(args) } @@ -679,7 +725,7 @@ class Quantification private[terms] (val q: Quantifier, /* TODO: Rename */ } object Quantification - extends ConditionalFlyweightFactory[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] { + extends CondFlyweightTermFactory[(Quantifier, Seq[Var], Term, Seq[Trigger], String, Boolean, Option[Int]), Quantification] { private val qidCounter = new AtomicInteger() @@ -748,7 +794,7 @@ class Plus(val p0: Term, val p1: Term) extends ArithmeticTerm override val op = "+" } -object Plus extends ConditionalFlyweightFactory[(Term, Term), Plus] { +object Plus extends CondFlyweightTermFactory[(Term, Term), Plus] { import predef.Zero override def apply(v0: (Term, Term)) = v0 match { @@ -767,7 +813,7 @@ class Minus(val p0: Term, val p1: Term) extends ArithmeticTerm override val op = "-" } -object Minus extends ConditionalFlyweightFactory[(Term, Term), Minus] { +object Minus extends CondFlyweightTermFactory[(Term, Term), Minus] { import predef.Zero override def apply(v1: (Term, Term)) = v1 match { @@ -786,7 +832,7 @@ class Times(val p0: Term, val p1: Term) extends ArithmeticTerm override val op = "*" } -object Times extends ConditionalFlyweightFactory[(Term, Term), Times] { +object Times extends CondFlyweightTermFactory[(Term, Term), Times] { import predef.{Zero, One} override def apply(v0: (Term, Term)) =v0 match { @@ -807,7 +853,7 @@ class Div(val p0: Term, val p1: Term) extends ArithmeticTerm override val op = "/" } -object Div extends GeneralConditionalFlyweightFactory[(Term, Term), Div, Div] { +object Div extends CondFlyweightFactory[(Term, Term), Div, Div] { override def actualCreate(args: (Term, Term)): Div = new Div(args._1, args._2) } @@ -817,7 +863,7 @@ class Mod(val p0: Term, val p1: Term) extends ArithmeticTerm override val op = "%" } -object Mod extends GeneralConditionalFlyweightFactory[(Term, Term), Mod, Mod] { +object Mod extends CondFlyweightFactory[(Term, Term), Mod, Mod] { override def actualCreate(args: (Term, Term)): Mod = new Mod(args._1, args._2) } @@ -837,7 +883,7 @@ class Not(val p: Term) extends BooleanTerm } } -object Not extends ConditionalFlyweightFactory[Term, Not] { +object Not extends CondFlyweightTermFactory[Term, Not] { override def apply(e0: Term) = e0 match { case Not(e1) => e1 @@ -864,7 +910,7 @@ class Or private[terms] (val ts: Seq[Term]) extends BooleanTerm * that conflicts with using extractor objects to simplify terms, * since extractor objects can't be type-parametrised. */ -object Or extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], Term, Or] { +object Or extends GeneralCondFlyweightFactory[Iterable[Term], Seq[Term], Term, Or] { def apply(ts: Term*) = createOr(ts) def apply(ts: Iterable[Term]) = createOr(ts.toSeq) @@ -905,7 +951,7 @@ class And private[terms](val ts: Seq[Term]) extends BooleanTerm override lazy val toString = ts.mkString(" && ") } -object And extends AGeneralConditionalFlyweightFactory[Iterable[Term], Seq[Term], Term, And] { +object And extends GeneralCondFlyweightFactory[Iterable[Term], Seq[Term], Term, And] { def apply(ts: Term*) = createAnd(ts) def apply(ts: Iterable[Term]) = createAnd(ts.toSeq) @@ -932,7 +978,7 @@ class Implies(val p0: Term, val p1: Term) extends BooleanTerm override val op = "==>" } -object Implies extends ConditionalFlyweightFactory[(Term, Term), Implies] { +object Implies extends CondFlyweightTermFactory[(Term, Term), Implies] { @tailrec override def apply(v0: (Term, Term)): Term = v0 match { case (True, e1) => e1 @@ -952,7 +998,7 @@ class Iff(val p0: Term, val p1: Term) extends BooleanTerm override val op = "<==>" } -object Iff extends ConditionalFlyweightFactory[(Term, Term), Iff] { +object Iff extends CondFlyweightTermFactory[(Term, Term), Iff] { override def apply(v0: (Term, Term)) = v0 match { case (True, e1) => e1 case (e0, True) => e0 @@ -974,7 +1020,7 @@ class Ite private[terms] (val t0: Term, val t1: Term, val t2: Term) override lazy val toString = s"($t0 ? $t1 : $t2)" } -object Ite extends ConditionalFlyweightFactory[(Term, Term, Term), Ite] { +object Ite extends CondFlyweightTermFactory[(Term, Term, Term), Ite] { override def apply(v0: (Term, Term, Term)) = v0 match { case (_, e1, e2) if e1 == e2 => e1 case (True, e1, _) => e1 @@ -1037,7 +1083,7 @@ object Equals extends ((Term, Term) => BooleanTerm) { /* Represents built-in equality, e.g., '=' in SMT-LIB */ class BuiltinEquals private[terms] (val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[BuiltinEquals] with Equals -object BuiltinEquals extends GeneralConditionalFlyweightFactory[(Term, Term), BooleanTerm, BuiltinEquals] { +object BuiltinEquals extends CondFlyweightFactory[(Term, Term), BooleanTerm, BuiltinEquals] { override def apply(v0: (Term, Term)) = v0 match { case (p0: PermLiteral, p1: PermLiteral) => // NOTE: The else-case (False) is only justified because permission literals are stored in a normal form @@ -1055,7 +1101,7 @@ class CustomEquals private[terms] (val p0: Term, val p1: Term) extends Condition override val op = "===" } -object CustomEquals extends GeneralConditionalFlyweightFactory[(Term, Term), BooleanTerm, CustomEquals] { +object CustomEquals extends CondFlyweightFactory[(Term, Term), BooleanTerm, CustomEquals] { override def actualCreate(args: (Term, Term)): CustomEquals = new CustomEquals(args._1, args._2) } @@ -1068,7 +1114,7 @@ class Less private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm override val op = "<" } -object Less extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), Less] { +object Less extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), Less] { override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True else False @@ -1085,7 +1131,7 @@ class AtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm override val op = "<=" } -object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), AtMost] { +object AtMost extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), AtMost] { override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True else False @@ -1102,7 +1148,7 @@ class Greater private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm override val op = ">" } -object Greater extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), Greater] { +object Greater extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), Greater] { override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True else False @@ -1119,7 +1165,7 @@ class AtLeast private[terms] (val p0: Term, val p1: Term) extends ComparisonTerm override val op = ">=" } -object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ConditionalFlyweightFactory[(Term, Term), AtLeast] { +object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ CondFlyweightTermFactory[(Term, Term), AtLeast] { override def apply(v0: (Term, Term)) = v0 match { case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True else False case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True else False @@ -1193,7 +1239,7 @@ class FractionPermLiteral private[terms] (r: Rational) extends PermLiteral(r) wi override lazy val toString = literal.toString } -object FractionPermLiteral extends GeneralConditionalFlyweightFactory[Rational, Permissions, FractionPermLiteral] { +object FractionPermLiteral extends CondFlyweightFactory[Rational, Permissions, FractionPermLiteral] { override def apply(r: Rational) = r match { case Rational(n, _) if n == 0 => NoPerm case Rational(n, d) if n == d => FullPerm @@ -1211,7 +1257,7 @@ class FractionPerm private[terms] (val n: Term, val d: Term) override lazy val toString = s"$n/$d" } -object FractionPerm extends GeneralConditionalFlyweightFactory[(Term, Term), Permissions, FractionPerm] { +object FractionPerm extends CondFlyweightFactory[(Term, Term), Permissions, FractionPerm] { override def apply(v: (Term, Term)) = v match { case (IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => FractionPermLiteral(Rational(i1, i2)) case _ => createIfNonExistent(v) @@ -1225,7 +1271,7 @@ class IsValidPermVar private[terms] (val v: Var) extends BooleanTerm with Condit override lazy val toString = s"PVar($v)" } -object IsValidPermVar extends ConditionalFlyweightFactory[Var, IsValidPermVar] { +object IsValidPermVar extends CondFlyweightTermFactory[Var, IsValidPermVar] { override def actualCreate(args: Var): IsValidPermVar = new IsValidPermVar((args)) } @@ -1234,7 +1280,7 @@ class IsReadPermVar private[terms] (val v: Var) extends BooleanTerm with Conditi override lazy val toString = s"RdVar($v)" } -object IsReadPermVar extends ConditionalFlyweightFactory[Var, IsReadPermVar] { +object IsReadPermVar extends CondFlyweightTermFactory[Var, IsReadPermVar] { override def actualCreate(args: Var): IsReadPermVar = new IsReadPermVar((args)) } @@ -1245,7 +1291,7 @@ class PermTimes private[terms] (val p0: Term, val p1: Term) override val op = "*" } -object PermTimes extends ConditionalFlyweightFactory[(Term, Term), PermTimes] { +object PermTimes extends CondFlyweightTermFactory[(Term, Term), PermTimes] { override def apply(v0: (Term, Term)) = v0 match { case (FullPerm, t) => t case (t, FullPerm) => t @@ -1266,7 +1312,7 @@ class IntPermTimes private[terms] (val p0: Term, val p1: Term) override val op = "*" } -object IntPermTimes extends ConditionalFlyweightFactory[(Term, Term), IntPermTimes] { +object IntPermTimes extends CondFlyweightTermFactory[(Term, Term), IntPermTimes] { import predef.{Zero, One} override def apply(v0: (Term, Term)) = v0 match { @@ -1290,7 +1336,7 @@ class PermIntDiv private[terms] (val p0: Term, val p1: Term) override val op = "/" } -object PermIntDiv extends ConditionalFlyweightFactory[(Term, Term), PermIntDiv] { +object PermIntDiv extends CondFlyweightTermFactory[(Term, Term), PermIntDiv] { import predef.One override def apply(v0: (Term, Term)) = v0 match { @@ -1312,7 +1358,7 @@ class PermPermDiv private[terms] (val p0: Term, val p1: Term) override val op = "/" } -object PermPermDiv extends ConditionalFlyweightFactory[(Term, Term), PermPermDiv] { +object PermPermDiv extends CondFlyweightTermFactory[(Term, Term), PermPermDiv] { override def actualCreate(args: (Term, Term)): PermPermDiv = new PermPermDiv(args._1, args._2) } @@ -1331,7 +1377,7 @@ class PermPlus private[terms] (val p0: Term, val p1: Term) override val op = "+" } -object PermPlus extends ConditionalFlyweightFactory[(Term, Term), PermPlus] { +object PermPlus extends CondFlyweightTermFactory[(Term, Term), PermPlus] { override def apply(v0: (Term, Term)) = v0 match { case (NoPerm, t1) => t1 case (t0, NoPerm) => t0 @@ -1359,7 +1405,7 @@ class PermMinus private[terms] (val p0: Term, val p1: Term) } } -object PermMinus extends ConditionalFlyweightFactory[(Term, Term), PermMinus] { +object PermMinus extends CondFlyweightTermFactory[(Term, Term), PermMinus] { override def apply(v0: (Term, Term)) = v0 match { case (t0, NoPerm) => t0 case (p0, p1) if p0 == p1 => NoPerm @@ -1383,7 +1429,7 @@ class PermLess private[terms] (val p0: Term, val p1: Term) override val op = "<" } -object PermLess extends ConditionalFlyweightFactory[(Term, Term), PermLess] { +object PermLess extends CondFlyweightTermFactory[(Term, Term), PermLess] { override def apply(v0: (Term, Term)): Term = { v0 match { case (t0, t1) if t0 == t1 => False @@ -1408,7 +1454,7 @@ class PermAtMost private[terms] (val p0: Term, val p1: Term) extends ComparisonT override val op = "<=" } -object PermAtMost extends ConditionalFlyweightFactory[(Term, Term), PermAtMost] { +object PermAtMost extends CondFlyweightTermFactory[(Term, Term), PermAtMost] { override def apply(v0: (Term, Term)) = v0 match { case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal <= p1.literal) True else False case (t0, t1) if t0 == t1 => True @@ -1428,7 +1474,7 @@ class PermMin private[terms] (val p0: Term, val p1: Term) extends Permissions override lazy val toString = s"min ($p0, $p1)" } -object PermMin extends ConditionalFlyweightFactory[(Term, Term), PermMin] { +object PermMin extends CondFlyweightTermFactory[(Term, Term), PermMin] { override def apply(v0: (Term, Term)) = v0 match { case (t0, t1) if t0 == t1 => t0 case (p0: PermLiteral, p1: PermLiteral) => if (p0.literal > p1.literal) p1 else p0 @@ -1458,7 +1504,7 @@ class SeqRanged private[terms] (val p0: Term, val p1: Term) extends SeqTerm /* w override lazy val toString = s"[$p0..$p1]" } -object SeqRanged extends ConditionalFlyweightFactory[(Term, Term), SeqRanged] { +object SeqRanged extends CondFlyweightTermFactory[(Term, Term), SeqRanged] { override def actualCreate(args: (Term, Term)): SeqRanged = new SeqRanged(args._1, args._2) } @@ -1468,7 +1514,7 @@ class SeqNil private[terms] (val elementsSort: Sort) extends SeqTerm with Litera override val equalityDefiningMembers: Sort = elementsSort } -object SeqNil extends ConditionalFlyweightFactory[Sort, SeqNil] { +object SeqNil extends CondFlyweightTermFactory[Sort, SeqNil] { override def actualCreate(args: Sort): SeqNil = new SeqNil(args) } @@ -1480,7 +1526,7 @@ class SeqSingleton private[terms] (val p: Term) extends SeqTerm /* with UnaryOp[ override lazy val toString = s"[$p]" } -object SeqSingleton extends GeneralConditionalFlyweightFactory[Term, SeqTerm, SeqSingleton] { +object SeqSingleton extends CondFlyweightFactory[Term, SeqTerm, SeqSingleton] { override def actualCreate(args: Term): SeqSingleton = new SeqSingleton(args) } @@ -1493,7 +1539,7 @@ class SeqAppend private[terms] (val p0: Term, val p1: Term) extends SeqTerm override val op = "++" } -object SeqAppend extends ConditionalFlyweightFactory[(Term, Term), SeqAppend] { +object SeqAppend extends CondFlyweightTermFactory[(Term, Term), SeqAppend] { override def apply(v0: (Term, Term)) = { utils.assertSameSorts[sorts.Seq](v0._1, v0._2) createIfNonExistent(v0) @@ -1511,7 +1557,7 @@ class SeqDrop private[terms] (val p0: Term, val p1: Term) extends SeqTerm override lazy val toString = p0.toString + "[" + p1.toString + ":]" } -object SeqDrop extends ConditionalFlyweightFactory[(Term, Term), SeqDrop] { +object SeqDrop extends CondFlyweightTermFactory[(Term, Term), SeqDrop] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) @@ -1531,7 +1577,7 @@ class SeqTake private[terms] (val p0: Term, val p1: Term) extends SeqTerm override lazy val toString = p0.toString + "[:" + p1.toString + "]" } -object SeqTake extends ConditionalFlyweightFactory[(Term, Term), SeqTake] { +object SeqTake extends CondFlyweightTermFactory[(Term, Term), SeqTake] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) @@ -1549,7 +1595,7 @@ class SeqLength private[terms] (val p: Term) extends Term override lazy val toString = s"|$p|" } -object SeqLength extends ConditionalFlyweightFactory [Term, SeqLength] { +object SeqLength extends CondFlyweightTermFactory [Term, SeqLength] { override def apply(t: Term) = { utils.assertSort(t, "term", "Seq", _.isInstanceOf[sorts.Seq]) createIfNonExistent(t) @@ -1566,7 +1612,7 @@ class SeqAt private[terms] (val p0: Term, val p1: Term) extends Term override lazy val toString = s"$p0[$p1]" } -object SeqAt extends ConditionalFlyweightFactory[(Term, Term), SeqAt] { +object SeqAt extends CondFlyweightTermFactory[(Term, Term), SeqAt] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) @@ -1583,7 +1629,7 @@ class SeqIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm override lazy val toString = s"$p1 in $p0" } -object SeqIn extends ConditionalFlyweightFactory[(Term, Term), SeqIn] { +object SeqIn extends CondFlyweightTermFactory[(Term, Term), SeqIn] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) @@ -1604,7 +1650,7 @@ class SeqUpdate private[terms] (val t0: Term, val t1: Term, val t2: Term) override lazy val toString = s"$t0[$t1] := $t2" } -object SeqUpdate extends ConditionalFlyweightFactory[(Term, Term, Term), SeqUpdate] { +object SeqUpdate extends CondFlyweightTermFactory[(Term, Term, Term), SeqUpdate] { override def apply(v0: (Term, Term, Term)) = { val (t0, t1, t2) = v0 utils.assertSort(t0, "first operand", "Seq", _.isInstanceOf[sorts.Seq]) @@ -1637,7 +1683,7 @@ class EmptySet private[terms] (val elementsSort: Sort) extends ConditionalFlywei override val equalityDefiningMembers: Sort = elementsSort } -object EmptySet extends ConditionalFlyweightFactory[Sort, EmptySet] { +object EmptySet extends CondFlyweightTermFactory[Sort, EmptySet] { override def actualCreate(args: Sort): EmptySet = new EmptySet(args) } @@ -1649,7 +1695,7 @@ class SingletonSet private [terms] (val p: Term) extends ConditionalFlyweight[Te override val equalityDefiningMembers: Term = p } -object SingletonSet extends PreciseConditionalFlyweightFactory[Term, SingletonSet] { +object SingletonSet extends PreciseCondFlyweightFactory[Term, SingletonSet] { override def actualCreate(args: Term): SingletonSet = new SingletonSet(args) } @@ -1662,7 +1708,7 @@ class SetAdd private[terms] (val p0: Term, val p1: Term) extends SetTerm override val op = "+" } -object SetAdd extends ConditionalFlyweightFactory[(Term, Term), SetAdd] { +object SetAdd extends CondFlyweightTermFactory[(Term, Term), SetAdd] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Set]) @@ -1678,7 +1724,7 @@ class SetUnion(val p0: Term, val p1: Term) extends ConditionalFlyweightBinaryOp[ override val op = "∪" } -object SetUnion extends PreciseConditionalFlyweightFactory[(Term, Term), SetUnion] { +object SetUnion extends PreciseCondFlyweightFactory[(Term, Term), SetUnion] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) @@ -1692,7 +1738,7 @@ class SetIntersection private[terms] (val p0: Term, val p1: Term) extends Condit override val op = "∩" } -object SetIntersection extends PreciseConditionalFlyweightFactory[(Term, Term), SetIntersection] { +object SetIntersection extends PreciseCondFlyweightFactory[(Term, Term), SetIntersection] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) @@ -1707,7 +1753,7 @@ class SetSubset private[terms] (val p0: Term, val p1: Term) extends BooleanTerm override val op = "⊂" } -object SetSubset extends PreciseConditionalFlyweightFactory[(Term, Term), SetSubset] { +object SetSubset extends PreciseCondFlyweightFactory[(Term, Term), SetSubset] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) @@ -1722,7 +1768,7 @@ class SetDisjoint private[terms] (val p0: Term, val p1: Term) extends BooleanTer override val op = "disj" } -object SetDisjoint extends PreciseConditionalFlyweightFactory[(Term, Term), SetDisjoint] { +object SetDisjoint extends PreciseCondFlyweightFactory[(Term, Term), SetDisjoint] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) @@ -1736,7 +1782,7 @@ class SetDifference private[terms] (val p0: Term, val p1: Term) extends Conditio override val op = "\\" } -object SetDifference extends PreciseConditionalFlyweightFactory[(Term, Term), SetDifference] { +object SetDifference extends PreciseCondFlyweightFactory[(Term, Term), SetDifference] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Set](t0, t1) @@ -1752,7 +1798,7 @@ class SetIn private[terms] (val p0: Term, val p1: Term) extends BooleanTerm override val op = "in" } -object SetIn extends PreciseConditionalFlyweightFactory[(Term, Term), SetIn] { +object SetIn extends PreciseCondFlyweightFactory[(Term, Term), SetIn] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t1, "second operand", "Set", _.isInstanceOf[sorts.Set]) @@ -1771,7 +1817,7 @@ class SetCardinality private[terms] (val p: Term) extends Term override lazy val toString = s"|$p|" } -object SetCardinality extends PreciseConditionalFlyweightFactory[Term, SetCardinality] { +object SetCardinality extends PreciseCondFlyweightFactory[Term, SetCardinality] { override def apply(t: Term) = { utils.assertSort(t, "term", "Set", _.isInstanceOf[sorts.Set]) createIfNonExistent(t) @@ -1800,7 +1846,7 @@ class EmptyMultiset private[terms] (val elementsSort: Sort) extends MultisetTerm override val equalityDefiningMembers: Sort = elementsSort } -object EmptyMultiset extends PreciseConditionalFlyweightFactory[Sort, EmptyMultiset] { +object EmptyMultiset extends PreciseCondFlyweightFactory[Sort, EmptyMultiset] { override def actualCreate(args: Sort): EmptyMultiset = new EmptyMultiset(args) } @@ -1812,7 +1858,7 @@ class SingletonMultiset private[terms] (val p: Term) extends MultisetTerm /* wit override val equalityDefiningMembers: Term = p } -object SingletonMultiset extends PreciseConditionalFlyweightFactory[Term, SingletonMultiset] { +object SingletonMultiset extends PreciseCondFlyweightFactory[Term, SingletonMultiset] { override def actualCreate(args: Term): SingletonMultiset = new SingletonMultiset((args)) } @@ -1822,7 +1868,7 @@ class MultisetAdd private[terms] (val p0: Term, val p1: Term) extends BinaryMult override val op = "+" } -object MultisetAdd extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetAdd] { +object MultisetAdd extends PreciseCondFlyweightFactory[(Term, Term), MultisetAdd] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Set", _.isInstanceOf[sorts.Multiset]) @@ -1838,7 +1884,7 @@ class MultisetUnion private[terms] (val p0: Term, val p1: Term) extends BinaryMu override val op = "∪" } -object MultisetUnion extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetUnion] { +object MultisetUnion extends PreciseCondFlyweightFactory[(Term, Term), MultisetUnion] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) @@ -1852,7 +1898,7 @@ class MultisetIntersection private[terms] (val p0: Term, val p1: Term) extends B override val op = "∩" } -object MultisetIntersection extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetIntersection] { +object MultisetIntersection extends PreciseCondFlyweightFactory[(Term, Term), MultisetIntersection] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) @@ -1867,7 +1913,7 @@ class MultisetSubset private[terms] (val p0: Term, val p1: Term) extends Boolean override val op = "⊂" } -object MultisetSubset extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetSubset] { +object MultisetSubset extends PreciseCondFlyweightFactory[(Term, Term), MultisetSubset] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) @@ -1881,7 +1927,7 @@ class MultisetDifference private[terms] (val p0: Term, val p1: Term) extends Bin override val op = "\\" } -object MultisetDifference extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetDifference] { +object MultisetDifference extends PreciseCondFlyweightFactory[(Term, Term), MultisetDifference] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSameSorts[sorts.Multiset](t0, t1) @@ -1898,7 +1944,7 @@ class MultisetCardinality private[terms] (val p: Term) extends Term override lazy val toString = s"|$p|" } -object MultisetCardinality extends PreciseConditionalFlyweightFactory[Term, MultisetCardinality] { +object MultisetCardinality extends PreciseCondFlyweightFactory[Term, MultisetCardinality] { override def apply(t: Term) = { utils.assertSort(t, "term", "Multiset", _.isInstanceOf[sorts.Multiset]) createIfNonExistent(t) @@ -1914,7 +1960,7 @@ class MultisetCount private[terms] (val p0: Term, val p1: Term) extends Term override lazy val toString = s"$p0($p1)" } -object MultisetCount extends PreciseConditionalFlyweightFactory[(Term, Term), MultisetCount] { +object MultisetCount extends PreciseCondFlyweightFactory[(Term, Term), MultisetCount] { override def apply(v0: (Term, Term)) = { val (ms, el) = v0 utils.assertSort(ms, "first operand", "Multiset", _.isInstanceOf[sorts.Multiset]) @@ -1940,7 +1986,7 @@ class EmptyMap private[terms] (val keySort: Sort, val valueSort: Sort) extends M override val equalityDefiningMembers: (Sort, Sort) = (keySort, valueSort) } -object EmptyMap extends PreciseConditionalFlyweightFactory[(Sort, Sort), EmptyMap] { +object EmptyMap extends PreciseCondFlyweightFactory[(Sort, Sort), EmptyMap] { override def actualCreate(args: (Sort, Sort)): EmptyMap = new EmptyMap(args._1, args._2) } @@ -1951,7 +1997,7 @@ class MapLookup private[terms] (val base: Term, val key: Term) extends Term with override lazy val toString = s"$p0[$p1]" } -object MapLookup extends PreciseConditionalFlyweightFactory[(Term, Term), MapLookup] { +object MapLookup extends PreciseCondFlyweightFactory[(Term, Term), MapLookup] { override def apply(v0: (Term, Term)) = { val (t0, t1) = v0 utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map]) @@ -1967,7 +2013,7 @@ class MapCardinality private[terms] (val p: Term) extends Term with ConditionalF override lazy val toString = s"|$p|" } -object MapCardinality extends PreciseConditionalFlyweightFactory[Term, MapCardinality] { +object MapCardinality extends PreciseCondFlyweightFactory[Term, MapCardinality] { override def apply(t: Term) : MapCardinality = { utils.assertSort(t, "term", "Map", _.isInstanceOf[sorts.Map]) createIfNonExistent(t) @@ -1983,7 +2029,7 @@ class MapUpdate private[terms] (val base: Term, val key: Term, val value: Term) override val equalityDefiningMembers = (base, key, value) } -object MapUpdate extends PreciseConditionalFlyweightFactory[(Term, Term, Term), MapUpdate] { +object MapUpdate extends PreciseCondFlyweightFactory[(Term, Term, Term), MapUpdate] { override def apply(v0: (Term, Term, Term)) : MapUpdate = { val (t0, t1, t2) = v0 utils.assertSort(t0, "first operand", "Map", _.isInstanceOf[sorts.Map]) @@ -2001,7 +2047,7 @@ class MapDomain private[terms] (val p: Term) extends SetTerm with ConditionalFly override lazy val toString = s"domain($p)" } -object MapDomain extends PreciseConditionalFlyweightFactory[Term, MapDomain] { +object MapDomain extends PreciseCondFlyweightFactory[Term, MapDomain] { override def apply(t0: Term) = { utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map]) createIfNonExistent(t0) @@ -2016,7 +2062,7 @@ class MapRange private[terms] (val p: Term) extends SetTerm with ConditionalFlyw override lazy val toString = s"range($p)" } -object MapRange extends PreciseConditionalFlyweightFactory[Term, MapRange] { +object MapRange extends PreciseCondFlyweightFactory[Term, MapRange] { override def apply(t0: Term) = { utils.assertSort(t0, "term", "Map", _.isInstanceOf[sorts.Map]) createIfNonExistent(t0) @@ -2038,7 +2084,7 @@ class Combine(val p0: Term, val p1: Term) extends SnapshotTerm override lazy val toString = s"($p0, $p1)" } -object Combine extends ConditionalFlyweightFactory[(Term, Term), Combine] { +object Combine extends CondFlyweightTermFactory[(Term, Term), Combine] { override def apply(v0: (Term, Term)) = createIfNonExistent(v0._1.convert(sorts.Snap), v0._2.convert(sorts.Snap)) override def actualCreate(args: (Term, Term)): Combine = new Combine(args._1, args._2) @@ -2051,7 +2097,7 @@ class First(val p: Term) extends SnapshotTerm utils.assertSort(p, "term", sorts.Snap) } -object First extends ConditionalFlyweightFactory[Term, First] { +object First extends CondFlyweightTermFactory[Term, First] { override def apply(t: Term) = t match { case Combine(t1, _) => t1 case _ => createIfNonExistent(t) @@ -2067,7 +2113,7 @@ class Second(val p: Term) extends SnapshotTerm utils.assertSort(p, "term", sorts.Snap) } -object Second extends ConditionalFlyweightFactory[Term, Second] { +object Second extends CondFlyweightTermFactory[Term, Second] { override def apply(t: Term) = t match { case Combine(_, t2) => t2 case _ => createIfNonExistent(t) @@ -2086,7 +2132,7 @@ class Lookup(val field: String, val fvf: Term, val at: Term) extends Term with C val sort = fvf.sort.asInstanceOf[sorts.FieldValueFunction].codomainSort } -object Lookup extends PreciseConditionalFlyweightFactory[(String, Term, Term), Lookup] { +object Lookup extends PreciseCondFlyweightFactory[(String, Term, Term), Lookup] { override def actualCreate(args: (String, Term, Term)): Lookup = new Lookup(args._1, args._2, args._3) } @@ -2098,7 +2144,7 @@ class PermLookup(val field: String, val pm: Term, val at: Term) extends Term wit val sort = sorts.Perm } -object PermLookup extends PreciseConditionalFlyweightFactory[(String, Term, Term), PermLookup] { +object PermLookup extends PreciseCondFlyweightFactory[(String, Term, Term), PermLookup] { override def actualCreate(args: (String, Term, Term)): PermLookup = new PermLookup(args._1, args._2, args._3) } @@ -2110,7 +2156,7 @@ class Domain(val field: String, val fvf: Term) extends SetTerm /*with PossibleTr override val equalityDefiningMembers: (String, Term) = (field, fvf) } -object Domain extends ConditionalFlyweightFactory[(String, Term), Domain] { +object Domain extends CondFlyweightTermFactory[(String, Term), Domain] { override def actualCreate(args: (String, Term)): Domain = new Domain(args._1, args._2) } @@ -2122,7 +2168,7 @@ class FieldTrigger(val field: String, val fvf: Term, val at: Term) extends Term override val equalityDefiningMembers: (String, Term, Term) = (field, fvf, at) } -object FieldTrigger extends PreciseConditionalFlyweightFactory[(String, Term, Term), FieldTrigger] { +object FieldTrigger extends PreciseCondFlyweightFactory[(String, Term, Term), FieldTrigger] { override def actualCreate(args: (String, Term, Term)): FieldTrigger = new FieldTrigger(args._1, args._2, args._3) } @@ -2135,7 +2181,7 @@ class PredicateLookup(val predname: String, val psf: Term, val args: Seq[Term]) override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, psf, args) } -object PredicateLookup extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicateLookup] { +object PredicateLookup extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicateLookup] { override def actualCreate(args: (String, Term, Seq[Term])): PredicateLookup = new PredicateLookup(args._1, args._2, args._3) } @@ -2146,7 +2192,7 @@ class PredicatePermLookup(val predname: String, val pm: Term, val args: Seq[Term override val equalityDefiningMembers: (String, Term, Seq[Term]) = (predname, pm, args) } -object PredicatePermLookup extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicatePermLookup] { +object PredicatePermLookup extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicatePermLookup] { override def actualCreate(args: (String, Term, Seq[Term])): PredicatePermLookup = new PredicatePermLookup(args._1, args._2, args._3) } @@ -2157,7 +2203,7 @@ class PredicateDomain(val predname: String, val psf: Term) extends SetTerm /*wit override val equalityDefiningMembers: (String, Term) = (predname, psf) } -object PredicateDomain extends ConditionalFlyweightFactory[(String, Term), PredicateDomain] { +object PredicateDomain extends CondFlyweightTermFactory[(String, Term), PredicateDomain] { override def actualCreate(args: (String, Term)): PredicateDomain = new PredicateDomain(args._1, args._2) } @@ -2168,7 +2214,7 @@ class PredicateTrigger(val predname: String, val psf: Term, val args: Seq[Term]) override val equalityDefiningMembers: (String, Term, Stack[Term]) = (predname, psf, args) } -object PredicateTrigger extends PreciseConditionalFlyweightFactory[(String, Term, Seq[Term]), PredicateTrigger] { +object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[Term]), PredicateTrigger] { override def actualCreate(args: (String, Term, Seq[Term])): PredicateTrigger = new PredicateTrigger(args._1, args._2, args._3) } @@ -2226,7 +2272,7 @@ class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with Conditiona override val equalityDefiningMembers: MagicWandChunk = chunk } -object MagicWandChunkTerm extends ConditionalFlyweightFactory[MagicWandChunk, MagicWandChunkTerm] { +object MagicWandChunkTerm extends CondFlyweightTermFactory[MagicWandChunk, MagicWandChunkTerm] { override def actualCreate(args: MagicWandChunk): MagicWandChunkTerm = new MagicWandChunkTerm(args) } @@ -2357,7 +2403,7 @@ class SortWrapper(val t: Term, val to: Sort) override val sort = to } -object SortWrapper extends ConditionalFlyweightFactory[(Term, Sort), SortWrapper] { +object SortWrapper extends CondFlyweightTermFactory[(Term, Sort), SortWrapper] { override def apply(v0: (Term, Sort)) = v0 match { case (t, to) if t.sort == to => t case (sw: SortWrapper, to) if sw.t.sort == to => sw.t @@ -2376,7 +2422,7 @@ class Distinct(val ts: Set[DomainFun]) extends BooleanTerm with ConditionalFlywe override lazy val toString = s"Distinct($ts)" } -object Distinct extends ConditionalFlyweightFactory[Set[DomainFun], Distinct] { +object Distinct extends CondFlyweightTermFactory[Set[DomainFun], Distinct] { override def apply(ts: Set[DomainFun]): Term = if (ts.size >= 2) createIfNonExistent(ts) else True @@ -2393,7 +2439,7 @@ class Let(val bindings: Map[Var, Term], val body: Term) extends Term with Condit override lazy val toString = s"let ${bindings.map(p => s"${p._1} = ${p._2}")} in $body" } -object Let extends ConditionalFlyweightFactory[(Map[Var, Term], Term), Let] { +object Let extends CondFlyweightTermFactory[(Map[Var, Term], Term), Let] { def apply(v: Var, t: Term, body: Term): Term = apply(Map(v -> t), body) def apply(vs: Seq[Var], ts: Seq[Term], body: Term): Term = apply(toMap(vs zip ts), body) From 3ff003aa39f2b877f2b83b86e52f471ecbf210f0 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 13 Mar 2023 23:11:03 +0100 Subject: [PATCH 10/15] Added some comments --- src/main/scala/decider/TermToZ3APIConverter.scala | 14 +++++--------- src/main/scala/decider/Z3ProverAPI.scala | 4 ++++ .../scala/rules/MoreCompleteExhaleSupporter.scala | 14 ++++++-------- 3 files changed, 15 insertions(+), 17 deletions(-) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 5ed3e1b5e..8cf6d83fe 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -259,15 +259,11 @@ class TermToZ3APIConverter val qvarExprs = vars.map(v => convert(v)).toArray val nonEmptyTriggers = triggers.filter(_.p.nonEmpty) val patterns = if (nonEmptyTriggers.nonEmpty) { - // Simplify trigger terms; Z3 does this automatically when used via stdio, and it sometimes makes - // triggers valid that would otherwise be rejected. - val beforeSimplify = nonEmptyTriggers.map(t => t.p.map(trm => convertTerm(trm))) - //val afterSimplfiy = beforeSimplify.map(t => t.map(trm => trm.simplify())) - //if (beforeSimplify != afterSimplfiy){ - // println("***") - //} - beforeSimplify.map(t => ctx.mkPattern(t: _*)).toArray - //nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm).simplify()): _*)).toArray + // ME: Maybe we should simplify trigger terms here? There is some evidence that Z3 does this + // automatically when used via stdio, and it sometimes makes triggers valid that would otherwise be + // rejected. On the other hand, it's not at all obvious that simplification does not change the shape + // of a trigger term, which would not be what we want. + nonEmptyTriggers.map(t => ctx.mkPattern(t.p.map(trm => convertTerm(trm)): _*)).toArray } else null val weightValue = weight.getOrElse(1) if (quant == Forall) { diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index dc1a95234..ddd8b54d3 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -228,6 +228,10 @@ class Z3ProverAPI(uniqueId: String, preambleAssumes.add(termConverter.convert(term).asInstanceOf[BoolExpr]) } catch { case e: Z3Exception => + // The only reason we get an exception here is that we've tried to assume a quantifier with an invalid trigger. + // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores + // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually + // walk through all quantifiers and remove invalid terms inside the trigger. val cleanTerm = term.transform{ case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty => val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{ diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index b95dc2a8b..e34aad0a4 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -247,14 +247,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { if (moreNeeded) { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm)) - val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) - //val pTakenArgs = additionalArgs - //val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody) - //val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort) - val pTaken = pTakenBody //App(pTakenMacro, pTakenArgs) - - //currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl) - //v.symbExLog.addMacro(pTaken, pTakenBody) + + // ME: We used to create macros here, however, most of the time the created terms are simple. + // When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different + // (leading to new terms that have to be translated), whereas without macros, we can usually use a term + // that already exists. + val pTaken = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken)) pNeeded = PermMinus(pNeeded, pTaken) From 450786ecb855c00a0b7cb127f2d5390af06d875d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 31 Mar 2023 19:43:33 +0200 Subject: [PATCH 11/15] Supporting user-provided Z3 args via API --- src/main/scala/decider/Z3ProverAPI.scala | 66 +++++++++++++++++++++--- 1 file changed, 58 insertions(+), 8 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index 0d73c4353..970f9cbcb 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -13,13 +13,15 @@ import viper.silicon.state.IdentifierFactory import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier -import viper.silver.reporter.{InternalWarningMessage, Reporter} +import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage, Reporter} import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel} import java.io.PrintWriter import java.nio.file.Path import scala.collection.mutable import com.microsoft.z3._ +import com.microsoft.z3.enumerations.Z3_param_kind +import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams import viper.silicon.reporting.ExternalToolError import scala.jdk.CollectionConverters.MapHasAsJava @@ -28,8 +30,8 @@ import scala.util.Random object Z3ProverAPI { val name = "Z3-API" - val minVersion = Version("4.8.6.0") - val maxVersion = Some(Version("4.8.7.0")) /* X.Y.Z if that is the *last supported* version */ + val minVersion = Version("4.8.7.0") + val maxVersion = Some(Version("4.12.1.0")) /* X.Y.Z if that is the *last supported* version */ // these are not actually used, but since there is a lot of code that expects command line parameters and a // config file, we just supply this information here (whose contents will then be ignored) @@ -49,7 +51,7 @@ object Z3ProverAPI { "delay_units" -> true, "smt.mbqi" -> false, "mbqi" -> false, - "pp.bv_literals" -> false, + // "pp.bv_literals" -> false, "model.v2" -> true ) val intParams = Map( @@ -67,6 +69,7 @@ object Z3ProverAPI { "smt.qi.eager_threshold" -> 100.0, "qi.eager_threshold" -> 100.0, ) + val oldVersionOnlyParams = Set("smt.arith.solver", "arith.solver") } @@ -115,19 +118,66 @@ class Z3ProverAPI(uniqueId: String, logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile) ctx = new Context(Z3ProverAPI.initialOptions.asJava) val params = ctx.mkParams() + val useOldVersionParams = version() <= Version("4.8.7.0") Z3ProverAPI.boolParams.foreach{ - case (k, v) => params.add(k, v) + case (k, v) => + if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) + params.add(k, v) } Z3ProverAPI.intParams.foreach{ - case (k, v) => params.add(k, v) + case (k, v) => + if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) + params.add(k, v) } Z3ProverAPI.doubleParams.foreach{ - case (k, v) => params.add(k, v) + case (k, v) => + if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) + params.add(k, v) } Z3ProverAPI.stringParams.foreach{ - case (k, v) => params.add(k, v) + case (k, v) => + if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) + params.add(k, v) + } + val userProvidedArgs: Array[String] = Verifier.config.proverArgs match { + case None => + Array() + + case Some(rawArgs) => + val args = if (rawArgs.startsWith("'") && rawArgs.startsWith("'")) { + rawArgs.substring(1, rawArgs.length - 1) + } else { + rawArgs + } + // One can pass some options. This allows to check whether they have been received. + val msg = s"Additional command-line arguments are $args" + reporter report ConfigurationConfirmation(msg) + logger debug msg + args.split(' ').map(_.trim) } prover = ctx.mkSolver() + val descrs = prover.getParameterDescriptions + for (arg <- userProvidedArgs) { + val splitArg = arg.split("=") + var key = splitArg(0) + if (key.startsWith("smt.")) + key = key.substring(4) + val vl = splitArg(1) + val keySymbol = ctx.mkSymbol(key) + val param_kind = descrs.getKind(keySymbol) + param_kind match { + case Z3_param_kind.Z3_PK_BOOL => + params.add(keySymbol, vl.toBoolean) + case Z3_param_kind.Z3_PK_UINT => + params.add(key, vl.toInt) + case Z3_param_kind.Z3_PK_DOUBLE => + params.add(keySymbol, vl.toDouble) + case Z3_param_kind.Z3_PK_STRING => + params.add(keySymbol, vl) + case _ => + reporter.report(InternalWarningMessage("Z3 error: unknown parameter" + key)) + } + } prover.setParameters(params) termConverter.start() termConverter.ctx = ctx From 1e65bb38bbfa727733c90231e7b0b15191541a7a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 3 Apr 2023 14:54:33 +0200 Subject: [PATCH 12/15] Adding Z3 options to parsed file, taking options from correct command line arg --- src/main/scala/decider/Z3ProverAPI.scala | 69 +++++++++++------------- 1 file changed, 32 insertions(+), 37 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index 970f9cbcb..6d8ef07b6 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -48,28 +48,22 @@ object Z3ProverAPI { val initialOptions = Map("auto_config" -> "false", "type_check" -> "true") val boolParams = Map( "smt.delay_units" -> true, - "delay_units" -> true, "smt.mbqi" -> false, - "mbqi" -> false, // "pp.bv_literals" -> false, "model.v2" -> true ) val intParams = Map( "smt.case_split" -> 3, - "case_split" -> 3, "smt.qi.max_multi_patterns" -> 1000, - "qi.max_multi_patterns" -> 1000, "smt.arith.solver" -> 2, - "arith.solver" -> 2 ) val stringParams: Map[String, String] = Map( // currently none ) val doubleParams = Map( "smt.qi.eager_threshold" -> 100.0, - "qi.eager_threshold" -> 100.0, ) - val oldVersionOnlyParams = Set("smt.arith.solver", "arith.solver") + val oldVersionOnlyParams = Set("smt.arith.solver") } @@ -118,62 +112,55 @@ class Z3ProverAPI(uniqueId: String, logfileWriter = if (Verifier.config.disableTempDirectory()) null else viper.silver.utility.Common.PrintWriter(Verifier.config.proverLogFile(uniqueId).toFile) ctx = new Context(Z3ProverAPI.initialOptions.asJava) val params = ctx.mkParams() + + // When setting parameters via API, we have to remove the smt. prefix + def removeSmtPrefix(s: String) = { + if (s.startsWith("smt.")) + s.substring(4) + else + s + } + val useOldVersionParams = version() <= Version("4.8.7.0") Z3ProverAPI.boolParams.foreach{ case (k, v) => if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(k, v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.intParams.foreach{ case (k, v) => if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(k, v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.doubleParams.foreach{ case (k, v) => if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(k, v) + params.add(removeSmtPrefix(k), v) } Z3ProverAPI.stringParams.foreach{ case (k, v) => if (useOldVersionParams || !oldVersionOnlyParams.contains(k)) - params.add(k, v) - } - val userProvidedArgs: Array[String] = Verifier.config.proverArgs match { - case None => - Array() - - case Some(rawArgs) => - val args = if (rawArgs.startsWith("'") && rawArgs.startsWith("'")) { - rawArgs.substring(1, rawArgs.length - 1) - } else { - rawArgs - } - // One can pass some options. This allows to check whether they have been received. - val msg = s"Additional command-line arguments are $args" - reporter report ConfigurationConfirmation(msg) - logger debug msg - args.split(' ').map(_.trim) + params.add(removeSmtPrefix(k), v) } + val userProvidedArgs = Verifier.config.proverConfigArgs prover = ctx.mkSolver() val descrs = prover.getParameterDescriptions - for (arg <- userProvidedArgs) { - val splitArg = arg.split("=") - var key = splitArg(0) - if (key.startsWith("smt.")) - key = key.substring(4) - val vl = splitArg(1) + for ((origKey, vl) <- userProvidedArgs) { + val key = if (origKey.startsWith("smt.")) + origKey.substring(4) + else + origKey val keySymbol = ctx.mkSymbol(key) val param_kind = descrs.getKind(keySymbol) param_kind match { case Z3_param_kind.Z3_PK_BOOL => - params.add(keySymbol, vl.toBoolean) + params.add(key, vl.toBoolean) case Z3_param_kind.Z3_PK_UINT => params.add(key, vl.toInt) case Z3_param_kind.Z3_PK_DOUBLE => - params.add(keySymbol, vl.toDouble) + params.add(key, vl.toDouble) case Z3_param_kind.Z3_PK_STRING => - params.add(keySymbol, vl) + params.add(key, vl) case _ => reporter.report(InternalWarningMessage("Z3 error: unknown parameter" + key)) } @@ -374,7 +361,15 @@ class Z3ProverAPI(uniqueId: String, if (!preamblePhaseOver) { preamblePhaseOver = true - val merged = emittedPreambleString.mkString("\n") + // Setting all options again , since otherwise some of them seem to get lost. + val standardOptionPrefix = Seq("(set-option :auto_config false)", "(set-option :type_check true)") ++ + Z3ProverAPI.boolParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ + Z3ProverAPI.intParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ + Z3ProverAPI.doubleParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ + Z3ProverAPI.stringParams.map(bp => s"(set-option :${bp._1} ${bp._2})") + val customOptionPrefix = Verifier.config.proverConfigArgs.map(a => s"(set-option :${a._1} ${a._2})") + + val merged = (standardOptionPrefix ++ customOptionPrefix ++ emittedPreambleString).mkString("\n") val parsed = ctx.parseSMTLIB2String(merged, emittedSortSymbols.toArray, emittedSorts.toArray, emittedFuncSymbols.toArray, emittedFuncs.toArray) prover.add(parsed: _*) prover.add(preambleAssumes.toSeq : _*) From 774468d528b16937c0e683d29d44ef5fee866fd5 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 12 Apr 2023 15:50:04 +0200 Subject: [PATCH 13/15] Addressing review comments --- src/main/scala/decider/Z3ProverAPI.scala | 2 +- src/main/scala/reporting/Converter.scala | 2 +- src/main/scala/rules/Evaluator.scala | 2 +- src/main/scala/state/Terms.scala | 7 ++----- src/main/scala/supporters/ExpressionTranslator.scala | 2 +- 5 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index 131c1f40b..cab4c90ac 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -13,7 +13,7 @@ import viper.silicon.state.IdentifierFactory import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier -import viper.silver.reporter.{ConfigurationConfirmation, InternalWarningMessage, Reporter} +import viper.silver.reporter.{InternalWarningMessage, Reporter} import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel} import java.io.PrintWriter diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala index 6ac77ce62..b4e2fedbd 100644 --- a/src/main/scala/reporting/Converter.scala +++ b/src/main/scala/reporting/Converter.scala @@ -254,7 +254,7 @@ object Converter { case Unit => UnprocessedModelEntry(ConstantEntry(snapUnitId)) case IntLiteral(x) => LitIntEntry(x) case t: BooleanLiteral => LitBoolEntry(t.value) - case Null => VarEntry(model.entries(nullRefId).toString, sorts.Ref) + case Null => VarEntry(model.entries(nullRefId).toString, sorts.Ref) case Var(_, sort) => val key: String = term.toString val entry: Option[ModelEntry] = model.entries.get(key) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index fc33f11e0..fc456abbc 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -1141,7 +1141,7 @@ object evaluator extends EvaluationRules { pve: PartialVerificationError, v: Verifier) (Q: (State, T, Verifier) => VerificationResult) - : VerificationResult = { + : VerificationResult = { evalBinOp(s, e0, e1, (t0, t1) => termOp((t0, t1)), pve, v)(Q) } diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala index c1bccae34..6f3795875 100644 --- a/src/main/scala/state/Terms.scala +++ b/src/main/scala/state/Terms.scala @@ -14,6 +14,7 @@ import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.{Map, Stack, state, toMap} import viper.silicon.state.{Identifier, MagicWandChunk, MagicWandIdentifier, SortBasedIdentifier} import viper.silicon.verifier.Verifier +import scala.collection.concurrent.TrieMap sealed trait Node { def toString: String @@ -499,7 +500,7 @@ trait ConditionalFlyweight[T, V] { self: AnyRef => } } - override def toString: String = { + override lazy val toString: String = { val argString = equalityDefiningMembers match { case p: Product => p.productIterator.mkString(", ") @@ -557,8 +558,6 @@ trait CondFlyweightFactory[T, U, V <: U with ConditionalFlyweight[T, V]] extends */ trait GeneralCondFlyweightFactory[IF, T <: IF, U, V <: U with ConditionalFlyweight[T, V]] extends (IF => U) { - import scala.collection.concurrent.TrieMap - var pool = new TrieMap[T, V]() def createIfNonExistent(args: T): V = { @@ -2248,8 +2247,6 @@ object MagicWandSnapshot { // Since MagicWandSnapshot subclasses Combine, we apparently cannot inherit the normal subclass, so we // have to copy paste the code here. - import scala.collection.concurrent.TrieMap - var pool = new TrieMap[(Term, Term), MagicWandSnapshot]() def createIfNonExistent(args: (Term, Term)): MagicWandSnapshot = { diff --git a/src/main/scala/supporters/ExpressionTranslator.scala b/src/main/scala/supporters/ExpressionTranslator.scala index 132e70450..353dac8c1 100644 --- a/src/main/scala/supporters/ExpressionTranslator.scala +++ b/src/main/scala/supporters/ExpressionTranslator.scala @@ -206,7 +206,7 @@ trait ExpressionTranslator { case as: ast.AnySetIntersection => translateAnySetBinExp(as, SetIntersection, MultisetIntersection) case as: ast.AnySetSubset => translateAnySetBinExp(as, SetSubset, MultisetSubset, as.left) case as: ast.AnySetMinus => translateAnySetBinExp(as, SetDifference, MultisetDifference) - case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, v0 => MultisetCount(v0._2, v0._1), as.right) + case as: ast.AnySetContains => translateAnySetBinExp(as, SetIn, { case (t0, t1) => MultisetCount(t1, t0) }, as.right) case as: ast.AnySetCardinality => translateAnySetUnExp(as, SetCardinality, MultisetCardinality, as.exp) /* Maps */ From db18de01ec3247b9931bc22f81c9ce6760c8d139 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 19 Apr 2023 14:23:58 +0200 Subject: [PATCH 14/15] Incorporated remaining review suggestions --- src/main/scala/decider/Decider.scala | 2 +- src/main/scala/decider/Z3ProverAPI.scala | 18 +++++++-------- .../rules/MoreCompleteExhaleSupporter.scala | 23 ++++++++++++++----- src/main/scala/state/Triggers.scala | 10 ++++---- 4 files changed, 31 insertions(+), 22 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 8beaf0adf..29e284443 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -120,7 +120,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => private def getProver(prover: String): Prover = prover match { case Z3ProverStdIO.name => new Z3ProverStdIO(uniqueId, termConverter, identifierFactory, reporter) case Cvc5ProverStdIO.name => new Cvc5ProverStdIO(uniqueId, termConverter, identifierFactory, reporter) - case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter) + case Z3ProverAPI.name => new Z3ProverAPI(uniqueId, new TermToZ3APIConverter(), identifierFactory, reporter, triggerGenerator) case prover => val msg1 = s"Unknown prover '$prover' provided. Defaulting to ${Z3ProverStdIO.name}." logger warn msg1 diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index 09683d95a..ed98ee7ba 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -9,8 +9,8 @@ package viper.silicon.decider import com.typesafe.scalalogging.LazyLogging import viper.silicon.common.config.Version import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat} -import viper.silicon.state.IdentifierFactory -import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, sorts} +import viper.silicon.state.{IdentifierFactory, State} +import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier import viper.silver.reporter.{InternalWarningMessage, Reporter} @@ -63,6 +63,7 @@ object Z3ProverAPI { val doubleParams = Map( "smt.qi.eager_threshold" -> 100.0, ) + val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams val oldVersionOnlyParams = Set("smt.arith.solver") } @@ -70,7 +71,8 @@ object Z3ProverAPI { class Z3ProverAPI(uniqueId: String, termConverter: TermToZ3APIConverter, identifierFactory: IdentifierFactory, - reporter: Reporter) + reporter: Reporter, + triggerGenerator: TriggerGenerator) extends Prover with LazyLogging { @@ -254,11 +256,11 @@ class Z3ProverAPI(uniqueId: String, // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually // walk through all quantifiers and remove invalid terms inside the trigger. + triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger) val cleanTerm = term.transform{ case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty => val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{ - case i: Ite => i - case i: Implies => i + case t => triggerGenerator.isForbiddenInTrigger(t) }.nonEmpty)) q.copy(triggers = goodTriggers) }() @@ -369,10 +371,8 @@ class Z3ProverAPI(uniqueId: String, // Setting all options again , since otherwise some of them seem to get lost. val standardOptionPrefix = Seq("(set-option :auto_config false)", "(set-option :type_check true)") ++ - Z3ProverAPI.boolParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ - Z3ProverAPI.intParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ - Z3ProverAPI.doubleParams.map(bp => s"(set-option :${bp._1} ${bp._2})") ++ - Z3ProverAPI.stringParams.map(bp => s"(set-option :${bp._1} ${bp._2})") + Z3ProverAPI.allParams.map(bp => s"(set-option :${bp._1} ${bp._2})") + val customOptionPrefix = Verifier.config.proverConfigArgs.map(a => s"(set-option :${a._1} ${a._2})") val merged = (standardOptionPrefix ++ customOptionPrefix ++ emittedPreambleString).mkString("\n") diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index c5593affc..1a9f18b51 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -245,13 +245,24 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { relevantChunks.sortWith(sortFunction) foreach { ch => if (moreNeeded) { val eq = And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 }) - pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm)) - // ME: We used to create macros here, however, most of the time the created terms are simple. - // When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different - // (leading to new terms that have to be translated), whereas without macros, we can usually use a term - // that already exists. - val pTaken = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) + val pTaken = if (Verifier.config.useFlyweight) { + // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different + // (leading to new terms that have to be translated), whereas without macros, we can usually use a term + // that already exists. + Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) + } else { + val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm) + val pTakenArgs = additionalArgs + val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody) + val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort) + currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl) + val pTakenApp = App(pTakenMacro, pTakenArgs) + v.symbExLog.addMacro(pTakenApp, pTakenBody) + pTakenApp + } + + pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm)) val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken)) pNeeded = PermMinus(pNeeded, pTaken) diff --git a/src/main/scala/state/Triggers.scala b/src/main/scala/state/Triggers.scala index 757e25440..b03048530 100644 --- a/src/main/scala/state/Triggers.scala +++ b/src/main/scala/state/Triggers.scala @@ -80,7 +80,7 @@ class TriggerGenerator } /* True iff the given node is a possible trigger */ - def isPossibleTrigger(e: Term): Boolean = e match { + def isPossibleTrigger(e: Term): Boolean = (customIsPossibleTrigger orElse { case _: Var => false case app: App => app.applicable.isInstanceOf[Function] case _: CustomEquals @@ -106,11 +106,10 @@ class TriggerGenerator | _: PredicateLookup => true case _ => false - } + }: PartialFunction[Term, Boolean])(e) /* True iff the given node is not allowed in triggers */ - def isForbiddenInTrigger(term: Term) = term match { - case app: App => app.applicable.isInstanceOf[Macro] + def isForbiddenInTrigger(term: Term) = (customIsForbiddenInTrigger orElse { case _: Plus | _: Minus | _: Times | _: Div | _: Mod | _: Not | _: Or | _: And | _: Implies | _: Iff | _: Ite | _: BuiltinEquals @@ -118,10 +117,9 @@ class TriggerGenerator | _: PermTimes | _: IntPermTimes | _: PermIntDiv | _: PermPermDiv |_: PermPlus | _: PermMinus | _: PermLess | _: PermAtMost | _: Distinct - | _: Let => true case _ => false - } + }: PartialFunction[Term, Boolean])(term) val advancedIsForbiddenInTrigger:PartialFunction[Term, Boolean] = { case _: Plus | _: Minus => false From 28481ad9ffd9261b7cb23b4a71d2a8d33c36b0c9 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 19 Apr 2023 14:49:52 +0200 Subject: [PATCH 15/15] Adapted test annotations --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index d6161459c..231b73fb5 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d6161459c32f58c47c162a467ea675fdfac8fd17 +Subproject commit 231b73fb515b38547bc434ed0b9c94d969edc129