Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for sets to the arrays encoding #1093

Merged
merged 54 commits into from
Nov 18, 2021
Merged

Add support for sets to the arrays encoding #1093

merged 54 commits into from
Nov 18, 2021

Commits on Oct 27, 2021

  1. Add arrays encoding config to solver context

    @rodrigo7491
    rodrigo7491 committed Oct 27, 2021
    Configuration menu
    Copy the full SHA
    5208883 View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2021

  1. Add array initialization upon const declaration

    @rodrigo7491
    rodrigo7491 committed Oct 28, 2021
    Configuration menu
    Copy the full SHA
    0e19a0f View commit details
    Browse the repository at this point in the history

  2. Add array encoding option to OfflineExecutionContext

    @rodrigo7491
    rodrigo7491 committed Oct 28, 2021
    Configuration menu
    Copy the full SHA
    163758a View commit details
    Browse the repository at this point in the history

  3. refactor bmcmt unit tests to account for encoding solver config

    @rodrigo7491
    rodrigo7491 committed Oct 28, 2021
    Configuration menu
    Copy the full SHA
    8606e4d View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2021

  1. Add array updates via smt store

    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    dfd8070 View commit details
    Browse the repository at this point in the history

  2. Add metrics update to cells 0 and 1

    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    88c03b8 View commit details
    Browse the repository at this point in the history

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    ad1d4c3 View commit details
    Browse the repository at this point in the history

  4. update arrays version of SymbStateRewriterAuto

    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    4807397 View commit details
    Browse the repository at this point in the history

  5. first iteration of arrays encoding rule table

    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    16cec0a View commit details
    Browse the repository at this point in the history

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Oct 29, 2021
    Configuration menu
    Copy the full SHA
    1f29cc2 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2021

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    a7aeed4 View commit details
    Browse the repository at this point in the history

  2. Add set equality using SMT equality

    @rodrigo7491
    rodrigo7491 committed Nov 1, 2021
    Configuration menu
    Copy the full SHA
    d97f428 View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2021

  1. make inCache store "select" expressions

    @rodrigo7491
    rodrigo7491 committed Nov 2, 2021
    Configuration menu
    Copy the full SHA
    83faa8a View commit details
    Browse the repository at this point in the history

  2. Add set membership rule with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 2, 2021
    Configuration menu
    Copy the full SHA
    d68bb01 View commit details
    Browse the repository at this point in the history

  3. remove redundant "select" equalities

    @rodrigo7491
    rodrigo7491 committed Nov 2, 2021
    Configuration menu
    Copy the full SHA
    b32db1e View commit details
    Browse the repository at this point in the history

  4. Add set inclusion rule with arrays

    @rodrigo7491
    rodrigo7491 committed Nov 2, 2021
    Configuration menu
    Copy the full SHA
    7efcec4 View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2021

  1. fix set membership predicate generation

    @rodrigo7491
    rodrigo7491 committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    6f568bb View commit details
    Browse the repository at this point in the history

  2. Add support for power sets in the arrays encoding

    @rodrigo7491
    rodrigo7491 committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    9c84447 View commit details
    Browse the repository at this point in the history

  3. fix subset relation with power sets

    @rodrigo7491
    rodrigo7491 committed Nov 3, 2021
    Configuration menu
    Copy the full SHA
    508124d View commit details
    Browse the repository at this point in the history

Commits on Nov 4, 2021

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

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

� Conflicts:
�	tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala
    @rodrigo7491
    rodrigo7491 committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    d2e7ee0 View commit details
    Browse the repository at this point in the history

  2. add integer range with SMT arrays

    @rodrigo7491
    rodrigo7491 committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    cbd7898 View commit details
    Browse the repository at this point in the history

