Skip to content

Commit

Permalink
Using builtin equals for definitions
Browse files Browse the repository at this point in the history
  • Loading branch information
marcoeilers committed Nov 24, 2023
1 parent c64be11 commit 5409bd4
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/supporters/functions/FunctionData.scala
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ class FunctionData(val programFunction: ast.Function,

val limitedAxiom =
Forall(arguments,
limitedFunctionApplication === functionApplication,
BuiltinEquals(limitedFunctionApplication, functionApplication),
Trigger(functionApplication))

val triggerAxiom =
Expand Down Expand Up @@ -258,7 +258,7 @@ class FunctionData(val programFunction: ast.Function,
optBody.map(translatedBody => {
val pre = preconditionFunctionApplication
val nestedDefinitionalAxioms = generateNestedDefinitionalAxioms
val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(functionApplication === translatedBody))))
val body = And(nestedDefinitionalAxioms ++ List(Implies(pre, And(BuiltinEquals(functionApplication, translatedBody)))))
val allTriggers = (
Seq(Trigger(functionApplication))
++ predicateTriggers.values.map(pt => Trigger(Seq(triggerFunctionApplication, pt))))
Expand Down

0 comments on commit 5409bd4

Please sign in to comment.