Skip to content

Simplification property tests: separate Predicate and TermLike generators #2804

@ana-pantilie

Description

@ana-pantilie

Context for this issue: we made the decision that the TermLike simplifier should not call the Predicate simplifier (see #2770). This requires that any TermLike pattern should not contain children patterns which are Predicates. In the future, we would like to fully disentangle the representation of Predicates from TermLikes (see #2640).

Right now, our unit tests we rely on a TermLike generator to generate any type of Kore pattern. This has also lead to sporadic failures of our property tests, as it generates patterns which are too general. We need to implement a separate Predicate generator, and disallow any predicate pattern generation in the TermLike one.

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions