Add command-line argument to set Z3 tactic to be used by KoreServer (#…

…660) `kore-rpc` now supports (and `kore-rpc-booster` will soon support, after runtimeverification/hs-backend-booster#317 is merged) the `--smt-tactic` option, that allows customizing the Z3 tactic used for checking satisfiability. THis PR allows setting this argument from command-line in `pyk`-powered tools. --------- Co-authored-by: devops <[email protected]>
runtimeverification · Sep 25, 2023 · db8f951 · db8f951
1 parent 40069ca
commit db8f951
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 2 deletions.
diff --git a/pyk/package/version b/pyk/package/version
@@ -1 +1 @@
-0.1.447
+0.1.448
diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.447"
+version = "0.1.448"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py
@@ -101,6 +101,12 @@ def smt_args(self) -> ArgumentParser:
             type=int,
             help='Number of times to retry SMT queries with scaling timeouts.',
         )
+        args.add_argument(
+            '--smt-tactic',
+            dest='smt_tactic',
+            type=str,
+            help='Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)',
+        )
         return args
 
     @cached_property

diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py
@@ -850,6 +850,7 @@ def __init__(
         smt_timeout: int | None = None,
         smt_retry_limit: int | None = None,
         smt_reset_interval: int | None = None,
+        smt_tactic: str | None = None,
         command: str | Iterable[str] | None = None,
         bug_report: BugReport | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
@@ -881,6 +882,8 @@ def __init__(
             smt_server_args += ['--smt-retry-limit', str(smt_retry_limit)]
         if smt_reset_interval:
             smt_server_args += ['--smt-reset-interval', str(smt_reset_interval)]
+        if smt_tactic:
+            smt_server_args += ['--smt-tactic', smt_tactic]
 
         haskell_log_args = (
             [
@@ -980,6 +983,7 @@ def __init__(
         smt_timeout: int | None = None,
         smt_retry_limit: int | None = None,
         smt_reset_interval: int | None = None,
+        smt_tactic: str | None = None,
         command: str | Iterable[str] | None,
         bug_report: BugReport | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
@@ -1027,6 +1031,7 @@ def __init__(
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             smt_reset_interval=smt_reset_interval,
+            smt_tactic=smt_tactic,
             command=args,
             bug_report=bug_report,
             haskell_log_format=haskell_log_format,
@@ -1045,6 +1050,7 @@ def kore_server(
     bug_report: BugReport | None = None,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
+    smt_tactic: str | None = None,
     haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
     haskell_log_entries: Iterable[str] = (),
     log_axioms_file: Path | None = None,
@@ -1059,6 +1065,7 @@ def kore_server(
             bug_report=bug_report,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
+            smt_tactic=smt_tactic,
             haskell_log_format=haskell_log_format,
             haskell_log_entries=haskell_log_entries,
             log_axioms_file=log_axioms_file,
@@ -1072,6 +1079,7 @@ def kore_server(
         bug_report=bug_report,
         smt_timeout=smt_timeout,
         smt_retry_limit=smt_retry_limit,
+        smt_tactic=smt_tactic,
         haskell_log_format=haskell_log_format,
         haskell_log_entries=haskell_log_entries,
         log_axioms_file=log_axioms_file,