Add support for sets to the arrays encoding #1093

rodrigo7491 · 2021-11-12T16:29:06Z

Tests added for any new code
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entry added to UNRELEASED.md for any new functionality

This PR contains the initial version of the arrays encoding. It adds support for basic types, which are unchanged from the original encoding, as well as sets. A number of encoding rules was changed, either explicitly, through new RewritingRule classes, or implicitly, through changes to Z3SolverContext that make the SMT constraints produced be different from those of the original rules. A number of existing unit and integration tests are now running with the arrays encoding. Below is an overview of the changes. Closes #1092.

SolverConfig. A new field was added to the solver configuration, to record the encoding being used. This field is set based on the check command options.
SolverContext. The core of the changes is in Z3SolverContext, as this is where the SMT constraints are made. See the updated ADR for details.
SymbStateRewriter. Three new explicit rules were added to ruleLookupTable in SymbStateRewriterImplWithArrays: EqRuleWithArrays, SetInRuleWithArrays, and SetInclusionRuleWithArrays.
Unit tests. The unit tests were refactored to account for the two possible encodings in the solver configuration. The most relevant refactoring change was in RewriterBase. To see which unit tests were enabled to run with the arrays encoding, check TestArenaWithArrays, TestRewriterWithArrays, and TestRecordingSolverContextWithArrays.
Integration tests. Some tests were enabled to run with the arrays encoding, by tagging them with array-encoding in cli-integration-tests. The CI setup to run the tagged tests is not part of this PR.
Documentation. ADR11 was updated to reflect the implementation changes made. Its high level description was not changed.

…into ro/tla-sets-as-smt-arrays

…into ro/tla-sets-as-smt-arrays � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

…into ro/tla-sets-as-smt-arrays

… and wrong ssa treatment during incremental solving

…into ro/tla-sets-as-smt-arrays

…into ro/tla-sets-as-smt-arrays � Conflicts: � UNRELEASED.md

konnov

The first batch of comments. I will continue today.

docs/src/adr/011adr-smt-arrays.md

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterAutoWithArrays.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/EqRuleWithArrays.scala

konnov · 2021-11-17T11:05:22Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala

+    val rightDomain = state.arena.getDom(powsetCell)
+    val rightDomainElems = state.arena.getHas(rightDomain)
+    // 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.


Good point. We should figure out how to deal with records that can be used as discriminated unions. Perhaps, ADTs should help us.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala

Co-authored-by: Igor Konnov <igor@informal.systems>

konnov

More comments. More yet to come :)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

…verConfig.scala Co-authored-by: Igor Konnov <igor@informal.systems>

Kukovec

Most comments are minor, but I think the lookup table one is pretty important.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImplWithArrays.scala

Kukovec · 2021-11-17T15:55:39Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala

+          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 _ =>


