assumptions.py

from sage.structure.sage_object import SageObject
from sage.rings.all import ZZ, QQ, RR, CC
from sage.symbolic.ring import is_SymbolicVariable
_assumptions = []

class GenericDeclaration(SageObject):

    def __init__(self, var, assumption):
        """
        This class represents generic assumptions, such as a variable being
        an integer or a function being increasing. It passes such
        information to maxima's declare (wrapped in a context so it is able
        to forget).
        
        INPUT:
        
        
        -  ``var`` - the variable about which assumptions are
           being made
        
        -  ``assumption`` - a Maxima feature, either user
           defined or in the list given by maxima('features')
        
        
        EXAMPLES::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'integer')
            sage: decl.assume()
            sage: sin(x*pi)
            sin(pi*x)
            sage: sin(x*pi).simplify()
            0
            sage: decl.forget()
            sage: sin(x*pi)
            sin(pi*x)
        
        Here is the list of acceptable features.

        ::

            sage: maxima('features')
            [integer,noninteger,even,odd,rational,irrational,real,imaginary,complex,analytic,increasing,decreasing,oddfun,evenfun,posfun,constant,commutative,lassociative,rassociative,symmetric,antisymmetric,integervalued]
        """
        self._var = var
        self._assumption = assumption
        self._context = None
        
    def __repr__(self):
        """
        EXAMPLES::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: GenericDeclaration(x, 'foo')
            x is foo
        """
        return "%s is %s" % (self._var, self._assumption)
        
    def __cmp__(self, other):
        """
        TESTS::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration as GDecl
            sage: var('y')
            y
            sage: GDecl(x, 'integer') == GDecl(x, 'integer')
            True
            sage: GDecl(x, 'integer') == GDecl(x, 'rational')
            False
            sage: GDecl(x, 'integer') == GDecl(y, 'integer')
            False
        """
        if isinstance(self, GenericDeclaration) and isinstance(other, GenericDeclaration):
            return cmp( (self._var, self._assumption),
                        (other._var, other._assumption) )
        else:
            return cmp(type(self), type(other))
            
    def assume(self):
        """
        TEST::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'even')
            sage: decl.assume()
            sage: cos(x*pi).simplify()
            1
            sage: decl2 = GenericDeclaration(x, 'odd')
            sage: decl2.assume()
            Traceback (most recent call last):
            ...
            ValueError: Assumption is inconsistent
            sage: decl.forget()
        """
        from sage.calculus.calculus import maxima
        if self._context is None:
            # We get the list here because features may be added with time.
            valid_features = list(maxima("features"))
            if self._assumption not in [repr(x).strip() for x in list(valid_features)]:
                raise ValueError, "%s not a valid assumption, must be one of %s" % (self._assumption, valid_features)
            cur = maxima.get("context")
            self._context = maxima.newcontext('context' + maxima._next_var_name())
            try:
                maxima.eval("declare(%s, %s)" % (repr(self._var), self._assumption))
