Commits

Anonymous committed 2ba967e

Refactoring aisy.py (making it partially object-oriented).

  • Participants
  • Parent commits c3d26af

Comments (0)

Files changed (2)

 # coding=utf-8
 
 """
-An example of synthesis tool from Aiger http://fmv.jku.at/aiger/ circuits format.
-Implementations of some functions are omitted to give you chance to implement them.
+    aisy.py
+    -------
 
-Basic stuff is left: parsing, and some helper functions.
+    An example of synthesis tool from `Aiger <http://fmv.jku.at/aiger/>`_ circuits format.
+    Implementations of some functions are omitted to give you chance to implement them.
 
-Installation requirements:
-  - pycudd library: http://bears.ece.ucsb.edu/pycudd.html
-  - swig library: http://www.swig.org/
-  - (probably) python2.7 headers
+    Basic stuff is left: parsing, and some helper functions.
 
-After installing pycudd library add cudd libraries into your LD_LIBRARY_PATH:
+    Installation requirements:
+    * pycudd library: http://bears.ece.ucsb.edu/pycudd.html
+    * swig library: http://www.swig.org/
+    * (probably) python2.7 headers
 
-export LD_LIBRARY_PATH=/path/to/pycudd2.0.2/cudd-2.4.2/lib
+    After installing pycudd library add cudd libraries into your ``LD_LIBRARY_PATH``::
 
-To run:
+        export LD_LIBRARY_PATH=/path/to/pycudd2.0.2/cudd-2.4.2/lib
 
-./aisy.py -h
+    To run::
 
-Some self-testing functionality is included in ``run_status_tests.py``.
+        ./aisy.py -h
 
-More extensive tests are provided by Robert in script ``performance_test.sh``.
-This script also runs model checker to check the results.
+    Some self-testing functionality is included in ``run_status_tests.py``.
 
-More details you will find in the code, on web-page of the course.
+    More extensive tests are provided in Robert's script ``performance_test.sh``.
+    This script also runs a model checker to check the results.
 
-Email me in case questions/suggestions/bugs: ayrat.khalimov at gmail
+    You can find more details in the source code and
+    additionally on the webpage of the course.
 
-----------------------
+    Email me in case questions/suggestions/bugs: ayrat.khalimov at gmail
 """
 
-status = ["TODO: check the case when output functions depend on error fake latch"]
-
-
 import argparse
 import logging
 import pycudd
 import sys
-from aiger_swig.aiger_wrap import *
-from aiger_swig.aiger_wrap import aiger
+from aiger_swig.aiger_wrap import aiger_open_and_read_from_file, get_aiger_symbol
+from aiger_swig.aiger_wrap import aiger, aiger_init, aiger_symbol, aiger_is_input
+from aiger_swig.aiger_wrap import aiger_is_latch, aiger_is_and, aiger_redefine_input_as_and
+from aiger_swig.aiger_wrap import aiger_reencode, aiger_write_to_string, aiger_ascii_mode
 
-#don't change status numbers since they are used by the performance script
-EXIT_STATUS_REALIZABLE = 10
-EXIT_STATUS_UNREALIZABLE = 20
 
+__todo__ = ["TODO: check the case when output functions depend on error fake latch"]
 
-#: :type: aiger
-spec = None
+# don't change status numbers since they are used by the performance script
+EXIT_STATUS_REALIZABLE = 10
+EXIT_STATUS_UNREALIZABLE = 20
 
-#: :type: DdManager
-cudd = None
 
-# error output can be latched or unlatched, latching makes things look like in lectures, lets emulate this
-#: :type: aiger_symbol
-error_fake_latch = None
 
 
 #: :type: Logger
 logger = None
 
 
-def setup_logging(verbose):
-    global logger
-    level = None
-    if verbose is 0:
-        level = logging.INFO
-    elif verbose >= 1:
-        level = logging.DEBUG
-
-    logging.basicConfig(format="%(asctime)-10s%(message)s",
-                        datefmt="%H:%M:%S",
-                        level=level,
-                        stream=sys.stdout)
-
-    logger = logging.getLogger(__name__)
-
+# BDD Tools
 
 def is_negated(l):
     return (l & 1) == 1
 
-
 def strip_lit(l):
     return l & ~1
 
+def get_unprimed_variable_as_bdd(cudd, lit):
+    stripped_lit = strip_lit(lit)
+    return cudd.IthVar(stripped_lit)
 
-def introduce_error_latch_if():
-    global error_fake_latch
-    if error_fake_latch:
-        return
-
-    error_fake_latch = aiger_symbol()
-    #: :type: aiger_symbol
-    error_symbol = get_err_symbol()
-
-    error_fake_latch.lit = (int(spec.maxvar) + 1) * 2
-    error_fake_latch.name = 'fake_error_latch'
-    error_fake_latch.next = error_symbol.lit
-
-
-def iterate_latches_and_error():
-    introduce_error_latch_if()
+def get_primed_variable_as_bdd(cudd, lit):
+    stripped_lit = strip_lit(lit)
+    # we know that odd vars cannot be used as names of latches/inputs
+    return cudd.IthVar(stripped_lit + 1)
 
-    for i in range(int(spec.num_latches)):
-        yield get_aiger_symbol(spec.latches, i)
+def make_bdd_eq(value1, value2):
+    return (value1 & value2) | (~value1 & ~value2)
 
-    yield error_fake_latch
+def get_cube(cudd, variables):
+    assert len(variables)
 
+    cube = cudd.One()
+    for v in variables:
+        cube &= v
+    return cube
 
-def parse_into_spec(aiger_file_name):
-    global spec
-    logger.info('parsing..')
-    #: :type: aiger
-    spec = aiger_init()
+def negated(lit):
+    return lit ^ 1
 
-    err = aiger_open_and_read_from_file(spec, aiger_file_name)
-    assert not err, err
+def next_lit(maxvar):
+    """ :return: next possible to add to the spec literal """
+    return (int(maxvar) + 1) * 2
 
