From ee21548029a2eeaf594ba5301a1304ca8d1496e2 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 14 Aug 2023 10:11:59 -0400 Subject: [PATCH 1/3] Add --smt-timeout flag to kprove --- .../org/kframework/backend/haskell/HaskellRewriter.java | 4 ++++ .../java/org/kframework/utils/options/SMTOptions.java | 9 +++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index 94b11f4ed92..8f71a03f944 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -129,6 +129,10 @@ public RewriterResult execute(K k, Optional 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)); diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java index be98722ed52..aaffb89b69a 100644 --- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java @@ -41,16 +41,13 @@ public Class 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; } From e59b44a633ea3305b70cee9011cc9d509a6f09a9 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 14 Aug 2023 10:17:07 -0400 Subject: [PATCH 2/3] Add missing period. --- .../src/main/java/org/kframework/utils/options/SMTOptions.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java index aaffb89b69a..db6fde3fbc4 100644 --- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java @@ -41,7 +41,7 @@ public Class 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) + @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. " + From 2224eaf28e63a995042ef21c4df3608dce1415ff Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 14 Aug 2023 11:24:02 -0400 Subject: [PATCH 3/3] Pass --smt-timeout in all places --- .../org/kframework/backend/haskell/HaskellRewriter.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index 8f71a03f944..cc95b117946 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -226,6 +226,10 @@ public K search(K initialConfiguration, Optional depth, Optional 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.");