diff --git a/UNRELEASED.md b/UNRELEASED.md index 84488f67af..79eb12305c 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -10,3 +10,7 @@ * Some bug fix, see #124 DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE --> + +### Features + + * Added support for sets to the SMT encoding with arrays, see #1092 diff --git a/docs/src/adr/011adr-smt-arrays.md b/docs/src/adr/011adr-smt-arrays.md index 6e33d13db1..2ef3fbe564 100644 --- a/docs/src/adr/011adr-smt-arrays.md +++ b/docs/src/adr/011adr-smt-arrays.md @@ -2,7 +2,7 @@ | author | revision | | ------------- | --------:| -| Rodrigo Otoni | 1 | +| Rodrigo Otoni | 1.1 | This ADR describes an alternative encoding of the [KerA+] fragment of TLA+ into SMT. Compound data structures, e.g. sets, are currently encoded using the [core theory] of SMT, @@ -19,10 +19,11 @@ treatment of different TLA+ operators are described. The encoding using arrays is to be an alternative, not a replacement, to the already existing encoding. Given this, a new option is to be added to the `check` command of the CLI. The default encoding will be -the existing one. The option description is shown below. +the existing one. The option description is shown below. The envvar `SMT_ENCODING` can also be used to +set the encoding, see the [model checking parameters] for details. ``` ---smt-encoding=STRING : the SMT encoding: oopsla19, arrays (experimental), default: oopsla19 +--smt-encoding : the SMT encoding: oopsla19, arrays (experimental), default: oopsla19 (overrides envvar SMT_ENCODING) ``` ### Code changes @@ -30,26 +31,28 @@ the existing one. The option description is shown below. The following changes will be made to implement the new CLI option: - Add new string variable to class `CheckCmd` to enable the new option. +- Add new `smtEncoding` field to `SolverConfig`. - Add new class `SymbStateRewriterImplWithArrays`, which extends class `SymbStateRewriterImpl`. -- Use the new option to select between different `SymbStateRewriter` +- Use the new option to set the `SolverConfig` encoding field and select between different `SymbStateRewriter` implementations in classes `BoundedCheckerPassImpl` and `SymbStateRewriterAuto`. ## 2. Testing the new encoding -The new encoding should provide the same results as the existing one, the available test suit -will thus be used to test the new encoding. To achieve this, the test suit needs to be made parametric -w.r.t. the implementations of `SymbStateRewriter`. +The new encoding should provide the same results as the existing one, the available test suite +will thus be used to test the new encoding. To achieve this, the unit tests needs to be made parametric +w.r.t. the `SolverConfig` encoding field and the implementations of `SymbStateRewriter`, and the +integration tests need to be tagged to run with the new encoding. ### Code changes The following changes will be made to implement the tests for the new encoding: -- Refactor the classes in `tla-bmcmt/src/test` to enable unit testing with different - implementations of `SymbStateRewriter`. -- Add unit tests for the new encoding, which should be similar to existing tests, but use - `SymbStateRewriterImplWithArrays` instead of `SymbStateRewriterImpl`. -- Add integration tests for the new encoding, which should be similar to existing tests, but - have the `smt-encoding` flag set to `arrays`. +- Refactor the classes in `tla-bmcmt/src/test` to enable unit testing with different configurations + of `SolverConfig` and implementations of `SymbStateRewriter`. +- Add unit tests for the new encoding, which should be similar to existing tests, but use a + different solver configuration and `SymbStateRewriterImplWithArrays` instead of `SymbStateRewriterImpl`. +- Add integration tests for the new encoding by tagging existing tests with `array-encoding`, which + will be run by the CI with envvar `SMT_ENCODING` set to `arrays`. ## 3. Encoding sets @@ -126,11 +129,25 @@ For consistency, the new encoding uses constant arrays to declare both finite an The following changes will be made to implement the new encoding of sets: -- Add alternative rewriting rules for sets, via new classes extending `RewritingRule`. - - The new rules will use SMT equality directly, instead of relying on class `LazyEquality`. -- In class `SymbStateRewriterImplWithArrays`, overwrite `ruleLookupTable` with the new rules. - - Existing rules will be reused when appropriate, e.g. rules for handling Boolean constants. -- In class `Z3SolverContext`, add appropriate methods to handle SMT constraints over arrays. +- Add alternative rewriting rules for sets when appropriate, by extending the existing rules. + - All alternative rules will be suffixed with `WithArrays`. + - The new rules will not rely on `LazyEquality` and will aim to use SMT equality directly. + - Only the generation of SMT constraints will be modified by the new rules, the other Arena + elements will remain unchanged. +- In class `SymbStateRewriterImplWithArrays`, add the new rules to `ruleLookupTable` by overriding + the entries to their older versions. +- In class `Z3SolverContext`, add/change appropriate methods to handle SMT constraints over arrays. + - The main changes will de done in `declareCell`, `declareInPredIfNeeded`, and `getInPred`, as + these methods are directly responsible for creating the SMT constraints representing sets and + set membership. + - Cases for `FinSetT` and `PowSetT` will be added to `getOrMkCellSort`, as these types are no + longer represented by uninterpreted constants. + - `cellCache` will be changed to contain a list of cells, in order to handle the effects of + `push` and `pop` in the SSA assignment of sets. + - A new cache, `inStored`, will provide the required information to `getInPred` to enable it to + return either a `store` or a `select` constraint, when appropriate. + - Special cases for `TlaOper.eq` and `TlaBoolOper.equiv` will be added to `toExpr`, to allow the + set filter rule to propagate SSA sets when the filter predicate evaluates for false. ## 4. Encoding tuples and records @@ -151,4 +168,5 @@ TODO [SMT-LIB Standard]: http://smtlib.cs.uiowa.edu/index.shtml [Version 2.6]: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf [TLA+ Model Checking Made Symbolic]: https://dl.acm.org/doi/10.1145/3360549 +[model checking parameters]: https://apalache.informal.systems/docs/apalache/running.html#model-checker-command-line-parameters [represented internally in Z3]: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arrays diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 64047716ab..6a7010b7ea 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -232,7 +232,7 @@ EXITCODE: ERROR (12) ## running the check command -#### check factorization find a counterexample +#### check factorization find a counterexample (array-encoding) ```sh $ apalache-mc check --length=2 --inv=Inv factorization.tla | sed 's/I@.*//' @@ -243,7 +243,7 @@ Checker has found an error EXITCODE: ERROR (12) ``` -### check Fix531.tla reports no error: regression for issue 531 +### check Fix531.tla reports no error: regression for issue 531 (array-encoding) ```sh $ apalache-mc check --length=1 Fix531.tla | sed 's/I@.*//' @@ -253,7 +253,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check UnchangedExpr471.tla reports no error: regression for issue 471 +### check UnchangedExpr471.tla reports no error: regression for issue 471 (array-encoding) ```sh $ apalache-mc check --cinit=ConstInit --length=1 UnchangedExpr471.tla | sed 's/I@.*//' @@ -263,7 +263,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check ExistTuple476.tla reports no error: regression for issue 476 +### check ExistTuple476.tla reports no error: regression for issue 476 (array-encoding) ```sh $ apalache-mc check --length=1 ExistTuple476.tla | sed 's/I@.*//' @@ -323,7 +323,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Bug20201118 succeeds: regression for issue 333 +### check Bug20201118 succeeds: regression for issue 333 (array-encoding) ```sh $ apalache-mc check --length=10 --init=Init --next=Next --inv=Inv Bug20201118.tla | sed 's/I@.*//' @@ -333,7 +333,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Fix333 succeeds: another regression for issue 333 +### check Fix333 succeeds: another regression for issue 333 (array-encoding) ```sh $ apalache-mc check --length=2 --init=Init --next=Next --inv=Inv Fix333.tla | sed 's/I@.*//' @@ -353,7 +353,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Bug593 fails correctly: regression for issue 593 +### check Bug593 fails correctly: regression for issue 593 (array-encoding) ```sh $ apalache-mc check Bug593.tla | sed 's/I@.*//' @@ -393,7 +393,7 @@ EXITCODE: ERROR (12) ``` -### check ast.tla succeeds [array-encoding] +### check ast.tla succeeds ```sh $ apalache-mc check --length=5 ast.tla | sed 's/I@.*//' @@ -443,7 +443,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Bug20190921 succeeds +### check Bug20190921 succeeds (array-encoding) ```sh $ apalache-mc check --length=5 --cinit=CInit Bug20190921.tla | sed 's/I@.*//' @@ -453,7 +453,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check RangeWithConst succeeds +### check RangeWithConst succeeds (array-encoding) ```sh $ apalache-mc check --cinit=CInit --inv=Inv --length=1 RangeWithConst.tla | sed 's/I@.*//' @@ -633,7 +633,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Counter.tla errors +### check Counter.tla errors (array-encoding) ```sh $ apalache-mc check --length=10 --inv=Inv Counter.tla | sed 's/I@.*//' @@ -646,7 +646,7 @@ EXITCODE: ERROR (12) ### y2k.tla -#### check y2k with length 20 and ConstInit errors +#### check y2k with length 20 and ConstInit errors (array-encoding) ```sh $ apalache-mc check --length=20 --inv=Safety --cinit=ConstInit y2k_cinit.tla | sed 's/I@.*//' @@ -657,7 +657,7 @@ Checker has found an error EXITCODE: ERROR (12) ``` -#### check y2k with length 19 succeeds +#### check y2k with length 19 succeeds (array-encoding) ```sh $ apalache-mc check --length=19 --inv=Safety y2k_instance.tla | sed 's/I@.*//' @@ -667,7 +667,7 @@ The outcome is: NoError EXITCODE: OK ``` -#### check y2k with length 30 errors +#### check y2k with length 30 errors (array-encoding) ```sh $ apalache-mc check --length=30 --inv=Safety y2k_instance.tla | sed 's/I@.*//' @@ -678,7 +678,7 @@ Checker has found an error EXITCODE: ERROR (12) ``` -### check Counter.tla errors +### check Counter.tla errors (array-encoding) ```sh $ apalache-mc check --length=10 --inv=Inv Counter.tla | sed 's/I@.*//' @@ -689,7 +689,7 @@ Checker has found an error EXITCODE: ERROR (12) ``` -### check NatCounter.tla errors +### check NatCounter.tla errors (array-encoding) ```sh $ apalache-mc check --length=10 --inv=Inv NatCounter.tla | sed 's/I@.*//' @@ -709,7 +709,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check HandshakeWithTypes.tla with length 4 succeeds +### check HandshakeWithTypes.tla with length 4 succeeds (array-encoding) ```sh $ apalache-mc check --length=4 --inv=Inv HandshakeWithTypes.tla | sed 's/I@.*//' @@ -719,7 +719,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check HandshakeWithTypes.tla with lengh 5 deadlocks +### check HandshakeWithTypes.tla with lengh 5 deadlocks (array-encoding) ```sh $ apalache-mc check --length=5 --inv=Inv HandshakeWithTypes.tla | sed 's/I@.*//' @@ -729,7 +729,7 @@ The outcome is: Deadlock EXITCODE: ERROR (12) ``` -### check trivial violation of FALSE invariant +### check trivial violation of FALSE invariant (array-encoding) ```sh $ apalache-mc check --length=2 --inv=Inv Bug20200306.tla | sed 's/I@.*//' @@ -739,7 +739,7 @@ The outcome is: Error EXITCODE: ERROR (12) ``` -### check Init without an assignment fails +### check Init without an assignment fails (array-encoding) ```sh $ apalache-mc check --length=1 --inv=Inv Assignments20200309.tla @@ -748,7 +748,7 @@ EXITCODE: ERROR (255) [255] ``` -### check Inline.tla suceeds +### check Inline.tla suceeds (array-encoding) ```sh $ apalache-mc check --length=5 Inline.tla | sed 's/I@.*//' @@ -919,8 +919,7 @@ EXITCODE: ERROR (255) [255] ``` - -### check Empty.tla fails +### check Empty.tla fails (array-encoding) ```sh $ apalache-mc check Empty.tla @@ -929,7 +928,7 @@ EXITCODE: ERROR (255) [255] ``` -### check NoVars.tla succeeds +### check NoVars.tla succeeds (array-encoding) ```sh $ apalache-mc check --inv=Inv --length=1 NoVars.tla | sed 's/I@.*//' @@ -939,7 +938,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check HourClock.tla without Init fails +### check HourClock.tla without Init fails (array-encoding) ```sh $ apalache-mc check --init=NonExistantInit HourClock.tla @@ -948,7 +947,7 @@ EXITCODE: ERROR (255) [255] ``` -### check HourClock.tla without Next fails +### check HourClock.tla without Next fails (array-encoding) ```sh $ apalache-mc check --next=NonExistantNext HourClock.tla @@ -957,7 +956,7 @@ EXITCODE: ERROR (255) [255] ``` -### check HourClock.tla without Inv fails +### check HourClock.tla without Inv fails (array-encoding) ```sh $ apalache-mc check --inv=NonExistantInv HourClock.tla @@ -966,7 +965,7 @@ EXITCODE: ERROR (255) [255] ``` -### check NonNullaryLet succeeds: regression for issue 429 +### check NonNullaryLet succeeds: regression for issue 429 (array-encoding) ```sh $ apalache-mc check NonNullaryLet.tla | sed 's/I@.*//' @@ -976,7 +975,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check CaseNoOther succeeds +### check CaseNoOther succeeds (array-encoding) ```sh $ apalache-mc check CaseNoOther.tla | sed 's/I@.*//' @@ -986,7 +985,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check CaseNoOtherBool succeeds +### check CaseNoOtherBool succeeds (array-encoding) ```sh $ apalache-mc check CaseNoOtherBool.tla | sed 's/I@.*//' @@ -996,7 +995,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Callback.tla succeeds +### check Callback.tla succeeds (array-encoding) `Callback.tla` demonstrates that one can implement non-determinism with the existential operator and use a callback to do an assignment to a variable. As it requires tricky operator inlining, here is the test. @@ -1022,7 +1021,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check Selections succeeds +### check Selections succeeds (array-encoding) ```sh $ apalache-mc check Selections.tla | sed 's/I@.*//' @@ -1050,7 +1049,7 @@ $ apalache-mc check ITE_CASE.tla | sed 's/I@.*//' EXITCODE: ERROR (255) ``` -### check Deadlock712 succeeds +### check Deadlock712 succeeds (array-encoding) This test shows that Apalache may miss a deadlock, as discussed in issue 712. Once this is fixed, Apalache should find a deadlock. @@ -1063,7 +1062,7 @@ The outcome is: NoError EXITCODE: OK ``` -### check use of TLA_PATH for modules in child directory succeeds +### check use of TLA_PATH for modules in child directory succeeds (array-encoding) ```sh $ TLA_PATH=./tla-path-tests apalache-mc check ./tla-path-tests/ImportingModule.tla | sed 's/I@.*//' diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAuto.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAuto.scala index aa71202cd6..99fcbc8734 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAuto.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAuto.scala @@ -46,7 +46,7 @@ class SymbStateRewriterAuto(private var _solverContext: SolverContext) extends S private val exprGradeStoreImpl = new ExprGradeStoreImpl() private val exprGradeAnalysis = new ExprGradeAnalysis(exprGradeStoreImpl) - private val impl = new SymbStateRewriterImpl(solverContext, exprGradeStore) + protected val impl = new SymbStateRewriterImpl(solverContext, exprGradeStore) override def contextLevel: Int = impl.contextLevel diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAutoWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAutoWithArrays.scala index 26c585df22..7556e3065f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAutoWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAutoWithArrays.scala @@ -2,4 +2,6 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -class SymbStateRewriterAutoWithArrays(_solverContext: SolverContext) extends SymbStateRewriterAuto(_solverContext) {} +class SymbStateRewriterAutoWithArrays(_solverContext: SolverContext) extends SymbStateRewriterAuto(_solverContext) { + override protected val impl = new SymbStateRewriterImplWithArrays(solverContext, exprGradeStore) +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala index dd64c1256b..8144ee8c5a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala @@ -107,7 +107,7 @@ class SymbStateRewriterImpl(private var _solverContext: SolverContext, val exprCache = new ExprCache(exprGradeStore) @transient - private lazy val substRule = new SubstRule(this) + protected lazy val substRule = new SubstRule(this) /** * The store that contains formula hints. By default, empty. @@ -136,11 +136,14 @@ class SymbStateRewriterImpl(private var _solverContext: SolverContext, lazy val statListener: RuleStatListener = new RuleStatListener() solverContext.setSmtListener(statListener) // subscribe to the SMT solver + @transient + lazy val ruleLookupTable: Map[String, List[RewritingRule]] = defaultRuleLookupTable + // A nice way to guess the candidate rules by looking at the expression key. // We use simple expressions to generate the keys. // For each key, there is a short list of rules that may be applicable. @transient - lazy val ruleLookupTable: Map[String, List[RewritingRule]] = { + lazy val defaultRuleLookupTable: Map[String, List[RewritingRule]] = { Map( // the order is only important to improve readability @@ -193,8 +196,8 @@ class SymbStateRewriterImpl(private var _solverContext: SolverContext, // sets key(tla.in(tla.name("x"), tla.name("S"))) -> List(new SetInRule(this)), - key(tla.enumSet(tla.name("x"))) -> - List(new SetCtorRule(this)), + key(tla.enumSet(tla.name("x"))) + -> List(new SetCtorRule(this)), key(tla.subseteq(tla.name("x"), tla.name("S"))) -> List(new SetInclusionRule(this)), key(tla.cup(tla.name("X"), tla.name("Y"))) @@ -577,7 +580,7 @@ class SymbStateRewriterImpl(private var _solverContext: SolverContext, * @param ex a TLA+ expression * @return a string that gives us an equivalence class for similar operations (see the code) */ - private def key(ex: TlaEx): String = { + protected def key(ex: TlaEx): String = { ex match { // TODO: Is this correct? case OperEx(TlaOper.apply, NameEx(_), _*) => diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImplWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImplWithArrays.scala index 1cf734d368..af1c38799f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImplWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImplWithArrays.scala @@ -3,7 +3,122 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.tla.bmcmt.analyses.{ExprGradeStore, ExprGradeStoreImpl} import at.forsyte.apalache.tla.bmcmt.rewriter.MetricProfilerListener import at.forsyte.apalache.tla.bmcmt.smt.SolverContext +import at.forsyte.apalache.tla.bmcmt.rules._ +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.lir.convenience.tla +import at.forsyte.apalache.tla.lir.oper._ +import at.forsyte.apalache.tla.lir.UntypedPredefs._ class SymbStateRewriterImplWithArrays(_solverContext: SolverContext, exprGradeStore: ExprGradeStore = new ExprGradeStoreImpl(), profilerListener: Option[MetricProfilerListener] = None) - extends SymbStateRewriterImpl(_solverContext, exprGradeStore, profilerListener) {} + extends SymbStateRewriterImpl(_solverContext, exprGradeStore, profilerListener) { + + // TODO: remove unsupportedRules after passing over all rules + @transient + override lazy val ruleLookupTable: Map[String, List[RewritingRule]] = + (defaultRuleLookupTable ++ newRules) -- unsupportedRules.keys + + val newRules: Map[String, List[RewritingRule]] = { + Map( + // logic + key(tla.eql(tla.name("x"), tla.name("y"))) + -> List(new EqRuleWithArrays(this)), // TODO: update with additional elements later + // sets + key(tla.in(tla.name("x"), tla.name("S"))) + -> List(new SetInRuleWithArrays(this)), // TODO: add support for funSet later + key(tla.subseteq(tla.name("x"), tla.name("S"))) + -> List(new SetInclusionRuleWithArrays(this)) + // TODO: consider copying one array and storing the edges of the other in SetCupRule + ) + } + + val unsupportedRules: Map[String, List[RewritingRule]] = { + Map( + // logic + key(tla.choose(tla.name("x"), tla.name("S"), tla.name("p"))) + -> List(new ChooseRule(this)), + // control flow + key(tla.letIn(tla.int(1), TlaOperDecl("A", List(), tla.int(2)))) + -> List(new LetInRule(this)), + key(tla.appDecl(TlaOperDecl("userOp", List(), tla.int(3)))) -> + List(new UserOperRule(this)), + // functions + key(tla.except(tla.name("f"), tla.int(1), tla.int(42))) + -> List(new FunExceptRule(this)), + key(tla.funSet(tla.name("X"), tla.name("Y"))) + -> List(new FunSetCtorRule(this)), + key(tla.dom(tla.funDef(tla.name("e"), tla.name("x"), tla.name("S")))) + -> List(new DomainRule(this, intRangeCache)), // also works for records + key(tla.recFunDef(tla.name("e"), tla.name("x"), tla.name("S"))) + -> List(new RecFunDefAndRefRule(this)), + key(tla.recFunRef()) + -> List(new RecFunDefAndRefRule(this)), + // tuples, records, and sequences + key(tla.head(tla.tuple(tla.name("x")))) + -> List(new SeqOpsRule(this)), + key(tla.tail(tla.tuple(tla.name("x")))) + -> List(new SeqOpsRule(this)), + key(tla.subseq(tla.tuple(tla.name("x")), tla.int(2), tla.int(4))) + -> List(new SeqOpsRule(this)), + key(tla.len(tla.tuple(tla.name("x")))) + -> List(new SeqOpsRule(this)), + key(tla.append(tla.tuple(tla.name("x")), tla.int(10))) + -> List(new SeqOpsRule(this)), + key(tla.concat(tla.name("Seq1"), tla.name("Seq2"))) + -> List(new SeqOpsRule(this)), + // FiniteSets + key(OperEx(ApalacheOper.constCard, tla.ge(tla.card(tla.name("S")), tla.int(3)))) + -> List(new CardinalityConstRule(this)), + key(OperEx(TlaFiniteSetOper.cardinality, tla.name("S"))) + -> List(new CardinalityRule(this)), + key(OperEx(TlaFiniteSetOper.isFiniteSet, tla.name("S"))) + -> List(new IsFiniteSetRule(this)), + // misc + key(OperEx(TlaOper.label, tla.str("lab"), tla.str("x"))) + -> List(new LabelRule(this)), + key(OperEx(ApalacheOper.gen, tla.int(2))) + -> List(new GenRule(this)), + // folds + key(OperEx(ApalacheOper.foldSet, tla.name("A"), tla.name("v"), tla.name("S"))) + -> List(new FoldSetRule(this)), + key(OperEx(ApalacheOper.foldSeq, tla.name("A"), tla.name("v"), tla.name("s"))) + -> List(new FoldSeqRule(this)), + // TLC + key(OperEx(TlcOper.print, tla.bool(true), tla.str("msg"))) + -> List(new TlcRule(this)), + key(OperEx(TlcOper.printT, tla.str("msg"))) + -> List(new TlcRule(this)), + key(OperEx(TlcOper.assert, tla.bool(true), tla.str("msg"))) + -> List(new TlcRule(this)), + key(OperEx(TlcOper.colonGreater, tla.int(1), tla.int(2))) // :> + -> List(new TlcRule(this)), + key(OperEx(TlcOper.atat, NameEx("fun"), NameEx("pair"))) // @@ + -> List(new TlcRule(this)) + // ----------------------------------------------------------------------- + // RULES BELOW WERE NOT REMOVED TO RUN UNIT TESTS, WILL BE LOOKED AT LATER + // ----------------------------------------------------------------------- + /* + // logic + key(OperEx(ApalacheOper.skolem, tla.exists(tla.name("x"), tla.name("S"), tla.name("p")))) + -> List(new QuantRule(this)), + key(tla.exists(tla.name("x"), tla.name("S"), tla.name("p"))) + -> List(new QuantRule(this)), + key(tla.forall(tla.name("x"), tla.name("S"), tla.name("p"))) + -> List(new QuantRule(this)), + // control flow + key(tla.ite(tla.name("cond"), tla.name("then"), tla.name("else"))) + -> List(new IfThenElseRule(this)), + // functions + key(tla.funDef(tla.name("e"), tla.name("x"), tla.name("S"))) + -> List(new FunCtorRule(this)), + key(tla.appFun(tla.name("f"), tla.name("x"))) + -> List(new FunAppRule(this)), + // tuples, records, and sequences + key(tla.tuple(tla.name("x"), tla.int(2))) + -> List(new TupleOrSeqCtorRule(this)), + key(tla.enumFun(tla.str("a"), tla.int(2))) + -> List(new RecCtorRule(this)) + */ + ) + } +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index 440a0803dc..25cb419afd 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -83,17 +83,17 @@ class BoundedCheckerPassImpl @Inject() (val options: PassOptions, hintsStore: Fo val tuning = options.getOrElse[Map[String, String]]("general", "tuning", Map[String, String]()) val debug = options.getOrElse[Boolean]("general", "debug", false) val saveDir = options.getOrError[Path]("io", "outdir").toFile + val smtEncoding = options.get[Option[String]]("checker", "smt-encoding").flatten.getOrElse(oopsla19Encoding) val params = new ModelCheckerParams(input, stepsBound, saveDir, tuning, debug) params.discardDisabled = options.getOrElse[Boolean]("checker", "discardDisabled", true) params.checkForDeadlocks = !options.getOrElse[Boolean]("checker", "noDeadlocks", false) params.nMaxErrors = options.getOrElse[Int]("checker", "maxError", 1) - - params.smtEncoding = options.get[Option[String]]("checker", "smt-encoding").flatten.getOrElse(oopsla19Encoding) + params.smtEncoding = smtEncoding val smtProfile = options.getOrElse[Boolean]("smt", "prof", false) val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt - val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed) + val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding) options.getOrElse[String]("checker", "algo", "incremental") match { /* diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/EqRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/EqRuleWithArrays.scala new file mode 100644 index 0000000000..a1b7946cd4 --- /dev/null +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/EqRuleWithArrays.scala @@ -0,0 +1,50 @@ +package at.forsyte.apalache.tla.bmcmt.rules + +import at.forsyte.apalache.tla.bmcmt.types.{BoolT, FinSetT} +import at.forsyte.apalache.tla.bmcmt.{RewriterException, SymbState, SymbStateRewriter} +import at.forsyte.apalache.tla.lir.convenience.tla +import at.forsyte.apalache.tla.lir.UntypedPredefs._ +import at.forsyte.apalache.tla.lir.oper.TlaOper +import at.forsyte.apalache.tla.lir.{MalformedTlaError, OperEx} + +class EqRuleWithArrays(rewriter: SymbStateRewriter) extends EqRule(rewriter) { + override def apply(state: SymbState): SymbState = state.ex match { + case OperEx(TlaOper.eq, lhs, rhs) => + var newState = rewriter.rewriteUntilDone(state.setRex(lhs)) + val leftCell = newState.asCell + newState = rewriter.rewriteUntilDone(newState.setRex(rhs)) + val rightCell = newState.asCell + + if (!leftCell.cellType.comparableWith(rightCell.cellType)) { + // Cells of incomparable types cannot be equal. + // This is a dangerous state, as the type checker should have caught this. Throw an error. + // It is not really a typing error, but an internal error that should be treated as such. + val msg = + "Checking values of incomparable types for equality: %s and %s".format(leftCell.cellType, rightCell.cellType) + throw new MalformedTlaError(msg, newState.ex) + } else { + newState = newState.updateArena(_.appendCell(BoolT())) + val eqPred = newState.arena.topCell + + // TODO: add additional elements as development in the "arrays" encoding progresses + (leftCell.cellType, rightCell.cellType) match { + case (FinSetT(_), FinSetT(_)) => + // direct SMT equality of arrays is used here + val eqCons = tla.equiv(eqPred.toNameEx, tla.eql(leftCell.toNameEx, rightCell.toNameEx)) + rewriter.solverContext.assertGroundExpr(eqCons) + newState.setRex(eqPred.toNameEx) + + // Copied from EqRule. Using super.apply leads to problems, probably due to rewriter updates. + case _ => + // produce equality constraints, so that we can use SMT equality + newState = rewriter.lazyEq.cacheOneEqConstraint(newState, leftCell, rightCell) + // and now we can use the SMT equality + val eqCons = tla.equiv(eqPred.toNameEx, rewriter.lazyEq.cachedEq(leftCell, rightCell)) + rewriter.solverContext.assertGroundExpr(eqCons) + newState.setRex(eqPred.toNameEx) + } + } + case _ => + throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex) + } +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala index dddf8f55e4..ed81a5703e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala @@ -68,7 +68,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { } } - private def powSetIn(state: SymbState, powsetCell: ArenaCell, elemCell: ArenaCell): SymbState = { + protected def powSetIn(state: SymbState, powsetCell: ArenaCell, elemCell: ArenaCell): SymbState = { def checkType: PartialFunction[(CellT, CellT), Unit] = { case (PowSetT(FinSetT(expectedType)), FinSetT(actualType)) => assert(expectedType == actualType) @@ -80,7 +80,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { } // TODO: pick a function from funsetCell and check for function equality - private def funSetIn(state: SymbState, funsetCell: ArenaCell, funCell: ArenaCell): SymbState = { + protected def funSetIn(state: SymbState, funsetCell: ArenaCell, funCell: ArenaCell): SymbState = { // checking whether f \in [S -> T] def flagTypeError(): Nothing = { val msg = s"Not implemented (open an issue): f \\in S for f: %s and S: %s." @@ -123,7 +123,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { rewriter.rewriteUntilDone(nextState.setRex(pred.toNameEx)) } - private def intOrNatSetIn(state: SymbState, setCell: ArenaCell, elemCell: ArenaCell, + protected def intOrNatSetIn(state: SymbState, setCell: ArenaCell, elemCell: ArenaCell, elemType: types.CellT): SymbState = { if (setCell == state.arena.cellIntSet()) { // Do nothing, it is just true. The type checker should have taken care of that. @@ -139,7 +139,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { } } - private def basicIn(state: SymbState, setCell: ArenaCell, elemCell: ArenaCell, elemType: types.CellT) = { + protected def basicIn(state: SymbState, setCell: ArenaCell, elemCell: ArenaCell, elemType: types.CellT): SymbState = { val potentialElems = state.arena.getHas(setCell) // The types of the element and the set may slightly differ, but they must be unifiable. // For instance, [a |-> 1] \in { [a |-> 2], [a |-> 3, b -> "foo"] } @@ -161,7 +161,6 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { val elemsInAndEq = potentialElems.map(inAndEq) rewriter.solverContext.assertGroundExpr(tla.eql(pred, tla.or(elemsInAndEq: _*))) eqState.setRex(pred) - //} } } } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala new file mode 100644 index 0000000000..d09b66d786 --- /dev/null +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala @@ -0,0 +1,85 @@ +package at.forsyte.apalache.tla.bmcmt.rules + +import at.forsyte.apalache.tla.bmcmt.implicitConversions.Crossable +import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt +import at.forsyte.apalache.tla.bmcmt.types.{BoolT, CellT, FinSetT, PowSetT} +import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter, types} +import at.forsyte.apalache.tla.lir.TlaEx +import at.forsyte.apalache.tla.lir.convenience.tla +import at.forsyte.apalache.tla.lir.UntypedPredefs._ + +class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewriter) { + private val simplifier = new ConstSimplifierForSmt + + override protected def powSetIn(state: SymbState, powsetCell: ArenaCell, elemCell: ArenaCell): SymbState = { + def checkType: PartialFunction[(CellT, CellT), Unit] = { + case (PowSetT(FinSetT(expectedType)), FinSetT(actualType)) => + assert(expectedType == actualType) + } + // double check that the type finder did its job + checkType(powsetCell.cellType, elemCell.cellType) + + val setElems = state.arena.getHas(elemCell) + val powsetDomain = state.arena.getDom(powsetCell) + val powsetDomainElems = state.arena.getHas(powsetDomain) + // EqConstraints need to be generated, since missing in-relations, e.g. in sets of tuples, will lead to errors. + // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT. + var newState = rewriter.lazyEq.cacheEqConstraints(state, setElems cross powsetDomainElems) + + def isInPowset(setElem: ArenaCell): TlaEx = { + newState = newState.updateArena(_.appendCell(BoolT())) + val pred = newState.arena.topCell + + def isInAndEqSetElem(powsetDomainElem: ArenaCell) = { + // powsetDomainElem \in powsetDomain /\ powsetDomainElem = setElem + simplifier.simplifyShallow(tla.and(tla.in(powsetDomainElem.toNameEx, powsetDomain.toNameEx), + tla.eql(powsetDomainElem.toNameEx, setElem.toNameEx))) + } + + val elemsInAndEqSetElem = powsetDomainElems.map(isInAndEqSetElem) + // pred <=> (setElem \in elemCell => elemsInAndEqSetElem.1 \/ ... \/ elemsInAndEqSetElem.n) + rewriter.solverContext.assertGroundExpr(simplifier.simplifyShallow(tla.equiv(pred.toNameEx, + tla.or(tla.not(tla.in(setElem.toNameEx, elemCell.toNameEx)), tla.or(elemsInAndEqSetElem: _*))))) + pred.toNameEx + } + + val isSubset = simplifier.simplifyShallow(tla.and(setElems.map(isInPowset): _*)) + newState = newState.updateArena(_.appendCell(BoolT())) + val pred = newState.arena.topCell.toNameEx + rewriter.solverContext.assertGroundExpr(tla.eql(pred, isSubset)) + newState.setRex(pred) + } + + // TODO: update when functions are supported by SMT arrays + override protected def funSetIn(state: SymbState, funsetCell: ArenaCell, funCell: ArenaCell): SymbState = { + super.funSetIn(state, funsetCell, funCell) + } + + override protected def basicIn(state: SymbState, setCell: ArenaCell, elemCell: ArenaCell, + elemType: types.CellT): SymbState = { + val potentialElems = state.arena.getHas(setCell) + // The types of the element and the set may slightly differ, but they must be unifiable. + // For instance, [a |-> 1] \in { [a |-> 2], [a |-> 3, b -> "foo"] } + assert(elemCell.cellType.unify(elemType).nonEmpty) + if (potentialElems.isEmpty) { + // the set cell points to no other cell => return false + state.setRex(state.arena.cellFalse().toNameEx) + } else { + var nextState = state.updateArena(_.appendCell(BoolT())) + val pred = nextState.arena.topCell.toNameEx + + // EqConstraints need to be generated, since missing in-relations, e.g. in sets of tuples, will lead to errors. + // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT. + val eqState = rewriter.lazyEq.cacheEqConstraints(nextState, potentialElems.map((_, elemCell))) + + def inAndEq(elem: ArenaCell) = { + simplifier + .simplifyShallow(tla.and(tla.in(elem.toNameEx, setCell.toNameEx), tla.eql(elem.toNameEx, elemCell.toNameEx))) + } + + val elemsInAndEq = potentialElems.map(inAndEq) + rewriter.solverContext.assertGroundExpr(simplifier.simplifyShallow(tla.eql(pred, tla.or(elemsInAndEq: _*)))) + eqState.setRex(pred) + } + } +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala new file mode 100644 index 0000000000..77d96cea00 --- /dev/null +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala @@ -0,0 +1,81 @@ +package at.forsyte.apalache.tla.bmcmt.rules + +import at.forsyte.apalache.tla.bmcmt.implicitConversions.Crossable +import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt +import at.forsyte.apalache.tla.bmcmt.types.{BoolT, FinSetT, PowSetT} +import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter} +import at.forsyte.apalache.tla.lir.{OperEx, TlaEx} +import at.forsyte.apalache.tla.lir.convenience._ +import at.forsyte.apalache.tla.lir.UntypedPredefs._ +import at.forsyte.apalache.tla.lir.oper.TlaSetOper + +class SetInclusionRuleWithArrays(rewriter: SymbStateRewriter) extends SetInclusionRule(rewriter) { + private val simplifier = new ConstSimplifierForSmt + + override def apply(state: SymbState): SymbState = { + state.ex match { + case OperEx(TlaSetOper.subseteq, left, right) => + val leftState = rewriter.rewriteUntilDone(state.setRex(left)) + val leftCell = leftState.arena.findCellByNameEx(leftState.ex) + val rightState = rewriter.rewriteUntilDone(leftState.setRex(right)) + val rightCell = rightState.arena.findCellByNameEx(rightState.ex) + (leftCell.cellType, rightCell.cellType) match { + case (FinSetT(_), FinSetT(_)) => + subset(rightState, leftCell, rightCell, false) + + case (FinSetT(FinSetT(t1)), PowSetT(FinSetT(t2))) => + if (t1 != t2) { + throw new RewriterException( + "Unexpected set types: %s and %s in %s" + .format(t1, t2, state.ex), state.ex) + } else { + subset(rightState, leftCell, rightCell, true) + } + + case _ => + throw new RewriterException( + "Unexpected set types: %s and %s in %s" + .format(leftCell.cellType, rightCell.cellType, state.ex), state.ex) + } + + case _ => + throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex) + } + } + + // TODO: similar to SetInRuleWithArrays.powSetIn, potential for refactoring. + private def subset(state: SymbState, leftCell: ArenaCell, rightCell: ArenaCell, rightIsPowSet: Boolean): SymbState = { + // We check if the elements of leftCell are in rightCell, in order to establish the subset relation. + // If rightCell is a power set, we check if the elements in the sets of leftCell are in the domain of rightCell. + val leftElems = + if (rightIsPowSet) state.arena.getHas(leftCell).flatMap(state.arena.getHas) + else state.arena.getHas(leftCell) + val rightElemOrDomain = if (rightIsPowSet) state.arena.getDom(rightCell) else rightCell + val rightElemOrDomainElems = state.arena.getHas(rightElemOrDomain) + // EqConstraints need to be generated, since missing in-relations, e.g. in sets of tuples, will lead to errors. + // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT. + var newState = rewriter.lazyEq.cacheEqConstraints(state, leftElems cross rightElemOrDomainElems) + + def isInRightSet(leftElem: ArenaCell): TlaEx = { + newState = newState.updateArena(_.appendCell(BoolT())) + val pred = newState.arena.topCell + + def isInAndEqLeftElem(rightElemOrDomainElem: ArenaCell) = { + // rightElemOrDomainElem \in rightElemOrDomain /\ rightElemOrDomainElem = leftElem + simplifier.simplifyShallow(tla.and(tla.in(rightElemOrDomainElem.toNameEx, rightElemOrDomain.toNameEx), + tla.eql(rightElemOrDomainElem.toNameEx, leftElem.toNameEx))) + } + val elemsInAndEqLeftElem = rightElemOrDomainElems.map(isInAndEqLeftElem) + // pred <=> (leftElem \in leftCell => elemsInAndEqLeftElem.1 \/ ... \/ elemsInAndEqLeftElem.n) + rewriter.solverContext.assertGroundExpr(simplifier.simplifyShallow(tla.equiv(pred.toNameEx, + tla.or(tla.not(tla.in(leftElem.toNameEx, leftCell.toNameEx)), tla.or(elemsInAndEqLeftElem: _*))))) + pred.toNameEx + } + + val isSubset = simplifier.simplifyShallow(tla.and(leftElems.map(isInRightSet): _*)) + newState = newState.updateArena(_.appendCell(BoolT())) + val pred = newState.arena.topCell + rewriter.solverContext.assertGroundExpr(tla.eql(pred.toNameEx, isSubset)) + newState.setRex(pred.toNameEx) + } +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index 68c9e57a8a..d55368bc63 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala @@ -7,15 +7,16 @@ package at.forsyte.apalache.tla.bmcmt.smt * @param debug Enable the debug mode (activated with --debug). Write the log file to log%d.smt. * @param profile Enable the profile mode (activated with --profile). Report the metrics. * @param randomSeed The random seed to be passed to z3 as :random-seed. + * @param smtEncoding The SMT encoding to be used. * - * @author Igor Konnov + * @author Igor Konnov, Rodrigo Otoni */ -sealed case class SolverConfig(debug: Boolean, profile: Boolean, randomSeed: Int) {} +sealed case class SolverConfig(debug: Boolean, profile: Boolean, randomSeed: Int, smtEncoding: String) {} object SolverConfig { /** * Get the default configuration. */ - val default: SolverConfig = new SolverConfig(debug = false, profile = false, randomSeed = 0) + val default: SolverConfig = new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = "oopsla19") } 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 index d16f466c7a..16c31ff78f 100644 --- 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 @@ -7,7 +7,7 @@ import java.util.concurrent.atomic.AtomicLong import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.profiler.{IdleSmtListener, SmtListener} import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt -import at.forsyte.apalache.tla.bmcmt.types.{BoolT, CellT, IntT} +import at.forsyte.apalache.tla.bmcmt.types.{BoolT, CellT, FinSetT, IntT, PowSetT} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.io.UTFPrinter import at.forsyte.apalache.tla.lir.oper._ @@ -46,6 +46,10 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { // logWriter.println(";; %s = %s".format(p, Global.getParameter(p))) } + private def arraysEnabled(): Boolean = { + config.smtEncoding == "arrays" + } + var level: Int = 0 var nBoolConsts: Int = 0 // the solver introduces Boolean constants internally private val z3context: Context = new Context() @@ -78,8 +82,8 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { * Let's cache the constants, if Z3 cannot do it well. * Again, the cache carries the context level, to support push and pop. */ - private val cellCache: mutable.Map[Int, (ExprSort, CellT, Int)] = - new mutable.HashMap[Int, (ExprSort, CellT, Int)] + private val cellCache: mutable.Map[Int, List[(ExprSort, CellT, Int)]] = + new mutable.HashMap[Int, List[(ExprSort, CellT, Int)]] /** * A cache for the in-relation between a set and its potential element. @@ -87,6 +91,18 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { private val inCache: mutable.Map[(Int, Int), (ExprSort, Int)] = new mutable.HashMap[(Int, Int), (ExprSort, Int)] + /** + * A map flagging which in-relations were previously accessed. Used in the encoding with SMT arrays. + */ + private val inStored: mutable.Map[(Int, Int), List[(Boolean, Int)]] = + new mutable.HashMap[(Int, Int), List[(Boolean, Int)]] + + /** + * A tuple storing an array select and the condition to use it. + * Used to propagate SSA arrays in set filters when the filter predicate evaluates for false. + */ + private var propagatedArraySelect: (Boolean, ExprSort) = (false, z3context.mkFalse().asInstanceOf[ExprSort]) + /** * Sometimes, we lose a fresh arena in the rewriting rules. As this situation is very hard to debug, * we are tracking here the largest cell id per SMT context. If the user is trying to add a cell @@ -103,6 +119,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { logWriter.close() cellCache.clear() inCache.clear() + inStored.clear() funDecls.clear() cellSorts.clear() } @@ -129,9 +146,18 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { val cellSort = getOrMkCellSort(cell.cellType) log(s"(declare-const $cell $cellSort)") val cellName = cell.toString - z3context.mkConstDecl(cellName, cellSort) val const = z3context.mkConst(cellName, cellSort) - cellCache += (cell.id -> (const, cell.cellType, level)) + cellCache += (cell.id -> List((const, cell.cellType, level))) + + // If arrays are used to encode sets, they are initialized here to represent empty sets. + if (cellSort.isInstanceOf[ArraySort[Sort, BoolSort]]) { + val arrayDomain = cellSort.asInstanceOf[ArraySort[Sort, Sort]].getDomain() + val arrayInitializer = z3context.mkEq(const, z3context.mkConstArray(arrayDomain, z3context.mkFalse())) + + log(s"(assert $arrayInitializer)") + z3solver.add(arrayInitializer) + _metrics = _metrics.addNSmtExprs(1) + } if (cell.id <= 1) { // Either FALSE or TRUE. Add an explicit assert at the SMT level. @@ -146,6 +172,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { log(s"(assert $z3expr)") z3solver.add(z3expr) + _metrics = _metrics.addNSmtExprs(1) } _metrics = _metrics.addNCells(1) @@ -156,29 +183,77 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { val setT = set.cellType val name = s"in_${elemT.signature}${elem.id}_${setT.signature}${set.id}" if (!inCache.contains((set.id, elem.id))) { - smtListener.onIntroSmtConst(name) - log(s";; declare edge predicate $name: Bool") - log(s"(declare-const $name Bool)") - nBoolConsts += 1 - val const = z3context.mkConst(name, z3context.getBoolSort) - inCache += ((set.id, elem.id) -> ((const.asInstanceOf[ExprSort], level))) - - _metrics = _metrics.addNConsts(1) + if (arraysEnabled) { + val updatedSetName = set.toString + "_" + name + val setSort = getOrMkCellSort(set.cellType) + log(s";; declare edge inclusion $name") + log(s"(declare-const $updatedSetName $setSort)") + val updatedSet = z3context.mkConst(updatedSetName, setSort) + // The updated set is cached here, it needs to be added to a predicate later, via "getInPred". + // The inStored map is used to ensure that the first call to "getInPred" related to the declared inPred will + // return a "store", and the subsequent calls will return a "select". + inCache += ((set.id, elem.id) -> (updatedSet, level)) + inStored += ((set.id, elem.id) -> List((false, level))) + _metrics = _metrics.addNConsts(1) + } else { + smtListener.onIntroSmtConst(name) + log(s";; declare edge predicate $name: Bool") + log(s"(declare-const $name Bool)") + nBoolConsts += 1 + val const = z3context.mkConst(name, z3context.getBoolSort) + inCache += ((set.id, elem.id) -> ((const.asInstanceOf[ExprSort], level))) + _metrics = _metrics.addNConsts(1) + } } } private def getInPred(setId: Int, elemId: Int): ExprSort = { inCache.get((setId, elemId)) match { case None => - val setT = cellCache(setId)._2 - val elemT = cellCache(elemId)._2 + val setT = cellCache(setId).head._2 + val elemT = cellCache(elemId).head._2 val name = s"in_${elemT.signature}${elemId}_${setT.signature}$setId" logWriter.flush() // flush the SMT log throw new IllegalStateException( s"SMT $id: The Boolean constant $name (set membership) is missing from the SMT context") case Some((const, _)) => - const + if (arraysEnabled) { + val (setExpr, setT, _) = cellCache(setId).head + val (elemExpr, elemT, _) = cellCache(elemId).head + + // inPred can either represent an array update, i.e. a "store", or an array access, i.e. a "select", as the + // the current implementation is adhering to the interface made for the original encoding. + // TODO: Should we split this method and abandon the concept of an in-relation? + inStored.get(setId, elemId) match { + case None => + val name = setExpr.toString + "_" + s"in_${elemT.signature}${elemId}_${setT.signature}$setId" + logWriter.flush() // flush the SMT log + throw new IllegalStateException(s"SMT $id: The Array constant $name is missing from the SMT context") + + // Array "store" + case Some(list) if list.head._1 == false => + val storedExpr = if (propagatedArraySelect._1) propagatedArraySelect._2 else z3context.mkTrue() + propagatedArraySelect = propagatedArraySelect.copy(_1 = false) + val store = z3context.mkStore( + setExpr.asInstanceOf[Expr[ArraySort[Sort, BoolSort]]], elemExpr.asInstanceOf[Expr[Sort]], + storedExpr.asInstanceOf[Expr[BoolSort]]) + val eqStore = z3context.mkEq(const, store) + // inStored records that the array was set in the current level + inStored += ((setId, elemId) -> ((true, level) :: inStored(setId, elemId))) + // cellCache records the current SSA array representing the set being handled + cellCache += (setId -> ((const, setT, level) :: cellCache(setId))) + eqStore.asInstanceOf[ExprSort] + + // Array "select" + case Some(list) if list.head._1 == true => + z3context + .mkSelect(setExpr.asInstanceOf[ArrayExpr[Sort, BoolSort]], elemExpr.asInstanceOf[Expr[Sort]]) + .asInstanceOf[ExprSort] + } + } else { + const + } } } @@ -317,8 +392,11 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { // clean the caches cellSorts.retain((_, value) => value._2 <= level) funDecls.retain((_, value) => value._2 <= level) - cellCache.retain((_, value) => value._3 <= level) + cellCache.foreach(entry => cellCache += entry.copy(_2 = entry._2.filter(_._3 <= level))) + cellCache.retain((_, value) => value.nonEmpty) inCache.retain((_, value) => value._2 <= level) + inStored.foreach(entry => inStored += entry.copy(_2 = entry._2.filter(_._2 <= level))) + inStored.retain((_, value) => value.nonEmpty) } } @@ -332,8 +410,11 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { // clean the caches cellSorts.retain((_, value) => value._2 <= level) funDecls.retain((_, value) => value._2 <= level) - cellCache.retain((_, value) => value._3 <= level) + cellCache.foreach(entry => cellCache += entry.copy(_2 = entry._2.filter(_._3 <= level))) + cellCache.retain((_, value) => value.nonEmpty) inCache.retain((_, value) => value._2 <= level) + inStored.foreach(entry => inStored += entry.copy(_2 = entry._2.filter(_._2 <= level))) + inStored.retain((_, value) => value.nonEmpty) } } @@ -408,6 +489,12 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { case IntT() => z3context.getIntSort + case FinSetT(elemType) if arraysEnabled => + z3context.mkArraySort(getOrMkCellSort(elemType), z3context.getBoolSort) + + case PowSetT(domType) if arraysEnabled => + z3context.mkArraySort(getOrMkCellSort(domType), z3context.getBoolSort) + case _ => log(s"(declare-sort $sig 0)") z3context.mkUninterpretedSort(sig) @@ -424,7 +511,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { private def toExpr(ex: TlaEx): (ExprSort, Long) = { simplifier.simplifyShallow(ex) match { case NameEx(name) => - val nm = cellCache(ArenaCell.idFromName(name))._1 // the cached cell + val nm = cellCache(ArenaCell.idFromName(name)).head._1 // the cached cell (nm, 1) case ValEx(TlaBool(false)) => @@ -456,7 +543,8 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { case OperEx(TlaOper.eq, lhs @ NameEx(lname), rhs @ NameEx(rname)) => if (ArenaCell.isValidName(lname) && ArenaCell.isValidName(rname)) { // just comparing cells - val eq = z3context.mkEq(cellCache(ArenaCell.idFromName(lname))._1, cellCache(ArenaCell.idFromName(rname))._1) + val eq = z3context.mkEq(cellCache(ArenaCell.idFromName(lname)).head._1, + cellCache(ArenaCell.idFromName(rname)).head._1) (eq.asInstanceOf[ExprSort], 1) } else { // comparing integers and Boolean to cells, Booleans to Booleans, and Integers to Integers @@ -466,6 +554,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { (eq.asInstanceOf[ExprSort], 1 + ln + rn) } + case OperEx(TlaOper.eq, lhs @ OperEx(TlaSetOper.in, _, _), rhs) if arraysEnabled => + // Used for set filters in the arrays encoding, see addCellCons in SetFilterRule. + // Leads to constraints of the form "set_2 = (store set_1 index (and pred (select set_1 index)))" + val (re, rn) = toExpr(rhs) + propagatedArraySelect = (true, re) + val (le, ln) = toExpr(lhs) + (le.asInstanceOf[ExprSort], ln + rn) + case OperEx(TlaOper.eq, lhs, rhs) => val (le, ln) = toExpr(lhs) val (re, rn) = toExpr(rhs) @@ -506,6 +602,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { val imp = z3context.mkImplies(lhsZ3.asInstanceOf[BoolExpr], rhsZ3.asInstanceOf[BoolExpr]) (imp.asInstanceOf[ExprSort], 1 + ln + rn) + case OperEx(TlaBoolOper.equiv, lhs @ OperEx(TlaSetOper.in, _, _), rhs) if arraysEnabled => + // Used for set filters in the arrays encoding, see addCellCons in SetFilterRule. + // Leads to constraints of the form "set_2 = (store set_1 index (and pred (select set_1 index)))" + val (rhsZ3, rn) = toExpr(rhs) + propagatedArraySelect = (true, rhsZ3) + val (lhsZ3, ln) = toExpr(lhs) + (lhsZ3.asInstanceOf[ExprSort], ln + rn) + case OperEx(TlaBoolOper.equiv, lhs, rhs) => val (lhsZ3, ln) = toExpr(lhs) val (rhsZ3, rn) = toExpr(rhs) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/OfflineExecutionContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/OfflineExecutionContext.scala index 83c4f96e9d..1d18e5a529 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/OfflineExecutionContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/OfflineExecutionContext.scala @@ -1,7 +1,7 @@ package at.forsyte.apalache.tla.bmcmt.trex import at.forsyte.apalache.tla.bmcmt.smt.RecordingSolverContext -import at.forsyte.apalache.tla.bmcmt.{SymbStateRewriter, SymbStateRewriterImpl} +import at.forsyte.apalache.tla.bmcmt.{SymbStateRewriter, SymbStateRewriterImpl, SymbStateRewriterImplWithArrays} import com.typesafe.scalalogging.LazyLogging /** @@ -41,7 +41,10 @@ class OfflineExecutionContext(var rewriter: SymbStateRewriter) override def recover(snapshot: OfflineExecutionContextSnapshot): Unit = { val solver = RecordingSolverContext.createZ3(Some(snapshot.smtLog), snapshot.solverConfig) // TODO: issue #105, remove references to SolverContext, so recovery becomes less of a hack - val newRewriter = new SymbStateRewriterImpl(solver, rewriter.exprGradeStore) + val newRewriter = rewriter match { + case _: SymbStateRewriterImplWithArrays => new SymbStateRewriterImplWithArrays(solver, rewriter.exprGradeStore) + case _ => new SymbStateRewriterImpl(solver, rewriter.exprGradeStore) + } newRewriter.formulaHintsStore = rewriter.formulaHintsStore newRewriter.config = rewriter.config newRewriter.recover(snapshot.rewriterSnapshot) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/EncodingBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/EncodingBase.scala new file mode 100644 index 0000000000..d6f10c99e7 --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/EncodingBase.scala @@ -0,0 +1,6 @@ +package at.forsyte.apalache.tla.bmcmt + +object EncodingBase { + val oopsla19EncodingType = "oopsla19" + val arraysEncodingType = "arrays" +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala index f002980b9f..3ded2c940e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala @@ -2,41 +2,30 @@ package at.forsyte.apalache.tla.bmcmt import java.io.{PrintWriter, StringWriter} -import at.forsyte.apalache.tla.bmcmt.smt.{PreproSolverContext, SolverConfig, SolverContext, Z3SolverContext} +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.UntypedPredefs._ -import org.scalatest.{fixture, BeforeAndAfterEach} +import org.scalatest.fixture -trait RewriterBase extends fixture.FunSuite with BeforeAndAfterEach { +trait RewriterBase extends fixture.FunSuite { protected type FixtureParam = String - protected val oopsla19RewriterType = "oopsla19" - protected val arraysRewriterType = "arrays" - protected var solverContext: SolverContext = _ protected var arena: Arena = _ - override def beforeEach() { - solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true))) - arena = Arena.create(solverContext) - } - - override def afterEach() { - solverContext.dispose() - } - protected def create(rewriterType: String): SymbStateRewriter = { rewriterType match { - case `oopsla19RewriterType` => new SymbStateRewriterAuto(solverContext) - case `arraysRewriterType` => new SymbStateRewriterAutoWithArrays(solverContext) + case `oopsla19EncodingType` => new SymbStateRewriterAuto(solverContext) + case `arraysEncodingType` => new SymbStateRewriterAutoWithArrays(solverContext) case oddRewriterType => throw new IllegalArgumentException(s"Unexpected rewriter of type $oddRewriterType") } } protected def createWithoutCache(rewriterType: String): SymbStateRewriter = { rewriterType match { - case `oopsla19RewriterType` => new SymbStateRewriterImpl(solverContext) - case `arraysRewriterType` => new SymbStateRewriterImplWithArrays(solverContext) + case `oopsla19EncodingType` => new SymbStateRewriterImpl(solverContext) + case `arraysEncodingType` => new SymbStateRewriterImplWithArrays(solverContext) case oddRewriterType => throw new IllegalArgumentException(s"Unexpected cacheless rewriter of type $oddRewriterType") } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala index c363bf9d48..57fbe6f2e2 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArena.scala @@ -1,24 +1,15 @@ package at.forsyte.apalache.tla.bmcmt -import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} +import at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext import at.forsyte.apalache.tla.bmcmt.types.{BoolT, FinSetT, UnknownT} -import org.junit.runner.RunWith -import org.scalatest.junit.JUnitRunner -import org.scalatest.{BeforeAndAfterEach, FunSuite} +import org.scalatest.fixture -@RunWith(classOf[JUnitRunner]) -class TestArena extends FunSuite with BeforeAndAfterEach { - private var solver: Z3SolverContext = _ +trait TestArena extends fixture.FunSuite { + protected type FixtureParam = Any - override protected def beforeEach(): Unit = { - solver = new Z3SolverContext(SolverConfig.default.copy(debug = true)) - } - - override protected def afterEach(): Unit = { - solver.dispose() - } + protected var solver: Z3SolverContext = _ - test("create cells") { + test("create cells") { _ => val emptyArena = Arena.create(solver) val arena = emptyArena.appendCell(UnknownT()) assert(emptyArena.cellCount + 1 == arena.cellCount) @@ -28,7 +19,7 @@ class TestArena extends FunSuite with BeforeAndAfterEach { assert(BoolT() == arena2.topCell.cellType) } - test("add 'has' edges") { + test("add 'has' edges") { _ => val arena = Arena.create(solver).appendCell(FinSetT(UnknownT())) val set = arena.topCell val arena2 = arena.appendCell(BoolT()) @@ -37,7 +28,7 @@ class TestArena extends FunSuite with BeforeAndAfterEach { assert(List(elem) == arena3.getHas(set)) } - test("BOOLEAN has FALSE and TRUE") { + test("BOOLEAN has FALSE and TRUE") { _ => val arena = Arena.create(solver) val boolean = arena.cellBooleanSet() assert(List(arena.cellFalse(), arena.cellTrue()) == arena.getHas(arena.cellBooleanSet())) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithArrays.scala new file mode 100644 index 0000000000..d44f974b46 --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithArrays.scala @@ -0,0 +1,17 @@ +package at.forsyte.apalache.tla.bmcmt + +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} +import org.junit.runner.RunWith +import org.scalatest.Outcome +import org.scalatest.junit.JUnitRunner + +@RunWith(classOf[JUnitRunner]) +class TestArenaWithArrays extends TestArena { + override protected def withFixture(test: OneArgTest): Outcome = { + solver = new Z3SolverContext(SolverConfig.default.copy(debug = true, smtEncoding = arraysEncodingType)) + val result = test() + solver.dispose() + result + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithOOPSLA19.scala new file mode 100644 index 0000000000..7143ffbe06 --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestArenaWithOOPSLA19.scala @@ -0,0 +1,17 @@ +package at.forsyte.apalache.tla.bmcmt + +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} +import org.junit.runner.RunWith +import org.scalatest.Outcome +import org.scalatest.junit.JUnitRunner + +@RunWith(classOf[JUnitRunner]) +class TestArenaWithOOPSLA19 extends TestArena { + override protected def withFixture(test: OneArgTest): Outcome = { + solver = new Z3SolverContext(SolverConfig.default.copy(debug = true, smtEncoding = oopsla19EncodingType)) + val result = test() + solver.dispose() + result + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala index df6cd65fb9..b9aec17693 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala @@ -1,5 +1,26 @@ package at.forsyte.apalache.tla.bmcmt +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import at.forsyte.apalache.tla.bmcmt.rules.aux._ +import at.forsyte.apalache.tla.bmcmt.smt.{PreproSolverContext, SolverConfig, Z3SolverContext} +import org.junit.runner.RunWith +import org.scalatest.Outcome +import org.scalatest.junit.JUnitRunner + // TODO: Extend rewriter tests gradually as development in the "arrays" encoding progresses -class TestRewriterWithArrays {} +@RunWith(classOf[JUnitRunner]) +class TestRewriterWithArrays + extends TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle with TestSymbStateRewriter + with TestSymbStateRewriterAction with TestSymbStateRewriterBool with TestSymbStateRewriterExpand + with TestSymbStateRewriterInt with TestSymbStateRewriterPowerset with TestSymbStateRewriterSet + with TestSymbStateRewriterStr { + override protected def withFixture(test: OneArgTest): Outcome = { + solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, + smtEncoding = arraysEncodingType))) + arena = Arena.create(solverContext) + val result = test(arraysEncodingType) + solverContext.dispose() + result + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala index 473664f3c5..b73fd5dc05 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala @@ -1,6 +1,8 @@ package at.forsyte.apalache.tla.bmcmt +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ import at.forsyte.apalache.tla.bmcmt.rules.aux._ +import at.forsyte.apalache.tla.bmcmt.smt.{PreproSolverContext, SolverConfig, Z3SolverContext} import org.junit.runner.RunWith import org.scalatest.Outcome import org.scalatest.junit.JUnitRunner @@ -17,6 +19,11 @@ class TestRewriterWithOOPSLA19 with TestSymbStateRewriterTlc with TestSymbStateRewriterTuple with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle { override protected def withFixture(test: OneArgTest): Outcome = { - test(oopsla19RewriterType) + solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, + smtEncoding = oopsla19EncodingType))) + arena = Arena.create(solverContext) + val result = test(oopsla19EncodingType) + solverContext.dispose() + result } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala index 849c6a608b..6eaf9ad62e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala @@ -1,5 +1,6 @@ package at.forsyte.apalache.tla.bmcmt +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ import at.forsyte.apalache.tla.bmcmt.analyses.ExprGradeStoreImpl import at.forsyte.apalache.tla.bmcmt.smt.{RecordingSolverContext, SolverConfig} import org.junit.runner.RunWith @@ -9,7 +10,8 @@ import org.scalatest.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { - val solver = RecordingSolverContext.createZ3(None, SolverConfig(debug = false, profile = false, 0)) + val solver = RecordingSolverContext.createZ3(None, + SolverConfig(debug = false, profile = false, 0, smtEncoding = oopsla19EncodingType)) val rewriter = new SymbStateRewriterImpl(solver, new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala index 2344dbf542..2c0270096c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterBool.scala @@ -5,9 +5,8 @@ import at.forsyte.apalache.tla.bmcmt.types.{BoolT, FinSetT, IntT} import at.forsyte.apalache.tla.lir.TypedPredefs._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.tla -import org.scalatest.BeforeAndAfterEach -trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with BeforeAndAfterEach { +trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs { // these are handy variables that will be overwritten by before private var x: ArenaCell = new ArenaCell(100000, IntT()) private var y: ArenaCell = new ArenaCell(100001, IntT()) @@ -15,9 +14,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be private var xyBinding = Binding() private val boolTypes = Map("b" -> BoolT1(), "i" -> IntT1(), "I" -> SetT1(IntT1())) - override def beforeEach() { - super.beforeEach() - + def prepareArena() { arena = arena.appendCell(BoolT()) // we have to give bindings to the type finder x = arena.topCell arena = arena.appendCell(BoolT()) // we have to give bindings to the type finder @@ -28,6 +25,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("FALSE ~~> $C$0") { rewriterType: String => + prepareArena() val ex = tla.bool(false).typed() val state = new SymbState(ex, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -42,6 +40,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("TRUE ~~> $C$1") { rewriterType: String => + prepareArena() val ex = tla.bool(true).typed() val state = new SymbState(ex, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -56,6 +55,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("BOOLEAN ~~> c_BOOLEAN") { rewriterType: String => + prepareArena() val boolset = tla.booleanSet().typed(SetT1(BoolT1())) val state = new SymbState(boolset, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -71,6 +71,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be test("x => y ~~> ~x \\/ y") { rewriterType: String => // outside of KerA+, should be handled by Keramelizer and Normalizer + prepareArena() val ex = tla .impl(tla.name("x") ? "b", tla.name("y") ? "b") .typed(boolTypes, "b") @@ -93,6 +94,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be test("""IF-THEN-ELSE with \E: IF \E i \in {}: x' \in {i} THEN x' ELSE 0""") { rewriterType: String => // this tricky test comes from Bakery, where an assignment is made in one branch of a conjunction + prepareArena() val exists = tla .apalacheSkolem(tla.exists(tla.name("i") ? "i", tla.enumSet() ? "I", @@ -111,6 +113,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""~c_i ~~> b_new""") { rewriterType: String => + prepareArena() arena = arena.appendCell(BoolT()) val cell = arena.topCell @@ -142,6 +145,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""~x ~~> TRUE""") { rewriterType: String => + prepareArena() val ex = tla .not(tla.name("x") ? "b") .typed(boolTypes, "b") @@ -153,6 +157,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""FALSE = TRUE ~~> FALSE""") { rewriterType: String => + prepareArena() val ex = tla .eql(arena.cellFalse().toNameEx ? "b", arena.cellTrue().toNameEx ? "b") .typed(boolTypes, "b") @@ -166,6 +171,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""x = TRUE ~~> FALSE when x = FALSE""") { rewriterType: String => + prepareArena() val ex = tla .eql(tla.name("x") ? "b", tla.bool(true) ? "b") .typed(boolTypes, "b") @@ -178,6 +184,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""~(x = TRUE) ~~> TRUE when x = FALSE""") { rewriterType: String => + prepareArena() val ex = tla .not(tla.eql(tla.name("x") ? "b", tla.bool(true)) ? "b") .typed(boolTypes, "b") @@ -192,6 +199,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""FALSE /\ TRUE ~~> $B$0""") { rewriterType: String => + prepareArena() val ex = tla .and(tla.bool(false), tla.bool(true)) .typed(BoolT1()) @@ -207,6 +215,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""c_1 /\ c_2 ~~> b_new""") { rewriterType: String => + prepareArena() arena = arena.appendCell(BoolT()) val c1 = arena.topCell arena = arena.appendCell(BoolT()) @@ -251,6 +260,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""empty \/ ~~> $B$0""") { rewriterType: String => + prepareArena() val ex = tla.or().typed(BoolT1()) val state = new SymbState(ex, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -264,6 +274,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""empty /\ ~~> $B$1""") { rewriterType: String => + prepareArena() val ex = tla.and().typed(BoolT1()) val state = new SymbState(ex, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -277,6 +288,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""FALSE \/ TRUE ~~> $B$1""") { rewriterType: String => + prepareArena() val ex = tla.or(tla.bool(false), tla.bool(true)).typed(BoolT1()) val state = new SymbState(ex, arena, Binding()) create(rewriterType).rewriteOnce(state) match { @@ -290,6 +302,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""c_1 \/ c_2 ~~> b_new""") { rewriterType: String => + prepareArena() arena = arena.appendCell(BoolT()) val left = arena.topCell arena = arena.appendCell(BoolT()) @@ -327,6 +340,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""~($B$1 = $B$2) ~~> $B$3""") { rewriterType: String => + prepareArena() arena = arena.appendCell(BoolT()) val left = arena.topCell arena = arena.appendCell(BoolT()) @@ -387,6 +401,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\E x \in {}: TRUE ~~> FALSE""") { rewriterType: String => + prepareArena() val ex = tla .exists(tla.name("x") ? "i", tla.enumSet() ? "I", tla.bool(true)) .typed(boolTypes, "b") @@ -396,6 +411,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\E x \in {1, 2, 3}: x = 2 ~~> $B$k""") { rewriterType: String => + prepareArena() val set123 = tla.enumSet(tla.int(1), tla.int(2), tla.int(3)).typed(SetT1(IntT1())) val ex = tla @@ -415,6 +431,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be /** Jure, 9.12.19: Why should this throw? */ test("""\E x \in {1, 2}: y' := x ~~> 2 assignments, regression""") { rewriterType: String => + prepareArena() val set12 = tla .enumSet(tla.int(1), tla.int(2)) .typed(SetT1(IntT1())) @@ -461,6 +478,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\E x \in {1, 2, 3}: x > 4 ~~> $B$k""") { rewriterType: String => + prepareArena() val set123 = tla.enumSet(tla.int(1), tla.int(2), tla.int(3)).typed(SetT1(IntT1())) val ex = tla @@ -479,6 +497,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\E x \in {t \in {1}: FALSE}: x > 4, regression""") { rewriterType: String => + prepareArena() def dynEmpty(left: TlaEx): TlaEx = { tla .filter(tla.name("t") ? "i", left ? "I", tla.bool(false)) @@ -501,6 +520,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""skolem: \E i \in Nat: i = 10 /\ x' \in {i}""") { rewriterType: String => + prepareArena() // this works for skolem constants only val ex = tla @@ -525,6 +545,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be test("""skolemization over range: \E i \in a..b: i % 3 = 1 /\ x' \in {i}""") { rewriterType: String => // this works for skolem constants only + prepareArena() val ex = tla .apalacheSkolem( @@ -559,6 +580,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\A x \in {1, 2, 3}: x < 10 ~~> $B$k""") { rewriterType: String => + prepareArena() val set123 = tla.enumSet(tla.int(1), tla.int(2), tla.int(3)).typed(SetT1(IntT1())) val ex = tla @@ -577,6 +599,7 @@ trait TestSymbStateRewriterBool extends RewriterBase with TestingPredefs with Be } test("""\A x \in {1, 2, 3}: x > 2 ~~> $B$k""") { rewriterType: String => + prepareArena() val set123 = tla.enumSet(tla.int(1), tla.int(2), tla.int(3)).typed(SetT1(IntT1())) val ex = tla diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala index f779887fd7..90e18b6470 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala @@ -794,7 +794,8 @@ trait TestSymbStateRewriterSet extends RewriterBase { apalacheSkolem(exists(name("S") as recSetT, powerset, and(mem, forallForm) as boolT) as boolT) as boolT // reset the solver and arena - solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true))) + solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, + smtEncoding = rewriterType))) arena = Arena.create(solverContext) val rewriter2 = create(rewriterType) val state2 = new SymbState(existsForm2, arena, Binding()) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala index 8108d7871a..5803cb5d5c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala @@ -2,21 +2,20 @@ package at.forsyte.apalache.tla.bmcmt.smt import at.forsyte.apalache.tla.bmcmt.Arena import at.forsyte.apalache.tla.bmcmt.types.IntT -import at.forsyte.apalache.tla.lir.{BuilderVal, TlaEx} +import at.forsyte.apalache.tla.lir.TlaEx import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.UntypedPredefs._ -import org.junit.runner.RunWith -import org.scalatest.FunSuite -import org.scalatest.junit.JUnitRunner +import org.scalatest.fixture -@RunWith(classOf[JUnitRunner]) -class TestRecordingSolverContext extends FunSuite { - private val defaultSolverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0) +trait TestRecordingSolverContext extends fixture.FunSuite { + protected type FixtureParam = Any + + protected var solverConfig: SolverConfig = _ private val int42: TlaEx = tla.int(42) - test("operations proxied") { - val solver = RecordingSolverContext.createZ3(None, defaultSolverConfig) + test("operations proxied") { _ => + val solver = RecordingSolverContext.createZ3(None, solverConfig) var arena = Arena.create(solver).appendCell(IntT()) val x = arena.topCell solver.assertGroundExpr(tla.eql(x.toNameEx, int42)) @@ -24,8 +23,8 @@ class TestRecordingSolverContext extends FunSuite { assert(solver.evalGroundExpr(x.toNameEx) == int42) } - test("write and read") { - val solver = RecordingSolverContext.createZ3(None, defaultSolverConfig) + test("write and read") { _ => + val solver = RecordingSolverContext.createZ3(None, solverConfig) var arena = Arena.create(solver).appendCell(IntT()) val x = arena.topCell solver.assertGroundExpr(tla.eql(x.toNameEx, int42)) @@ -37,14 +36,14 @@ class TestRecordingSolverContext extends FunSuite { solver.assertGroundExpr(tla.gt(x.toNameEx, tla.int(1000))) assert(!solver.sat()) // restore the context - val restoredSolver = RecordingSolverContext.createZ3(Some(log), defaultSolverConfig) + val restoredSolver = RecordingSolverContext.createZ3(Some(log), solverConfig) // the restored context should be satisfiable assert(restoredSolver.sat()) assert(restoredSolver.evalGroundExpr(x.toNameEx) == int42) } - test("pop on empty") { - val solver = RecordingSolverContext.createZ3(None, defaultSolverConfig) + test("pop on empty") { _ => + val solver = RecordingSolverContext.createZ3(None, solverConfig) assertThrows[IllegalArgumentException](solver.pop(2)) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala new file mode 100644 index 0000000000..7441d7397d --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala @@ -0,0 +1,14 @@ +package at.forsyte.apalache.tla.bmcmt.smt + +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import org.junit.runner.RunWith +import org.scalatest.Outcome +import org.scalatest.junit.JUnitRunner + +@RunWith(classOf[JUnitRunner]) +class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext { + override protected def withFixture(test: OneArgTest): Outcome = { + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = arraysEncodingType) + test() + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala new file mode 100644 index 0000000000..0c80041864 --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala @@ -0,0 +1,14 @@ +package at.forsyte.apalache.tla.bmcmt.smt + +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ +import org.junit.runner.RunWith +import org.scalatest.Outcome +import org.scalatest.junit.JUnitRunner + +@RunWith(classOf[JUnitRunner]) +class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext { + override protected def withFixture(test: OneArgTest): Outcome = { + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = oopsla19EncodingType) + test() + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala index db32e855cd..fd364f3d1a 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala @@ -1,5 +1,6 @@ package at.forsyte.apalache.tla.bmcmt.trex +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ import at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl import at.forsyte.apalache.tla.bmcmt.analyses._ import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} @@ -17,7 +18,8 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19 extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot] with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { - val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0)) + val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, + smtEncoding = oopsla19EncodingType)) val rewriter = new SymbStateRewriterImpl(solver, new ExprGradeStoreImpl()) val exeCtx = new IncrementalExecutionContext(rewriter) try { diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala index 5a8b53616e..d9fedc0476 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala @@ -1,5 +1,6 @@ package at.forsyte.apalache.tla.bmcmt.trex +import at.forsyte.apalache.tla.bmcmt.EncodingBase._ import at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl import at.forsyte.apalache.tla.bmcmt.analyses._ import at.forsyte.apalache.tla.bmcmt.smt.{RecordingSolverContext, SolverConfig} @@ -15,7 +16,8 @@ import org.scalatest.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { - val solver = RecordingSolverContext.createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0)) + val solver = RecordingSolverContext.createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = oopsla19EncodingType)) val rewriter = new SymbStateRewriterImpl(solver, new ExprGradeStoreImpl()) val exeCtx = new OfflineExecutionContext(rewriter) try {