+def get_optimized_and_lit(a_lit, b_lit, maxvar):
+    if a_lit == 0 or b_lit == 0:
+        return 0
 
-def get_lit_type(stripped_lit):
-    if stripped_lit == error_fake_latch.lit:
-        return None, error_fake_latch, None
+    if a_lit == 1 and b_lit == 1:
+        return 1
 
-    input_ = aiger_is_input(spec, stripped_lit)
-    latch_ = aiger_is_latch(spec, stripped_lit)
-    and_ = aiger_is_and(spec, strip_lit(stripped_lit))
+    if a_lit == 1:
+        return b_lit
 
-    return input_, latch_, and_
+    if b_lit == 1:
+        return a_lit
 
+    if a_lit > 1 and b_lit > 1:
+        a_b_lit = next_lit(maxvar)
+        aiger_add_and(self.spec, a_b_lit, a_lit, b_lit)
+        return a_b_lit
 
-def get_bdd_for_value(lit):  # lit is variable index with sign
-    stripped_lit = strip_lit(lit)
+    assert 0, 'impossible'
 
-    # we faked error latch and so we cannot call directly aiger_is_input, aiger_is_latch, aiger_is_and
-    input_, latch_, and_ = get_lit_type(stripped_lit)
 
-    if stripped_lit == 0:
-        res = cudd.Zero()
+# classes for processing
+
+class AigerParser(object):
+    def __init__(self, filepath, log=None):
+        self.log = log or logging.getLogger(__name__)
+        self.filepath = filepath
+
+        #: :type: aiger
+        self.spec = None
+
+    def parse(self):
+        """Read AIGER file from `filepath` and parse it"""
+        self.log.info('parsing..')
+        self.spec = aiger_init()
+
+        err = aiger_open_and_read_from_file(self.spec, self.filepath)
+        assert not err, err
+
+        return self.spec
+
+
+class AigerSynthesis(object):
+    DYN_REORDERINGS = {
+        'SAME': 0,
+        'NONE': 1,
+        'RANDOM': 2,
+        'RANDOM_PIVOT': 3,
+        'SIFT': 4,
+        'SIFT_CONVERGE': 5,
+        'SYMM_SIFT': 6,
+        'SYMM_SIFT_CONV': 7,
+        'WINDOW2': 8,
+        'WINDOW3': 9,
+        'WINDOW4': 10,
+        'WINDOW2_CONV': 11,
+        'WINDOW3_CONV': 12,
+        'WINDOW4_CONV': 13,
+        'GROUP_SIFT': 14,
+        'GROUP_SIFT_CONV': 15,
+        'ANNEALING': 16,
+        'GENETIC': 17,
+        'LINEAR': 18,
+        'LINEAR_CONVERGE': 19,
+        'LAZY_SIFT': 20,
+        'EXACT': 21
+    }
+
+    def __init__(self, parser, reordering='LINEAR'):
+        # error output can be latched or unlatched
+        # latching makes things look like in lectures, let's emulate this
+        #: :type: aiger_symbol
+        self.error_latch = None
 
-    elif input_ or latch_:
-        res = cudd.IthVar(stripped_lit)    # use internal mapping of cudd
+        # take parsed file to work with it
+        self.spec = parser.parse()
 
-    elif and_:
-        #: :type: aiger_and
-        arg1 = get_bdd_for_value(int(and_.rhs0))
-        arg2 = get_bdd_for_value(int(and_.rhs1))
-        res = arg1 & arg2
+        self.init_cudd(reordering)
 
-    else:
-        assert 0, 'should be impossible: if it is output then it is still either latch or and'
+    def init_cudd(self, reordering='LINEAR'):
+        #: :type: DdManager
+        self.cudd = pycudd.DdManager()
+        self.cudd.SetDefault()
+        if reordering.upper() != 'NONE':
+            self.cudd.AutodynEnable(self.DYN_REORDERINGS[reordering.upper()])
+        else:
+            self.cudd.AutodynDisable()
+        self.cudd.EnableReorderingReporting()
 
-    if is_negated(lit):
-        res = ~res
+    def introduce_error_latch_if(self):
+        if self.error_latch:
+            return
 
-    return res
+        self.error_latch = aiger_symbol()
+        #: :type: aiger_symbol
+        error_symbol = self.get_err_symbol()
+    
+        self.error_latch.lit = (int(self.spec.maxvar) + 1) * 2
+        self.error_latch.name = 'fake_error_latch'
+        self.error_latch.next = error_symbol.lit
 
 
-def get_unprimed_variable_as_bdd(lit):
-    stripped_lit = strip_lit(lit)
-    return cudd.IthVar(stripped_lit)
+    def iterate_latches_and_error(self):
+        self.introduce_error_latch_if()
 
+        for i in range(int(self.spec.num_latches)):
+            yield get_aiger_symbol(self.spec.latches, i)
 
-def get_primed_variable_as_bdd(lit):
-    stripped_lit = strip_lit(lit)
-    return cudd.IthVar(stripped_lit + 1)  # we know that odd vars cannot be used as names of latches/inputs
+        yield self.error_latch
 
+    def get_lit_type(self, stripped_lit):
+        if stripped_lit == self.error_latch.lit:
+            return None, self.error_latch, None
 
-def make_bdd_eq(value1, value2):
-    return (value1 & value2) | (~value1 & ~value2)
+        input_ = aiger_is_input(self.spec, stripped_lit)
+        latch_ = aiger_is_latch(self.spec, stripped_lit)
+        and_ = aiger_is_and(self.spec, strip_lit(stripped_lit))
 
+        return input_, latch_, and_
 
-def compose_transition_bdd():
-    """ :return: BDD representing transition function of spec: ``T(x,i,c,x')``
-    """
 
-    logger.info('compose_transition_bdd, nof_latches={0}...'.format(len(list(iterate_latches_and_error()))))
+    def get_bdd_for_value(self, lit):  # lit is variable index with sign
+        stripped_lit = strip_lit(lit)
 
