Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 82
    • Issues 82
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 11
    • Merge requests 11
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !231

Many improvements to `multiset_solver`

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/multiset_solver into master Mar 10, 2021
  • Overview 21
  • Commits 11
  • Pipelines 0
  • Changes 2
  1. Support ∈
  2. Support ⊂
  3. Support case splitting on multiplicity x {[ y ]}, but only do this when there's no other way.

With the improved multiset_solver I am able to solve pretty much all lemmas in the gmultiset file automatically (apart from those that involve elements, size, and other connectives that are out of scope).

The new version also handles @fpottier's test case x ∈ X → {[x]} ⊆ X from #86 (closed).

In addition, I added a bunch of other test cases.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/multiset_solver