Skip to content

Various updates in preparation for Z3 version update #585

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
marcoeilers wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Various updates in preparation for Z3 version update #585

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
af20496
Fixing some issues to prepare for Z3 4.16
marcoeilers May 19, 2026
30ee823
Trying to fix some sequence axiom issues
marcoeilers May 19, 2026
1d537fd
Merge branch 'master' into meilers_z3_416
marcoeilers May 20, 2026
9779fe2
Cleanup, implemented Alex' suggestion on sequence axiom
marcoeilers Aug 14, 2026
4539def
Merge branch 'master' into meilers_z3_416
marcoeilers Aug 14, 2026
8f6223c
Adapting test annotations
marcoeilers Aug 14, 2026
e54345f
Merge
marcoeilers Aug 14, 2026
482ebe8
Merge
marcoeilers Aug 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 16 additions & 13 deletions src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -447,35 +447,38 @@ class DefaultHeapModule(val verifier: Verifier)
val pmT = predicateMaskFieldTypeOf(p)
val varDecls = p.formalArgs map mainModule.translateLocalVarDecl
val vars = varDecls map (_.l)
val predArgGetters = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}"), Seq(LocalVarDecl(Identifier("pred"), t)), v.typ))
val predArgGetters2 = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}_sm"), Seq(LocalVarDecl(Identifier("pred"), pmT)), v.typ))
val predId:BigInt = getPredicateOrWandId(p.name)
val f0 = FuncApp(predicate, vars, t)
val f1 = predicateMaskField(f0)
val f2 = FuncApp(pmField, vars, pmT)
TypeDecl(predicateMetaTypeOf(p)) ++
Func(predicate, varDecls, t) ++
Func(pmField, varDecls, pmT) ++
predArgGetters ++
predArgGetters2 ++
Axiom(MaybeForall(varDecls, Trigger(f1), f1 === f2)) ++
Axiom(MaybeForall(varDecls, Trigger(f0), isPredicateField(f0))) ++
Axiom(MaybeForall(varDecls, Trigger(f0), getPredicateOrWandId(f0) === IntLit(predId))) ++
Func(predicateTriggerIdentifier(p), Seq(LocalVarDecl(heapName, heapTyp), LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
Func(predicateTriggerAnyStateIdentifier(p), Seq(LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
{
// axiom that two predicate identifiers can only be the same, if all arguments
// are the same (e.g., we immediatly know that valid(1) != valid(2))
// are the same (e.g., we immediately know that valid(1) != valid(2))
if (vars.size == 0) Nil
else {
val varDecls2 = varDecls map (
v => LocalVarDecl(Identifier(v.name.name + "2")(v.name.namespace), v.typ))
val vars2 = varDecls2 map (_.l)
var varsEqual = All((vars zip vars2) map {
case (v1, v2) => v1 === v2
})
val f0_2 = FuncApp(predicate, vars2, t)
val f2_2 = FuncApp(pmField, vars2, t)
Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f0, f0_2)),
(f0 === f0_2) ==> varsEqual)) ++
Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f2, f2_2)),
(f2 === f2_2) ==> varsEqual))
val argGetApply = predArgGetters map (f => FuncApp(f.name, Seq(f0), f.typ))
val argGetEqual = argGetApply.zip(vars).map {
case (get, v) => get === v
}
val argGetAxiom = Axiom(Forall(varDecls, Trigger(f0), All(argGetEqual)))
val argGetApply2 = predArgGetters2 map (f => FuncApp(f.name, Seq(f2), f.typ))
val argGetEqual2 = argGetApply2.zip(vars).map {
case (get, v) => get === v
}
val argGetAxiom2 = Axiom(Forall(varDecls, Trigger(f2), All(argGetEqual2)))
argGetAxiom ++ argGetAxiom2
}
}
}
Expand Down
46 changes: 30 additions & 16 deletions src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -596,8 +596,8 @@ class QuantifiedPermModule(val verifier: Verifier)
//if the permission is a wildcard, we check that we have some permission > 0 for all locations and assume that the permission substracted is smaller than the permission held.
val wildcardAssms:Stmt =
if(isWildcard) {
(Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++
(Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation)))))
Locally(Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++
(Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(Trigger(currentPermission(translatedRecv, translatedLocation))), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation)))))
} else {
Nil
}
Expand Down Expand Up @@ -649,13 +649,18 @@ class QuantifiedPermModule(val verifier: Verifier)
CommentBlock("assume permission updates for independent locations", independentLocations) ++
(mask := qpMask)