-    #: :type: DdNode
-    transition = cudd.One()
-    for l in iterate_latches_and_error():
-        #: :type: aiger_symbol
-        l = l
+        # we faked error latch and so we cannot call directly aiger_is_input, aiger_is_latch, aiger_is_and
+        input_, latch_, and_ = self.get_lit_type(stripped_lit)
 
-        next_value_bdd = get_bdd_for_value(int(l.next))
+        if stripped_lit == 0:
+            res = self.cudd.Zero()
 
-        next_value_variable = get_primed_variable_as_bdd(l.lit)
-        # print'next_value_variable for latch ' + str(l.lit) + ' ' + str(l.name)
-        # print'0123456789'
-        # next_value_variable.PrintMinterm()
+        elif input_ or latch_:
+            res = self.cudd.IthVar(stripped_lit)    # use internal mapping of cudd
 
-        latch_transition = make_bdd_eq(next_value_variable, next_value_bdd)
-        # print'latch transition'
-        # latch_transition.PrintMinterm()
+        elif and_:
+            #: :type: aiger_and
+            arg1 = self.get_bdd_for_value(int(and_.rhs0))
+            arg2 = self.get_bdd_for_value(int(and_.rhs1))
+            res = arg1 & arg2
 
-        transition &= latch_transition
+        else:
+            assert 0, 'should be impossible: if it is output then it is still either latch or and'
 
-    # print('final transition BDD is')
-    # transition.PrintMinterm()
+        if is_negated(lit):
+            res = ~res
 
-    return transition
+        return res
 
+    def compose_transition_bdd(self):
+        """ :return: BDD representing transition function of spec: ``T(x,i,c,x')``
+        """
 
-def get_err_symbol():
-    assert spec.num_outputs == 1
-    return spec.outputs  # swig return one element instead of array, to iterate over array use iterate_symbols
+        logger.info('compose_transition_bdd, nof_latches={0}...'.format(len(list(self.iterate_latches_and_error()))))
 
+        #: :type: DdNode
+        transition = self.cudd.One()
+        for l in self.iterate_latches_and_error():
+            #: :type: aiger_symbol
+            l = l
 
-def get_cube(variables):
-    assert len(variables)
+            next_value_bdd = self.get_bdd_for_value(int(l.next))
 
-    cube = cudd.One()
-    for v in variables:
-        cube &= v
-    return cube
+            next_value_variable = get_primed_variable_as_bdd(self.cudd, l.lit)
+            # print'next_value_variable for latch ' + str(l.lit) + ' ' + str(l.name)
+            # print'0123456789'
+            # next_value_variable.PrintMinterm()
 
+            latch_transition = make_bdd_eq(next_value_variable, next_value_bdd)
+            # print'latch transition'
+            # latch_transition.PrintMinterm()
 
-def _get_bdd_vars(filter_func):
-    var_bdds = []
+            transition &= latch_transition
 
-    for i in range(int(spec.num_inputs)):
-        input_aiger_symbol = get_aiger_symbol(spec.inputs, i)
-        if filter_func(input_aiger_symbol.name.strip()):
-            out_var_bdd = get_bdd_for_value(input_aiger_symbol.lit)
-            var_bdds.append(out_var_bdd)
+        # print('final transition BDD is')
+        # transition.PrintMinterm()
+        return transition
 
-    return var_bdds
 
+    def get_err_symbol(self):
+        assert self.spec.num_outputs == 1
+        # swig return one element instead of array, to iterate over array use iterate_symbols
+        return self.spec.outputs
 
-def get_controllable_vars_bdds():
-    return _get_bdd_vars(lambda name: name.startswith('controllable'))
+    def _get_bdd_vars(self, filter_func):
+        var_bdds = []
 
+        for i in range(int(self.spec.num_inputs)):
+            input_aiger_symbol = get_aiger_symbol(self.spec.inputs, i)
+            if filter_func(input_aiger_symbol.name.strip()):
+                out_var_bdd = self.get_bdd_for_value(input_aiger_symbol.lit)
+                var_bdds.append(out_var_bdd)
 
-def get_uncontrollable_output_bdds():
-    return _get_bdd_vars(lambda name: not name.startswith('controllable'))
+        return var_bdds
 
 
-def get_all_latches_as_bdds():
-    bdds = [get_bdd_for_value(l.lit) for l in iterate_latches_and_error()]
-    return bdds
+    def get_controllable_vars_bdds(self):
+        return self._get_bdd_vars(lambda name: name.startswith('controllable'))
 
 
-def _prime_unprime_latches_in_bdd(bdd, should_prime):
-    latch_bdds = get_all_latches_as_bdds()
-    num_latches = len(latch_bdds)
-    #: :type: DdArray
-    primed_var_array = pycudd.DdArray(num_latches)
-    curr_var_array = pycudd.DdArray(num_latches)
+    def get_uncontrollable_output_bdds(self):
+        return self._get_bdd_vars(lambda name: not name.startswith('controllable'))
 
-    for l_bdd in latch_bdds:
-        #: :type: DdNode
-        l_bdd = l_bdd
-        curr_var_array.Push(l_bdd)
 
-        lit = l_bdd.NodeReadIndex()
-        new_l_bdd = get_primed_variable_as_bdd(lit)
-        primed_var_array.Push(new_l_bdd)
+    def get_all_latches_as_bdds(self):
+        bdds = [self.get_bdd_for_value(l.lit) for l in self.iterate_latches_and_error()]
+        return bdds
 
-    if should_prime:
-        replaced_states_bdd = bdd.SwapVariables(curr_var_array, primed_var_array, num_latches)
-    else:
-        replaced_states_bdd = bdd.SwapVariables(primed_var_array, curr_var_array, num_latches)
 
-    return replaced_states_bdd
+    def _prime_unprime_latches_in_bdd(self, bdd, should_prime):
+        latch_bdds = self.get_all_latches_as_bdds()
+        num_latches = len(latch_bdds)
+        #: :type: DdArray
+        primed_var_array = pycudd.DdArray(num_latches)
+        curr_var_array = pycudd.DdArray(num_latches)
 
