Verification Project – Python Libraries

aig.py

# -*- coding: utf-8 -*-

# Copyright (C) 2017, Maximilian Köhl <[email protected]>


def _literal(string):
    literal = int(string)
    return -(literal // 2) if literal & 1 else literal // 2


class Signal:
    def __init__(self, literal, name=None):
        self.literal = literal
        self.name = name

    def __str__(self):
        kind = self.__class__.__name__
        return '<{} {} name="{}">'.format(kind, self.literal, self.name or '')


class Input(Signal):
    pass


class Output(Signal):
    pass


class Latch(Signal):
    def __init__(self, literal, successor, name=None):
        super().__init__(literal, name)
        self.successor = successor


class And(Signal):
    def __init__(self, literal, left, right, name=None):
        super().__init__(literal, name)
        self.left = left
        self.right = right


class AIG:
    def __init__(self, inputs, latches, outputs, ands, mapping, comments):
        self.inputs = inputs
        self.latches = latches
        self.outputs = outputs
        self.ands = ands
        self.mapping = mapping
        self.comments = comments

    @classmethod
    def from_file(cls, filename: str):
        """ Read a file in the AIGER ASCII format and returns an AIG. """
        with open(filename, 'rt') as file:
            magic, *numbers = file.readline().split()
            assert magic == 'aag'
            max_var, num_ins, num_latches, num_outs, num_ands = map(int, numbers)

            inputs = []
            for _ in range(num_ins):
                inputs.append(Input(_literal(file.readline().strip())))

            latches = []
            for _ in range(num_latches):
                literal, successor = map(_literal, file.readline().split())
                latches.append(Latch(literal, successor))

            outputs = []
            for _ in range(num_outs):
                outputs.append(Output(_literal(file.readline().strip())))

            ands = []
            for _ in range(num_ands):
                literal, left, right = map(_literal, file.readline().split())
                ands.append(And(literal, left, right))

            mapping = {}
            for line in file:
                if line.strip() == 'c':
                    break
                if line[0] in {'i', 'l', 'o'}:
                    position, _, name = line[1:].partition(' ')
                    index = int(position)
                    name = name.strip()
                    if line[0] == 'i':
                        inputs[index].name = name
                        mapping[name] = inputs[index]
                    elif line[0] == 'l':
                        latches[index].name = name
                        mapping[name] = latches[index]
                    elif line[0] == 'o':
                        outputs[index].name = name
                        mapping[name] = outputs[index]

            comments = file.readlines()

            return cls(inputs, latches, outputs, ands, mapping, comments)

ltl.py

# -*- coding: utf-8 -*-

# Copyright (C) 2017, Maximilian Köhl <[email protected]>

import enum
import re
import typing

from collections import namedtuple


def literal(string):
    return re.escape(string)


class LTL(enum.Enum):
    # boolean connectives
    AND = '∧', (literal('&'), literal('/\\'), literal('∧'),)
    OR = '∨', (literal('|'), literal('\\/'), literal('∨'),)
    NOT = '¬', (literal('!'), literal('~'), literal('¬'),)
    IMPL = '⇒', (literal('->'), literal('⇒'),)
    EQUIV = '⇔', (literal('='), literal('⇔'),)
    XOR = '^', (literal('^'),)

    # temporal connectives
    NEXT = 'X', (literal('X'),)
    UNTIL = 'U', (literal('U'),)
    WEAK = 'W', (literal('W'),)
    RELEASE = 'R', (literal('R'),)
    FINALLY = 'F', (literal('F'), literal('<>'), literal('◇'),)
    GLOBALLY = 'G', (literal('G'), literal('[]'), literal('☐'),)

    # parenthesis
    LEFT_PAR = '(', (literal('('),)
    RIGHT_PAR = ')', (literal(')'),)

    # booleans
    TRUE = 'true', (literal('true'),)
    FALSE = 'false', (literal('false'),)

    # propositions
    PROPOSITION = 'proposition', ('\w+',)

    # whitespaces
    WHITESPACE = None, ('\s+',)

    # error
    ERROR = None, ('.',)

    # end of formula
    EOF = None, ('',)


_regex = re.compile('|'.join('(?P<' + name + '>' + '|'.join(member.value[1]) + ')'
                             for name, member in LTL.__members__.items()))


Token = namedtuple('Token', ['kind', 'start', 'end', 'value'])


def tokenize(string):
    for match in _regex.finditer(string):
        kind = LTL[match.lastgroup]
        if kind is LTL.WHITESPACE:
            continue
        elif kind is LTL.ERROR:
            raise Exception('unknown token at position {}'.format(match.start()))
        yield Token(kind, match.start(), match.end(), match.group(0))
    yield Token(LTL.EOF, len(string), len(string), '')


_atoms = {LTL.TRUE, LTL.FALSE, LTL.PROPOSITION}
_unary_operators = {LTL.NOT, LTL.NEXT, LTL.FINALLY, LTL.GLOBALLY}

_binary_operators = {LTL.OR: 3, LTL.AND: 4, LTL.IMPL: 2, LTL.EQUIV: 1,
                     LTL.XOR: 5, LTL.UNTIL: 0, LTL.WEAK: 0, LTL.RELEASE: 0}


class LTLAst:
    def __init__(self, kind: LTL):
        self.kind = kind

    def is_atom(self):
        return self.kind in _atoms

    def is_proposition(self):
        return isinstance(self, LTLProposition)

    def is_binary_operator(self):
        return isinstance(self, LTLBinaryOperator)

    def is_unary_operator(self):
        return isinstance(self, LTLUnaryOperator)

    def __eq__(self, other):
        return self.kind is other.kind

    def __hash__(self):
        return hash(self.kind)

    def __str__(self):
        return self.kind.value[0]

    def __and__(self, other):
        if self.kind is LTL.TRUE:
            return other
        elif other.kind is LTL.TRUE:
            return self
        return LTLBinaryOperator(LTL.AND, self, other)

    def __or__(self, other):
        if self.kind is LTL.FALSE:
            return other
        elif other.kind is LTL.FALSE:
            return self
        return LTLBinaryOperator(LTL.OR, self, other)

    def __xor__(self, other):
        return LTLBinaryOperator(LTL.XOR, self, other)

    def __lshift__(self, other):
        return LTLBinaryOperator(LTL.IMPL, self, other)

    def __invert__(self):
        return LTLUnaryOperator(LTL.NOT, self)


class LTLProposition(LTLAst):
    def __init__(self, proposition: str):
        super().__init__(LTL.PROPOSITION)
        self.proposition = proposition

    def __str__(self):
        return str(self.proposition)

    def __eq__(self, other):
        return self.kind is other.kind and self.proposition == other.proposition

    def __hash__(self):
        return hash((self.kind, self.proposition))


class LTLBinaryOperator(LTLAst):
    def __init__(self, kind: LTL, left: LTLAst, right: LTLAst):
        super().__init__(kind)
        self.left = left
        self.right = right

    def __str__(self):
        return '({} {} {})'.format(self.left, super().__str__(), self.right)

    def __eq__(self, other):
        if self.kind is not other.kind:
            return False
        return self.left == other.left and self.right == other.right

    def __hash__(self):
        return hash((self.kind, self.left, self.right))


class LTLUnaryOperator(LTLAst):
    def __init__(self, kind: LTL, operand: LTLAst):
        super().__init__(kind)
        self.operand = operand

    def __str__(self):
        return '{} {}'.format(super().__str__(), self.operand)

    def __eq__(self, other):
        return self.kind is other.kind and self.operand == other.operand

    def __hash__(self):
        return hash((self.kind, self.operand))


class Tokenizer:
    def __init__(self, string):
        self.generator = tokenize(string)
        self.current = next(self.generator)

    def advance(self):
        previous = self.current
        try:
            self.current = next(self.generator)
        except StopIteration:
            pass
        return previous

    def is_atom(self):
        return self.current.kind in _atoms

    def is_proposition(self):
        return self.current.kind is LTL.PROPOSITION

    def is_binary_operator(self):
        return self.current.kind in _binary_operators

    def is_unary_operator(self):
        return self.current.kind in _unary_operators

    def is_end(self):
        return self.current.kind is LTL.EOF

    def precedence(self):
        return _binary_operators[self.current.kind]


def _parse_primary_expression(tokenizer: Tokenizer) -> LTLAst:
    if tokenizer.is_proposition():
        return LTLProposition(tokenizer.advance().value)
    elif tokenizer.is_atom():
        return LTLAst(tokenizer.advance().kind)
    elif tokenizer.current.kind is LTL.LEFT_PAR:
        tokenizer.advance()
        expression = _parse_binary_expression(tokenizer, 0)
        token = tokenizer.advance()
        if token.kind is not LTL.RIGHT_PAR:
            raise Exception('expected closing parenthesis but got {}'.format(token))
        return expression
    else:
        raise Exception('unexpected token {}'.format(tokenizer.current))


def _parse_unary_expression(tokenizer: Tokenizer) -> LTLAst:
    if tokenizer.is_unary_operator():
        operator = tokenizer.advance()
        operand = _parse_unary_expression(tokenizer)
        return LTLUnaryOperator(operator.kind, operand)
    else:
        return _parse_primary_expression(tokenizer)


def _parse_binary_expression(tokenizer: Tokenizer, min_precedence: int) -> LTLAst:
    left = _parse_unary_expression(tokenizer)
    while tokenizer.is_binary_operator() and tokenizer.precedence() >= min_precedence:
        precedence = tokenizer.precedence()
        operator = tokenizer.advance()
        right = _parse_binary_expression(tokenizer, precedence + 1)
        left = LTLBinaryOperator(operator.kind, left, right)
    return left


def parse(string: str) -> LTLAst:
    tokenizer = Tokenizer(string)
    ast = _parse_binary_expression(tokenizer, 0)
    if not tokenizer.is_end():
        raise Exception('expected end of formula but found {}'.format(tokenizer.current))
    return ast


_boolean_kinds = {LTL.TRUE, LTL.FALSE, LTL.PROPOSITION, LTL.NOT,
                  LTL.AND, LTL.OR, LTL.XOR, LTL.IMPL, LTL.EQUIV}


def is_boolean(formula: LTLAst) -> bool:
    if formula.kind not in _boolean_kinds:
        return False
    elif isinstance(formula, LTLUnaryOperator):
        return is_boolean(formula.operand)
    elif isinstance(formula, LTLBinaryOperator):
        return is_boolean(formula.left) and is_boolean(formula.right)
    else:
        return True


def extract_invariant(formula: LTLAst) -> typing.Optional[LTLAst]:
    if isinstance(formula, LTLUnaryOperator) and formula.kind == LTL.GLOBALLY:
        return is_boolean(formula.operand) and formula.operand


def symbol(name: str):
    return LTLProposition(name)


true = LTLAst(LTL.TRUE)
false = LTLAst(LTL.FALSE)


def equiv(left: LTLAst, right: LTLAst):
    return LTLBinaryOperator(LTL.EQUIV, left, right)

sat.py

# -*- coding: utf-8 -*-

# Copyright (C) 2017, Maximilian Köhl <[email protected]>

import ctypes
import ctypes.util
import os
import typing


_libpicosat = ctypes.util.find_library('libpicosat')
if _libpicosat is None:
    _libpicosat = os.environ.get('LIBPICOSAT')
if _libpicosat is None:
    _libpicosat = 'libpicosat'

_library = ctypes.CDLL(_libpicosat)

_picosat_init = _library.picosat_init
_picosat_init.restype = ctypes.c_void_p

_picosat_reset = _library.picosat_reset
_picosat_reset.argtypes = [ctypes.c_void_p]

_picosat_add = _library.picosat_add
_picosat_add.argtypes = [ctypes.c_void_p, ctypes.c_int]

_picosat_assume = _library.picosat_assume
_picosat_assume.argtypes = [ctypes.c_void_p, ctypes.c_int]

_picosat_sat = _library.picosat_sat
_picosat_sat.argtypes = [ctypes.c_void_p, ctypes.c_int]
_picosat_sat.restype = ctypes.c_int

_picosat_deref = _library.picosat_deref
_picosat_deref.argtypes = [ctypes.c_void_p, ctypes.c_int]
_picosat_deref.restype = ctypes.c_int

_PICOSAT_SATISFIABLE = 10


class Solver:
    def __init__(self):
        self.sat = _picosat_init()
        self._has_solution = False

    def __del__(self):
        _picosat_reset(self.sat)

    def add_clause(self, literals: typing.Iterable[int]):
        for literal in literals:
            _picosat_add(self.sat, literal)
        _picosat_add(self.sat, 0)

    def add_assumption(self, literal):
        _picosat_assume(self.sat, literal)

    def get_solution(self, literal):
        assert self._has_solution
        return _picosat_deref(self.sat, literal) == 1

    def is_satisfiable(self, limit=-1):
        self._has_solution = _picosat_sat(self.sat, limit) == _PICOSAT_SATISFIABLE
        return self._has_solution