Skip to content

Instantly share code, notes, and snippets.

@koehlma

koehlma/aig.py

Created January 20, 2017 19:20
Show Gist options
  • Save koehlma/a40c6d5ba8c16aef3225cf49d446bd5b to your computer and use it in GitHub Desktop.
Save koehlma/a40c6d5ba8c16aef3225cf49d446bd5b to your computer and use it in GitHub Desktop.
Download ZIP
Verification Project – Python Libraries
Raw
aig.py
# -*- coding: utf-8 -*-
# Copyright (C) 2017, Maximilian Köhl <mail@koehlma.de>
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)
Raw
ltl.py
# -*- coding: utf-8 -*-
# Copyright (C) 2017, Maximilian Köhl <mail@koehlma.de>
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)
Raw
sat.py
# -*- coding: utf-8 -*-
# Copyright (C) 2017, Maximilian Köhl <mail@koehlma.de>
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment