__init__.py 521 Bytes
Newer Older
1
from abc import ABCMeta, abstractmethod
2

3
4
import z3

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
5
def dt_enum(name, elements):
6
7
8
9
10
    d = z3.Datatype(name)
    for element in elements:
        d.declare(element)
    d = d.create()
    return d, [d.__getattribute__(element) for element in elements]
11

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
12
13
14
15
def int_enum(name, elements):
    d = z3.IntSort()
    return d, [z3.IntVal(i) for i in range(1, len(elements) + 1)]

16
17
class Automaton(metaclass=ABCMeta):
    @abstractmethod
18
    def export(self, model):
19
        """Returns a z3gi.model for this automaton."""
20
        pass