+        for l_bdd in latch_bdds:
+            #: :type: DdNode
+            l_bdd = l_bdd
+            curr_var_array.Push(l_bdd)
 
-def prime_latches_in_bdd(states_bdd):
-    primed_states_bdd = _prime_unprime_latches_in_bdd(states_bdd, True)
-    return primed_states_bdd
+            lit = l_bdd.NodeReadIndex()
+            new_l_bdd = get_primed_variable_as_bdd(self.cudd, lit)
+            primed_var_array.Push(new_l_bdd)
 
+        if should_prime:
+            replaced_states_bdd = bdd.SwapVariables(curr_var_array, primed_var_array, num_latches)
+        else:
+            replaced_states_bdd = bdd.SwapVariables(primed_var_array, curr_var_array, num_latches)
 
-def unprime_latches_in_bdd(bdd):
-    unprimed_bdd = _prime_unprime_latches_in_bdd(bdd, False)
-    return unprimed_bdd
+        return replaced_states_bdd
 
 
-def pre_sys_bdd(dst_states_bdd, transition_bdd):
-    """ Calculate predecessor states of given states.
+    def prime_latches_in_bdd(self, states_bdd):
+        primed_states_bdd = self._prime_unprime_latches_in_bdd(states_bdd, True)
+        return primed_states_bdd
 
-    :return: BDD representation of predecessor states
 
-    :hints: if current states are not primed they should be primed before calculation (why?)
-    :hints: calculation of ``∃o t(a,b,o)`` using cudd: ``t.ExistAbstract(get_cube(o))``
-    :hints: calculation of ``∀i t(a,b,i)`` using cudd: ``t.UnivAbstract(get_cube(i))``
-    """
+    def unprime_latches_in_bdd(self, bdd):
+        unprimed_bdd = self._prime_unprime_latches_in_bdd(bdd, False)
+        return unprimed_bdd
 
-    #: :type: DdNode
-    transition_bdd = transition_bdd
-    #: :type: DdNode
-    primed_dst_states_bdd = prime_latches_in_bdd(dst_states_bdd)
-
-    #: :type: DdNode
-    intersection = transition_bdd & primed_dst_states_bdd  # all predecessors (i.e., if sys and env cooperate)
-
-    # print
-    # print('dst_states_bdd (after priming)')
-    # print"0123456789"
-    # primed_dst_states_bdd.PrintMinterm()
-    # print('transition_bdd')
-    # transition_bdd.PrintMinterm()
-    # print('intersection == set of states from which the system can reach safe states are (wo quantifications)')
-    # print"0123456789"
-    # intersection.PrintMinterm()
-
-    # cudd requires to create a cube first..
-    if len(get_controllable_vars_bdds()) != 0:
-        out_vars_cube_bdd = get_cube(get_controllable_vars_bdds())
-        exist_outs = intersection.ExistAbstract(out_vars_cube_bdd)  # ∃o tau(t,i,t',o)
-    else:
-        exist_outs = intersection
-    # print
-    # print
-    #
-    # print('exist_outs: quantified vars')
-    # print"0123456789"
-    # out_vars_cube_bdd.PrintMinterm()
-    # print('before quantifying')
-    # intersection.PrintMinterm()
-    # print('after quantifying')
-    # exist_outs.PrintMinterm()
-
-    next_state_vars_cube = prime_latches_in_bdd(get_cube(get_all_latches_as_bdds()))
-    exist_next_state = exist_outs.ExistAbstract(next_state_vars_cube)  # ∃o ∃t'  tau(t,i,t',o)
-
-    # print('exists_next_states: quantified vars')
-    # next_state_vars_cube.PrintMinterm()
-    # print('before quantifying')
-    # exist_outs.PrintMinterm()
-    # print('after quantifying')
-    # exist_next_state.PrintMinterm()
-
-    uncontrollable_output_bdds = get_uncontrollable_output_bdds()
-    if uncontrollable_output_bdds:
-        in_vars_cube_bdd = get_cube(uncontrollable_output_bdds)
-        forall_inputs = exist_next_state.UnivAbstract(in_vars_cube_bdd)  # ∀i ∃o ∃t'  tau(t,i,t',o)
-    else:
-        forall_inputs = exist_next_state
 
-    # print('forall_exists')
-    # forall_inputs.PrintMinterm()
+    def pre_sys_bdd(self, dst_states_bdd, transition_bdd):
+        """ Calculate predecessor states of given states.
 
-    return forall_inputs
+        :return: BDD representation of predecessor states
 
+        :hints: if current states are not primed they should be primed before calculation (why?)
+        :hints: calculation of ``∃o t(a,b,o)`` using cudd: ``t.ExistAbstract(get_cube(o))``
+        :hints: calculation of ``∀i t(a,b,i)`` using cudd: ``t.UnivAbstract(get_cube(i))``
+        """
 
-def calc_win_region(init_state_bdd, transition_bdd, not_error_bdd):
-    """ Calculate a winning region for the safety game: win = greatest_fix_point.X [not_error & pre_sys(X)]
-    :return: BDD representing the winning region
-    """
+        #: :type: DdNode
+        transition_bdd = transition_bdd
+        #: :type: DdNode
+        primed_dst_states_bdd = self.prime_latches_in_bdd(dst_states_bdd)
 
-    logger.info('calc_win_region..')
+        #: :type: DdNode
+        intersection = transition_bdd & primed_dst_states_bdd  # all predecessors (i.e., if sys and env cooperate)
 