Commits on Nov 9, 2021

  1. add set map with SMT arrays

    @rodrigo7491
    rodrigo7491 committed Nov 9, 2021
    Configuration menu
    Copy the full SHA
    e00d243 View commit details
    Browse the repository at this point in the history

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Nov 9, 2021
    Configuration menu
    Copy the full SHA
    a6e86d1 View commit details
    Browse the repository at this point in the history

  3. fix bug in set membership with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 9, 2021
    Configuration menu
    Copy the full SHA
    0ae3471 View commit details
    Browse the repository at this point in the history

  4. fix bug in set inclusion with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 9, 2021
    Configuration menu
    Copy the full SHA
    89a78e0 View commit details
    Browse the repository at this point in the history

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

    … and wrong ssa treatment during incremental solving
    @rodrigo7491
    rodrigo7491 committed Nov 9, 2021
    Configuration menu
    Copy the full SHA
    6f44287 View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2021

  1. add set filter with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    59826d2 View commit details
    Browse the repository at this point in the history

  2. add big union with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    59cfa4d View commit details
    Browse the repository at this point in the history

  3. fix issue with equality of empty sets with smt arrays

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    1589b59 View commit details
    Browse the repository at this point in the history

  4. fix issue with equality delegation

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    7527ec9 View commit details
    Browse the repository at this point in the history

  5. add stub rules for unit tests

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    7e5bae7 View commit details
    Browse the repository at this point in the history

  6. update context pop

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    da3193b View commit details
    Browse the repository at this point in the history

  7. add tuple comparisons in set membership rule

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    4d1c6b7 View commit details
    Browse the repository at this point in the history

  8. add unit tests for arrays encoding

    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    8cf4c66 View commit details
    Browse the repository at this point in the history

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Nov 10, 2021
    Configuration menu
    Copy the full SHA
    d263c31 View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2021

  1. fix powerset membership with arrays

    @rodrigo7491
    rodrigo7491 committed Nov 11, 2021
    Configuration menu
    Copy the full SHA
    883e294 View commit details
    Browse the repository at this point in the history

  2. add unit tests for powersets using arrays encoding

    @rodrigo7491
    rodrigo7491 committed Nov 11, 2021
    Configuration menu
    Copy the full SHA
    80d9fec View commit details
    Browse the repository at this point in the history

  3. add additional unit tests for arrays encoding

    @rodrigo7491
    rodrigo7491 committed Nov 11, 2021
    Configuration menu
    Copy the full SHA
    8228b22 View commit details
    Browse the repository at this point in the history

Commits on Nov 12, 2021

  1. add integration tests for arrays encoding

    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    79657d3 View commit details
    Browse the repository at this point in the history

  2. polish code and comments

    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    968439b View commit details
    Browse the repository at this point in the history

  3. update adr11

    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    26d5dd0 View commit details
    Browse the repository at this point in the history

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

    …into ro/tla-sets-as-smt-arrays
    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    eebfa25 View commit details
    Browse the repository at this point in the history

  5. update UNRELEASED.md

    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    9864996 View commit details
    Browse the repository at this point in the history

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

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

� Conflicts:
�	UNRELEASED.md
    @rodrigo7491
    rodrigo7491 committed Nov 12, 2021
    Configuration menu
    Copy the full SHA
    0f6b8b6 View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2021

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

    Co-authored-by: Igor Konnov <igor@informal.systems>
    @rodrigo7491 @konnov
    rodrigo7491 and konnov authored Nov 17, 2021
    Configuration menu
    Copy the full SHA
    ca863ec View commit details
    Browse the repository at this point in the history

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

    @rodrigo7491
    rodrigo7491 authored Nov 17, 2021
    Configuration menu
    Copy the full SHA
    7bd5c3b View commit details
    Browse the repository at this point in the history

  3. minor refactoring

    @rodrigo7491
    rodrigo7491 committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    762ab51 View commit details
    Browse the repository at this point in the history

  4. minor refactoring

    @rodrigo7491
    rodrigo7491 committed Nov 17, 2021
    Configuration menu
    Copy the full SHA
    177b4f5 View commit details
    Browse the repository at this point in the history

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

    …verConfig.scala

Co-authored-by: Igor Konnov <igor@informal.systems>
    @rodrigo7491 @konnov
    rodrigo7491 and konnov authored Nov 17, 2021
    Configuration menu
    Copy the full SHA
    ae5c74c View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2021

  1. change conjunction to implication in membership constraints

    @rodrigo7491
    rodrigo7491 committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    2301528 View commit details
    Browse the repository at this point in the history

  2. add comments to set membership constraints

    @rodrigo7491
    rodrigo7491 committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    e4fb1a3 View commit details
    Browse the repository at this point in the history

  3. change EncodingBase from trait to object

    @rodrigo7491
    rodrigo7491 committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    ed582dd View commit details
    Browse the repository at this point in the history

  4. rename useArrays to arraysEnabled

    @rodrigo7491
    rodrigo7491 committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    08116e8 View commit details
    Browse the repository at this point in the history

  5. refactor ruleLookupTable

    @rodrigo7491
    rodrigo7491 committed Nov 18, 2021
    Configuration menu
    Copy the full SHA
    2879cbb View commit details
    Browse the repository at this point in the history