<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 warnings import warn
from six.moves import xrange

from pysmt.exceptions import SolverAPINotFound
from pysmt.constants import Fraction, is_pysmt_fraction, is_pysmt_integer

try:
    import mathsat
except ImportError:
    raise SolverAPINotFound

from pysmt.logics import LRA, QF_UFLIA, QF_UFLRA, QF_BV, PYSMT_QF_LOGICS
from pysmt.oracles import get_logic

import pysmt.operators as op
from pysmt import typing as types
from pysmt.solvers.solver import (IncrementalTrackingSolver, UnsatCoreSolver,
                                  Model, Converter, SolverOptions)
from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
from pysmt.walkers import DagWalker
from pysmt.exceptions import (SolverReturnedUnknownResultError,
                              SolverNotConfiguredForUnsatCoresError,
                              SolverStatusError,
                              InternalSolverError,
                              NonLinearError, PysmtValueError, PysmtTypeError)
from pysmt.decorators import clear_pending_pop, catch_conversion_error
from pysmt.solvers.qelim import QuantifierEliminator
from pysmt.solvers.interpolation import Interpolator
from pysmt.walkers.identitydag import IdentityDagWalker


class MSatEnv(object):
    """A wrapper for the msat_env object.

    Objects within pySMT should only reference the msat_environment
    through this object. When calling a function from the underlying
    wrapper, the inner instance of msat_env needs to be used.
    This is done using the __call__ method: e.g.,
       env = MSatEnv()
       mathsat.function(env())
    """
    __slots__ = ['msat_env']

    def __init__(self, msat_config=None):
        if msat_config is None:
            self.msat_env = mathsat.msat_create_env()
        else:
            self.msat_env = mathsat.msat_create_env(msat_config)

    def __del__(self):
        mathsat.msat_destroy_env(self.msat_env)

    def __call__(self):
        return self.msat_env


class MathSAT5Model(Model):
    """Stand-alone model"""

    def __init__(self, environment, msat_env):
        Model.__init__(self, environment)
        self.msat_env = msat_env
        self.converter = MSatConverter(environment, self.msat_env)
        self.msat_model = None

        msat_model = mathsat.msat_get_model(self.msat_env())
        if mathsat.MSAT_ERROR_MODEL(msat_model):
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise InternalSolverError(msat_msg)
        self.msat_model = msat_model

    def __del__(self):
        if self.msat_model is not None:
            mathsat.msat_destroy_model(self.msat_model)
        del self.msat_env

    def get_value(self, formula, model_completion=True):
        titem = self.converter.convert(formula)
        msat_res = mathsat.msat_model_eval(self.msat_model, titem)
        if mathsat.MSAT_ERROR_TERM(msat_res):
            raise InternalSolverError("get model value")
        val = self.converter.back(msat_res)
        if self.environment.stc.get_type(formula).is_real_type() and \
               val.is_int_constant():
            val = self.environment.formula_manager.Real(val.constant_value())
        return val

    def iterator_over(self, language):
        for x in language:
            yield x, self.get_value(x, model_completion=True)

    def __iter__(self):
        """Overloading of iterator from Model.  We iterate only on the
        variables defined in the assignment.
        """
        it = mathsat.msat_model_create_iterator(self.msat_model)
        if mathsat.MSAT_ERROR_MODEL_ITERATOR(it):
            raise InternalSolverError("model iteration")

        while mathsat.msat_model_iterator_has_next(it):
            t, v = mathsat.msat_model_iterator_next(it)
            if mathsat.msat_term_is_constant(self.msat_env(), t):
                pt = self.converter.back(t)
                pv = self.converter.back(v)
                if self.environment.stc.get_type(pt).is_real_type() and \
                       pv.is_int_constant():
                    pv = self.environment.formula_manager.Real(
                        pv.constant_value())
                yield (pt, pv)

        mathsat.msat_destroy_model_iterator(it)

    def __contains__(self, x):
        """Returns whether the model contains a value for 'x'."""
        return x in (v for v, _ in self)

# EOC MathSAT5Model


class MathSATOptions(SolverOptions):

    def __init__(self, **base_options):
        SolverOptions.__init__(self, **base_options)

    @staticmethod
    def _set_option(msat_config, name, value):
        """Sets the given option. Might raise a ValueError."""
        check = mathsat.msat_set_option(msat_config, name, value)
        if check != 0:
            raise PysmtValueError("Error setting the option '%s=%s'" % (name,value))

    def __call__(self, solver):
        if self.generate_models:
            self._set_option(solver.msat_config, "model_generation", "true")

        if self.unsat_cores_mode is not None:
            self._set_option(solver.msat_config, "unsat_core_generation", "1")

        if self.random_seed is not None:
            self._set_option(solver.msat_config,
                             "random_seed", str(self.random_seed))

        for k,v in self.solver_options.items():
            self._set_option(solver.msat_config, str(k), str(v))

        if "debug.api_call_trace_filename" in self.solver_options:
            self._set_option(solver.msat_config, "debug.api_call_trace", "1")

        # Force semantics of division by 0
        self._set_option(solver.msat_config, "theory.bv.div_by_zero_mode", "0")

# EOC MathSATOptions