-    new_set_bdd = cudd.One()
-    while True:
-        curr_set_bdd = new_set_bdd
+        # print
+        # print('dst_states_bdd (after priming)')
+        # print"0123456789"
+        # primed_dst_states_bdd.PrintMinterm()
+        # print('transition_bdd')
+        # transition_bdd.PrintMinterm()
+        # print('intersection == set of states from which the system can reach safe states are (wo quantifications)')
+        # print"0123456789"
+        # intersection.PrintMinterm()
+
+        # cudd requires to create a cube first..
+        if len(self.get_controllable_vars_bdds()) != 0:
+            out_vars_cube_bdd = get_cube(self.cudd, self.get_controllable_vars_bdds())
+            exist_outs = intersection.ExistAbstract(out_vars_cube_bdd)  # ∃o tau(t,i,t',o)
+        else:
+            exist_outs = intersection
+        # print
+        # print
+        #
+        # print('exist_outs: quantified vars')
+        # print"0123456789"
+        # out_vars_cube_bdd.PrintMinterm()
+        # print('before quantifying')
+        # intersection.PrintMinterm()
+        # print('after quantifying')
+        # exist_outs.PrintMinterm()
+
+        next_state_vars_cube = self.prime_latches_in_bdd(get_cube(self.cudd, self.get_all_latches_as_bdds()))
+        exist_next_state = exist_outs.ExistAbstract(next_state_vars_cube)  # ∃o ∃t'  tau(t,i,t',o)
+
+        # print('exists_next_states: quantified vars')
+        # next_state_vars_cube.PrintMinterm()
+        # print('before quantifying')
+        # exist_outs.PrintMinterm()
+        # print('after quantifying')
+        # exist_next_state.PrintMinterm()
+
+        uncontrollable_output_bdds = self.get_uncontrollable_output_bdds()
+        if uncontrollable_output_bdds:
+            in_vars_cube_bdd = get_cube(self.cudd, uncontrollable_output_bdds)
+            forall_inputs = exist_next_state.UnivAbstract(in_vars_cube_bdd)  # ∀i ∃o ∃t'  tau(t,i,t',o)
+        else:
+            forall_inputs = exist_next_state
 
-        new_set_bdd = not_error_bdd & pre_sys_bdd(curr_set_bdd, transition_bdd)
+        # print('forall_exists')
+        # forall_inputs.PrintMinterm()
 
-        if (new_set_bdd & init_state_bdd) == cudd.Zero():
-            return cudd.Zero()
+        return forall_inputs
 
-        if new_set_bdd == curr_set_bdd:
-            return new_set_bdd
 
+    def calc_win_region(self, init_state_bdd, transition_bdd, not_error_bdd):
+        """ Calculate a winning region for the safety game: win = greatest_fix_point.X [not_error & pre_sys(X)]
+        :return: BDD representing the winning region
+        """
 
-def get_nondet_strategy(win_region_bdd, transition_bdd):
-    """ Get non-deterministic strategy from the winning region.
-    If the system outputs controllable values that satisfy this non-deterministic strategy, then the system wins.
-    I.e., a non-deterministic strategy describes for each state all possible plausible output values:
+        logger.info('calc_win_region..')
 
-    ``strategy(x,i,c) = ∃x' W(x) & T(x,i,c,x') & W(x') ``
+        new_set_bdd = self.cudd.One()
+        while True:
+            curr_set_bdd = new_set_bdd
 
-    (Why system cannot lose if adhere to this strategy?)
+            new_set_bdd = not_error_bdd & self.pre_sys_bdd(curr_set_bdd, transition_bdd)
 
-    :return: non deterministic strategy bdd
-    :note: The strategy is still not-deterministic. Determinization step is done later.
-    """
+            if (new_set_bdd & init_state_bdd) == self.cudd.Zero():
+                return self.cudd.Zero()
 
-    logger.info('get_nondet_strategy..')
+            if new_set_bdd == curr_set_bdd:
+                return new_set_bdd
 
-    #: :type: DdNode
-    primed_win_region_bdd = prime_latches_in_bdd(win_region_bdd)
 
-    # print'primed_win_region_bdd'
-    # print'0123456789'
-    # primed_win_region_bdd.PrintMinterm()
-    # print
+    def get_nondet_strategy(self, win_region_bdd, transition_bdd):
+        """ Get non-deterministic strategy from the winning region.
+        If the system outputs controllable values that satisfy this non-deterministic strategy, then the system wins.
+        I.e., a non-deterministic strategy describes for each state all possible plausible output values:
 
-    intersection = (primed_win_region_bdd & transition_bdd)
+        ``strategy(x,i,c) = ∃x' W(x) & T(x,i,c,x') & W(x') ``
 
-    next_vars_cube = prime_latches_in_bdd(get_cube(get_all_latches_as_bdds()))
-    strategy = intersection.ExistAbstract(next_vars_cube)
+        (Why system cannot lose if adhere to this strategy?)
 
-    return strategy
+        :return: non deterministic strategy bdd
+        :note: The strategy is still not-deterministic. Determinization step is done later.
+        """
 
+        logger.info('get_nondet_strategy..')
 
-def compose_init_state_bdd():
-    """ Initial state is 'all latches are zero' """
+        #: :type: DdNode
+        primed_win_region_bdd = self.prime_latches_in_bdd(win_region_bdd)
 
-    logger.info('compose_init_state_bdd..')
+        # print'primed_win_region_bdd'
+        # print'0123456789'
+        # primed_win_region_bdd.PrintMinterm()
+        # print
 
-    init_state_bdd = cudd.One()
-    for l in iterate_latches_and_error():
-        #: :type: aiger_symbol
-        l = l
-        l_curr_value_bdd = get_bdd_for_value(l.lit)
-        init_state_bdd &= make_bdd_eq(l_curr_value_bdd, cudd.Zero())
+        intersection = (primed_win_region_bdd & transition_bdd)
 
-    return init_state_bdd
+        next_vars_cube = self.prime_latches_in_bdd(get_cube(self.cudd, self.get_all_latches_as_bdds()))
+        strategy = intersection.ExistAbstract(next_vars_cube)
 
+        return strategy
 
-def extract_output_funcs(non_det_strategy, init_state_bdd, transition_bdd):
-    """
-    Calculate BDDs for output functions given a non-deterministic winning strategy.
-    Cofactor-based approach.
 
-    :return: dictionary ``controllable_variable_bdd -> func_bdd``
-    """
+    def compose_init_state_bdd(self):
+        """ Initial state is 'all latches are zero' """
 
