From e355cd86a90efdfd44de71675c416a85bc3da2ba Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 25 Sep 2023 18:18:00 +0200 Subject: [PATCH 1/4] Fixing issue 751 --- src/main/scala/decider/TermToZ3APIConverter.scala | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 8cf6d83fe..c591aec27 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -471,9 +471,17 @@ class TermToZ3APIConverter // workaround: since we cannot create a function application with just the name, we let Z3 parse // a string that uses the function, take the AST, and get the func decl from there, so that we can // programmatically create a func app. - val decls = args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ") + + + val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort. + // ME: The parsing happens in a fresh context that doesn't know any of our current declarations. + // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there + // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however, + // such functions exist. So we re-declare *only* this sort. + val decls = declPreamble + args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ") val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})" val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))" + println(assertion) val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null) val app = workaround(0).getArgs()(0) val decl = app.getFuncDecl From 6b85bac8a47a89b7ac8ddb1d686ee6f64468384d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 25 Sep 2023 18:41:18 +0200 Subject: [PATCH 2/4] Caching for SMT func decls --- .../scala/decider/TermToZ3APIConverter.scala | 47 +++++++++++-------- 1 file changed, 28 insertions(+), 19 deletions(-) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index c591aec27..4ba1b4776 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 smtFuncDeclCache = mutable.HashMap[(String, Seq[Sort]), (Z3FuncDecl, Seq[Z3Expr])]() val termCache = mutable.HashMap[Term, Z3Expr]() def convert(s: Sort): Z3Sort = convertSort(s) @@ -472,26 +473,33 @@ class TermToZ3APIConverter // a string that uses the function, take the AST, and get the func decl from there, so that we can // programmatically create a func app. - - val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort. - // ME: The parsing happens in a fresh context that doesn't know any of our current declarations. - // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there - // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however, - // such functions exist. So we re-declare *only* this sort. - val decls = declPreamble + args.zipWithIndex.map{case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})"}.mkString(" ") - val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})" - val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))" - println(assertion) - val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null) - val app = workaround(0).getArgs()(0) - val decl = app.getFuncDecl - val actualArgs = if (decl.getArity > args.length){ - // the function name we got wasn't just a function name but also contained a first argument. - // this happens with float operations where functionName contains a rounding mode. - app.getArgs.toSeq.slice(0, decl.getArity - args.length) ++ args.map(convertTerm(_)) - }else { - args.map(convertTerm(_)) + val cacheKey = (functionName, args.map(_.sort)) + val (decl, additionalArgs: Seq[Z3Expr]) = if (smtFuncDeclCache.contains(cacheKey)) { + smtFuncDeclCache(cacheKey) + } else { + val declPreamble = "(define-sort $Perm () Real) " // ME: Re-declare the Perm sort. + // ME: The parsing happens in a fresh context that doesn't know any of our current declarations. + // In principle, it might be necessary to re-declare all sorts we're using anywhere. However, I don't see how there + // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however, + // such functions exist. So we re-declare *only* this sort. + val decls = declPreamble + args.zipWithIndex.map { case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})" }.mkString(" ") + val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})" + val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))" + val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null) + val app = workaround(0).getArgs()(0) + val decl = app.getFuncDecl + val additionalArgs = if (decl.getArity > args.length) { + // the function name we got wasn't just a function name but also contained a first argument. + // this happens with float operations where functionName contains a rounding mode. + app.getArgs.toSeq.slice(0, decl.getArity - args.length) + } else { + Seq() + } + smtFuncDeclCache.put(cacheKey, (decl, additionalArgs)) + (decl, additionalArgs) } + + val actualArgs = additionalArgs ++ args.map(convertTerm(_)) ctx.mkApp(decl, actualArgs.toArray : _*) } @@ -530,6 +538,7 @@ class TermToZ3APIConverter sanitizedNamesCache.clear() macros.clear() funcDeclCache.clear() + smtFuncDeclCache.clear() sortCache.clear() termCache.clear() unitConstructor = null From e28254a7b6c89d1fc044f27f5f3ddb8d85dbbb5b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 26 Sep 2023 03:31:16 +0200 Subject: [PATCH 3/4] Improved filtering of bad triggers --- src/main/scala/decider/Z3ProverAPI.scala | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index d5b9dfe77..c5b5c9b42 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -10,7 +10,7 @@ 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, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts} +import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, Var, sorts} import viper.silicon.{Config, Map} import viper.silicon.verifier.Verifier import viper.silver.reporter.{InternalWarningMessage, Reporter} @@ -258,11 +258,12 @@ class Z3ProverAPI(uniqueId: String, 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 { + val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => + ptrn.isInstanceOf[Var] || ptrn.shallowCollect { case t => triggerGenerator.isForbiddenInTrigger(t) }.nonEmpty)) q.copy(triggers = goodTriggers) - }() + }({t => true}) cleanTerm } From 8527848dc9f12bb5da739874f2a9259bd3c85575 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 26 Sep 2023 10:56:43 +0200 Subject: [PATCH 4/4] Fixing issue #707 for Z3 API as well --- src/main/scala/decider/TermToZ3APIConverter.scala | 5 ++++- src/main/scala/decider/Z3ProverAPI.scala | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala index 4ba1b4776..7b177ceea 100644 --- a/src/main/scala/decider/TermToZ3APIConverter.scala +++ b/src/main/scala/decider/TermToZ3APIConverter.scala @@ -483,7 +483,10 @@ class TermToZ3APIConverter // could be any Z3 internal functions that exist for those custom sorts. For the Real (i.e., Perm) sort, however, // such functions exist. So we re-declare *only* this sort. val decls = declPreamble + args.zipWithIndex.map { case (a, i) => s"(declare-const workaround${i} ${smtlibConverter.convert(a.sort)})" }.mkString(" ") - val funcAppString = s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})" + val funcAppString = if (args.nonEmpty) + s"(${functionName} ${(0 until args.length).map(i => "workaround" + i).mkString(" ")})" + else + functionName val assertion = decls + s" (assert (= ${funcAppString} ${funcAppString}))" val workaround = ctx.parseSMTLIB2String(assertion, null, null, null, null) val app = workaround(0).getArgs()(0) diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala index c5b5c9b42..c0cdbe12f 100644 --- a/src/main/scala/decider/Z3ProverAPI.scala +++ b/src/main/scala/decider/Z3ProverAPI.scala @@ -263,7 +263,7 @@ class Z3ProverAPI(uniqueId: String, case t => triggerGenerator.isForbiddenInTrigger(t) }.nonEmpty)) q.copy(triggers = goodTriggers) - }({t => true}) + }(_ => true) cleanTerm }