class MathSAT5Solver(IncrementalTrackingSolver, UnsatCoreSolver,
                     SmtLibBasicSolver, SmtLibIgnoreMixin):

    LOGICS = PYSMT_QF_LOGICS - set(l for l in PYSMT_QF_LOGICS if not l.theory.linear)
    OptionsClass = MathSATOptions

    def __init__(self, environment, logic, **options):
        IncrementalTrackingSolver.__init__(self,
                                           environment=environment,
                                           logic=logic,
                                           **options)

        self.msat_config = mathsat.msat_create_default_config(str(logic))
        self.options(self)
        self.msat_env = MSatEnv(self.msat_config)
        mathsat.msat_destroy_config(self.msat_config)
        self.converter = MSatConverter(environment, self.msat_env)

        # Shortcuts
        self.realType = mathsat.msat_get_rational_type(self.msat_env())
        self.intType = mathsat.msat_get_integer_type(self.msat_env())
        self.boolType = mathsat.msat_get_bool_type(self.msat_env())
        self.mgr = environment.formula_manager

    @clear_pending_pop
    def _reset_assertions(self):
        mathsat.msat_reset_env(self.msat_env())

    @clear_pending_pop
    def declare_variable(self, var):
        raise NotImplementedError

    @clear_pending_pop
    def _add_assertion(self, formula, named=None):
        self._assert_is_boolean(formula)

        result = formula
        if self.options.unsat_cores_mode == "named":
            # If we want named unsat cores, we need to rewrite the
            # formulae as implications
            key = self.mgr.FreshSymbol(template="_assertion_%d")
            result = (key, named, formula)
            formula = self.mgr.Implies(key, formula)

        term = self.converter.convert(formula)
        res = mathsat.msat_assert_formula(self.msat_env(), term)

        if res != 0:
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise InternalSolverError(msat_msg)

        return result

    def _named_assertions(self):
        if self.options.unsat_cores_mode == "named":
            return [t[0] for t in self.assertions]
        return None

    def _named_assertions_map(self):
        if self.options.unsat_cores_mode == "named":
            return dict((t[0], (t[1],t[2])) for t in self.assertions)
        return None

    @clear_pending_pop
    def _solve(self, assumptions=None):
        res = None

        n_ass = self._named_assertions()
        if n_ass is not None and len(n_ass) > 0:
            if assumptions is None:
                assumptions = n_ass
            else:
                assumptions += n_ass

        if assumptions is not None:
            bool_ass = []
            other_ass = []
            for x in assumptions:
                if x.is_literal():
                    bool_ass.append(self.converter.convert(x))
                else:
                    other_ass.append(x)

            if len(other_ass) > 0:
                self.push()
                self.add_assertion(self.mgr.And(other_ass))
                self.pending_pop = True

            if len(bool_ass) > 0:
                res = mathsat.msat_solve_with_assumptions(self.msat_env(), bool_ass)
            else:
                res = mathsat.msat_solve(self.msat_env())

        else:
            res = mathsat.msat_solve(self.msat_env())

        assert res in [mathsat.MSAT_UNKNOWN,mathsat.MSAT_SAT,mathsat.MSAT_UNSAT]
        if res == mathsat.MSAT_UNKNOWN:
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise SolverReturnedUnknownResultError(msat_msg)

        return (res == mathsat.MSAT_SAT)

    def _check_unsat_core_config(self):
        if self.options.unsat_cores_mode is None:
            raise SolverNotConfiguredForUnsatCoresError

        if self.last_result is None or self.last_result:
            raise SolverStatusError("The last call to solve() was not" \
                                    " unsatisfiable")

        if self.last_command != "solve":
            raise SolverStatusError("The solver status has been modified by a" \
                                    " '%s' command after the last call to" \
                                    " solve()" % self.last_command)

    def get_unsat_core(self):
        """After a call to solve() yielding UNSAT, returns the unsat core as a
        set of formulae"""
        self._check_unsat_core_config()
        if self.options.unsat_cores_mode == "all":

            terms = mathsat.msat_get_unsat_core(self.msat_env())
            if terms is None:
                raise InternalSolverError(
                    mathsat.msat_last_error_message(self.msat_env()))
            return set(self.converter.back(t) for t in terms)
        else:
            return self.get_named_unsat_core().values()

    def get_named_unsat_core(self):
        """After a call to solve() yielding UNSAT, returns the unsat core as a
        dict of names to formulae"""
        self._check_unsat_core_config()
        if self.options.unsat_cores_mode == "named":

            assumptions = mathsat.msat_get_unsat_assumptions(self.msat_env())
            pysmt_assumptions = set(self.converter.back(t) for t in assumptions)

            res = {}
            n_ass_map = self._named_assertions_map()
            cnt = 0
            for key in pysmt_assumptions:
                if key in n_ass_map:
                    (name, formula) = n_ass_map[key]
                    if name is None:
                        name = "_a_%d" % cnt
                        cnt += 1
                    res[name] = formula
            return res

        else:
            return dict(("_a%d" % i, f)
                        for i,f in enumerate(self.get_unsat_core()))

    @clear_pending_pop
    def all_sat(self, important, callback):
        self.push()
        mathsat.msat_all_sat(self.msat_env(),
                             [self._var2term(x) for x in important],
                             callback)
        self.pop()

    @clear_pending_pop
    def _push(self, levels=1):
        for _ in xrange(levels):
            mathsat.msat_push_backtrack_point(self.msat_env())

    @clear_pending_pop
    def _pop(self, levels=1):
        for _ in xrange(levels):
            mathsat.msat_pop_backtrack_point(self.msat_env())

    def _var2term(self, var):
        decl = mathsat.msat_find_decl(self.msat_env(), var.symbol_name())
        titem = mathsat.msat_make_term(self.msat_env(), decl, [])
        return titem

    def set_preferred_var(self, var):
        tvar = self.converter.convert(var)
        mathsat.msat_add_preferred_for_branching(self.msat_env(), tvar)
        return

    def print_model(self, name_filter=None):
        if name_filter is not None:
            raise NotImplementedError
        for v in self.converter.symbol_to_decl.keys():
            var = self.mgr.Symbol(v)
            assert var is not None
            print("%s = %s", (v, self.get_value(var)))

    def get_value(self, item):
        self._assert_no_function_type(item)

        titem = self.converter.convert(item)
        tval = mathsat.msat_get_model_value(self.msat_env(), titem)
        val = self.converter.back(tval)
        if self.environment.stc.get_type(item).is_real_type() and \
               val.is_int_constant():
            val = self.mgr.Real(val.constant_value())
        return val

    def get_model(self):
        return MathSAT5Model(self.environment, self.msat_env)

    def _exit(self):
        del self.msat_env