-    logger.info('extract_output_funcs..')
+        logger.info('compose_init_state_bdd..')
 
-    output_models = dict()
-    all_outputs = get_controllable_vars_bdds()
-    for c in get_controllable_vars_bdds():
-        logger.info('getting output function for ' + aiger_is_input(spec, strip_lit(c.NodeReadIndex())).name)
+        init_state_bdd = self.cudd.One()
+        for l in self.iterate_latches_and_error():
+            #: :type: aiger_symbol
+            l = l
+            l_curr_value_bdd = self.get_bdd_for_value(l.lit)
+            init_state_bdd &= make_bdd_eq(l_curr_value_bdd, self.cudd.Zero())
 
-        others = set(set(all_outputs).difference({c}))
-        if others:
-            others_cube = get_cube(others)
-            #: :type: DdNode
-            c_arena = non_det_strategy.ExistAbstract(others_cube)
-        else:
-            c_arena = non_det_strategy
+        return init_state_bdd
 
-        can_be_true = c_arena.Cofactor(c)  # states (x,i) in which c can be true
-        can_be_false = c_arena.Cofactor(~c)
 
-        # print'can_be_true'
-        # print'0123456789'
-        # can_be_true.PrintMinterm()
-        # print'can_be_false'
-        # can_be_false.PrintMinterm()
-        # print
+    def extract_output_funcs(self, non_det_strategy, init_state_bdd, transition_bdd):
+        """
+        Calculate BDDs for output functions given a non-deterministic winning strategy.
+        Cofactor-based approach.
 
-        # We need to intersect with can_be_true to narrow the search.
-        # Negation can cause including states from !W (with err=1)
-        #: :type: DdNode
-        must_be_true = (~can_be_false) & can_be_true
-        must_be_false = (~can_be_true) & can_be_false
+        :return: dictionary ``controllable_variable_bdd -> func_bdd``
+        """
 
-        # print'must_be_true'
-        # print'0123456789'
-        # must_be_true.PrintMinterm()
-        # print'must_be_false'
-        # must_be_false.PrintMinterm()
-        # print
+        logger.info('extract_output_funcs..')
 
-        care_set = (must_be_true | must_be_false)
+        output_models = dict()
+        all_outputs = self.get_controllable_vars_bdds()
+        for c in self.get_controllable_vars_bdds():
+            logger.info('getting output function for ' + aiger_is_input(self.spec, strip_lit(c.NodeReadIndex())).name)
 
-        # print'care set is'
-        # print'0123456789'
-        # care_set.PrintMinterm()
+            others = set(set(all_outputs).difference({c}))
+            if others:
+                others_cube = get_cube(self.cudd, others)
+                #: :type: DdNode
+                c_arena = non_det_strategy.ExistAbstract(others_cube)
+            else:
+                c_arena = non_det_strategy
 
-        # We use 'restrict' operation, but we could also do just:
-        # c_model = must_be_true -> care_set
-        # ..but this is (probably) less efficient, since we cannot set c=1 if it is not in care_set, but we could.
-        #
-        # Restrict on the other side applies optimizations to find smaller bdd.
-        # It cannot be expressed using boolean logic operations since we would need to say:
-        # must_be_true = ite(care_set, must_be_true, "don't care")
-        # and "don't care" cannot be expressed in boolean logic.
+            can_be_true = c_arena.Cofactor(c)  # states (x,i) in which c can be true
+            can_be_false = c_arena.Cofactor(~c)
 
-        # Restrict operation:
-        #   on care_set: must_be_true.restrict(care_set) <-> must_be_true
-        c_model = must_be_true.Restrict(care_set)
+            # print'can_be_true'
+            # print'0123456789'
+            # can_be_true.PrintMinterm()
+            # print'can_be_false'
+            # can_be_false.PrintMinterm()
+            # print
 
-        output_models[c] = c_model
+            # We need to intersect with can_be_true to narrow the search.
+            # Negation can cause including states from !W (with err=1)
+            #: :type: DdNode
+            must_be_true = (~can_be_false) & can_be_true
+            must_be_false = (~can_be_true) & can_be_false
 
-        non_det_strategy = non_det_strategy & make_bdd_eq(c, c_model)
+            # print'must_be_true'
+            # print'0123456789'
+            # must_be_true.PrintMinterm()
+            # print'must_be_false'
+            # must_be_false.PrintMinterm()
+            # print
 
-        # print'c_model'
-        # c_model.PrintMinterm()
-        # print
+            care_set = (must_be_true | must_be_false)
 
-    return output_models
+            # print'care set is'
+            # print'0123456789'
+            # care_set.PrintMinterm()
 
+            # We use 'restrict' operation, but we could also do just:
+            # c_model = must_be_true -> care_set
+            # ..but this is (probably) less efficient, since we cannot set c=1 if it is not in care_set, but we could.
+            #
+            # Restrict on the other side applies optimizations to find smaller bdd.
+            # It cannot be expressed using boolean logic operations since we would need to say:
+            # must_be_true = ite(care_set, must_be_true, "don't care")
+            # and "don't care" cannot be expressed in boolean logic.
 
-def synthesize():
-    """ Calculate winning region and extract output functions.
+            # Restrict operation:
+            #   on care_set: must_be_true.restrict(care_set) <-> must_be_true
+            c_model = must_be_true.Restrict(care_set)
 
-    :return: - if realizable: dictionary: controllable_variable_bdd -> func_bdd
-             - if not: None
-    """
-    logger.info('synthesize..')
+            output_models[c] = c_model
 
-    #: :type: DdNode
-    init_state_bdd = compose_init_state_bdd()    #: :type: DdNode
+            non_det_strategy = non_det_strategy & make_bdd_eq(c, c_model)
 
-    transition_bdd = compose_transition_bdd()
+            # print'c_model'
+            # c_model.PrintMinterm()
+            # print
 
-    #: :type: DdNode
-    not_error_bdd = ~get_bdd_for_value(error_fake_latch.lit)
-    win_region = calc_win_region(init_state_bdd, transition_bdd, not_error_bdd)
+        return output_models
 
