Skip to content
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

Jump to bottom

Equivalence checking updates #1145

Open
wants to merge 6 commits into
base: scala-2
Choose a base branch
from
Open

Equivalence checking updates #1145

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
fa47b1d
Fix timeouts
drganam May 31, 2021
7fcd448
Update Trace description
drganam May 31, 2021
451deb4
Add --norm
drganam May 31, 2021
1d6d43b
Track status
drganam Jun 2, 2021
63a066a
Fix tparams
Aug 30, 2021
08b1fee
Fix tparams for preconditions
drganam Sep 1, 2021
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
7 changes: 7 additions & 0 deletions core/src/main/scala/stainless/Component.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,13 @@ object optModels extends inox.OptionDef[Seq[String]] {
val usageRhs = "f1,f2,..."
}

object optNorm extends inox.OptionDef[String] {
val name = "norm"
val default = ""
val parser = inox.OptionParsers.stringParser
val usageRhs = "f"
}

trait ComponentRun { self =>
val component: Component
val trees: ast.Trees
Expand Down
1 change: 1 addition & 0 deletions core/src/main/scala/stainless/MainHelpers.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
optFunctions -> Description(General, "Only consider functions f1,f2,..."),
optCompareFuns -> Description(General, "Only consider functions f1,f2,... for equivalence checking"),
optModels -> Description(General, "Consider functions f1, f2, ... as model functions for equivalence checking"),
optNorm -> Description(General, "Use function f as normalization function for equivalence checking"),
extraction.utils.optDebugObjects -> Description(General, "Only print debug output for functions/adts named o1,o2,..."),
extraction.utils.optDebugPhases -> Description(General, {
"Only print debug output for phases p1,p2,...\nAvailable: " +
Expand Down
2 changes: 1 addition & 1 deletion core/src/main/scala/stainless/Report.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
val rows = processRows(full)
val width = if (rows.isEmpty) 1 else rows.head.cellsSize // all rows must have the same size
val color = if (isSuccess) Console.GREEN else Console.RED

val footer =
f"total: ${stats.total}%-4d " +
f"valid: ${stats.valid}%-4d (${stats.validFromCache} from cache) " +
Expand Down
6 changes: 3 additions & 3 deletions core/src/main/scala/stainless/extraction/package.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import scala.language.existentials
package object extraction {

val phases: Seq[(String, String)] = Seq(
"UserFiltering" -> "Removes all the library functions not used by the user",
"UserFiltering" -> "Remove all the library functions not used by the user",
"Preprocessing" -> "A preprocessing phase before the pipeline",
"PartialFunctions" -> "Lift partial function preconditions",
"XlangLowering" -> "Lowering phase at the end of xlang phases",
Expand All @@ -52,8 +52,8 @@ package object extraction {
"FunctionSpecialization" -> "Specialize functions",
"FunctionInlining" -> "Transitively inline marked functions",
"LeonInlining" -> "Transitively inline marked functions (closer to what Leon did)",
"Trace" -> "Apply the traceInduct tactic during verification of the annotated function.",
"SizedADTExtraction" -> "Transforms calls to 'indexedAt' to the 'SizedADT' tree",
"Trace" -> "Compare --compareFuns functions for equivalence. Expand @traceInduct",
"SizedADTExtraction" -> "Transform calls to 'indexedAt' to the 'SizedADT' tree",
"InductElimination" -> "Replace @induct annotation by explicit recursion",
"MeasureInference" -> "Infer and inject measures in recursive functions",
"PartialEvaluation" -> "Partially evaluate marked function calls",
Expand Down
Loading