val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else
CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2))

val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++
CommentBlock("check if receiver " + recv.toString + " is injective", Locally(injectiveAssertion)) ++
CommentBlock("check if sufficient permission is held", Locally(enoughPerm))

val res1 = Havoc(qpMask) ++
MaybeComment("wild card assumptions", stmts ++
wildcardAssms) ++
CommentBlock("check that the permission amount is positive", permPositive) ++
CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++
CommentBlock("check if sufficient permission is held", enoughPerm) ++
CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
checks ++
inverseAssumptions ++
maskUpdateStmt

vsFresh.foreach(v => env.undefine(v.localVar))
Expand Down Expand Up @@ -769,8 +774,8 @@ class QuantifiedPermModule(val verifier: Verifier)
//if we exhale a wildcard permission, assert that we hold some permission to all affected locations and restrict the wildcard value
val wildcardAssms:Stmt =
if(isWildcard) {
Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason)) ++
Assume(Forall(translatedLocals, Seq(), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource))))
Locally(Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason))) ++
Assume(Forall(translatedLocals, Seq(Trigger(currentPermission(translateNull, translatedResource))), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource))))
} else {
Nil
}
Expand Down Expand Up @@ -846,13 +851,18 @@ class QuantifiedPermModule(val verifier: Verifier)
CommentBlock("assume permission updates for independent locations ", independentLocations) ++
(mask := qpMask)

val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else
CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2))

val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++
CommentBlock("check if receiver " + accPred.toString + " is injective", Locally(injectiveAssertion)) ++
CommentBlock("check if sufficient permission is held", Locally(enoughPerm))

val res1 = Havoc(qpMask) ++
MaybeComment("wildcard assumptions", stmts ++
wildcardAssms) ++
CommentBlock("check that the permission amount is positive", permPositive) ++
CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++
CommentBlock("check if sufficient permission is held", enoughPerm) ++
CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
checks ++
inverseAssumptions ++
maskUpdateStmts

vsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
Expand Down Expand Up @@ -1048,6 +1058,10 @@ class QuantifiedPermModule(val verifier: Verifier)
}
}

def Locally(s: Stmt): Stmt = {
NondetIf(s ++ Assume(FalseLit()))
}

/*
translate inhaling a forall expressions
*/
Expand Down Expand Up @@ -1205,15 +1219,15 @@ class QuantifiedPermModule(val verifier: Verifier)

val reas = reasons.QPAssertionNotInjective(fieldAccess)
var err = error.dueTo(reas)
val injectiveAssertion = Assert(is_injective, err)
val injectiveAssertion = Locally(Assert(is_injective, err))

val res1 = Havoc(qpMask) ++
stmts ++
(if (!verifier.assumeInjectivityOnInhale) injectiveAssertion
else Nil) ++
CommentBlock("Define Inverse Function", Assume(invAssm1) ++
Assume(invAssm2)) ++
(if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", permPositive) else Nil) ++
(if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive)) else Nil) ++
CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++
// CommentBlock("Assume injectivity", injectiveAssumption) ++
CommentBlock("Define permissions", Assume(Forall(obj, triggerForPermissionUpdateAxiom, condTrueLocations && condFalseLocations)) ++
Expand Down Expand Up @@ -1383,7 +1397,7 @@ class QuantifiedPermModule(val verifier: Verifier)
}
val injectTrigger = Seq(Trigger(Seq(triggerFunApp, triggerFunApp2)))
val err = error.dueTo(reasons.QPAssertionNotInjective(accPred.loc))
val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err)
val injectiveAssertion = Locally(Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err))