-    # print'win region is'
-    if win_region == cudd.Zero():
-        return None
 
-    # win_region.PrintMinterm()
+    def synthesize(self):
+        """ Calculate winning region and extract output functions.
 
-    non_det_strategy = get_nondet_strategy(win_region, transition_bdd)
+        :return: - if realizable: dictionary: controllable_variable_bdd -> func_bdd
+                 - if not: None
+        """
+        logger.info('synthesize..')
 
-    func_by_var = extract_output_funcs(non_det_strategy, init_state_bdd, transition_bdd)
+        #: :type: DdNode
+        init_state_bdd = self.compose_init_state_bdd()    #: :type: DdNode
 
-    return func_by_var
+        transition_bdd = self.compose_transition_bdd()
 
+        #: :type: DdNode
+        not_error_bdd = ~self.get_bdd_for_value(self.error_latch.lit)
+        win_region = self.calc_win_region(init_state_bdd, transition_bdd, not_error_bdd)
 
-def negated(lit):
-    return lit ^ 1
+        # print'win region is'
+        if win_region == self.cudd.Zero():
+            return None
 
+        # win_region.PrintMinterm()
 
-def next_lit():
-    """ :return: next possible to add to the spec literal """
-    return (int(spec.maxvar) + 1) * 2
+        non_det_strategy = self.get_nondet_strategy(win_region, transition_bdd)
 
+        func_by_var = self.extract_output_funcs(non_det_strategy, init_state_bdd, transition_bdd)
 
-def get_optimized_and_lit(a_lit, b_lit):
-    if a_lit == 0 or b_lit == 0:
-        return 0
+        return func_by_var
 
-    if a_lit == 1 and b_lit == 1:
-        return 1
+    def walk(self, a_bdd):
+        """
+        Walk given BDD node (recursively).
+        If given input BDD requires intermediate AND gates for its representation, the function adds them.
+        Literal representing given input BDD is `not` added to the spec.
 
-    if a_lit == 1:
-        return b_lit
+        :returns: literal representing input BDD
+        :warning: variables in cudd nodes may be complemented, check with: ``node.IsComplement()``
+        """
 
-    if b_lit == 1:
-        return a_lit
+        #: :type: DdNode
+        a_bdd = a_bdd
+        if a_bdd.IsConstant():
+            res = int(a_bdd == self.cudd.One())   # in aiger 0/1 = False/True
+            return res
 
-    if a_lit > 1 and b_lit > 1:
-        a_b_lit = next_lit()
-        aiger_add_and(spec, a_b_lit, a_lit, b_lit)
-        return a_b_lit
+        # get an index of variable,
+        # all variables used in bdds also introduced in aiger,
+        # except fake error latch literal,
+        # but fake error latch will not be used in output functions (at least we don't need this..)
+        a_lit = a_bdd.NodeReadIndex()
 
-    assert 0, 'impossible'
+        assert a_lit != self.error_latch.lit, 'using error latch in the definition of output function is not allowed'
 
+        #: :type: DdNode
+        t_bdd = a_bdd.T()
+        #: :type: DdNode
+        e_bdd = a_bdd.E()
 
-def walk(a_bdd):
-    """
-    Walk given BDD node (recursively).
-    If given input BDD requires intermediate AND gates for its representation, the function adds them.
-    Literal representing given input BDD is `not` added to the spec.
+        t_lit = self.walk(t_bdd)
+        e_lit = self.walk(e_bdd)
 
-    :returns: literal representing input BDD
-    :warning: variables in cudd nodes may be complemented, check with: ``node.IsComplement()``
-    """
+        # ite(a_bdd, then_bdd, else_bdd)
+        # = a*then + !a*else
+        # = !(!(a*then) * !(!a*else))
+        # -> in general case we need 3 more ANDs
 
-    #: :type: DdNode
-    a_bdd = a_bdd
-    if a_bdd.IsConstant():
-        res = int(a_bdd == cudd.One())   # in aiger 0/1 = False/True
-        return res
+        a_t_lit = get_optimized_and_lit(a_lit, t_lit, self.spec.maxvar)
 
-    # get an index of variable,
-    # all variables used in bdds also introduced in aiger,
-    # except fake error latch literal,
-    # but fake error latch will not be used in output functions (at least we don't need this..)
-    a_lit = a_bdd.NodeReadIndex()
+        na_e_lit = get_optimized_and_lit(negated(a_lit), e_lit, self.spec.maxvar)
 
-    assert a_lit != error_fake_latch.lit, 'using error latch in the definition of output function is not allowed'
+        n_a_t_lit = negated(a_t_lit)
+        n_na_e_lit = negated(na_e_lit)
 
-    #: :type: DdNode
-    t_bdd = a_bdd.T()
-    #: :type: DdNode
-    e_bdd = a_bdd.E()
+        ite_lit = get_optimized_and_lit(n_a_t_lit, n_na_e_lit, self.spec.maxvar)
 
-    t_lit = walk(t_bdd)
-    e_lit = walk(e_bdd)
+        res = negated(ite_lit)
+        if a_bdd.IsComplement():
+            res = negated(res)
 
-    # ite(a_bdd, then_bdd, else_bdd)
-    # = a*then + !a*else
-    # = !(!(a*then) * !(!a*else))
-    # -> in general case we need 3 more ANDs
+        return res
 
-    a_t_lit = get_optimized_and_lit(a_lit, t_lit)
 
-    na_e_lit = get_optimized_and_lit(negated(a_lit), e_lit)
+    def model_to_aiger(self, c_bdd, func_bdd, introduce_output):
+        """ Update aiger spec with a definition of ``c_bdd``
+        """
+        #: :type: DdNode
+        c_bdd = c_bdd
+        c_lit = c_bdd.NodeReadIndex()
 
-    n_a_t_lit = negated(a_t_lit)
-    n_na_e_lit = negated(na_e_lit)
+        func_as_aiger_lit = self.walk(func_bdd)
 