class MSatConverter(Converter, DagWalker):

    def __init__(self, environment, msat_env):
        DagWalker.__init__(self, environment)

        self.msat_env = msat_env
        self.mgr = environment.formula_manager
        self._get_type = environment.stc.get_type

        # Maps a Symbol into the corresponding msat_decl instance in the msat_env
        self.symbol_to_decl = {}
        # Maps a msat_decl instance inside the msat_env into the corresponding
        # Symbol
        self.decl_to_symbol = {}

        self.boolType = mathsat.msat_get_bool_type(self.msat_env())
        self.realType = mathsat.msat_get_rational_type(self.msat_env())
        self.intType = mathsat.msat_get_integer_type(self.msat_env())

        # Back Conversion
        self.back_memoization = {}
        self.back_fun = {
            mathsat.MSAT_TAG_TRUE: lambda term, args: self.mgr.TRUE(),
            mathsat.MSAT_TAG_FALSE:lambda term, args: self.mgr.FALSE(),
            mathsat.MSAT_TAG_AND: self._back_adapter(self.mgr.And),
            mathsat.MSAT_TAG_OR:  self._back_adapter(self.mgr.Or),
            mathsat.MSAT_TAG_NOT: self._back_adapter(self.mgr.Not),
            mathsat.MSAT_TAG_IFF: self._back_adapter(self.mgr.Iff),
            mathsat.MSAT_TAG_ITE: self._back_adapter(self.mgr.Ite),
            mathsat.MSAT_TAG_EQ:  self._back_adapter(self.mgr.Equals),
            mathsat.MSAT_TAG_LEQ: self._back_adapter(self.mgr.LE),
            mathsat.MSAT_TAG_PLUS: self._back_adapter(self.mgr.Plus),
            mathsat.MSAT_TAG_TIMES: self._back_adapter(self.mgr.Times),
            mathsat.MSAT_TAG_BV_MUL: self._back_adapter(self.mgr.BVMul),
            mathsat.MSAT_TAG_BV_ADD: self._back_adapter(self.mgr.BVAdd),
            mathsat.MSAT_TAG_BV_UDIV: self._back_adapter(self.mgr.BVUDiv),
            mathsat.MSAT_TAG_BV_UREM: self._back_adapter(self.mgr.BVURem),
            mathsat.MSAT_TAG_BV_CONCAT: self._back_adapter(self.mgr.BVConcat),
            mathsat.MSAT_TAG_BV_OR: self._back_adapter(self.mgr.BVOr),
            mathsat.MSAT_TAG_BV_XOR:self._back_adapter(self.mgr.BVXor),
            mathsat.MSAT_TAG_BV_AND:self._back_adapter(self.mgr.BVAnd),
            mathsat.MSAT_TAG_BV_NOT:self._back_adapter(self.mgr.BVNot),
            mathsat.MSAT_TAG_BV_SUB:self._back_adapter(self.mgr.BVSub),
            mathsat.MSAT_TAG_BV_NEG:self._back_adapter(self.mgr.BVNeg),
            mathsat.MSAT_TAG_BV_SREM:self._back_adapter(self.mgr.BVSRem),
            mathsat.MSAT_TAG_BV_SDIV:self._back_adapter(self.mgr.BVSDiv),
            mathsat.MSAT_TAG_BV_ULT: self._back_adapter(self.mgr.BVULT),
            mathsat.MSAT_TAG_BV_SLT: self._back_adapter(self.mgr.BVSLT),
            mathsat.MSAT_TAG_BV_ULE: self._back_adapter(self.mgr.BVULE),
            mathsat.MSAT_TAG_BV_SLE: self._back_adapter(self.mgr.BVSLE),
            mathsat.MSAT_TAG_BV_LSHL: self._back_adapter(self.mgr.BVLShl),
            mathsat.MSAT_TAG_BV_LSHR: self._back_adapter(self.mgr.BVLShr),
            mathsat.MSAT_TAG_BV_ASHR: self._back_adapter(self.mgr.BVAShr),
            mathsat.MSAT_TAG_BV_COMP: self._back_adapter(self.mgr.BVComp),
            mathsat.MSAT_TAG_ARRAY_READ: self._back_adapter(self.mgr.Select),
            mathsat.MSAT_TAG_ARRAY_WRITE: self._back_adapter(self.mgr.Store),
            # Slightly more complext conversion
            mathsat.MSAT_TAG_BV_EXTRACT: self._back_bv_extract,
            mathsat.MSAT_TAG_BV_ZEXT: self._back_bv_zext,
            mathsat.MSAT_TAG_BV_SEXT: self._back_bv_sext,
            mathsat.MSAT_TAG_BV_ROL: self._back_bv_rol,
            mathsat.MSAT_TAG_BV_ROR: self._back_bv_ror,
            mathsat.MSAT_TAG_ARRAY_CONST: self._back_array_const,
            # Symbols, Constants and UFs have TAG_UNKNOWN
            mathsat.MSAT_TAG_UNKNOWN: self._back_tag_unknown,
        }

        # Handling of UF bool args
        self._ufrewriter = MSatBoolUFRewriter(environment)

        return

    def back(self, expr):
        return self._walk_back(expr, self.mgr)

    def _most_generic(self, ty1, ty2):
        """Returns teh most generic, yet compatible type between ty1 and ty2"""
        if ty1 == ty2:
            return ty1

        assert ty1 in [types.REAL, types.INT]
        assert ty2 in [types.REAL, types.INT]
        return types.REAL

    def _get_signature(self, term, args):
        """Returns the signature of the given term.
        For example:
        - a term x & y returns a function type Bool -> Bool -> Bool,
        - a term 14 returns Int
        - a term x ? 13 : 15.0 returns Bool -> Real -> Real -> Real
        """
        res = None

        if mathsat.msat_term_is_true(self.msat_env(), term) or \
            mathsat.msat_term_is_false(self.msat_env(), term) or \
            mathsat.msat_term_is_boolean_constant(self.msat_env(), term):
            res = types.BOOL

        elif mathsat.msat_term_is_number(self.msat_env(), term):
            ty = mathsat.msat_term_get_type(term)
            if mathsat.msat_is_integer_type(self.msat_env(), ty):
                res = types.INT
            elif mathsat.msat_is_rational_type(self.msat_env(), ty):
                res = types.REAL
            else:
                assert "_" in str(term), "Unrecognized type for '%s'" % str(term)
                width = int(str(term).split("_")[1])
                res = types.BVType(width)

        elif mathsat.msat_term_is_and(self.msat_env(), term) or \
             mathsat.msat_term_is_or(self.msat_env(), term) or \
             mathsat.msat_term_is_iff(self.msat_env(), term):
            res = types.FunctionType(types.BOOL, [types.BOOL, types.BOOL])

        elif mathsat.msat_term_is_not(self.msat_env(), term):
            res = types.FunctionType(types.BOOL, [types.BOOL])

        elif mathsat.msat_term_is_term_ite(self.msat_env(), term):
            t1 = self.env.stc.get_type(args[1])
            t2 = self.env.stc.get_type(args[2])
            t = self._most_generic(t1, t2)
            res = types.FunctionType(t, [types.BOOL, t, t])

        elif mathsat.msat_term_is_equal(self.msat_env(), term) or \
             mathsat.msat_term_is_leq(self.msat_env(), term):
            t1 = self.env.stc.get_type(args[0])
            t2 = self.env.stc.get_type(args[1])
            t = self._most_generic(t1, t2)
            res = types.FunctionType(types.BOOL, [t, t])

        elif mathsat.msat_term_is_plus(self.msat_env(), term) or \
             mathsat.msat_term_is_times(self.msat_env(), term):
            t1 = self.env.stc.get_type(args[0])
            t2 = self.env.stc.get_type(args[1])
            t = self._most_generic(t1, t2)
            res = types.FunctionType(t, [t, t])

        elif mathsat.msat_term_is_constant(self.msat_env(), term):
            ty = mathsat.msat_term_get_type(term)
            return self._msat_type_to_type(ty)

        elif mathsat.msat_term_is_uf(self.msat_env(), term):
            d = mathsat.msat_term_get_decl(term)
            fun = self.get_symbol_from_declaration(d)
            res = fun.symbol_type()

        elif mathsat.msat_term_is_bv_times(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_plus(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_minus(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_or(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_and(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_lshl(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_lshr(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_ashr(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_xor(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_urem(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_udiv(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_sdiv(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_srem(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_concat(self.msat_env(), term):
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(t, [t, t])

        elif mathsat.msat_term_is_bv_not(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_neg(self.msat_env(), term):
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(t, [t])

        elif mathsat.msat_term_is_bv_ult(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_slt(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_uleq(self.msat_env(), term) or \
             mathsat.msat_term_is_bv_sleq(self.msat_env(), term):
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(types.BOOL, [t, t])

        elif mathsat.msat_term_is_bv_comp(self.msat_env(), term):
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(types.BVType(1), [t, t])

        elif mathsat.msat_term_is_bv_rol(self.msat_env(), term)[0] or \
             mathsat.msat_term_is_bv_ror(self.msat_env(), term)[0]:
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(t, [t])

        elif mathsat.msat_term_is_bv_sext(self.msat_env(), term)[0]:
            _, amount = mathsat.msat_term_is_bv_sext(self.msat_env(), term)
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(types.BVType(amount + t.width), [t])

        elif mathsat.msat_term_is_bv_zext(self.msat_env(), term)[0]:
            _, amount = mathsat.msat_term_is_bv_zext(self.msat_env(), term)
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(types.BVType(amount + t.width), [t])

        elif mathsat.msat_term_is_bv_extract(self.msat_env(), term)[0]:
            _, msb, lsb = mathsat.msat_term_is_bv_extract(self.msat_env(), term)
            t = self.env.stc.get_type(args[0])
            res = types.FunctionType(types.BVType(msb - lsb + 1), [t])

        elif mathsat.msat_term_is_array_read(self.msat_env(), term):
            t1 = self.env.stc.get_type(args[0])
            t = t1.elem_type
            res = types.FunctionType(t, [t1, t1.index_type])

        elif mathsat.msat_term_is_array_write(self.msat_env(), term):
            at = self.env.stc.get_type(args[0])
            res = types.FunctionType(at, [at, at.index_type, at.elem_type])

        elif mathsat.msat_term_is_array_const(self.msat_env(), term):
            ty = mathsat.msat_term_get_type(term)
            pyty = self._msat_type_to_type(ty)
            return types.FunctionType(pyty, [self.env.stc.get_type(args[0])])

        else:
            raise PysmtTypeError("Unsupported expression:",
                                 mathsat.msat_term_repr(term))
        return res

    def _back_single_term(self, term, mgr, args):
        """Builds the pysmt formula given a term and the list of formulae
        obtained by converting the term children.

        :param term: The MathSAT term to be transformed in pysmt formulae
        :type term: MathSAT term

        :param mgr: The formula manager to be sued to build the
        formulae, it should allow for type unsafety.
        :type mgr: Formula manager

        :param args: List of the pysmt formulae obtained by converting
        all the args (obtained by mathsat.msat_term_get_arg()) to
        pysmt formulae
        :type args: List of pysmt formulae

        :returns The pysmt formula representing the given term
        :rtype Pysmt formula
        """
        decl = mathsat.msat_term_get_decl(term)
        tag = mathsat.msat_decl_get_tag(self.msat_env(), decl)

        try:<commit_msg>MathSAT: Map-based Type Signature back conversion<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 warnings import warn
from six.moves import xrange

from pysmt.exceptions import SolverAPINotFound
from pysmt.constants import Fraction, is_pysmt_fraction, is_pysmt_integer

try:
    import mathsat
except ImportError:
    raise SolverAPINotFound

from pysmt.logics import LRA, QF_UFLIA, QF_UFLRA, QF_BV, PYSMT_QF_LOGICS
from pysmt.oracles import get_logic

import pysmt.operators as op
from pysmt import typing as types
from pysmt.solvers.solver import (IncrementalTrackingSolver, UnsatCoreSolver,
                                  Model, Converter, SolverOptions)
from pysmt.solvers.smtlib import SmtLibBasicSolver, SmtLibIgnoreMixin
from pysmt.walkers import DagWalker
from pysmt.exceptions import (SolverReturnedUnknownResultError,
                              SolverNotConfiguredForUnsatCoresError,
                              SolverStatusError,
                              InternalSolverError,
                              NonLinearError, PysmtValueError, PysmtTypeError)
from pysmt.decorators import clear_pending_pop, catch_conversion_error
from pysmt.solvers.qelim import QuantifierEliminator
from pysmt.solvers.interpolation import Interpolator
from pysmt.walkers.identitydag import IdentityDagWalker


class MSatEnv(object):
    """A wrapper for the msat_env object.

    Objects within pySMT should only reference the msat_environment
    through this object. When calling a function from the underlying
    wrapper, the inner instance of msat_env needs to be used.
    This is done using the __call__ method: e.g.,
       env = MSatEnv()
       mathsat.function(env())
    """
    __slots__ = ['msat_env']

    def __init__(self, msat_config=None):
        if msat_config is None:
            self.msat_env = mathsat.msat_create_env()
        else:
            self.msat_env = mathsat.msat_create_env(msat_config)

    def __del__(self):
        mathsat.msat_destroy_env(self.msat_env)

    def __call__(self):
        return self.msat_env


class MathSAT5Model(Model):
    """Stand-alone model"""

    def __init__(self, environment, msat_env):
        Model.__init__(self, environment)
        self.msat_env = msat_env
        self.converter = MSatConverter(environment, self.msat_env)
        self.msat_model = None

        msat_model = mathsat.msat_get_model(self.msat_env())
        if mathsat.MSAT_ERROR_MODEL(msat_model):
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise InternalSolverError(msat_msg)
        self.msat_model = msat_model

    def __del__(self):
        if self.msat_model is not None:
            mathsat.msat_destroy_model(self.msat_model)
        del self.msat_env

    def get_value(self, formula, model_completion=True):
        titem = self.converter.convert(formula)
        msat_res = mathsat.msat_model_eval(self.msat_model, titem)
        if mathsat.MSAT_ERROR_TERM(msat_res):
            raise InternalSolverError("get model value")
        val = self.converter.back(msat_res)
        if self.environment.stc.get_type(formula).is_real_type() and \
               val.is_int_constant():
            val = self.environment.formula_manager.Real(val.constant_value())
        return val

    def iterator_over(self, language):
        for x in language:
            yield x, self.get_value(x, model_completion=True)

    def __iter__(self):
        """Overloading of iterator from Model.  We iterate only on the
        variables defined in the assignment.
        """
        it = mathsat.msat_model_create_iterator(self.msat_model)
        if mathsat.MSAT_ERROR_MODEL_ITERATOR(it):
            raise InternalSolverError("model iteration")

        while mathsat.msat_model_iterator_has_next(it):
            t, v = mathsat.msat_model_iterator_next(it)
            if mathsat.msat_term_is_constant(self.msat_env(), t):
                pt = self.converter.back(t)
                pv = self.converter.back(v)
                if self.environment.stc.get_type(pt).is_real_type() and \
                       pv.is_int_constant():
                    pv = self.environment.formula_manager.Real(
                        pv.constant_value())
                yield (pt, pv)

        mathsat.msat_destroy_model_iterator(it)

    def __contains__(self, x):
        """Returns whether the model contains a value for 'x'."""
        return x in (v for v, _ in self)

# EOC MathSAT5Model


class MathSATOptions(SolverOptions):

    def __init__(self, **base_options):
        SolverOptions.__init__(self, **base_options)

    @staticmethod
    def _set_option(msat_config, name, value):
        """Sets the given option. Might raise a ValueError."""
        check = mathsat.msat_set_option(msat_config, name, value)
        if check != 0:
            raise PysmtValueError("Error setting the option '%s=%s'" % (name,value))

    def __call__(self, solver):
        if self.generate_models:
            self._set_option(solver.msat_config, "model_generation", "true")

        if self.unsat_cores_mode is not None:
            self._set_option(solver.msat_config, "unsat_core_generation", "1")

        if self.random_seed is not None:
            self._set_option(solver.msat_config,
                             "random_seed", str(self.random_seed))

        for k,v in self.solver_options.items():
            self._set_option(solver.msat_config, str(k), str(v))

        if "debug.api_call_trace_filename" in self.solver_options:
            self._set_option(solver.msat_config, "debug.api_call_trace", "1")

        # Force semantics of division by 0
        self._set_option(solver.msat_config, "theory.bv.div_by_zero_mode", "0")

# EOC MathSATOptions


class MathSAT5Solver(IncrementalTrackingSolver, UnsatCoreSolver,
                     SmtLibBasicSolver, SmtLibIgnoreMixin):

    LOGICS = PYSMT_QF_LOGICS - set(l for l in PYSMT_QF_LOGICS if not l.theory.linear)
    OptionsClass = MathSATOptions

    def __init__(self, environment, logic, **options):
        IncrementalTrackingSolver.__init__(self,
                                           environment=environment,
                                           logic=logic,
                                           **options)

        self.msat_config = mathsat.msat_create_default_config(str(logic))
        self.options(self)
        self.msat_env = MSatEnv(self.msat_config)
        mathsat.msat_destroy_config(self.msat_config)
        self.converter = MSatConverter(environment, self.msat_env)

        # Shortcuts
        self.realType = mathsat.msat_get_rational_type(self.msat_env())
        self.intType = mathsat.msat_get_integer_type(self.msat_env())
        self.boolType = mathsat.msat_get_bool_type(self.msat_env())
        self.mgr = environment.formula_manager

    @clear_pending_pop
    def _reset_assertions(self):
        mathsat.msat_reset_env(self.msat_env())

    @clear_pending_pop
    def declare_variable(self, var):
        raise NotImplementedError

    @clear_pending_pop
    def _add_assertion(self, formula, named=None):
        self._assert_is_boolean(formula)

        result = formula
        if self.options.unsat_cores_mode == "named":
            # If we want named unsat cores, we need to rewrite the
            # formulae as implications
            key = self.mgr.FreshSymbol(template="_assertion_%d")
            result = (key, named, formula)
            formula = self.mgr.Implies(key, formula)

        term = self.converter.convert(formula)
        res = mathsat.msat_assert_formula(self.msat_env(), term)

        if res != 0:
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise InternalSolverError(msat_msg)

        return result

    def _named_assertions(self):
        if self.options.unsat_cores_mode == "named":
            return [t[0] for t in self.assertions]
        return None

    def _named_assertions_map(self):
        if self.options.unsat_cores_mode == "named":
            return dict((t[0], (t[1],t[2])) for t in self.assertions)
        return None

    @clear_pending_pop
    def _solve(self, assumptions=None):
        res = None

        n_ass = self._named_assertions()
        if n_ass is not None and len(n_ass) > 0:
            if assumptions is None:
                assumptions = n_ass
            else:
                assumptions += n_ass

        if assumptions is not None:
            bool_ass = []
            other_ass = []
            for x in assumptions:
                if x.is_literal():
                    bool_ass.append(self.converter.convert(x))
                else:
                    other_ass.append(x)

            if len(other_ass) > 0:
                self.push()
                self.add_assertion(self.mgr.And(other_ass))
                self.pending_pop = True

            if len(bool_ass) > 0:
                res = mathsat.msat_solve_with_assumptions(self.msat_env(), bool_ass)
            else:
                res = mathsat.msat_solve(self.msat_env())

        else:
            res = mathsat.msat_solve(self.msat_env())

        assert res in [mathsat.MSAT_UNKNOWN,mathsat.MSAT_SAT,mathsat.MSAT_UNSAT]
        if res == mathsat.MSAT_UNKNOWN:
            msat_msg = mathsat.msat_last_error_message(self.msat_env())
            raise SolverReturnedUnknownResultError(msat_msg)

        return (res == mathsat.MSAT_SAT)

    def _check_unsat_core_config(self):
        if self.options.unsat_cores_mode is None:
            raise SolverNotConfiguredForUnsatCoresError

        if self.last_result is None or self.last_result:
            raise SolverStatusError("The last call to solve() was not" \
                                    " unsatisfiable")

        if self.last_command != "solve":
            raise SolverStatusError("The solver status has been modified by a" \
                                    " '%s' command after the last call to" \
                                    " solve()" % self.last_command)

    def get_unsat_core(self):
        """After a call to solve() yielding UNSAT, returns the unsat core as a
        set of formulae"""
        self._check_unsat_core_config()
        if self.options.unsat_cores_mode == "all":

            terms = mathsat.msat_get_unsat_core(self.msat_env())
            if terms is None:
                raise InternalSolverError(
                    mathsat.msat_last_error_message(self.msat_env()))
            return set(self.converter.back(t) for t in terms)
        else:
            return self.get_named_unsat_core().values()

    def get_named_unsat_core(self):
        """After a call to solve() yielding UNSAT, returns the unsat core as a
        dict of names to formulae"""
        self._check_unsat_core_config()
        if self.options.unsat_cores_mode == "named":

            assumptions = mathsat.msat_get_unsat_assumptions(self.msat_env())
            pysmt_assumptions = set(self.converter.back(t) for t in assumptions)

            res = {}
            n_ass_map = self._named_assertions_map()
            cnt = 0
            for key in pysmt_assumptions:
                if key in n_ass_map:
                    (name, formula) = n_ass_map[key]
                    if name is None:
                        name = "_a_%d" % cnt
                        cnt += 1
                    res[name] = formula
            return res

        else:
            return dict(("_a%d" % i, f)
                        for i,f in enumerate(self.get_unsat_core()))

    @clear_pending_pop
    def all_sat(self, important, callback):
        self.push()
        mathsat.msat_all_sat(self.msat_env(),
                             [self._var2term(x) for x in important],
                             callback)
        self.pop()

    @clear_pending_pop
    def _push(self, levels=1):
        for _ in xrange(levels):
            mathsat.msat_push_backtrack_point(self.msat_env())

    @clear_pending_pop
    def _pop(self, levels=1):
        for _ in xrange(levels):
            mathsat.msat_pop_backtrack_point(self.msat_env())

    def _var2term(self, var):
        decl = mathsat.msat_find_decl(self.msat_env(), var.symbol_name())
        titem = mathsat.msat_make_term(self.msat_env(), decl, [])
        return titem

    def set_preferred_var(self, var):
        tvar = self.converter.convert(var)
        mathsat.msat_add_preferred_for_branching(self.msat_env(), tvar)
        return

    def print_model(self, name_filter=None):
        if name_filter is not None:
            raise NotImplementedError
        for v in self.converter.symbol_to_decl.keys():
            var = self.mgr.Symbol(v)
            assert var is not None
            print("%s = %s", (v, self.get_value(var)))

    def get_value(self, item):
        self._assert_no_function_type(item)

        titem = self.converter.convert(item)
        tval = mathsat.msat_get_model_value(self.msat_env(), titem)
        val = self.converter.back(tval)
        if self.environment.stc.get_type(item).is_real_type() and \
               val.is_int_constant():
            val = self.mgr.Real(val.constant_value())
        return val

    def get_model(self):
        return MathSAT5Model(self.environment, self.msat_env)

    def _exit(self):
        del self.msat_env


class MSatConverter(Converter, DagWalker):

    def __init__(self, environment, msat_env):
        DagWalker.__init__(self, environment)

        self.msat_env = msat_env
        self.mgr = environment.formula_manager
        self._get_type = environment.stc.get_type

        # Maps a Symbol into the corresponding msat_decl instance in the msat_env
        self.symbol_to_decl = {}
        # Maps a msat_decl instance inside the msat_env into the corresponding
        # Symbol
        self.decl_to_symbol = {}

        self.boolType = mathsat.msat_get_bool_type(self.msat_env())
        self.realType = mathsat.msat_get_rational_type(self.msat_env())
        self.intType = mathsat.msat_get_integer_type(self.msat_env())

        # Back Conversion
        self.back_memoization = {}
        self.back_fun = {
            mathsat.MSAT_TAG_TRUE: lambda term, args: self.mgr.TRUE(),
            mathsat.MSAT_TAG_FALSE:lambda term, args: self.mgr.FALSE(),
            mathsat.MSAT_TAG_AND: self._back_adapter(self.mgr.And),
            mathsat.MSAT_TAG_OR:  self._back_adapter(self.mgr.Or),
            mathsat.MSAT_TAG_NOT: self._back_adapter(self.mgr.Not),
            mathsat.MSAT_TAG_IFF: self._back_adapter(self.mgr.Iff),
            mathsat.MSAT_TAG_ITE: self._back_adapter(self.mgr.Ite),
            mathsat.MSAT_TAG_EQ:  self._back_adapter(self.mgr.Equals),
            mathsat.MSAT_TAG_LEQ: self._back_adapter(self.mgr.LE),
            mathsat.MSAT_TAG_PLUS: self._back_adapter(self.mgr.Plus),
            mathsat.MSAT_TAG_TIMES: self._back_adapter(self.mgr.Times),
            mathsat.MSAT_TAG_BV_MUL: self._back_adapter(self.mgr.BVMul),
            mathsat.MSAT_TAG_BV_ADD: self._back_adapter(self.mgr.BVAdd),
            mathsat.MSAT_TAG_BV_UDIV: self._back_adapter(self.mgr.BVUDiv),
            mathsat.MSAT_TAG_BV_UREM: self._back_adapter(self.mgr.BVURem),
            mathsat.MSAT_TAG_BV_CONCAT: self._back_adapter(self.mgr.BVConcat),
            mathsat.MSAT_TAG_BV_OR: self._back_adapter(self.mgr.BVOr),
            mathsat.MSAT_TAG_BV_XOR:self._back_adapter(self.mgr.BVXor),
            mathsat.MSAT_TAG_BV_AND:self._back_adapter(self.mgr.BVAnd),
            mathsat.MSAT_TAG_BV_NOT:self._back_adapter(self.mgr.BVNot),
            mathsat.MSAT_TAG_BV_SUB:self._back_adapter(self.mgr.BVSub),
            mathsat.MSAT_TAG_BV_NEG:self._back_adapter(self.mgr.BVNeg),
            mathsat.MSAT_TAG_BV_SREM:self._back_adapter(self.mgr.BVSRem),
            mathsat.MSAT_TAG_BV_SDIV:self._back_adapter(self.mgr.BVSDiv),
            mathsat.MSAT_TAG_BV_ULT: self._back_adapter(self.mgr.BVULT),
            mathsat.MSAT_TAG_BV_SLT: self._back_adapter(self.mgr.BVSLT),
            mathsat.MSAT_TAG_BV_ULE: self._back_adapter(self.mgr.BVULE),
            mathsat.MSAT_TAG_BV_SLE: self._back_adapter(self.mgr.BVSLE),
            mathsat.MSAT_TAG_BV_LSHL: self._back_adapter(self.mgr.BVLShl),
            mathsat.MSAT_TAG_BV_LSHR: self._back_adapter(self.mgr.BVLShr),
            mathsat.MSAT_TAG_BV_ASHR: self._back_adapter(self.mgr.BVAShr),
            mathsat.MSAT_TAG_BV_COMP: self._back_adapter(self.mgr.BVComp),
            mathsat.MSAT_TAG_ARRAY_READ: self._back_adapter(self.mgr.Select),
            mathsat.MSAT_TAG_ARRAY_WRITE: self._back_adapter(self.mgr.Store),
            # Slightly more complext conversion
            mathsat.MSAT_TAG_BV_EXTRACT: self._back_bv_extract,
            mathsat.MSAT_TAG_BV_ZEXT: self._back_bv_zext,
            mathsat.MSAT_TAG_BV_SEXT: self._back_bv_sext,
            mathsat.MSAT_TAG_BV_ROL: self._back_bv_rol,
            mathsat.MSAT_TAG_BV_ROR: self._back_bv_ror,
            mathsat.MSAT_TAG_ARRAY_CONST: self._back_array_const,
            # Symbols, Constants and UFs have TAG_UNKNOWN
            mathsat.MSAT_TAG_UNKNOWN: self._back_tag_unknown,
        }

        # Handling of UF bool args
        self._ufrewriter = MSatBoolUFRewriter(environment)

        # Signature Computation
        self.term_sig = {
            mathsat.MSAT_TAG_TRUE: lambda term, args: types.BOOL,
            mathsat.MSAT_TAG_FALSE: lambda term, args: types.BOOL,
            mathsat.MSAT_TAG_AND: lambda term, args:\
                types.FunctionType(types.BOOL, [types.BOOL, types.BOOL]),
            mathsat.MSAT_TAG_OR: lambda term, args:\
                types.FunctionType(types.BOOL, [types.BOOL, types.BOOL]),
            mathsat.MSAT_TAG_NOT: lambda term, args:\
                types.FunctionType(types.BOOL, [types.BOOL]),
            mathsat.MSAT_TAG_IFF: lambda term, args:\
                types.FunctionType(types.BOOL, [types.BOOL, types.BOOL]),
            mathsat.MSAT_TAG_ITE: self._sig_ite,
            mathsat.MSAT_TAG_EQ: self._sig_most_generic_bool_binary,
            mathsat.MSAT_TAG_LEQ: self._sig_most_generic_bool_binary,
            mathsat.MSAT_TAG_PLUS:  self._sig_most_generic_bool_binary,
            mathsat.MSAT_TAG_TIMES: self._sig_most_generic_bool_binary,
            mathsat.MSAT_TAG_BV_MUL: self._sig_binary,
            mathsat.MSAT_TAG_BV_ADD: self._sig_binary,
            mathsat.MSAT_TAG_BV_UDIV:self._sig_binary,
            mathsat.MSAT_TAG_BV_UREM:self._sig_binary,
            mathsat.MSAT_TAG_BV_CONCAT: self._sig_binary,
            mathsat.MSAT_TAG_BV_OR:  self._sig_binary,
            mathsat.MSAT_TAG_BV_XOR: self._sig_binary,
            mathsat.MSAT_TAG_BV_AND: self._sig_binary,
            mathsat.MSAT_TAG_BV_NOT:  self._sig_unary,
            mathsat.MSAT_TAG_BV_SUB: self._sig_binary,
            mathsat.MSAT_TAG_BV_NEG:  self._sig_unary,
            mathsat.MSAT_TAG_BV_SREM: self._sig_binary,
            mathsat.MSAT_TAG_BV_SDIV: self._sig_binary,
            mathsat.MSAT_TAG_BV_ULT:  self._sig_bool_binary,
            mathsat.MSAT_TAG_BV_SLT:  self._sig_bool_binary,
            mathsat.MSAT_TAG_BV_ULE:  self._sig_bool_binary,
            mathsat.MSAT_TAG_BV_SLE:  self._sig_bool_binary,
            mathsat.MSAT_TAG_BV_LSHL: self._sig_binary,
            mathsat.MSAT_TAG_BV_LSHR: self._sig_binary,
            mathsat.MSAT_TAG_BV_ASHR: self._sig_binary,
            mathsat.MSAT_TAG_BV_ROL: self._sig_binary,
            mathsat.MSAT_TAG_BV_ROR:  self._sig_binary,
            mathsat.MSAT_TAG_BV_EXTRACT: self._sig_bv_extract,
            mathsat.MSAT_TAG_BV_ZEXT: self._sig_bv_zext,
            mathsat.MSAT_TAG_BV_SEXT: self._sig_bv_sext,
            mathsat.MSAT_TAG_BV_COMP: self._sig_bv_comp,
            mathsat.MSAT_TAG_ARRAY_READ: self._sig_array_read,
            mathsat.MSAT_TAG_ARRAY_WRITE: self._sig_array_write,
            mathsat.MSAT_TAG_ARRAY_CONST: self._sig_array_const,
            ## Symbols, Constants and UFs have TAG_UNKNOWN
            mathsat.MSAT_TAG_UNKNOWN: self._sig_unknown,
        }

        return

    def back(self, expr):
        return self._walk_back(expr, self.mgr)

    def _most_generic(self, ty1, ty2):
        """Returns teh most generic, yet compatible type between ty1 and ty2"""
        if ty1 == ty2:
            return ty1

        assert ty1 in [types.REAL, types.INT]
        assert ty2 in [types.REAL, types.INT]
        return types.REAL

    def _get_signature(self, term, args):
        """Returns the signature of the given term.
        For example:
        - a term x & y returns a function type Bool -> Bool -> Bool,
        - a term 14 returns Int
        - a term x ? 13 : 15.0 returns Bool -> Real -> Real -> Real
        """
        decl = mathsat.msat_term_get_decl(term)
        tag = mathsat.msat_decl_get_tag(self.msat_env(), decl)
        try:
            return self.term_sig[tag](term, args)
        except KeyError:
            raise PysmtTypeError("Unsupported expression:",
                                 mathsat.msat_term_repr(term))

    def _sig_binary(self, term, args):
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(t, [t, t])

    def _sig_binary(self, term, args):
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(t, [t, t])

    def _sig_bool_binary(self, term, args):
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(types.BOOL, [t, t])

    def _sig_most_generic_bool_binary(self, term, args):
        t1 = self.env.stc.get_type(args[0])
        t2 = self.env.stc.get_type(args[1])
        t = self._most_generic(t1, t2)
        return types.FunctionType(types.BOOL, [t, t])

    def _sig_unary(self, term, args):
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(t, [t])

    def _sig_ite(self, term, args):
        t1 = self.env.stc.get_type(args[1])
        t2 = self.env.stc.get_type(args[2])
        t = self._most_generic(t1, t2)
        return types.FunctionType(t, [types.BOOL, t, t])

    def _sig_bv_comp(self, term,  args):
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(types.BVType(1), [t, t])

    def _sig_bv_sext(self, term, args):
        _, amount = mathsat.msat_term_is_bv_sext(self.msat_env(), term)
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(types.BVType(amount + t.width), [t])

    def _sig_bv_zext(self, term, args):
        _, amount = mathsat.msat_term_is_bv_zext(self.msat_env(), term)
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(types.BVType(amount + t.width), [t])

    def _sig_bv_extract(self, term, args):
        _, msb, lsb = mathsat.msat_term_is_bv_extract(self.msat_env(), term)
        t = self.env.stc.get_type(args[0])
        return types.FunctionType(types.BVType(msb - lsb + 1), [t])

    def _sig_array_read(self, term, args):
        t1 = self.env.stc.get_type(args[0])
        t = t1.elem_type
        return types.FunctionType(t, [t1, t1.index_type])

    def _sig_array_write(self, term, args):
        at = self.env.stc.get_type(args[0])
        return types.FunctionType(at, [at, at.index_type, at.elem_type])

    def _sig_array_const(self, term,  args):
        ty = mathsat.msat_term_get_type(term)
        pyty = self._msat_type_to_type(ty)
        return types.FunctionType(pyty, [self.env.stc.get_type(args[0])])

    def _sig_unknown(self, term, args):
        if mathsat.msat_term_is_boolean_constant(self.msat_env(), term):
            return types.BOOL
        elif mathsat.msat_term_is_number(self.msat_env(), term):
            ty = mathsat.msat_term_get_type(term)
            if mathsat.msat_is_integer_type(self.msat_env(), ty):
                res = types.INT
            elif mathsat.msat_is_rational_type(self.msat_env(), ty):
                res = types.REAL
            else:
                assert "_" in str(term), "Unrecognized type for '%s'" % str(term)
                width = int(str(term).split("_")[1])
                res = types.BVType(width)
            return res
        elif mathsat.msat_term_is_constant(self.msat_env(), term):
            ty = mathsat.msat_term_get_type(term)
            return self._msat_type_to_type(ty)
        elif mathsat.msat_term_is_uf(self.msat_env(), term):
            d = mathsat.msat_term_get_decl(term)
            fun = self.get_symbol_from_declaration(d)
            return fun.symbol_type()
        raise PysmtTypeError("Unsupported expression:",
                             mathsat.msat_term_repr(term))

    def _back_single_term(self, term, mgr, args):
        """Builds the pysmt formula given a term and the list of formulae
        obtained by converting the term children.

        :param term: The MathSAT term to be transformed in pysmt formulae
        :type term: MathSAT term

        :param mgr: The formula manager to be sued to build the
        formulae, it should allow for type unsafety.
        :type mgr: Formula manager

        :param args: List of the pysmt formulae obtained by converting
        all the args (obtained by mathsat.msat_term_get_arg()) to
        pysmt formulae
        :type args: List of pysmt formulae

        :returns The pysmt formula representing the given term
        :rtype Pysmt formula
        """
        decl = mathsat.msat_term_get_decl(term)
        tag = mathsat.msat_decl_get_tag(self.msat_env(), decl)

        try:
{'fraction_non_alphanumeric': 0.09421854034187037, 'fraction_numerical': 0.003208680940435214, 'mean_word_length': 2.3680901231333507, 'pattern_counts': {'":': 12, '<': 7, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5178182', 'n_tokens_mistral': 17234, 'n_tokens_neox': 16684, 'n_words': 3163}