# Path: etb/wrapper.py
# class Tool(object):
#     """
#     Any tool to interpret predicates. Each predicate the tool can deal
#     with should be a method with the same name as the predicate
#     itself, annotated with @Tool.predicate(argspec).
# 
#     Calling the method should return a list of substitutions that are
#     answers to the goal, and bind all the variables in it.
# 
#     the async() method should return False if the tool is very fast to
#     call, True otherwise, in which case it is run in a background
#     thread.
#     """
# 
#     def __init__(self, etb):
#         """Initialize the Tool with the given ETB instance.
#         """
#         self.etb = etb
#         self.log = logging.getLogger('etb.wrapper')
#         self.fs = ETBFS(etb)
#         self.clms = ETBClaims(etb)
#         self.path = os.path.abspath(inspect.getmodule(self).__file__) # pylint: disable=E1103
# 
#     def __repr__(self):
#         return self.__class__.__name__
# 
#     @staticmethod
#     def predicate(argspec, name=None):
#         """Decorator which, given an instance, exports the function.
#         """
#         def decorator(fun):
#             fun._argspec = argspec
#             if name is not None:
#                 fun._predicate_name = name
#             return fun
#         return decorator
# 
#     @staticmethod
#     def volatile(fun):
#         """Mark the function (hence the predicate) as volatile."""
#         fun._volatile = True
#         return fun
# 
#     @staticmethod
#     def sync(fun):
#         """Mark the function as sync, i.e. it will be interpreted
#         directly.
#         """
#         fun._async = False
#         return fun
# 
#     @staticmethod
#     def extern(fun):
#         """Mark the function as external, i.e., it will be available
#         to remote ETB nodes.
#         """
#         fun._extern = True
#         return fun
# 
#     def fail(self, reason):
#         """Report of failure of interpretation of the given goal,
#         e.g. because of wrong types, bad instantiation scheme,
#         non present tool, etc.
#         """
#         msg = "in tool wrapper {0}: {1}".format(self, reason)
#         raise Exception(msg)
# 
#     def bindResult(self, result, resultValue, current=None) :
#         """bind result to resultValue"""
#         if current is None:
#             current = {}
#         if current == []:
#             return []
#         result = terms.mk_var(result)
#         resultValue = terms.mk_term(resultValue)
#         if result.is_var():
#             current[result] = resultValue
#             return current
#         elif result == resultValue :
#             return current
#         else :
#             return []


from etb.wrapper import Tool
import etb.terms
# A library of util functions, without any tool invocation



class Utils(Tool):
    """Library of util functions, without tool invocation"""

    @Tool.sync
    @Tool.predicate("+left: value, +right: value")
    def equal(self, left, right):
        if left == right:
            return [{}]
        else:
            return []

    @Tool.sync
    @Tool.predicate("+left: value, +right: value")
    def lte(self, left, right):
        if int(left.val) <= int(right.val):
            return [{}]
        else:
            return []
        
    @Tool.sync

# Path: etb/wrapper.py
# class Tool(object):
#     """
#     Any tool to interpret predicates. Each predicate the tool can deal
#     with should be a method with the same name as the predicate
#     itself, annotated with @Tool.predicate(argspec).
# 
#     Calling the method should return a list of substitutions that are
#     answers to the goal, and bind all the variables in it.
# 
#     the async() method should return False if the tool is very fast to
#     call, True otherwise, in which case it is run in a background
#     thread.
#     """
# 
#     def __init__(self, etb):
#         """Initialize the Tool with the given ETB instance.
#         """
#         self.etb = etb
#         self.log = logging.getLogger('etb.wrapper')
#         self.fs = ETBFS(etb)
#         self.clms = ETBClaims(etb)
#         self.path = os.path.abspath(inspect.getmodule(self).__file__) # pylint: disable=E1103
# 
#     def __repr__(self):
#         return self.__class__.__name__
# 
#     @staticmethod
#     def predicate(argspec, name=None):
#         """Decorator which, given an instance, exports the function.
#         """
#         def decorator(fun):
#             fun._argspec = argspec
#             if name is not None:
#                 fun._predicate_name = name
#             return fun
#         return decorator
# 
#     @staticmethod
#     def volatile(fun):
#         """Mark the function (hence the predicate) as volatile."""
#         fun._volatile = True
#         return fun
# 
#     @staticmethod
#     def sync(fun):
#         """Mark the function as sync, i.e. it will be interpreted
#         directly.
#         """
#         fun._async = False
#         return fun
# 
#     @staticmethod
#     def extern(fun):
#         """Mark the function as external, i.e., it will be available
#         to remote ETB nodes.
#         """
#         fun._extern = True
#         return fun
# 
#     def fail(self, reason):
#         """Report of failure of interpretation of the given goal,
#         e.g. because of wrong types, bad instantiation scheme,
#         non present tool, etc.
#         """
#         msg = "in tool wrapper {0}: {1}".format(self, reason)
#         raise Exception(msg)
# 
#     def bindResult(self, result, resultValue, current=None) :
#         """bind result to resultValue"""
#         if current is None:
#             current = {}
#         if current == []:
#             return []
#         result = terms.mk_var(result)
#         resultValue = terms.mk_term(resultValue)
#         if result.is_var():
#             current[result] = resultValue
#             return current
#         elif result == resultValue :
#             return current
#         else :
#             return []


# Path: demos/k-induction/wrappers/utils.py
from etb.wrapper import Tool
import etb.terms

# A library of util functions, without any tool invocation



class Utils(Tool):
    """Library of util functions, without tool invocation"""

    @Tool.sync
    @Tool.predicate("+left: value, +right: value")
    def equal(self, left, right):
        if left == right:
            return [{}]
        else:
            return []

    @Tool.sync
    @Tool.predicate("+left: value, +right: value")
    def lte(self, left, right):
        if int(left.val) <= int(right.val):
            return [{}]
        else:
            return []
        
    @Tool.sync

    @Tool.predicate("+n: value, -pn: value")