val res1 = Havoc(qpMask) ++
Expand All @@ -1392,7 +1406,7 @@ class QuantifiedPermModule(val verifier: Verifier)
else Nil) ++
CommentBlock("Define Inverse Function", Assume(invAssm1) ++
Assume(invAssm2)) ++
(if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", permPositive)) else Nil) ++
(if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive))) else Nil) ++
CommentBlock("Define updated permissions", permissionsMap) ++
CommentBlock("Define independent locations", (independentLocations ++
independentResource)) ++
Expand Down
9 changes: 2 additions & 7 deletions src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ object SequenceAxiomatization {
| s0 != Seq#Empty() && s1 != Seq#Empty() && Seq#Length(s0) <= n && n < Seq#Length(Seq#Append(s0,s1)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s0)),Seq#Length(s0)) == n && Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, Seq#Sub(n,Seq#Length(s0))));
|// AS: added "reverse triggering" versions of the axioms
|axiom (forall<T> s0: Seq T, s1: Seq T, m: int :: { Seq#Index(s1, m), Seq#Append(s0,s1)} // m == n-|s0|, n == m + |s0|
| s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m));
| s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) && s1 != Seq#Append(s0,s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m));
Comment thread
marcoeilers marked this conversation as resolved.
Outdated
|
|function Seq#Update<T>(Seq T, int, T): Seq T;
|axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } {Seq#Length(s),Seq#Update(s,i,v)} // (diff 4: added trigger)
Expand Down Expand Up @@ -207,7 +207,7 @@ object SequenceAxiomatization {
|
|axiom (forall<T> s: Seq T, t: Seq T, n:int ::
| { Seq#Drop(Seq#Append(s,t),n) }
| n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s))));
| n > 0 && n > Seq#Length(s) && n < Seq#Length(Seq#Append(s,t)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s))));
|
|// diff 16: temporarily dropped general case of these
|//axiom (forall<T> s: Seq T, t: Seq T, m:int ::
Expand Down Expand Up @@ -335,11 +335,6 @@ object SequenceAxiomatization {
|*/
|// diff 9: skolemise equals (new)
|// AS: split axiom
|axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
| Seq#Equal(s0,s1) ==>
| Seq#Length(s0) == Seq#Length(s1) &&
| (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
| 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
|
|function Seq#SkolemDiff<T>(Seq T, Seq T) : int; // skolem function for Seq#Equals
|
Expand Down
6 changes: 0 additions & 6 deletions src/main/scala/viper/carbon/verifier/BoogieInterface.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,16 +51,10 @@ trait BoogieInterface {
"/errorTrace:0",
"/errorLimit:10000000",
"/proverOpt:O:smt.AUTO_CONFIG=false",
"/proverOpt:O:smt.PHASE_SELECTION=0",
Comment thread
marcoeilers marked this conversation as resolved.
"/proverOpt:O:smt.RESTART_STRATEGY=0",
"/proverOpt:O:smt.RESTART_FACTOR=|1.5|",
"/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true",
Comment thread
marcoeilers marked this conversation as resolved.
"/proverOpt:O:smt.CASE_SPLIT=3",
"/proverOpt:O:smt.DELAY_UNITS=true",
"/proverOpt:O:NNF.SK_HACK=true",

@alexanderjsummers alexanderjsummers Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume this option has gone? Not sure what it did, to be honest

@marcoeilers marcoeilers Aug 3, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It still exists, and the other removed ones also still exist IIRC.
The changes align our options with the ones Dafny uses (https://github.com/dafny-lang/dafny/blob/f3c2fedfb2b88272af5b64f5e45d803a3bc0043a/docs/DafnyRef/UserGuide.md?plain=1#L2751), which is also on the Z3 version we want to move to (4.16.0). My impression was that we at some point basically just copied the options Dafny used back then, so if they've switched things up, we probably should as well.
I believe this improved performance or completeness with newer Z3, but I'll recheck.

@marcoeilers marcoeilers Aug 14, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I checked, and the options change essentially makes no difference for performance or completeness, neither with old Z3 4.8.7 nor with new Z3 4.16.0. I still think we should make the change, since it would re-align the options we use in Silicon and Carbon, and those with Dafny as well.

"/proverOpt:O:smt.MBQI=false",
"/proverOpt:O:smt.QI.EAGER_THRESHOLD=100",
"/proverOpt:O:smt.BV.REFLECT=true",
Comment thread
marcoeilers marked this conversation as resolved.
"/proverOpt:O:smt.qi.max_multi_patterns=1000",
s"/proverOpt:PROVER_PATH=$z3Path")

Expand Down
2 changes: 1 addition & 1 deletion src/test/scala/viper/carbon/AllTests.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,5 +40,5 @@ class AllTests extends SilSuite {
lazy val verifiers = List(verifier)

val commandLineArguments: Seq[String] =
Seq()
Seq("--timeout=120")
}
Loading