Skip to content

Add --smt-timeout flag to kprove #3576

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

Merged
dwightguth merged 4 commits into from
Aug 14, 2023
Merged

Add --smt-timeout flag to kprove #3576

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
ee21548
Add --smt-timeout flag to kprove
Scott-Guest Aug 14, 2023
e59b44a
Add missing period.
Scott-Guest Aug 14, 2023
2224eaf
Pass --smt-timeout in all places
Scott-Guest Aug 14, 2023
68fa415
Merge branch 'develop' into kprove-z3-timeout
Aug 14, 2023
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
12 changes: 12 additions & 0 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,10 @@ public RewriterResult execute(K k, Optional<Integer> depth) {
args.add("--smt-prelude");
args.add(smtOptions.smtPrelude);
}
if (smtOptions.smtTimeout != null) {
args.add("--smt-timeout");
args.add(Integer.toString(smtOptions.smtTimeout));
}
koreCommand = args.toArray(koreCommand);
if (backendOptions.dryRun) {
System.out.println(String.join(" ", koreCommand));
Expand Down Expand Up @@ -222,6 +226,10 @@ public K search(K initialConfiguration, Optional<Integer> depth, Optional<Intege
args.add("--smt-prelude");
args.add(smtOptions.smtPrelude);
}
if (smtOptions.smtTimeout != null) {
args.add("--smt-timeout");
args.add(Integer.toString(smtOptions.smtTimeout));
}
koreCommand = args.toArray(koreCommand);
if (backendOptions.dryRun) {
System.out.println(String.join(" ", koreCommand));
Expand Down Expand Up @@ -313,6 +321,10 @@ private List<String> buildCommonProvingCommand(String defPath, String specPath,
args.add("--smt-prelude");
args.add(smtOptions.smtPrelude);
}
if (smtOptions.smtTimeout != null) {
args.add("--smt-timeout");
args.add(Integer.toString(smtOptions.smtTimeout));
}
if (kProveOptions.debugScript != null) {
if (!kProveOptions.debugger) {
throw KEMException.criticalError("Can only use --debug-script with --debugger.");
Expand Down
9 changes: 3 additions & 6 deletions kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,13 @@ public Class<SMTSolver> enumClass() {
@Parameter(names={"--smt-prelude", "--smt_prelude"}, description="Path to the SMT prelude file.", hidden = true)
public String smtPrelude;

@Parameter(names="--smt-timeout", description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
public Integer smtTimeout = null;

@Parameter(names="--z3-jni", description="Invokes Z3 as JNI library. Default is external process. " +
"JNI is slightly faster, but can potentially lead to JVM crash.", hidden = true)
public boolean z3JNI = false;

@Parameter(names="--z3-cnstr-timeout", description="The default soft timeout (in milli seconds) of Z3 for checking constraint satisfiability.", hidden = true)
public int z3CnstrTimeout = 50;

@Parameter(names="--z3-impl-timeout", description="The default soft timeout (in milli seconds) of Z3 for checking implication.", hidden = true)
public int z3ImplTimeout = 5000;

@Parameter(names="--z3-tactic", description="The solver tactic to use to check satisfiability in Z3.", hidden = true)
public String z3Tactic;
}