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 functools
19import itertools
20
21from warnings import warn
22from six import iteritems, PY2
23from six.moves import xrange
24from collections import deque
25
26import pysmt.smtlib.commands as smtcmd
27from pysmt.environment import get_env
28from pysmt.logics import get_logic_by_name, UndefinedLogicError
29from pysmt.exceptions import UnknownSmtLibCommandError, PysmtSyntaxError
30from pysmt.exceptions import PysmtTypeError
31from pysmt.smtlib.script import SmtLibCommand, SmtLibScript
32from pysmt.smtlib.annotations import Annotations
33from pysmt.utils import interactive_char_iterator
34from pysmt.constants import Fraction
35from pysmt.typing import _TypeDecl, PartialType
36
37
38def open_(fname):
39    """Transparently handle .bz2 files."""
40    if fname.endswith(".bz2"):
41        import bz2
42        if PY2:
43            return bz2.BZ2File(fname, "r")
44        else:
45            return bz2.open(fname, "rt")
46    return open(fname)
47
48
49def get_formula(script_stream, environment=None):
50    """
51    Returns the formula asserted at the end of the given script
52
53    script_stream is a file descriptor.
54    """
55    mgr = None
56    if environment is not None:
57        mgr = environment.formula_manager
58
59    parser = SmtLibParser(environment)
60    script = parser.get_script(script_stream)
61    return script.get_last_formula(mgr)
62
63
64def get_formula_strict(script_stream, environment=None):
65    """Returns the formula defined in the SMTScript.
66
67    This function assumes that only one formula is defined in the
68    SMTScript. It will raise an exception if commands such as pop and
69    push are present in the script, or if check-sat is called more
70    than once.
71    """
72    mgr = None
73    if environment is not None:
74        mgr = environment.formula_manager
75
76    parser = SmtLibParser(environment)
77    script = parser.get_script(script_stream)
78    return script.get_strict_formula(mgr)
79
80
81def get_formula_fname(script_fname, environment=None, strict=True):
82    """Returns the formula asserted at the end of the given script."""
83    with open_(script_fname) as script:
84        if strict:
85            return get_formula_strict(script, environment)
86        else:
87            return get_formula(script, environment)
88
89
90class SmtLibExecutionCache(object):
91    """Execution environment for SMT2 script execution"""
92    def __init__(self):
93        self.keys = {}
94        self.definitions = {}
95        self.annotations = Annotations()
96
97    def bind(self, name, value):
98        """Binds a symbol in this environment"""
99        lst = self.keys.setdefault(name, [])
100        lst.append(value)
101
102    def unbind(self, name):
103        """Unbinds the last binding of this symbol"""
104        self.keys[name].pop()
105
106    def define(self, name, parameters, expression):
107        self.definitions[name] = (parameters, expression)
108
109    def _define_adapter(self, formal_parameters, expression):
110        def res(*actual_parameters):
111            assert len(formal_parameters) == len(actual_parameters)
112            submap = dict(zip(formal_parameters, actual_parameters))
113            return expression.substitute(submap)
114        return res
115
116    def get(self, name):
117        """Returns the last binding for 'name'"""
118        if name in self.definitions:
119            (parameters, expression) = self.definitions[name]
120            if len(parameters) == 0:
121                return expression
122            return self._define_adapter(parameters, expression)
123        elif name in self.keys:
124            lst = self.keys[name]
125            if len(lst) > 0:
126                return lst[-1]
127            else:
128                return None
129        else:
130            return None
131
132    def update(self, value_map):
133        """Binds all the symbols in 'value_map'"""
134        for k, val in iteritems(value_map):
135            self.bind(k, val)
136
137    def unbind_all(self, values):
138        """UnBinds all the symbols in 'values'"""
139        for k in values:
140            self.unbind(k)
141
142# EOC SmtLibExecutionCache
143
144
145class Tokenizer(object):
146    """Takes a file-like object and produces a stream of tokens following
147    the LISP rules.
148
149    If interative is True, the file reading proceeds char-by-char with
150    no buffering. This is useful for interactive use for example with
151    a SMT-Lib2-compliant solver
152
153    The method add_extra_token allows to "push-back" a token, so that
154    it will be returned by the next call to consume_token, instead of
155    reading from the actual generator.
156
157    """
158
159    def __init__(self, handle, interactive=False):
160        if not interactive:
161            # reads char-by-char
162            if __debug__:
163                self.reader = self.char_iterator(handle)
164                self.__col_cnt = 0
165                self.__row_cnt = 0
166            else:
167                self.reader = itertools.chain.from_iterable(handle)
168                self.__col_cnt = None
169                self.__row_cnt = None
170        else:
171            self.reader = interactive_char_iterator(handle)
172            self.__col_cnt = None
173            self.__row_cnt = None
174        self.generator = self.create_generator(self.reader)
175        self.extra_queue = deque()
176
177    def add_extra_token(self, token):
178        self.extra_queue.append(token)
179
180    def consume_maybe(self):
181        """Consumes and returns a single token from the stream.
182           If the stream is empty `StopIteration` is thrown"""
183        if self.extra_queue:
184            return self.extra_queue.popleft()
185        else:
186            return next(self.generator)
187
188    def consume(self, msg=None):
189        """Consumes and returns a single token from the stream.
190           If the stream is empty, a PysmtSyntaxError is thrown"""
191        if self.extra_queue:
192            return self.extra_queue.popleft()
193        else:
194            try:
195                t = self.consume_maybe()
196            except StopIteration:
197                if msg:
198                    raise PysmtSyntaxError (msg, self.pos_info)
199                else:
200                    raise PysmtSyntaxError("Unexpected end of stream.",
201                                           self.pos_info)
202            return t
203
204    def raw_read(self):
205        return next(self.reader)
206
207    @property
208    def pos_info(self):
209        if self.__row_cnt is not None:
210            return (self.__row_cnt, self.__col_cnt)
211        return None
212
213    @staticmethod
214    def create_generator(reader):
215        """Takes a file-like object and produces a stream of tokens following
216        the LISP rules.
217
218        This is the method doing the heavy-lifting of tokenization.
219        """
220        spaces = set([" ", "\n", "\t"])
221        separators = set(["(", ")", "|", "\""])
222        specials = spaces | separators | set([";", ""])
223
224        try:
225            c = next(reader)
226            eof = False
227            while not eof:
228                if c in specials:
229                    # consume the spaces
230                    if c in spaces:
231                        c = next(reader)
232
233                    elif c in separators:
234                        if c == "|":
235                            s = []
236                            c = next(reader)
237                            while c and c != "|":
238                                if c == "\\": # This is a single '\'
239                                    c = next(reader)
240                                    if c != "|" and c != "\\":
241                                        # Only \| and \\ are supported escapings
242                                        raise PysmtSyntaxError(
243                                            "Unknown escaping in quoted symbol: "
244                                            "'\\%s'" % c, reader.pos_info)
245                                s.append(c)
246                                c = next(reader)
247                            if not c:
248                                raise PysmtSyntaxError("Expected '|'",
249                                                       reader.pos_info)
250                            yield "".join(s)
251                            c = next(reader)
252
253                        elif c == "\"":
254                            # String literals
255                            s = c
256                            num_quotes = 0
257                            while True:
258                                c = next(reader)
259                                if not c:
260                                    raise PysmtSyntaxError("Expected '\"'",
261                                                           reader.pos_info)
262
263                                if c != "\"" and num_quotes % 2 != 0:
264                                    break
265
266                                s += c
267                                if c == "\"":
268                                    num_quotes += 1
269
270                            yield s
271
272                        else:
273                            yield c
274                            c = next(reader)
275
276                    elif c == ";":
277                        while c and c != "\n":
278                            c = next(reader)
279                        c = next(reader)
280
281                    else:
282                        # EOF
283                        eof = True
284                        assert len(c) == 0
285                else:
286                    tk = []
287                    while c not in specials:
288                        tk.append(c)
289                        c = next(reader)
290                    yield "".join(tk)
291        except StopIteration:
292            # No more data to read, close generator
293            return
294
295    def char_iterator(self, handle):
296        c = handle.read(1)
297        while c:
298            if c == "\n":
299                self.__row_cnt += 1
300                self.__col_cnt = 0
301            elif c == "\r":
302                pass
303            else:
304                self.__col_cnt += 1
305            yield c
306            c = handle.read(1)
307
308
309# EOC Tokenizer
310
311
312class SmtLibParser(object):
313    """Parse an SmtLib file and builds an SmtLibScript object.
314
315    The main function is get_script (and its wrapper
316    get_script_fname).  This function relies on the tokenizer function
317    (to split the inputs in token) that is consumed by the get_command
318    function that returns a SmtLibCommand for each command in the
319    original file.
320
321    If the interactive flag is True, the file reading proceeds
322    char-by-char with no buffering. This is useful for interactive use
323    for example with a SMT-Lib2-compliant solver
324    """
325
326    def __init__(self, environment=None, interactive=False):
327        self.env = get_env() if environment is None else environment
328        self.interactive = interactive
329
330        # Placeholders for fields filled by self._reset
331        self.cache = None
332        self.logic = None
333        self._reset()
334
335        mgr = self.env.formula_manager
336
337        # Fixing the issue with integer/real numbers on arithmetic
338        # operators.
339        #
340        # We try to apply the operator as it is, in case of failure,
341        # we try to interpret as reals the constant operands that are
342        # integers
343        def fix_real(op, *args):
344            try:
345                return op(*args)
346            except PysmtTypeError:
347                get_type = self.env.stc.get_type
348                get_free_variables = self.env.fvo.get_free_variables
349                new_args = []
350                for x in args:
351                    if get_type(x).is_int_type() and\
352                       len(get_free_variables(x)) == 0:
353                        new_args.append(mgr.ToReal(x))
354                    else:
355                        new_args.append(x)
356                if args == new_args:
357                    raise
358                return op(*new_args)
359
360        self.LT = functools.partial(fix_real, mgr.LT)
361        self.GT = functools.partial(fix_real, mgr.GT)
362        self.LE = functools.partial(fix_real, mgr.LE)
363        self.GE = functools.partial(fix_real, mgr.GE)
364        self.Equals = functools.partial(fix_real, mgr.Equals)
365        self.EqualsOrIff = functools.partial(fix_real, mgr.EqualsOrIff)
366        self.Plus = functools.partial(fix_real, mgr.Plus)
367        self.Minus = functools.partial(fix_real, mgr.Minus)
368        self.Times = functools.partial(fix_real, mgr.Times)
369        self.Div = functools.partial(fix_real, mgr.Div)
370        self.Ite = functools.partial(fix_real, mgr.Ite)
371        self.AllDifferent = functools.partial(fix_real, mgr.AllDifferent)
372
373        # Tokens representing interpreted functions appearing in expressions
374        # Each token is handled by a dedicated function that takes the
375        # recursion stack, the token stream and the parsed token
376        # Common tokens are handled in the _reset function
377        self.interpreted = {"let" : self._enter_let,
378                            "!" : self._enter_annotation,
379                            "exists" : self._enter_quantifier,
380                            "forall" : self._enter_quantifier,
381                            '+':self._operator_adapter(self.Plus),
382                            '-':self._operator_adapter(self._minus_or_uminus),
383                            '*':self._operator_adapter(self.Times),
384                            '/':self._operator_adapter(self._division),
385                            'pow':self._operator_adapter(mgr.Pow),
386                            '>':self._operator_adapter(self.GT),
387                            '<':self._operator_adapter(self.LT),
388                            '>=':self._operator_adapter(self.GE),
389                            '<=':self._operator_adapter(self.LE),
390                            '=':self._operator_adapter(self._equals_or_iff),
391                            'not':self._operator_adapter(mgr.Not),
392                            'and':self._operator_adapter(mgr.And),
393                            'or':self._operator_adapter(mgr.Or),
394                            'xor':self._operator_adapter(mgr.Xor),
395                            '=>':self._operator_adapter(mgr.Implies),
396                            '<->':self._operator_adapter(mgr.Iff),
397                            'ite':self._operator_adapter(self.Ite),
398                            'distinct':self._operator_adapter(self.AllDifferent),
399                            'to_real':self._operator_adapter(mgr.ToReal),
400                            'concat':self._operator_adapter(mgr.BVConcat),
401                            'bvnot':self._operator_adapter(mgr.BVNot),
402                            'bvand':self._operator_adapter(mgr.BVAnd),
403                            'bvor':self._operator_adapter(mgr.BVOr),
404                            'bvneg':self._operator_adapter(mgr.BVNeg),
405                            'bvadd':self._operator_adapter(mgr.BVAdd),
406                            'bvmul':self._operator_adapter(mgr.BVMul),
407                            'bvudiv':self._operator_adapter(mgr.BVUDiv),
408                            'bvurem':self._operator_adapter(mgr.BVURem),
409                            'bvshl':self._operator_adapter(mgr.BVLShl),
410                            'bvlshr':self._operator_adapter(mgr.BVLShr),
411                            'bvsub':self._operator_adapter(mgr.BVSub),
412                            'bvult':self._operator_adapter(mgr.BVULT),
413                            'bvxor':self._operator_adapter(mgr.BVXor),
414                            '_':self._smtlib_underscore,
415                            # Extended Functions
416                            'bvnand':self._operator_adapter(mgr.BVNand),
417                            'bvnor':self._operator_adapter(mgr.BVNor),
418                            'bvxnor':self._operator_adapter(mgr.BVXnor),
419                            'bvcomp':self._operator_adapter(mgr.BVComp),
420                            'bvsdiv':self._operator_adapter(mgr.BVSDiv),
421                            'bvsrem':self._operator_adapter(mgr.BVSRem),
422                            'bvsmod':self._operator_adapter(mgr.BVSMod),
423                            'bvashr':self._operator_adapter(mgr.BVAShr),
424                            'bvule':self._operator_adapter(mgr.BVULE),
425                            'bvugt':self._operator_adapter(mgr.BVUGT),
426                            'bvuge':self._operator_adapter(mgr.BVUGE),
427                            'bvslt':self._operator_adapter(mgr.BVSLT),
428                            'bvsle':self._operator_adapter(mgr.BVSLE),
429                            'bvsgt':self._operator_adapter(mgr.BVSGT),
430                            'bvsge':self._operator_adapter(mgr.BVSGE),
431                            # Strings
432                            'str.len':self._operator_adapter(mgr.StrLength),
433                            'str.++':self._operator_adapter(mgr.StrConcat),
434                            'str.at':self._operator_adapter(mgr.StrCharAt),
435                            'str.contains':self._operator_adapter(mgr.StrContains),
436                            'str.indexof':self._operator_adapter(mgr.StrIndexOf),
437                            'str.replace':self._operator_adapter(mgr.StrReplace),
438                            'str.substr':self._operator_adapter(mgr.StrSubstr),
439                            'str.prefixof':self._operator_adapter(mgr.StrPrefixOf),
440                            'str.suffixof':self._operator_adapter(mgr.StrSuffixOf),
441                            'str.to.int':self._operator_adapter(mgr.StrToInt),
442                            'int.to.str':self._operator_adapter(mgr.IntToStr),
443                            'bv2nat':self._operator_adapter(mgr.BVToNatural),
444                            # arrays
445                            'select':self._operator_adapter(mgr.Select),
446                            'store':self._operator_adapter(mgr.Store),
447                            'as':self._enter_smtlib_as,
448                            }
449
450        # Command tokens
451        self.commands = {smtcmd.ASSERT : self._cmd_assert,
452                         smtcmd.CHECK_SAT : self._cmd_check_sat,
453                         smtcmd.CHECK_SAT_ASSUMING : self._cmd_check_sat_assuming,
454                         smtcmd.DECLARE_CONST : self._cmd_declare_const,
455                         smtcmd.DECLARE_FUN : self._cmd_declare_fun,
456                         smtcmd.DECLARE_SORT: self._cmd_declare_sort,
457                         smtcmd.DEFINE_FUN : self._cmd_define_fun,
458                         smtcmd.DEFINE_FUNS_REC : self._cmd_define_funs_rec,
459                         smtcmd.DEFINE_FUN_REC : self._cmd_define_fun_rec,
460                         smtcmd.DEFINE_SORT: self._cmd_define_sort,
461                         smtcmd.ECHO : self._cmd_echo,
462                         smtcmd.EXIT : self._cmd_exit,
463                         smtcmd.GET_ASSERTIONS: self._cmd_get_assertions,
464                         smtcmd.GET_ASSIGNMENT : self._cmd_get_assignment,
465                         smtcmd.GET_INFO: self._cmd_get_info,
466                         smtcmd.GET_MODEL: self._cmd_get_model,
467                         smtcmd.GET_OPTION: self._cmd_get_option,
468                         smtcmd.GET_PROOF: self._cmd_get_proof,
469                         smtcmd.GET_UNSAT_ASSUMPTIONS : self._cmd_get_unsat_assumptions,
470                         smtcmd.GET_UNSAT_CORE: self._cmd_get_unsat_core,
471                         smtcmd.GET_VALUE : self._cmd_get_value,
472                         smtcmd.POP : self._cmd_pop,
473                         smtcmd.PUSH : self._cmd_push,
474                         smtcmd.RESET : self._cmd_reset,
475                         smtcmd.RESET_ASSERTIONS : self._cmd_reset_assertions,
476                         smtcmd.SET_LOGIC : self._cmd_set_logic,
477                         smtcmd.SET_OPTION : self._cmd_set_option,
478                         smtcmd.SET_INFO : self._cmd_set_info,
479                     }
480
481    def _reset(self):
482        """Resets the parser to the initial state"""
483        self.cache = SmtLibExecutionCache()
484        self.logic = None
485        mgr = self.env.formula_manager
486        self.cache.update({'false':mgr.FALSE(), 'true':mgr.TRUE()})
487
488    def _minus_or_uminus(self, *args):
489        """Utility function that handles both unary and binary minus"""
490        mgr = self.env.formula_manager
491        if len(args) == 1:
492            lty = self.env.stc.get_type(args[0])
493            mult = None
494            if lty == self.env.type_manager.INT():
495                if args[0].is_int_constant():
496                    return mgr.Int(-1 * args[0].constant_value())
497                mult = mgr.Int(-1)
498            else:
499                if args[0].is_real_constant():
500                    return mgr.Real(-1 * args[0].constant_value())
501                mult = mgr.Real(-1)
502            return mgr.Times(mult, args[0])
503        else:
504            assert len(args) == 2
505            return self.Minus(args[0], args[1])
506
507    def _enter_smtlib_as(self, stack, tokens, key):
508        """Utility function that handles 'as' that is a special function in SMTLIB"""
509        #pylint: disable=unused-argument
510        const = self.parse_atom(tokens, "expression")
511        if const != "const":
512            raise PysmtSyntaxError("expected 'const' in expression after 'as'",
513                                   tokens.pos_info)
514        ty = self.parse_type(tokens, "expression")
515
516        def res(expr):
517            return self.env.formula_manager.Array(ty.index_type, expr)
518        def handler():
519            return res
520        stack[-1].append(handler)
521
522    def _smtlib_underscore(self, stack, tokens, key):
523        #pylint: disable=unused-argument
524        """Utility function that handles _ special function in SMTLIB"""
525        mgr = self.env.formula_manager
526
527        op = self.parse_atom(tokens, "expression")
528
529        fun = None
530        if op == "extract":
531            send = self.parse_atom(tokens, "expression")
532            sstart = self.parse_atom(tokens, "expression")
533            try:
534                start = int(sstart)
535                end = int(send)
536            except ValueError:
537                raise PysmtSyntaxError("Expected number in '_ extract' "
538                                       "expression", tokens.pos_info)
539            fun = lambda x : mgr.BVExtract(x, start, end)
540
541        elif op == "zero_extend":
542            swidth = self.parse_atom(tokens, "expression")
543            try:
544                width = int(swidth)
545            except ValueError:
546                raise PysmtSyntaxError("Expected number in '_ zero_extend' "
547                                       "expression", tokens.pos_info)
548            fun = lambda x: mgr.BVZExt(x, width)
549
550        elif op == "repeat":
551            scount = self.parse_atom(tokens, "expression")
552            try:
553                count = int(scount)
554            except ValueError:
555                raise PysmtSyntaxError("Expected number in '_ repeat' "
556                                       "expression", tokens.pos_info)
557            fun = lambda x: mgr.BVRepeat(x, count)
558
559        elif op == "rotate_left":
560            sstep = self.parse_atom(tokens, "expression")
561            try:
562                step = int(sstep)
563            except ValueError:
564                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
565                                       "expression", tokens.pos_info)
566            fun = lambda x: mgr.BVRol(x, step)
567
568        elif op == "rotate_right":
569            sstep = self.parse_atom(tokens, "expression")
570            try:
571                step = int(sstep)
572            except ValueError:
573                raise PysmtSyntaxError("Expected number in '_ rotate_left' "
574                                       "expression", tokens.pos_info)
575            fun = lambda x: mgr.BVRor(x, step)
576
577        elif op == "sign_extend":
578            swidth = self.parse_atom(tokens, "expression")
579            try:
580                width = int(swidth)
581            except ValueError:
582                raise PysmtSyntaxError("Expected number in '(_ sign_extend) "
583                                       "expression'", tokens.pos_info)
584            fun = lambda x: mgr.BVSExt(x, width)
585
586        elif op.startswith("bv"):
587            try:
588                v = int(op[2:])
589                width = int(self.parse_atom(tokens, "expression"))
590            except ValueError:
591                raise PysmtSyntaxError("Expected number in '_ bv' expression: "
592                                       "'%s'" % op, tokens.pos_info)
593            fun = mgr.BV(v, width)
594
595        else:
596            raise PysmtSyntaxError("Unexpected '_' expression '%s'" % op,
597                                   tokens.pos_info)
598
599        stack[-1].append(lambda : fun)
600
601    def _equals_or_iff(self, left, right):
602        """Utility function that treats = between booleans as <->"""
603        mgr = self.env.formula_manager
604        lty = self.env.stc.get_type(left)
605        if lty == self.env.type_manager.BOOL():
606            return mgr.Iff(left, right)
607        else:
608            return self.Equals(left, right)
609
610    def _division(self, left, right):
611        """Utility function that builds a division"""
612        mgr = self.env.formula_manager
613        if left.is_constant() and right.is_constant():
614            return mgr.Real(Fraction(left.constant_value()) / \
615                            Fraction(right.constant_value()))
616        return self.Div(left, right)
617
618    def _get_var(self, name, type_name):
619        """Returns the PySMT variable corresponding to a declaration"""
620        return self.env.formula_manager.Symbol(name=name,
621                                               typename=type_name)
622
623    def _get_quantified_var(self, name, type_name):
624        """Returns the PySMT variable corresponding to a declaration"""
625        try:
626            return self._get_var(name, type_name)
627        except PysmtTypeError:
628            return self.env.formula_manager.FreshSymbol(typename=type_name,
629                                                        template=name+"%d")
630
631    def atom(self, token, mgr):
632        """
633        Given a token and a FormulaManager, returns the pysmt representation of
634        the token
635        """
636        res = self.cache.get(token)
637        if res is None:
638            if token.startswith("#"):
639                # it is a BitVector
640                value = None
641                width = None
642                if token[1] == "b":
643                    # binary
644                    width = len(token) - 2
645                    value = int("0" + token[1:], 2)
646                else:
647                    if token[1] != "x":
648                        raise PysmtSyntaxError("Invalid bit-vector constant "
649                                               "'%s'" % token)
650                    width = (len(token) - 2) * 4
651                    value = int("0" + token[1:], 16)
652                res = mgr.BV(value, width)
653            elif token[0] == '"':
654                # String constant
655                val = token[1:-1]
656                val = val.replace('""', '"')
657                res = mgr.String(val)
658            else:
659                # it could be a number or a string
660                try:
661                    frac = Fraction(token)
662                    if frac.denominator == 1:
663                        # We found an integer, depending on the logic this can be
664                        # an Int or a Real
665                        if self.logic is None or \
666                           self.logic.theory.integer_arithmetic:
667                            if "." in token:
668                                res = mgr.Real(frac)
669                            else:
670                                res = mgr.Int(frac.numerator)
671                        else:
672                            res = mgr.Real(frac)
673                    else:
674                        res = mgr.Real(frac)
675
676                except ValueError:
677                    # a string constant
678                    res = token
679            self.cache.bind(token, res)
680        return res
681
682    def _exit_let(self, varlist, bdy):
683        """ Cleans the execution environment when we exit the scope of a 'let' """
684        for k in varlist:
685            self.cache.unbind(k)
686        return bdy
687
688    def _exit_quantifier(self, fun, vrs, body):
689        """
690        Cleans the execution environment when we exit the scope of a quantifier
691        """
692        variables = set()
693        for vname, var in vrs:
694            self.cache.unbind(vname)
695            variables.add(var)
696        return fun(variables, body)
697
698    def _enter_let(self, stack, tokens, key):
699        """Handles a let expression by recurring on the expression and
700        updating the cache
701        """
702        #pylint: disable=unused-argument
703        self.consume_opening(tokens, "expression")
704        newvals = {}
705        current = "("
706        self.consume_opening(tokens, "expression")
707        while current != ")":
708            if current != "(":
709                raise PysmtSyntaxError("Expected '(' in let binding",
710                                       tokens.pos_info)
711            vname = self.parse_atom(tokens, "expression")
712            expr = self.get_expression(tokens)
713            newvals[vname] = expr
714            self.cache.bind(vname, expr)
715            self.consume_closing(tokens, "expression")
716            current = tokens.consume()
717
718        stack[-1].append(self._exit_let)
719        stack[-1].append(newvals.keys())
720
721    def _operator_adapter(self, operator):
722        """Handles generic operator"""
723        def res(stack, tokens, key):
724            #pylint: disable=unused-argument
725            stack[-1].append(operator)
726        return res
727
728    def _enter_quantifier(self, stack, tokens, key):
729        """Handles quantifiers by defining the bound variable in the cache
730        before parsing the matrix
731        """
732        mgr = self.env.formula_manager
733        vrs = []
734        self.consume_opening(tokens, "expression")
735        current = "("
736        self.consume_opening(tokens, "expression")
737        while current != ")":
738            if current != "(":
739                raise PysmtSyntaxError("Expected '(' in let binding", tokens.pos_info)
740            vname = self.parse_atom(tokens, "expression")
741            typename = self.parse_type(tokens, "expression")
742
743            var = self._get_quantified_var(vname, typename)
744            self.cache.bind(vname, var)
745            vrs.append((vname, var))
746
747            self.consume_closing(tokens, "expression")
748            current = tokens.consume()
749
750        quant = None
751        if key == 'forall':
752            quant = mgr.ForAll
753        else:
754            quant = mgr.Exists
755
756        stack[-1].append(self._exit_quantifier)
757        stack[-1].append(quant)
758        stack[-1].append(vrs)
759
760    def _enter_annotation(self, stack, tokens, key):
761        """Deals with annotations"""
762        #pylint: disable=unused-argument
763
764        term = self.get_expression(tokens)
765
766        tk = tokens.consume()
767        while tk != ")":
768            if not tk.startswith(":"):
769                raise PysmtSyntaxError("Annotations keyword should start with"
770                                       " colon! Offending token: '%s'" % tk,
771                                       tokens.pos_info)
772            keyword = tk[1:]
773            tk = tokens.consume()
774            value = None
775            if tk == "(":
776                counter = 1
777                buff = [tk]
778                while counter != 0:
779                    tk = tokens.raw_read()
780                    if tk == "(":
781                        counter += 1
782                    elif tk == ")":
783                        counter -= 1
784                    buff.append(tk)
785                value = "".join(buff)
786            else:
787                value = tk
788            tk = tokens.consume()
789            self.cache.annotations.add(term, keyword, value)
790
791        assert len(stack[-1]) == 0
792        # re-add the ")" to the tokenizer because we consumed it, but
793        # get_expression needs it
794        tokens.add_extra_token(")")
795        stack[-1].append(lambda : term)
796
797    def get_expression(self, tokens):
798        """
799        Returns the pysmt representation of the given parsed expression
800        """
801        mgr = self.env.formula_manager
802        stack = []
803
804        try:
805            while True:
806                tk = tokens.consume_maybe()
807
808                if tk == "(":
809                    while tk == "(":
810                        stack.append([])
811                        tk = tokens.consume()
812
813                    if tk in self.interpreted:
814                        fun = self.interpreted[tk]
815                        fun(stack, tokens, tk)
816                    else:
817                        stack[-1].append(self.atom(tk, mgr))
818
819                elif tk == ")":
820                    try:
821                        lst = stack.pop()
822                        fun = lst.pop(0)
823                    except IndexError:
824                        raise PysmtSyntaxError("Unexpected ')'",
825                                               tokens.pos_info)
826
827                    try:
828                        res = fun(*lst)
829                    except TypeError as err:
830                        if not callable(fun):
831                            raise NotImplementedError("Unknown function '%s'" % fun)
832                        raise err
833
834                    if len(stack) > 0:
835                        stack[-1].append(res)
836                    else:
837                        return res
838
839                else:
840                    try:
841                        stack[-1].append(self.atom(tk, mgr))
842                    except IndexError:
843                        return self.atom(tk, mgr)
844        except StopIteration:
845            # No more data when trying to consume tokens
846            return
847
848    def get_script(self, script):
849        """
850        Takes a file object and returns a SmtLibScript object representing
851        the file
852        """
853        self._reset() # prepare the parser
854        res = SmtLibScript()
855        for cmd in self.get_command_generator(script):
856            res.add_command(cmd)
857        res.annotations = self.cache.annotations
858        return res
859
860    def get_command_generator(self, script):
861        """Returns a python generator of SmtLibCommand's given a file object
862        to read from
863
864        This function can be used interactively, and blocks until a
865        whole command is read from the script.
866
867        """
868        tokens = Tokenizer(script, interactive=self.interactive)
869        for cmd in self.get_command(tokens):
870            yield cmd
871        return
872
873    def get_script_fname(self, script_fname):
874        """Given a filename and a Solver, executes the solver on the file."""
875        with open_(script_fname) as script:
876            return self.get_script(script)
877
878    def parse_atoms(self, tokens, command, min_size, max_size=None):
879        """
880        Parses a sequence of N atoms (min_size <= N <= max_size) consuming
881        the tokens
882        """
883        if max_size is None:
884            max_size = min_size
885
886        res = []
887        current = None
888        for _ in xrange(min_size):
889            current = tokens.consume("Unexpected end of stream in %s "
890                                             "command." % command)
891            if current == ")":
892                raise PysmtSyntaxError("Expected at least %d arguments in "
893                                       "%s command." %\
894                                       (min_size, command),
895                                       tokens.pos_info)
896            if current == "(":
897                raise PysmtSyntaxError("Unexpected token '(' in %s "
898                                       "command." % command,
899                                       tokens.pos_info)
900            res.append(current)
901        for _ in xrange(min_size, max_size + 1):
902            current = tokens.consume("Unexpected end of stream in %s "
903                                             "command." % command)
904            if current == ")":
905                return res
906            if current == "(":
907                raise PysmtSyntaxError("Unexpected token '(' in %s "
908                                       "command." % command,
909                                       tokens.pos_info)
910            res.append(current)
911        raise PysmtSyntaxError("Unexpected token '%s' in %s command. Expected " \
912                               "at most %d arguments." %\
913                               (current, command, max_size),
914                               tokens.pos_info)
915
916    def parse_type(self, tokens, command, type_params=None, additional_token=None):
917        """Parses a single type name from the tokens"""
918        if additional_token is not None:
919            var = additional_token
920        else:
921            var = tokens.consume("Unexpected end of stream in %s command." % \
922                                         command)
923        res = None
924        if type_params and var in type_params:
925            return (var,) # This is a type parameter, it is handled recursively
926        elif var == "(":
927            op = tokens.consume("Unexpected end of stream in %s command." % \
928                                        command)
929            if op == "Array":
930                idxtype = self.parse_type(tokens, command)
931                elemtype = self.parse_type(tokens, command)
932                self.consume_closing(tokens, command)
933                res = self.env.type_manager.ArrayType(idxtype, elemtype)
934
935            elif op == "_":
936                ts = tokens.consume("Unexpected end of stream in %s command." % \
937                                            command)
938                if ts != "BitVec":
939                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
940                                           (ts, command),
941                                           tokens.pos_info)
942
943                size = 0
944                dim = tokens.consume()
945                try:
946                    size = int(dim)
947                except ValueError:
948                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
949                                           (dim, command),
950                                           tokens.pos_info)
951
952                self.consume_closing(tokens, command)
953                res = self.env.type_manager.BVType(size)
954            else:
955                # It must be a custom-defined type
956                base_type = self.cache.get(op)
957                if base_type is None or not isinstance(base_type, _TypeDecl):
958                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
959                                           (op, command),
960                                           tokens.pos_info)
961                pparams = []
962                has_free_params = False
963                for _ in range(base_type.arity):
964                    ty = self.parse_type(tokens, command, type_params=type_params)
965                    pparams.append(ty)
966                    if isinstance(ty, tuple):
967                        has_free_params = True
968                if has_free_params:
969                    def definition(*args):
970                        params = []
971                        for x in pparams:
972                            if isinstance(x, tuple):
973                                params.append(args[type_params.index(x[0])])
974                            else:
975                                params.append(x)
976                        return self.env.type_manager.get_type_instance(base_type, *params)
977                    res = PartialType("tmp", definition)
978                else:
979                    res = self.env.type_manager.get_type_instance(base_type, *pparams)
980                self.consume_closing(tokens, command)
981        elif var == "Bool":
982            res = self.env.type_manager.BOOL()
983        elif var == "Int":
984            res = self.env.type_manager.INT()
985        elif var == "Real":
986            res = self.env.type_manager.REAL()
987        elif var == "String":
988            res = self.env.type_manager.STRING()
989        else:
990            cached = self.cache.get(var)
991            if cached is not None:
992                res = self.cache.get(var)
993            else:
994                raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
995                                       (var, command),
996                                       tokens.pos_info)
997
998        if isinstance(res, _TypeDecl):
999            return res()
1000        else:
1001            return res
1002
1003
1004    def parse_atom(self, tokens, command):
1005        """Parses a single name from the tokens"""
1006        var = tokens.consume("Unexpected end of stream in %s command." % \
1007                                     command)
1008        if var == "(" or var == ")":
1009            raise PysmtSyntaxError("Unexpected token '%s' in %s command." % \
1010                                   (var, command),
1011                                   tokens.pos_info)
1012        return var
1013
1014    def parse_params(self, tokens, command):
1015        """Parses a list of types from the tokens"""
1016        self.consume_opening(tokens, command)
1017        current = tokens.consume("Unexpected end of stream in %s command." % \
1018                                         command)
1019        res = []
1020        while current != ")":
1021            res.append(self.parse_type(tokens, command, additional_token=current))
1022            current = tokens.consume("Unexpected end of stream in %s command." % \
1023                                             command)
1024        return res
1025
1026    def parse_named_params(self, tokens, command):
1027        """Parses a list of names and type from the tokens"""
1028        self.consume_opening(tokens, command)
1029        current = tokens.consume("Unexpected end of stream in %s command." % \
1030                                         command)
1031        res = []
1032        while current != ")":
1033            vname = self.parse_atom(tokens, command)
1034            typename = self.parse_type(tokens, command)
1035            res.append((vname, typename))
1036            self.consume_closing(tokens, command)
1037            current = tokens.consume("Unexpected end of stream in %s command." % \
1038                                             command)
1039        return res
1040
1041    def parse_expr_list(self, tokens, command):
1042        """Parses a list of expressions form the tokens"""
1043        self.consume_opening(tokens, command)
1044        res = []
1045        while True:
1046            try:
1047                current = self.get_expression(tokens)
1048                res.append(current)
1049            except PysmtSyntaxError:
1050                return res
1051
1052    def consume_opening(self, tokens, command):
1053        """ Consumes a single '(' """
1054        try:
1055            p = tokens.consume_maybe()
1056        except StopIteration:
1057            raise #Re-raise execption for higher-level management, see get_command()
1058        if p != "(":
1059            raise PysmtSyntaxError("Unexpected token '%s' in %s command. " \
1060                                   "Expected '('" %
1061                                   (p, command), tokens.pos_info)
1062
1063    def consume_closing(self, tokens, command):
1064        """ Consumes a single ')' """
1065        p = tokens.consume("Unexpected end of stream. Expected ')'")
1066        if p != ")":
1067            raise PysmtSyntaxError("Unexpected token '%s' in %s command. " \
1068                                   "Expected ')'" %
1069                                   (p, command), tokens.pos_info)
1070
1071    def _function_call_helper(self, v, *args):
1072        """ Helper function for dealing with function calls """
1073        return self.env.formula_manager.Function(v, args)
1074
1075    def get_assignment_list(self, script):
1076        """
1077        Parse an assignment list produced by get-model and get-value
1078        commands in SmtLib
1079        """
1080        symbols = self.env.formula_manager.symbols
1081        self.cache.update(symbols)
1082        tokens = Tokenizer(script, interactive=self.interactive)
1083        res = []
1084        self.consume_opening(tokens, "<main>")
1085        current = tokens.consume()
1086        while current != ")":
1087            if current != "(":
1088                raise PysmtSyntaxError("'(' expected", tokens.pos_info)
1089            vname = self.get_expression(tokens)
1090            expr = self.get_expression(tokens)
1091            self.consume_closing(tokens, current)
1092            res.append((vname, expr))
1093            current = tokens.consume()
1094        self.cache.unbind_all(symbols)
1095        return res
1096
1097    def get_command(self, tokens):
1098        """Builds an SmtLibCommand instance out of a parsed term."""
1099        while True:
1100            try:
1101                self.consume_opening(tokens, "<main>")
1102            except StopIteration:
1103                # No openings
1104                return
1105            current = tokens.consume()
1106            if current in self.commands:
1107                fun = self.commands[current]
1108                yield fun(current, tokens)
1109            else:
1110                raise UnknownSmtLibCommandError(current)
1111
1112    def _cmd_not_implemented(self, current, tokens):
1113        raise NotImplementedError("'%s' has not been implemented yet" % current)
1114
1115    def _cmd_set_info(self, current, tokens):
1116        """(set-info <attribute>)"""
1117        elements = self.parse_atoms(tokens, current, 2)
1118        return SmtLibCommand(current, elements)
1119
1120    def _cmd_set_option(self, current, tokens):
1121        """(set-option <option>)"""
1122        elements = self.parse_atoms(tokens, current, 2)
1123        return SmtLibCommand(current, elements)
1124
1125    def _cmd_assert(self, current, tokens):
1126        """(assert <term>)"""
1127        expr = self.get_expression(tokens)
1128        self.consume_closing(tokens, current)
1129        return SmtLibCommand(current, [expr])
1130
1131    def _cmd_check_sat(self, current, tokens):
1132        """(check-sat)"""
1133        self.parse_atoms(tokens, current, 0)
1134        return SmtLibCommand(current, [])
1135
1136    def _cmd_push(self, current, tokens):
1137        """(push <numeral>)"""
1138        elements = self.parse_atoms(tokens, current, 0, 1)
1139        levels = 1
1140        if len(elements) > 0:
1141            levels = int(elements[0])
1142        return SmtLibCommand(current, [levels])
1143
1144    def _cmd_pop(self, current, tokens):
1145        """(pop <numeral>)"""
1146        elements = self.parse_atoms(tokens, current, 0, 1)
1147        levels = 1
1148        if len(elements) > 0:
1149            levels = int(elements[0])
1150        return SmtLibCommand(current, [levels])
1151
1152    def _cmd_exit(self, current, tokens):
1153        """(exit)"""
1154        self.parse_atoms(tokens, current, 0)
1155        return SmtLibCommand(current, [])
1156
1157    def _cmd_set_logic(self, current, tokens):
1158        """(set-logic <symbol>)"""
1159        elements = self.parse_atoms(tokens, current, 1)
1160        name = elements[0]
1161        try:
1162            self.logic = get_logic_by_name(name)
1163            return SmtLibCommand(current, [self.logic])
1164        except UndefinedLogicError:
1165            warn("Unknown logic '" + name + \
1166                 "'. Ignoring set-logic command.")
1167            return SmtLibCommand(current, [None])
1168
1169    def _cmd_declare_const(self, current, tokens):
1170        """(declare-const <symbol> <sort>)"""
1171        var = self.parse_atom(tokens, current)
1172        typename = self.parse_type(tokens, current)
1173        self.consume_closing(tokens, current)
1174        v = self._get_var(var, typename)
1175        self.cache.bind(var, v)
1176        return SmtLibCommand(current, [v])
1177
1178    def _cmd_get_value(self, current, tokens):
1179        """(get-value (<term>+)"""
1180        params = self.parse_expr_list(tokens, current)
1181        self.consume_closing(tokens, current)
1182        return SmtLibCommand(current, params)
1183
1184    def _cmd_declare_fun(self, current, tokens):
1185        """(declare-fun <symbol> (<sort>*) <sort>)"""
1186        var = self.parse_atom(tokens, current)
1187        params = self.parse_params(tokens, current)
1188        typename = self.parse_type(tokens, current)
1189        self.consume_closing(tokens, current)
1190
1191        if params:
1192            typename = self.env.type_manager.FunctionType(typename, params)
1193
1194        v = self._get_var(var, typename)
1195        if v.symbol_type().is_function_type():
1196            self.cache.bind(var, \
1197                    functools.partial(self._function_call_helper, v))
1198        else:
1199            self.cache.bind(var, v)
1200        return SmtLibCommand(current, [v])
1201
1202    def _cmd_define_fun(self, current, tokens):
1203        """(define-fun <fun_def>)"""
1204        formal = []
1205        var = self.parse_atom(tokens, current)
1206        namedparams = self.parse_named_params(tokens, current)
1207        rtype = self.parse_type(tokens, current)
1208        bindings = []
1209        for (x,t) in namedparams:
1210            v = self.env.formula_manager.FreshSymbol(typename=t,
1211                                                        template="__"+x+"%d")
1212            self.cache.bind(x, v)
1213            formal.append(v) #remember the variable
1214            bindings.append(x) #remember the name
1215        # Parse expression using also parameters
1216        ebody = self.get_expression(tokens)
1217        #Discard parameters
1218        for x in bindings:
1219            self.cache.unbind(x)
1220        # Finish Parsing
1221        self.consume_closing(tokens, current)
1222        self.cache.define(var, formal, ebody)
1223        return SmtLibCommand(current, [var, formal, rtype, ebody])
1224
1225    def _cmd_declare_sort(self, current, tokens):
1226        """(declare-sort <symbol> <numeral>)"""
1227        (typename, arity) = self.parse_atoms(tokens, current, 2)
1228        try:
1229            type_ = self.env.type_manager.Type(typename, int(arity))
1230        except ValueError:
1231            raise PysmtSyntaxError("Expected an integer as arity of type %s."%\
1232                                   typename, tokens.pos_info)
1233        self.cache.bind(typename, type_)
1234        return SmtLibCommand(current, [type_])
1235
1236    def _cmd_define_sort(self, current, tokens):
1237        """(define-sort <name> <args> <fun_def>)"""
1238        name = self.parse_atom(tokens, current)
1239        self.consume_opening(tokens, current)
1240
1241        params = []
1242        cur = tokens.consume()
1243        while cur != ')':
1244            params.append(cur)
1245            cur = tokens.consume()
1246
1247        rtype = self.parse_type(tokens, current, type_params=params)
1248        if isinstance(rtype, PartialType):
1249            rtype.name = name
1250        elif isinstance(rtype, tuple):
1251            def definition(*args):
1252                return args[params.index(rtype[0])]
1253            rtype = PartialType(name, definition)
1254        self.consume_closing(tokens, current)
1255        self.cache.define(name, [], rtype)
1256        return SmtLibCommand(current, [name, [], rtype])
1257
1258    def _cmd_get_assertions(self, current, tokens):
1259        """(get-assertions)"""
1260        self.parse_atoms(tokens, current, 0)
1261        return SmtLibCommand(current, [])
1262
1263    def _cmd_get_info(self, current, tokens):
1264        """(get-info <info_flag>)"""
1265        keyword = self.parse_atoms(tokens, current, 1)
1266        return SmtLibCommand(current, keyword)
1267
1268    def _cmd_get_model(self, current, tokens):
1269        """(get-model)"""
1270        self.parse_atoms(tokens, current, 0)
1271        return SmtLibCommand(current, [])
1272
1273    def _cmd_get_option(self, current, tokens):
1274        """(get-option <keyword>)"""
1275        keyword = self.parse_atoms(tokens, current, 1)
1276        return SmtLibCommand(current, keyword)
1277
1278    def _cmd_get_proof(self, current, tokens):
1279        """(get-proof)"""
1280        self.parse_atoms(tokens, current, 0)
1281        return SmtLibCommand(current, [])
1282
1283    def _cmd_get_unsat_core(self, current, tokens):
1284        """(get-unsat-core)"""
1285        self.parse_atoms(tokens, current, 0)
1286        return SmtLibCommand(current, [])
1287
1288    def _cmd_check_sat_assuming(self, current, tokens):
1289        """(check-sat-assuming (<prop_literal>*) ) """
1290        params = self.parse_expr_list(tokens, current)
1291        self.consume_closing(tokens, current)
1292        return SmtLibCommand(current, params)
1293
1294    def _cmd_define_fun_rec(self, current, tokens):
1295        """(define-fun-rec <fun_def>)"""
1296        return self._cmd_not_implemented(current, tokens)
1297
1298    def _cmd_define_funs_rec(self, current, tokens):
1299        """(define-funs-rec (<fun_dec>^{n+1}) (<term>^{n+1>))"""
1300        return self._cmd_not_implemented(current, tokens)
1301
1302    def _cmd_echo(self, current, tokens):
1303        """(echo <string>)"""
1304        elements = self.parse_atoms(tokens, current, 1)
1305        return SmtLibCommand(current, elements)
1306
1307    def _cmd_get_assignment(self, current, tokens):
1308        """(get-assignment)"""
1309        self.parse_atoms(tokens, current, 0)
1310        return SmtLibCommand(current, [])
1311
1312    def _cmd_get_unsat_assumptions(self, current, tokens):
1313        """(get-unsat-assumptions)"""
1314        self.parse_atoms(tokens, current, 0)
1315        return SmtLibCommand(current, [])
1316
1317    def _cmd_reset(self, current, tokens):
1318        """(reset)"""
1319        self.parse_atoms(tokens, current, 0)
1320        return SmtLibCommand(current, [])
1321
1322    def _cmd_reset_assertions(self, current, tokens):
1323        """(reset-assertions)"""
1324        self.parse_atoms(tokens, current, 0)
1325        return SmtLibCommand(current, [])
1326
1327# EOC SmtLibParser
1328
1329
1330class SmtLib20Parser(SmtLibParser):
1331    """Parser for SMT-LIB 2.0."""
1332
1333    def __init__(self, environment=None, interactive=False):
1334        SmtLibParser.__init__(self, environment, interactive)
1335
1336        # Remove commands that were introduced in SMT-LIB 2.5
1337        del self.commands["check-sat-assuming"]
1338        del self.commands["declare-const"]
1339        del self.commands["define-fun-rec"]
1340        del self.commands["define-funs-rec"]
1341        del self.commands["echo"]
1342        del self.commands["get-assignment"]
1343        del self.commands["get-unsat-assumptions"]
1344        del self.commands["reset"]
1345        del self.commands["reset-assertions"]
1346
1347# EOC SmtLib20Parser
1348
1349
1350class SmtLibZ3Parser(SmtLibParser):
1351    """
1352    Parses extended Z3 SmtLib Syntax
1353    """
1354    def __init__(self, environment=None, interactive=False):
1355        SmtLibParser.__init__(self, environment, interactive)
1356
1357        # Z3 prints Pow as "^"
1358        self.interpreted["^"] = self.interpreted["pow"]
1359        self.interpreted["ext_rotate_left"] = \
1360                                self._operator_adapter(self._ext_rotate_left)
1361        self.interpreted["ext_rotate_right"] =\
1362                                self._operator_adapter(self._ext_rotate_right)
1363        mgr = self.env.formula_manager
1364        self.interpreted['bv2int'] = self._operator_adapter(mgr.BVToNatural)
1365
1366    def _ext_rotate_left(self, x, y):
1367        return self.env.formula_manager.BVRol(x, y.simplify().constant_value())
1368
1369    def _ext_rotate_right(self, x, y):
1370        return self.env.formula_manager.BVRor(x, y.simplify().constant_value())
1371
1372# EOC SmtLibZ3Parser
1373