-    ite_lit = get_optimized_and_lit(n_a_t_lit, n_na_e_lit)
+        aiger_redefine_input_as_and(self.spec, c_lit, func_as_aiger_lit, func_as_aiger_lit)
 
-    res = negated(ite_lit)
-    if a_bdd.IsComplement():
-        res = negated(res)
+        if introduce_output:
+            aiger_add_output(self.spec, c_lit, '')
 
-    return res
 
 
-def model_to_aiger(c_bdd, func_bdd, introduce_output):
-    """ Update aiger spec with a definition of ``c_bdd``
-    """
-    #: :type: DdNode
-    c_bdd = c_bdd
-    c_lit = c_bdd.NodeReadIndex()
-
-    func_as_aiger_lit = walk(func_bdd)
-
-    aiger_redefine_input_as_and(spec, c_lit, func_as_aiger_lit, func_as_aiger_lit)
-
-    if introduce_output:
-        aiger_add_output(spec, c_lit, '')
-
-
-def init_cudd():
-    global cudd
-    cudd = pycudd.DdManager()
-    cudd.SetDefault()
-    #CUDD_REORDER_SAME,
-    #CUDD_REORDER_NONE,
-    #CUDD_REORDER_RANDOM,
-    #CUDD_REORDER_RANDOM_PIVOT,
-    #CUDD_REORDER_SIFT,
-    #CUDD_REORDER_SIFT_CONVERGE,
-    #CUDD_REORDER_SYMM_SIFT,
-    #CUDD_REORDER_SYMM_SIFT_CONV,
-    #CUDD_REORDER_WINDOW2,
-    #CUDD_REORDER_WINDOW3,
-    #CUDD_REORDER_WINDOW4,
-    #CUDD_REORDER_WINDOW2_CONV,
-    #CUDD_REORDER_WINDOW3_CONV,
-    #CUDD_REORDER_WINDOW4_CONV,
-    #CUDD_REORDER_GROUP_SIFT,
-    #CUDD_REORDER_GROUP_SIFT_CONV,
-    #CUDD_REORDER_ANNEALING,
-    #CUDD_REORDER_GENETIC,
-    #CUDD_REORDER_LINEAR,
-    #CUDD_REORDER_LINEAR_CONVERGE,
-    #CUDD_REORDER_LAZY_SIFT,
-    #CUDD_REORDER_EXACT
-    cudd.AutodynEnable(4)
-    cudd.EnableReorderingReporting()
-
-
-def main(aiger_file_name, out_file_name, output_full_circuit):
+def main(aiger_file_name, out_file_name, output_full_circuit, reordering):
     """ Open aiger file, synthesize the circuit and write the result to output file.
 
     :returns: boolean value 'is realizable?'
     """
-    init_cudd()
+    parser = AigerParser(aiger_file_name)
+    syn = AigerSynthesis(parser)
 
-    parse_into_spec(aiger_file_name)
-
-    func_by_var = synthesize()
+    spec = parser.parse()
+    func_by_var = syn.synthesize()
 
     if func_by_var:
         for (c_bdd, func_bdd) in func_by_var.items():
-            model_to_aiger(c_bdd, func_bdd, output_full_circuit)
+            syn.model_to_aiger(c_bdd, func_bdd, output_full_circuit)
         
-        aiger_reencode(spec);  # some model checkers do not like unordered variable names (when e.g. latch is > add) 
+        # some model checkers do not like unordered variable names (when e.g. latch is > add) 
+        aiger_reencode(spec)
 
         if out_file_name:
             aiger_open_and_write_to_file(spec, out_file_name)
 
     return False
 
+def setup_logging(verbose):
+    global logger
+    level = None
+    if verbose is 0:
+        level = logging.INFO
+    elif verbose >= 1:
+        level = logging.DEBUG
+
+    logging.basicConfig(format="%(asctime)-10s%(message)s",
+                        datefmt="%H:%M:%S",
+                        level=level,
+                        stream=sys.stdout)
+
+    logger = logging.getLogger(__name__)
 
 def exit_if_status_request(args):
     if args.status:
 
 if __name__ == '__main__':
     parser = argparse.ArgumentParser(description='Aiger Format Based Simple Synthesizer')
-    parser.add_argument('aiger', metavar='aiger', type=str, nargs='?', default=None, help='input specification in AIGER format')
+    parser.add_argument('aiger', metavar='aiger', type=str, nargs='?', default=None,
+                        help='input specification in AIGER format')
     parser.add_argument('--out', '-o', metavar='out', type=str, required=False, default=None,
                         help='output file in AIGER format (if realizable)')
     parser.add_argument('--full', action='store_true', default=False,
                         help='produce a full circuit that has outputs other than error bit')
     parser.add_argument('--status', '-s', action='store_true', default=False,
                         help='Print current status of development')
+    parser.add_argument('--reordering', '-r', metavar='reordering', required=False, type=str, default='NONE',
+                        help='Which reordering to take')
 
     args = parser.parse_args()
     
 
     setup_logging(0)
     
-    is_realizable = main(args.aiger, args.out, args.full)
+    is_realizable = main(args.aiger, args.out, args.full, args.reordering)
 
     exit([EXIT_STATUS_UNREALIZABLE, EXIT_STATUS_REALIZABLE][is_realizable])

benchmarking/call_synth_tool.sh

 # $1 contains the input filename (the name of the AIGER-file).
 # $2 contains the output filename (your synthesis result, also in
 #    AIGER format).
-#COMMAND="echo call_synth_tool.sh called with parameters $1 $2"
+COMMAND="./ext_tools/blimc/blimc $1 $2"
 
 #other examples:
 
-COMMAND="/home/art_haali/learning/akdv14/aisy-classroom/aisy.py $1 --out=$2"
+COMMAND="../aisy.py $1 --out=$2"
 # COMMAND="${DIR}../bin/my_synth_tool --in=$1 --out=$2"
 # COMMAND="${DIR}../../bin/my_tool --input=$1 --verbose=0 -whatever_option"