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

SMT-LIB 2.6 conformance, support for cvc5, and generalization for alternative SMT-solvers #609

Merged
merged 23 commits into from
May 24, 2022
Merged

SMT-LIB 2.6 conformance, support for cvc5, and generalization for alternative SMT-solvers #609

Changes from 1 commit
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
7f22610
Update preamble to include explicit arities to conform to SMT-LIB 2.6
lfwa Dec 15, 2021
7d1cf97
Prelim changes for cvc5
lfwa Feb 21, 2022
7138589
Added support for cvc5
lfwa Apr 17, 2022
aed16cb
Removed outcommented line
lfwa Apr 17, 2022
a1badb1
Generalized last of Z3-specific options.
lfwa Apr 21, 2022
b7f61e7
Merge branch 'cvc5' into master
lfwa Apr 22, 2022
a10044f
Merge pull request #1 from lfwa/master
lfwa Apr 22, 2022
68ea2eb
Redo lost changes from commit 7aa97f1879aa5bc7a43bc35b2c92a9124530023d
lfwa Apr 22, 2022
bf234e8
Merge branch 'viperproject:master' into cvc5
lfwa Apr 22, 2022
494401d
Removed forwardArgumentsConverter
lfwa Apr 22, 2022
60de520
Ensure :pattern ((f x)) instead of pattern (f x) since pattern must …
lfwa Apr 22, 2022
6bc0d29
Removed non-cvc5-specifc keywords (duplicates).
lfwa Apr 22, 2022
2924e00
Clarification for default timeout.
lfwa Apr 22, 2022
56e4539
Clarified that the cvc5 solver is optional.
lfwa Apr 22, 2022
37e3adb
Revert back to default timeout of 0 for all provers.
lfwa Apr 24, 2022
6ab9858
Changed rawTimeout to timeout.
lfwa Apr 24, 2022
4215b09
Added call for timeout after converting back to option.
lfwa Apr 24, 2022
d5b896c
Reverted back original timeout.
lfwa Apr 24, 2022
115317d
Resolve conflicts
lfwa May 24, 2022
9e5757c
Merge branch 'master' into cvc5
lfwa May 24, 2022
84e97fc
Adapted code from upstream
May 24, 2022
0a8b718
IntelliJ suggestions
May 24, 2022
eaa1190
Code cosmetics
May 24, 2022
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
Prev Previous commit
Code cosmetics
  • Loading branch information
Malte Schwerhoff committed May 24, 2022
commit eaa11907cf43016c487eef7c2fba43f1f4d610a0
14 changes: 8 additions & 6 deletions src/main/scala/Config.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -416,8 +416,9 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
lazy val z3Exe: String = {
val isWindows = System.getProperty("os.name").toLowerCase.startsWith("windows")

rawZ3Exe.toOption.getOrElse(envOrNone(Z3ProverStdIO.exeEnvironmentalVariable)
.getOrElse("z3" + (if (isWindows) ".exe" else "")))
rawZ3Exe.toOption.getOrElse(
envOrNone(Z3ProverStdIO.exeEnvironmentalVariable)
.getOrElse("z3" + (if (isWindows) ".exe" else "")))
}

private val rawCvc5Exe = opt[String]("cvc5Exe",
Expand All @@ -430,8 +431,9 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
lazy val cvc5Exe: String = {
val isWindows = System.getProperty("os.name").toLowerCase.startsWith("windows")

rawCvc5Exe.toOption.getOrElse(envOrNone(Cvc5ProverStdIO.exeEnvironmentalVariable)
.getOrElse("cvc5" + (if (isWindows) ".exe" else "")))
rawCvc5Exe.toOption.getOrElse(
envOrNone(Cvc5ProverStdIO.exeEnvironmentalVariable)
.getOrElse("cvc5" + (if (isWindows) ".exe" else "")))
}

val defaultRawProverLogFile = "logfile"
Expand Down Expand Up @@ -715,8 +717,8 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
)

val prover: ScallopOption[String] = opt[String]("prover",
descr = (s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}. " +
s"(default: ${Z3ProverStdIO.name})."),
descr = s"One of the provers ${Z3ProverStdIO.name}, ${Cvc5ProverStdIO.name}. " +
s"(default: ${Z3ProverStdIO.name}).",
default = Some(Z3ProverStdIO.name),
noshort = true
)
Expand Down