<commit_before>#
# This file is part of pySMT.
#
#   Copyright 2014 <NAME> and <NAME>
#
#   Licensed under the Apache License, Version 2.0 (the "License");
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#       http://www.apache.org/licenses/LICENSE-2.0
#
#   Unless required by applicable law or agreed to in writing, software
#   distributed under the License is distributed on an "AS IS" BASIS,
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#   limitations under the License.
#
from functools import partial

from six.moves import xrange, cStringIO

import pysmt.operators as op
from pysmt.environment import get_env
from pysmt.walkers import TreeWalker, DagWalker, handles
from pysmt.utils import quote


class SmtPrinter(TreeWalker):

    def __init__(self, stream):
        TreeWalker.__init__(self)
        self.stream = stream
        self.write = self.stream.write
        self.mgr = get_env().formula_manager

    def printer(self, f):
        self.walk(f)

    def walk_threshold(self, formula):
        """This is a complete printer"""
        raise NotImplementedError

    def walk_nary(self, formula, operator):
        self.write("(%s" % operator)
        for s in formula.args():
            self.write(" ")
            yield s
        self.write(")")

    def walk_and(self, formula): return self.walk_nary(formula, "and")
    def walk_or(self, formula): return self.walk_nary(formula, "or")
    def walk_not(self, formula): return self.walk_nary(formula, "not")
    def walk_implies(self, formula): return self.walk_nary(formula, "=>")
    def walk_iff(self, formula): return self.walk_nary(formula, "=")
    def walk_plus(self, formula): return self.walk_nary(formula, "+")
    def walk_minus(self, formula): return self.walk_nary(formula, "-")
    def walk_times(self, formula): return self.walk_nary(formula, "*")
    def walk_equals(self, formula): return self.walk_nary(formula, "=")
    def walk_le(self, formula): return self.walk_nary(formula, "<=")
    def walk_lt(self, formula): return self.walk_nary(formula, "<")
    def walk_ite(self, formula): return self.walk_nary(formula, "ite")
    def walk_toreal(self, formula): return self.walk_nary(formula, "to_real")
    def walk_div(self, formula): return self.walk_nary(formula, "/")
    def walk_pow(self, formula): return self.walk_nary(formula, "pow")
    def walk_bv_and(self, formula): return self.walk_nary(formula, "bvand")
    def walk_bv_or(self, formula): return self.walk_nary(formula, "bvor")
    def walk_bv_not(self, formula): return self.walk_nary(formula, "bvnot")
    def walk_bv_xor(self, formula): return self.walk_nary(formula, "bvxor")
    def walk_bv_add(self, formula): return self.walk_nary(formula, "bvadd")
    def walk_bv_sub(self, formula): return self.walk_nary(formula, "bvsub")
    def walk_bv_neg(self, formula): return self.walk_nary(formula, "bvneg")
    def walk_bv_mul(self, formula): return self.walk_nary(formula, "bvmul")
    def walk_bv_udiv(self, formula): return self.walk_nary(formula, "bvudiv")
    def walk_bv_urem(self, formula): return self.walk_nary(formula, "bvurem")
    def walk_bv_lshl(self, formula): return self.walk_nary(formula, "bvshl")
    def walk_bv_lshr(self, formula): return self.walk_nary(formula, "bvlshr")
    def walk_bv_ult(self, formula): return self.walk_nary(formula, "bvult")
    def walk_bv_ule(self, formula): return self.walk_nary(formula, "bvule")
    def walk_bv_slt(self, formula): return self.walk_nary(formula, "bvslt")
    def walk_bv_sle(self, formula): return self.walk_nary(formula, "bvsle")
    def walk_bv_concat(self, formula): return self.walk_nary(formula, "concat")
    def walk_bv_comp(self, formula): return self.walk_nary(formula, "bvcomp")
    def walk_bv_ashr(self, formula): return self.walk_nary(formula, "bvashr")
    def walk_bv_sdiv(self, formula): return self.walk_nary(formula, "bvsdiv")
    def walk_bv_srem(self, formula): return self.walk_nary(formula, "bvsrem")
    def walk_array_select(self, formula): return self.walk_nary(formula, "select")
    def walk_array_store(self, formula): return self.walk_nary(formula, "store")

    def walk_symbol(self, formula):
        self.write(quote(formula.symbol_name()))

    def walk_function(self, formula):
        return self.walk_nary(formula, formula.function_name())

    def walk_int_constant(self, formula):
        if formula.constant_value() < 0:
            self.write("(- " + str(-formula.constant_value()) + ")")
        else:
            self.write(str(formula.constant_value()))

    def walk_real_constant(self, formula):
        if formula.constant_value() < 0:
            template = "(- %s)"
        else:
            template = "%s"

        (n,d) = abs(formula.constant_value().numerator), \
                    formula.constant_value().denominator
        if d != 1:
            res = template % ( "(/ " + str(n) + " " + str(d) + ")" )
        else:
            res = template % (str(n) + ".0")

        self.write(res)

    def walk_bool_constant(self, formula):
        if formula.constant_value():
            self.write("true")
        else:
            self.write("false")

    def walk_bv_constant(self, formula):
        self.write("#b" + formula.bv_bin_str())

    def walk_forall(self, formula):
        return self._walk_quantifier("forall", formula)

    def walk_exists(self, formula):
        return self._walk_quantifier("exists", formula)

    def _walk_quantifier(self, operator, formula):
        assert len(formula.quantifier_vars()) > 0
        self.write("(%s (" % operator)

        for s in formula.quantifier_vars():
            self.write("(")
            yield s
            self.write(" %s)" % s.symbol_type().as_smtlib(False))

        self.write(") ")
        yield formula.arg(0)
        self.write(")")

    def walk_bv_extract(self, formula):
        self.write("((_ extract %d %d) " % (formula.bv_extract_end(),
                                            formula.bv_extract_start()))
        yield formula.arg(0)
        self.write(")")

    @handles(op.BV_ROR, op.BV_ROL)
    def walk_bv_rotate(self, formula):
        if formula.is_bv_ror():
            rotate_type = "rotate_right"
        else:
            assert formula.is_bv_rol()
            rotate_type = "rotate_left"
        self.write("((_ %s %d ) " % (rotate_type,
                                     formula.bv_rotation_step()))
        yield formula.arg(0)
        self.write(")")

    @handles(op.BV_ZEXT, op.BV_SEXT)
    def walk_bv_extend(self, formula):
        if formula.is_bv_zext():
            extend_type = "zero_extend"
        else:
            assert formula.is_bv_sext()
            extend_type = "sign_extend"
        self.write("((_ %s %d ) " % (extend_type,<commit_msg>Remove trailing whitespace from bvrol and bvsext<commit_after>#
# This file is part of pySMT.
#
#   Copyright 2014 <NAME> and <NAME>
#
#   Licensed under the Apache License, Version 2.0 (the "License");
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#       http://www.apache.org/licenses/LICENSE-2.0
#
#   Unless required by applicable law or agreed to in writing, software
#   distributed under the License is distributed on an "AS IS" BASIS,
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#   limitations under the License.
#
from functools import partial

from six.moves import xrange, cStringIO

import pysmt.operators as op
from pysmt.environment import get_env
from pysmt.walkers import TreeWalker, DagWalker, handles
from pysmt.utils import quote


class SmtPrinter(TreeWalker):

    def __init__(self, stream):
        TreeWalker.__init__(self)
        self.stream = stream
        self.write = self.stream.write
        self.mgr = get_env().formula_manager

    def printer(self, f):
        self.walk(f)

    def walk_threshold(self, formula):
        """This is a complete printer"""
        raise NotImplementedError

    def walk_nary(self, formula, operator):
        self.write("(%s" % operator)
        for s in formula.args():
            self.write(" ")
            yield s
        self.write(")")

    def walk_and(self, formula): return self.walk_nary(formula, "and")
    def walk_or(self, formula): return self.walk_nary(formula, "or")
    def walk_not(self, formula): return self.walk_nary(formula, "not")
    def walk_implies(self, formula): return self.walk_nary(formula, "=>")
    def walk_iff(self, formula): return self.walk_nary(formula, "=")
    def walk_plus(self, formula): return self.walk_nary(formula, "+")
    def walk_minus(self, formula): return self.walk_nary(formula, "-")
    def walk_times(self, formula): return self.walk_nary(formula, "*")
    def walk_equals(self, formula): return self.walk_nary(formula, "=")
    def walk_le(self, formula): return self.walk_nary(formula, "<=")
    def walk_lt(self, formula): return self.walk_nary(formula, "<")
    def walk_ite(self, formula): return self.walk_nary(formula, "ite")
    def walk_toreal(self, formula): return self.walk_nary(formula, "to_real")
    def walk_div(self, formula): return self.walk_nary(formula, "/")
    def walk_pow(self, formula): return self.walk_nary(formula, "pow")
    def walk_bv_and(self, formula): return self.walk_nary(formula, "bvand")
    def walk_bv_or(self, formula): return self.walk_nary(formula, "bvor")
    def walk_bv_not(self, formula): return self.walk_nary(formula, "bvnot")
    def walk_bv_xor(self, formula): return self.walk_nary(formula, "bvxor")
    def walk_bv_add(self, formula): return self.walk_nary(formula, "bvadd")
    def walk_bv_sub(self, formula): return self.walk_nary(formula, "bvsub")
    def walk_bv_neg(self, formula): return self.walk_nary(formula, "bvneg")
    def walk_bv_mul(self, formula): return self.walk_nary(formula, "bvmul")
    def walk_bv_udiv(self, formula): return self.walk_nary(formula, "bvudiv")
    def walk_bv_urem(self, formula): return self.walk_nary(formula, "bvurem")
    def walk_bv_lshl(self, formula): return self.walk_nary(formula, "bvshl")
    def walk_bv_lshr(self, formula): return self.walk_nary(formula, "bvlshr")
    def walk_bv_ult(self, formula): return self.walk_nary(formula, "bvult")
    def walk_bv_ule(self, formula): return self.walk_nary(formula, "bvule")
    def walk_bv_slt(self, formula): return self.walk_nary(formula, "bvslt")
    def walk_bv_sle(self, formula): return self.walk_nary(formula, "bvsle")
    def walk_bv_concat(self, formula): return self.walk_nary(formula, "concat")
    def walk_bv_comp(self, formula): return self.walk_nary(formula, "bvcomp")
    def walk_bv_ashr(self, formula): return self.walk_nary(formula, "bvashr")
    def walk_bv_sdiv(self, formula): return self.walk_nary(formula, "bvsdiv")
    def walk_bv_srem(self, formula): return self.walk_nary(formula, "bvsrem")
    def walk_array_select(self, formula): return self.walk_nary(formula, "select")
    def walk_array_store(self, formula): return self.walk_nary(formula, "store")

    def walk_symbol(self, formula):
        self.write(quote(formula.symbol_name()))

    def walk_function(self, formula):
        return self.walk_nary(formula, formula.function_name())

    def walk_int_constant(self, formula):
        if formula.constant_value() < 0:
            self.write("(- " + str(-formula.constant_value()) + ")")
        else:
            self.write(str(formula.constant_value()))

    def walk_real_constant(self, formula):
        if formula.constant_value() < 0:
            template = "(- %s)"
        else:
            template = "%s"

        (n,d) = abs(formula.constant_value().numerator), \
                    formula.constant_value().denominator
        if d != 1:
            res = template % ( "(/ " + str(n) + " " + str(d) + ")" )
        else:
            res = template % (str(n) + ".0")

        self.write(res)

    def walk_bool_constant(self, formula):
        if formula.constant_value():
            self.write("true")
        else:
            self.write("false")

    def walk_bv_constant(self, formula):
        self.write("#b" + formula.bv_bin_str())

    def walk_forall(self, formula):
        return self._walk_quantifier("forall", formula)

    def walk_exists(self, formula):
        return self._walk_quantifier("exists", formula)

    def _walk_quantifier(self, operator, formula):
        assert len(formula.quantifier_vars()) > 0
        self.write("(%s (" % operator)

        for s in formula.quantifier_vars():
            self.write("(")
            yield s
            self.write(" %s)" % s.symbol_type().as_smtlib(False))

        self.write(") ")
        yield formula.arg(0)
        self.write(")")

    def walk_bv_extract(self, formula):
        self.write("((_ extract %d %d) " % (formula.bv_extract_end(),
                                            formula.bv_extract_start()))
        yield formula.arg(0)
        self.write(")")

    @handles(op.BV_ROR, op.BV_ROL)
    def walk_bv_rotate(self, formula):
        if formula.is_bv_ror():
            rotate_type = "rotate_right"
        else:
            assert formula.is_bv_rol()
            rotate_type = "rotate_left"
        self.write("((_ %s %d) " % (rotate_type,
                                     formula.bv_rotation_step()))
        yield formula.arg(0)
        self.write(")")

    @handles(op.BV_ZEXT, op.BV_SEXT)
    def walk_bv_extend(self, formula):
        if formula.is_bv_zext():
            extend_type = "zero_extend"
        else:
            assert formula.is_bv_sext()
            extend_type = "sign_extend"
        self.write("((_ %s %d) " % (extend_type,
{'fraction_non_alphanumeric': 0.12699559344072817, 'fraction_numerical': 0.0023116376507982374, 'mean_word_length': 3.1586061880444576, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5797807', 'n_tokens_mistral': 4665, 'n_tokens_neox': 4390, 'n_words': 1051}