2

I have a problem that I want to formulate using Z3. However, I not sure what is the best way to do that. Here is a description of what I want to encode and the anticipated output.

If I have a language grammar where x, y and z are non-terminals and "and", "or" and "a" are the language terminals:

  1. x ::= y "or" y 

       | y

  2. y ::= z "and" z 

      | z
  3. z ::= "a"

I want first to encode the previous rules and then I want to generate All possible terminal derivations that are accepted by the grammar.

The ultimate output would be :

a and a or a and a

a or a

a and a

a and a or a

a or a and a

...

I do not know where to start. What is the best way to encode the problem?

Any suggestion/guidance is very appreciated..

Thanks

user3126757
  • 33
  • 3

1 Answers1

1

The canonical way of using Z3 to generate all possible solutions to a constraint system is to iteratively "forbid" the previously found solution by adding it as a new (negative) constraint. See Leo's answer to this question.

Community
  • 1
  • 1
Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71