#            except TypeError, mess:
#                if 'inconsistent' in str(mess): # note Maxima doesn't tell you if declarations are redundant
#                    raise ValueError, "Assumption is inconsistent"
            except RuntimeError, mess:
                if 'inconsistent' in str(mess): # note Maxima doesn't tell you if declarations are redundant
                    raise ValueError, "Assumption is inconsistent"
                else:
                    raise
            maxima.set("context", cur)
            
        if not self in _assumptions:
            maxima.activate(self._context)
            _assumptions.append(self)
        
    def forget(self):
        """
        TEST::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'odd')
            sage: decl.assume()
            sage: cos(pi*x)
            cos(pi*x)
            sage: cos(pi*x).simplify()
            -1
            sage: decl.forget()
            sage: cos(x*pi).simplify()
            cos(pi*x)
        """
        from sage.calculus.calculus import maxima
        if self._context is not None:
            try:
                _assumptions.remove(self)
            except ValueError:
                return
            maxima.deactivate(self._context)
        else: # trying to forget a declaration explicitly rather than implicitly
            for x in _assumptions:
                if repr(self) == repr(x): # so by implication x is also a GenericDeclaration
                    x.forget()
                    break
            return
    
    def contradicts(self, soln):
        """
        Returns ``True`` if this assumption is violated by the given
        variable assignment(s).

        INPUT:

        - ``soln`` - Either a dictionary with variables as keys or a symbolic
            relation with a variable on the left hand side.
        
        EXAMPLES::
        
            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: GenericDeclaration(x, 'integer').contradicts(x==4)
            False
            sage: GenericDeclaration(x, 'integer').contradicts(x==4.0)
            False
            sage: GenericDeclaration(x, 'integer').contradicts(x==4.5)
            True
            sage: GenericDeclaration(x, 'integer').contradicts(x==sqrt(17))
            True
            sage: GenericDeclaration(x, 'noninteger').contradicts(x==sqrt(17))
            False
            sage: GenericDeclaration(x, 'noninteger').contradicts(x==17)
            True
            sage: GenericDeclaration(x, 'even').contradicts(x==3)
            True
            sage: GenericDeclaration(x, 'complex').contradicts(x==3)
            False
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==3)
            True
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==I)
            False

            sage: var('y,z')
            (y, z)
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==y+z)
            False

            sage: GenericDeclaration(x, 'rational').contradicts(y==pi)
            False
            sage: GenericDeclaration(x, 'rational').contradicts(x==pi)
            True
            sage: GenericDeclaration(x, 'irrational').contradicts(x!=pi)
            False
            sage: GenericDeclaration(x, 'rational').contradicts({x: pi, y: pi})
            True
            sage: GenericDeclaration(x, 'rational').contradicts({z: pi, y: pi})
            False
       """
        if isinstance(soln, dict):
            value = soln.get(self._var)
            if value is None:
                return False
        elif soln.lhs() == self._var:
            value = soln.rhs()
        else:
            return False
        try:
            CC(value)
        except:
            return False
        if self._assumption == 'integer':
            return value not in ZZ
        elif self._assumption == 'noninteger':
            return value in ZZ
        elif self._assumption == 'even':
            return value not in ZZ or ZZ(value) % 2 != 0
        elif self._assumption == 'odd':
            return value not in ZZ or ZZ(value) % 2 != 1
        elif self._assumption == 'rational':
            return value not in QQ
        elif self._assumption == 'irrational':
            return value in QQ
        elif self._assumption == 'real':
            return value not in RR
        elif self._assumption == 'imaginary':
            return value not in CC or CC(value).real() != 0
        elif self._assumption == 'complex':
            return value not in CC

def preprocess_assumptions(args):
    """
    Turns a list of the form (var1, var2, ..., 'property') into a
    sequence of declarations (var1 is property), (var2 is property),
    ...
    
    EXAMPLES::
    
        sage: from sage.symbolic.assumptions import preprocess_assumptions
        sage: preprocess_assumptions([x, 'integer', x > 4])
        [x is integer, x > 4]
        sage: var('x,y')
        (x, y)
        sage: preprocess_assumptions([x, y, 'integer', x > 4, y, 'even'])
        [x is integer, y is integer, x > 4, y is even]
    """
    args = list(args)
    last = None
    for i, x in reversed(list(enumerate(args))):
        if isinstance(x, str):
            del args[i]
            last = x
        elif ((not hasattr(x, 'assume') or is_SymbolicVariable(x))
              and last is not None):
            args[i] = GenericDeclaration(x, last)
        else:
            last = None
    return args

def assume(*args):
    """
    Make the given assumptions.
    
    INPUT:
    
    -  ``*args`` - assumptions
    
    EXAMPLES:

    Assumptions are typically used to ensure certain relations are
    evaluated as true that are not true in general.
    
    Here, we verify that for `x>0`, `\sqrt(x^2)=x`::

        sage: assume(x > 0)
        sage: bool(sqrt(x^2) == x)
        True

    This will be assumed in the current Sage session until forgotten::

        sage: forget()
        sage: bool(sqrt(x^2) == x)
        False
    

    Another major use case is in taking certain integrals and limits
    where the answers may depend on some sign condition::

        sage: var('x, n')
        (x, n)
        sage: assume(n+1>0)
        sage: integral(x^n,x)
        x^(n + 1)/(n + 1)
        sage: forget()

    ::

        sage: var('q, a, k')
        (q, a, k)
        sage: assume(q > 1)
        sage: sum(a*q^k, k, 0, oo)
        Traceback (most recent call last):
        ...
        ValueError: Sum is divergent.
        sage: forget()
        sage: assume(abs(q) < 1)
        sage: sum(a*q^k, k, 0, oo)
        -a/(q - 1)
        sage: forget()

    An integer constraint::
    
        sage: var('n, P, r, r2')
        (n, P, r, r2)
        sage: assume(n, 'integer')
        sage: c = P*e^(r*n)
        sage: d = P*(1+r2)^n
        sage: solve(c==d,r2)
        [r2 == e^r - 1]
    
    Simplifying certain well-known identities works as well::
    
        sage: sin(n*pi)
        sin(pi*n)
        sage: sin(n*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)

    If you make inconsistent or meaningless assumptions,
    Sage will let you know::

        sage: assume(x<0)
        sage: assume(x>0)
        Traceback (most recent call last):
        ...
        ValueError: Assumption is inconsistent
        sage: assume(x<1)
        Traceback (most recent call last):
        ...
        ValueError: Assumption is redundant
        sage: assumptions()
        [x < 0]
        sage: forget()
        sage: assume(x,'even')
        sage: assume(x,'odd')
        Traceback (most recent call last):
        ...
        ValueError: Assumption is inconsistent
        sage: forget()

    You can also use assumptions to evaluate simple
    truth values::

        sage: x, y, z = var('x, y, z')
        sage: assume(x>=y,y>=z,z>=x)
        sage: bool(x==z)
        True
        sage: bool(z<x)
        False
        sage: bool(z>y)
        False
        sage: bool(y==z)
        True
        sage: forget()
        sage: assume(x>=1,x<=1)
        sage: bool(x==1)
        True
        sage: bool(x>1)
        False
        sage: forget()

    TESTS:

    Test that you can do two non-relational
    declarations at once (fixing Trac ticket 7084)::

        sage: var('m,n')
        (m, n)
        sage: assume(n, 'integer'); assume(m, 'integer')
        sage: sin(n*pi).simplify()
        0
        sage: sin(m*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)
        sage: sin(m*pi).simplify()
        sin(pi*m)
    """
    for x in preprocess_assumptions(args):
        if isinstance(x, (tuple, list)):
            assume(*x)
        else:
            try:
                x.assume()
            except KeyError:
                raise TypeError, "assume not defined for objects of type '%s'"%type(x)