Technically, the case PowSetT(FinSetT(t1)), FinSetT(FinSetT(t1) should be possible too, no? Suboptimal, but not illegal.

This is equal to the original SetInclusionRule rule. I didn't think much about it since an exception is already thrown there. If we make a change it should be in both encodings I think. Maybe in a separate PR?

@konnov thoughts?

There is case _ => that throws an exception below. So it will be reported as an error. Perhaps, we should throw a better exception there that indicates that this case is not supported.

Yeah, but shouldn't

A == {1,2} B == SUBSET A \subseteq { x \in SUBSET A: \A y \in x: y < 5 } \* <=> SUBSET A \subseteq SUBSET A <=> TRUE

translate into exactly the case where the LHS is a PowSetT and the RHS is a standard FinSetT because of the filter?
You can't throw on this example.

I am not sure. You can try this example and see what happens. Maybe the left-hand side will get expanded. If it does not, we should fix ExpansionMarker to do that.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/EncodingBase.scala

konnov

This looks very good. See the other comments. As far as I understand, this PR contains the rules for set equality, set membership, and subseteq. Are other set operators planned for a separate PR?

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala

konnov · 2021-11-17T15:55:43Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

+        // 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)))


This looks like an error-prone approach. What happens if a rewriting rule does not use inPred at all and then store is used in a random place somewhere? An alternative would be to explicitly introduce two operators in ApalacheOper: store and select. These would be auxiliary operators that only appear in the internals of Apalache.

The point about using the cache wrongly could be made about any of the caches in the solver context. inStored is currently used only in declareInPredIfNeeded and getInPred.

I like the idea of adding store and select, I haven't though of adding new ApalacheOper before.

konnov · 2021-11-17T15:56:39Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala

+          // 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?


Yes, I would prefer having store and select as operators in the Apalache IR, as it seems you need them.

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala

rodrigo7491 · 2021-11-17T16:44:52Z

This looks very good. See the other comments. As far as I understand, this PR contains the rules for set equality, set membership, and subseteq. Are other set operators planned for a separate PR?

The PR contains rules for all set operators in the map, excluding the ones flagged at the bottom. Most rules, like set ctr, set union, etc., were added implicitly by changing the constraints they generated, as mentioned in the top comment.

konnov · 2021-11-17T19:59:27Z

This looks very good. See the other comments. As far as I understand, this PR contains the rules for set equality, set membership, and subseteq. Are other set operators planned for a separate PR?

The PR contains rules for all set operators in the map, excluding the ones flagged at the bottom. Most rules, like set ctr, set union, etc., were added implicitly by changing the constraints they generated, as mentioned in the top comment.

So it means they did not require any change?

rodrigo7491 · 2021-11-18T07:27:01Z

So it means they did not require any change?

The RewritingRule classes themselves no, but the "conceptual" rules did change, since they now generate different smt constraints and thus lead to a different 4-tuple state, as described in the paper.

konnov · 2021-11-18T07:54:30Z

So it means they did not require any change?

The RewritingRule classes themselves no, but the "conceptual" rules did change, since they now generate different smt constraints and thus lead to a different 4-tuple state, as described in the paper.

That's interesting. If we introduce store and select, you would have to rewrite those rules too, right?

rodrigo7491 · 2021-11-18T08:44:31Z

That's interesting. If we introduce store and select, you would have to rewrite those rules too, right?

Probably. It depends on how store and select end up being implemented. Since this is quite a fundamental change, should I do this here or in a follow up PR?

konnov · 2021-11-18T12:50:38Z

That's interesting. If we introduce store and select, you would have to rewrite those rules too, right?

Probably. It depends on how store and select end up being implemented. Since this is quite a fundamental change, should I do this here or in a follow up PR?

Yes, I think we can postpone it for another PR. This one is not going to break anything.

rodrigo7491 added 30 commits October 27, 2021 17:01

Add arrays encoding config to solver context

5208883

Add array initialization upon const declaration

0e19a0f

Add array encoding option to OfflineExecutionContext

163758a

refactor bmcmt unit tests to account for encoding solver config

8606e4d

Add array updates via smt store

dfd8070

Add metrics update to cells 0 and 1

88c03b8

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

ad1d4c3

…into ro/tla-sets-as-smt-arrays

update arrays version of SymbStateRewriterAuto

4807397

first iteration of arrays encoding rule table

16cec0a

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

1f29cc2

…into ro/tla-sets-as-smt-arrays

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

a7aeed4

…into ro/tla-sets-as-smt-arrays

Add set equality using SMT equality

d97f428

make inCache store "select" expressions

83faa8a

Add set membership rule with smt arrays

d68bb01

remove redundant "select" equalities

b32db1e

Add set inclusion rule with arrays

7efcec4

fix set membership predicate generation

6f568bb

Add support for power sets in the arrays encoding

9c84447

fix subset relation with power sets

508124d

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

d2e7ee0

…into ro/tla-sets-as-smt-arrays � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

add integer range with SMT arrays

cbd7898

add set map with SMT arrays

e00d243

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

a6e86d1

…into ro/tla-sets-as-smt-arrays

fix bug in set membership with smt arrays

0ae3471

fix bug in set inclusion with smt arrays

89a78e0

fix issues in the arrays encoding w.r.t. edges being asserted wrongly…

6f44287

… and wrong ssa treatment during incremental solving

add set filter with smt arrays

59826d2

add big union with smt arrays

59cfa4d

fix issue with equality of empty sets with smt arrays

1589b59

fix issue with equality delegation

7527ec9

rodrigo7491 added 3 commits November 12, 2021 16:34

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

eebfa25

…into ro/tla-sets-as-smt-arrays

update UNRELEASED.md

9864996

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

0f6b8b6

…into ro/tla-sets-as-smt-arrays � Conflicts: � UNRELEASED.md

konnov requested review from konnov and Kukovec November 15, 2021 13:18

konnov reviewed Nov 17, 2021

View reviewed changes

rodrigo7491 and others added 3 commits November 17, 2021 13:18

Update docs/src/adr/011adr-smt-arrays.md

ca863ec

Co-authored-by: Igor Konnov <igor@informal.systems>

Merge branch 'unstable' into ro/tla-sets-as-smt-arrays

7bd5c3b

minor refactoring

762ab51

konnov reviewed Nov 17, 2021

View reviewed changes

rodrigo7491 and others added 2 commits November 17, 2021 15:27

minor refactoring

177b4f5

Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Sol…

ae5c74c

…verConfig.scala Co-authored-by: Igor Konnov <igor@informal.systems>

Kukovec requested changes Nov 17, 2021

View reviewed changes

konnov reviewed Nov 17, 2021

View reviewed changes

rodrigo7491 added 4 commits November 18, 2021 10:28

change conjunction to implication in membership constraints

2301528

add comments to set membership constraints

e4fb1a3

change EncodingBase from trait to object

ed582dd

rename useArrays to arraysEnabled

08116e8

refactor ruleLookupTable

2879cbb

Kukovec approved these changes Nov 18, 2021

View reviewed changes

rodrigo7491 merged commit 3537de7 into unstable Nov 18, 2021

rodrigo7491 deleted the ro/tla-sets-as-smt-arrays branch November 18, 2021 16:29

rodrigo7491 mentioned this pull request Nov 19, 2021

[FEATURE] Add Apalache IR operators for SMT select and store #1106

Closed

rodrigo7491 mentioned this pull request Dec 7, 2021

[FEATURE] Refactor SMT encoding option flag use #1159

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for sets to the arrays encoding #1093

Add support for sets to the arrays encoding #1093

rodrigo7491 commented Nov 12, 2021 •

edited

Loading

konnov left a comment

konnov Nov 17, 2021

konnov left a comment

Kukovec left a comment

Kukovec Nov 17, 2021

rodrigo7491 Nov 17, 2021

Kukovec Nov 17, 2021

konnov Nov 17, 2021

Kukovec Nov 17, 2021 •

edited

Loading

konnov Nov 17, 2021

Kukovec Nov 18, 2021

konnov left a comment

konnov Nov 17, 2021

rodrigo7491 Nov 17, 2021

konnov Nov 17, 2021

rodrigo7491 commented Nov 17, 2021

konnov commented Nov 17, 2021

rodrigo7491 commented Nov 18, 2021

konnov commented Nov 18, 2021

rodrigo7491 commented Nov 18, 2021

konnov commented Nov 18, 2021

Add support for sets to the arrays encoding #1093

Add support for sets to the arrays encoding #1093

Conversation

rodrigo7491 commented Nov 12, 2021 • edited Loading

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov left a comment

Choose a reason for hiding this comment

Kukovec left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Kukovec Nov 17, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rodrigo7491 commented Nov 17, 2021

konnov commented Nov 17, 2021

rodrigo7491 commented Nov 18, 2021

konnov commented Nov 18, 2021

rodrigo7491 commented Nov 18, 2021

konnov commented Nov 18, 2021

rodrigo7491 commented Nov 12, 2021 •

edited

Loading

Kukovec Nov 17, 2021 •

edited

Loading