1#
2# This file is part of pySMT.
3#
4#   Copyright 2014 Andrea Micheli and Marco Gario
5#
6#   Licensed under the Apache License, Version 2.0 (the "License");
7#   you may not use this file except in compliance with the License.
8#   You may obtain a copy of the License at
9#
10#       http://www.apache.org/licenses/LICENSE-2.0
11#
12#   Unless required by applicable law or agreed to in writing, software
13#   distributed under the License is distributed on an "AS IS" BASIS,
14#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15#   See the License for the specific language governing permissions and
16#   limitations under the License.
17#
18import re
19import itertools
20
21
22def all_assignments(bool_variables, env):
23    """Generates all possible assignments for a set of boolean variables."""
24    mgr = env.formula_manager
25    for set_ in powerset(bool_variables):
26        yield dict((v, mgr.Bool(v in set_)) for v in bool_variables)
27
28
29def powerset(elements):
30    """Generates the powerset of the given elements set.
31
32    E.g., powerset([1,2,3]) --> () (1,) (2,) (3,) (1,2) (1,3) (2,3) (1,2,3)
33    """
34    return itertools.chain.from_iterable(itertools.combinations(elements, r)
35                                         for r in range(len(elements)+1))
36
37#
38# Bit Operations
39#
40def set_bit(v, index, x):
41    """Set the index:th bit of v to x, and return the new value."""
42    mask = 1 << index
43    if x:
44        v |= mask
45    else:
46        v &= ~mask
47    return v
48
49
50def twos_complement(val, bits):
51    """Retuns the 2-complemented value of val assuming bits word width"""
52    if (val & (1 << (bits - 1))) != 0: # if sign bit is set
53        val = val - (2 ** bits)        # compute negative value
54    return val
55
56
57#
58# Python Compatibility Functions
59#
60
61def interactive_char_iterator(handle):
62    c = handle.read(1)
63    while c:
64        yield c
65        c = handle.read(1)
66
67
68#
69# Symbol (un)quoting
70#
71_simple_symbol_prog = re.compile(r"^[~!@\$%\^&\*_\-+=<>\.\?\/A-Za-z][~!@\$%\^&\*_\-+=<>\.\?\/A-Za-z0-9]*$")
72_keywords = set(["Int", "Real", "Bool"])
73
74def quote(name, style='|'):
75    if name in _keywords or _simple_symbol_prog.match(name) is None:
76        name = name.replace("\\", "\\\\").replace("%s" % style, "\\%s" % style)
77        return "%s%s%s" % (style, name, style)
78    else:
79        return name
80
81
82def open_(fname):
83    """Transparently handle .bz2 files."""
84    if fname.endswith(".bz2"):
85        import bz2
86        if PY2:
87            return bz2.BZ2File(fname, "r")
88        else:
89            return bz2.open(fname, "rt")
90    return open(fname)
91