def forget(*args):
    """
    Forget the given assumption, or call with no arguments to forget
    all assumptions.
    
    Here an assumption is some sort of symbolic constraint.
    
    INPUT:
    
    
    -  ``*args`` - assumptions (default: forget all
       assumptions)
    
    
    EXAMPLES: We define and forget multiple assumptions::
    
        sage: var('x,y,z')
        (x, y, z)
        sage: assume(x>0, y>0, z == 1, y>0)
        sage: list(sorted(assumptions(), lambda x,y:cmp(str(x),str(y))))
        [x > 0, y > 0, z == 1]
        sage: forget(x>0, z==1)
        sage: assumptions()
        [y > 0]
        sage: assume(y, 'even', z, 'complex')
        sage: assumptions()
        [y > 0, y is even, z is complex]
        sage: cos(y*pi).simplify()
        1
        sage: forget(y,'even')
        sage: cos(y*pi).simplify()
        cos(pi*y)
        sage: assumptions()
        [y > 0, z is complex]
        sage: forget()
        sage: assumptions()
        []
    """
    if len(args) == 0:
        _forget_all()
        return
    for x in preprocess_assumptions(args):
        if isinstance(x, (tuple, list)):
            forget(*x)
        else:
            try:
                x.forget()
            except KeyError:
                raise TypeError, "forget not defined for objects of type '%s'"%type(x)

def assumptions():
    """
    List all current symbolic assumptions.
    
    EXAMPLES::
    
        sage: var('x,y,z, w')
        (x, y, z, w)
        sage: forget()
        sage: assume(x^2+y^2 > 0)
        sage: assumptions()
        [x^2 + y^2 > 0]
        sage: forget(x^2+y^2 > 0)
        sage: assumptions()
        []
        sage: assume(x > y)
        sage: assume(z > w)
        sage: list(sorted(assumptions(), lambda x,y:cmp(str(x),str(y))))
        [x > y, z > w]
        sage: forget()
        sage: assumptions()
        []
    """
    return list(_assumptions)

def _forget_all():
    """
    Forget all symbolic assumptions.
    
    This is called by ``forget()``.
    
    EXAMPLES::
    
        sage: var('x,y')
        (x, y)
        sage: assume(x > 0, y < 0)
        sage: bool(x*y < 0)      # means definitely true
        True
        sage: bool(x*y > 0)      # might not be true
        False
        sage: forget()    # implicitly calls _forget_all
        sage: bool(x*y < 0)      # might not be true
        False
        sage: bool(x*y > 0)      # might not be true
        False

    TESTS:

    Check that Trac ticket 7315 is fixed::

        sage: var('m,n')
        (m, n)
        sage: assume(n, 'integer'); assume(m, 'integer')
        sage: sin(n*pi).simplify()
        0
        sage: sin(m*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)
        sage: sin(m*pi).simplify()
        sin(pi*m)
    """
    from sage.calculus.calculus import maxima
    global _assumptions
    if len(_assumptions) == 0:
        return
    #maxima._eval_line('forget([%s]);'%(','.join([x._maxima_init_() for x in _assumptions])))
    for x in _assumptions[:]: # need to do this because x.forget() removes x from _assumptions
        x.forget()
    _assumptions = []