Merge pull request #1701 from informalsystems/ro/funSets-as-arrays

Encode function sets as SMT arrays
apalache-mc · May 3, 2022 · d0878ca · d0878ca
2 parents 0fff5ac + b98ba8c
commit d0878ca
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 2 deletions.
diff --git a/UNRELEASED.md b/UNRELEASED.md
@@ -10,3 +10,6 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Bug fixes
+
+* Fix usage of sets of function sets in the arrays encoding, see #1680
diff --git a/test/tla/OracleFunSet.tla b/test/tla/OracleFunSet.tla
@@ -0,0 +1,20 @@
+------ MODULE OracleFunSet --------
+\* A regression test for the use of sets of function sets, see:
+\* https://github.com/informalsystems/apalache/issues/1680
+
+VARIABLES
+   \* @type: Set(Bool -> Int);
+  witness,
+  \* @type: Bool;
+  found
+
+Init ==
+  /\ witness \in {[{TRUE} -> {222521218, 0}]}
+  /\ found \in BOOLEAN
+
+Next ==
+  UNCHANGED <<witness, found>>
+
+NotFound ==
+  ~found
+======================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -1403,6 +1403,17 @@ $ apalache-mc check --inv=Inv --length=6 --cinit=CInit SetAddDel.tla | sed 's/I@
 EXITCODE: OK
 ```
 
+### check OracleFunSet succeeds (array-encoding)
+
+Regression test for https://github.com/informalsystems/apalache/issues/1680
+Function sets themselves should be able to be set elements.
+
+```sh
+$ apalache-mc check OracleFunSet.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
 ## configure the check command
 
 Testing various flags that are set via command-line options and the TLC configuration file. The CLI has priority over

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -526,8 +526,11 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
           case PowSetT(domType) if encoding == arraysEncoding =>
             z3context.mkArraySort(getOrMkCellSort(domType), z3context.getBoolSort)
 
-          case FunT(FinSetT(domType), resType) if encoding == arraysEncoding =>
-            z3context.mkArraySort(getOrMkCellSort(domType), getOrMkCellSort(resType))
+          case FinFunSetT(domType, FinSetT(cdmElemType)) if encoding == arraysEncoding =>
+            z3context.mkArraySort(getOrMkCellSort(FunT(domType, cdmElemType)), z3context.getBoolSort)
+
+          case FunT(FinSetT(domElemType), resType) if encoding == arraysEncoding =>
+            z3context.mkArraySort(getOrMkCellSort(domElemType), getOrMkCellSort(resType))
 
           case _ =>
             log(s"(declare-sort $sig 0)")