def tableau_test(c, ps=None, verbose=False):
    lp = LogicParser()
    pc = lp.parse(c)
    pps = ([lp.parse(p) for p in ps] if ps else [])
    if not ps:
        ps = []
    print('%s |- %s: %s' % (', '.join(ps), pc, TableauProver().prove(pc, pps, verbose=verbose)))

def combination_prover_demo():
    lp = LogicParser()

    p1 = lp.parse(r'see(Socrates, John)')
    p2 = lp.parse(r'see(John, Mary)')
    c = lp.parse(r'-see(Socrates, Mary)')
    prover = Prover9Command(c, [p1,p2])
    print(prover.prove())
    command = ClosedDomainProver(
                  UniqueNamesProver(
                      ClosedWorldProver(prover)))
    for a in command.assumptions(): print(a)
    print(command.prove())

    def __init__(self):
        LogicParser.__init__(self)

        self.operator_precedence = dict(
                               [(x,1) for x in DrtTokens.LAMBDA_LIST]             + \
                               [(x,2) for x in DrtTokens.NOT_LIST]                + \
                               [(APP,3)]                                          + \
                               [(x,4) for x in DrtTokens.EQ_LIST+Tokens.NEQ_LIST] + \
                               [(DrtTokens.COLON,5)]                              + \
                               [(DrtTokens.DRS_CONC,6)]                           + \
                               [(x,7) for x in DrtTokens.OR_LIST]                 + \
                               [(x,8) for x in DrtTokens.IMP_LIST]                + \
                               [(None,9)])

def unique_names_demo():
    lp = LogicParser()

    p1 = lp.parse(r'man(Socrates)')
    p2 = lp.parse(r'man(Bill)')
    c = lp.parse(r'exists x.exists y.(x != y)')
    prover = Prover9Command(c, [p1,p2])
    print(prover.prove())
    unp = UniqueNamesProver(prover)
    print('assumptions:')
    for a in unp.assumptions(): print('   ', a)
    print('goal:', unp.goal())
    print(unp.prove())

    p1 = lp.parse(r'all x.(walk(x) -> (x = Socrates))')
    p2 = lp.parse(r'Bill = William')
    p3 = lp.parse(r'Bill = Billy')
    c = lp.parse(r'-walk(William)')
    prover = Prover9Command(c, [p1,p2,p3])
    print(prover.prove())
    unp = UniqueNamesProver(prover)
    print('assumptions:')
    for a in unp.assumptions(): print('   ', a)
    print('goal:', unp.goal())
    print(unp.prove())

 def __init__(self, grammar, drt_parser):
     assert isinstance(grammar, str) and grammar.endswith('.fcfg'), \
                         "%s is not a grammar name" % grammar
     self.drt_parser = drt_parser()
     self.presupp_parser = PresuppDrtParser()
     self.logic_parser = LogicParser()
     self.parser = load_parser(grammar, logic_parser=self.drt_parser) 

def demo():
    from nltk_contrib.drt import DRT

    DRT.testTp_equals()
    print '\n'
    
    lp = LogicParser()
    a = lp.parse(r'some x.((man x) and (walks x))')
    b = lp.parse(r'some x.((walks x) and (man x))')
    bicond = ApplicationExpression(ApplicationExpression(Operator('iff'), a), b)
    print "Trying to prove:\n '%s <-> %s'" % (a.infixify(), b.infixify())
    print 'tableau: %s' % get_prover(bicond, prover_name='tableau').prove()
    print 'Prover9: %s' % get_prover(bicond, prover_name='Prover9').prove()
    print '\n'
    
    demo_drt_glue_remove_duplicates()

    lp = LogicParser()
    a = lp.parse(r'all x.((man x) implies (mortal x))')
    b = lp.parse(r'(man socrates)')
    c1 = lp.parse(r'(mortal socrates)')
    c2 = lp.parse(r'(not (mortal socrates))')

    print get_prover(c1, [a,b], 'prover9').prove()
    print get_prover(c2, [a,b], 'prover9').prove()
    print get_model_builder(c1, [a,b], 'mace').build_model()
    print get_model_builder(c2, [a,b], 'mace').build_model()

def satdemo(trace=None):
    """Satisfiers of an open formula in a first order model."""

    print()
    print('*' * mult)
    print("Satisfiers Demo")
    print('*' * mult)

    folmodel(quiet=True)

    formulas = [
               'boy(x)',
               '(x = x)',
               '(boy(x) | girl(x))',
               '(boy(x) & girl(x))',
               'love(adam, x)',
               'love(x, adam)',
               '-(x = adam)',
               'exists z22. love(x, z22)',
               'exists y. love(y, x)',
               'all y. (girl(y) -> love(x, y))',
               'all y. (girl(y) -> love(y, x))',
               'all y. (girl(y) -> (boy(x) & love(y, x)))',
               '(boy(x) & all y. (girl(y) -> love(x, y)))',
               '(boy(x) & all y. (girl(y) -> love(y, x)))',
               '(boy(x) & exists y. (girl(y) & love(y, x)))',
               '(girl(x) -> dog(x))',
               'all y. (dog(y) -> (x = y))',
               'exists y. love(y, x)',
               'exists y. (love(adam, y) & love(y, x))'
                ]

    if trace:
        print(m2)

    lp = LogicParser()
    for fmla in formulas:
        print(fmla)
        lp.parse(fmla)

    parsed = [lp.parse(fmla) for fmla in formulas]

    for p in parsed:
        g2.purge()
        print("The satisfiers of '%s' are: %s" % (p, m2.satisfiers(p, 'x', g2, trace)))

def folmodel(quiet=False, trace=None):
    """Example of a first-order model."""

    global val2, v2, dom2, m2, g2

    v2 = [('adam', 'b1'), ('betty', 'g1'), ('fido', 'd1'),\
         ('girl', set(['g1', 'g2'])), ('boy', set(['b1', 'b2'])), ('dog', set(['d1'])),
         ('love', set([('b1', 'g1'), ('b2', 'g2'), ('g1', 'b1'), ('g2', 'b1')]))]
    val2 = Valuation(v2)
    dom2 = val2.domain
    m2 = Model(dom2, val2)
    g2 = Assignment(dom2, [('x', 'b1'), ('y', 'g2')])

    if not quiet:
        print()
        print('*' * mult)
        print("Models Demo")
        print("*" * mult)
        print("Model m2:\n", "-" * 14,"\n", m2)
        print("Variable assignment = ", g2)

        exprs = ['adam', 'boy', 'love', 'walks', 'x', 'y', 'z']
        lp = LogicParser()
        parsed_exprs = [lp.parse(e) for e in exprs]

        print()
        for parsed in parsed_exprs:
            try:
                print("The interpretation of '%s' in m2 is %s" % (parsed, m2.i(parsed, g2)))
            except Undefined:
                print("The interpretation of '%s' in m2 is Undefined" % parsed)


        applications = [('boy', ('adam')), ('walks', ('adam',)), ('love', ('adam', 'y')), ('love', ('y', 'adam'))]

        for (fun, args) in applications:
            try:
                funval = m2.i(lp.parse(fun), g2)
                argsval = tuple(m2.i(lp.parse(arg), g2) for arg in args)
                print("%s(%s) evaluates to %s" % (fun, args, argsval in funval))
            except Undefined:
                print("%s(%s) evaluates to Undefined" % (fun, args))

 def evaluate(self, expr, g, trace=None):
     """
     Call the ``LogicParser`` to parse input expressions, and
     provide a handler for ``satisfy``
     that blocks further propagation of the ``Undefined`` error.
     :param expr: An ``Expression`` of ``logic``.
     :type g: Assignment
     :param g: an assignment to individual variables.
     :rtype: bool or 'Undefined'
     """
     try:
         lp = LogicParser()
         parsed = lp.parse(expr)
         value = self.satisfy(parsed, g, trace=trace)
         if trace:
             print()
             print("'%s' evaluates to %s under M, %s" %  (expr, value, g))
         return value
     except Undefined:
         if trace:
             print()
             print("'%s' is undefined under M, %s" %  (expr, g))
         return 'Undefined'

 def evaluate(self, expr, g, trace=None):
     """
     Call the L{LogicParser} to parse input expressions, and
     provide a handler for L{satisfy}
     that blocks further propagation of the C{Undefined} error.
     :param expr: An C{Expression} of L{logic}.
     :type g: L{Assignment}
     :param g: an assignment to individual variables.
     :rtype: bool or 'Undefined'
     """
     try:
         lp = LogicParser()
         parsed = lp.parse(expr)
         value = self.satisfy(parsed, g, trace=trace)
         if trace:
             print
             print "'%s' evaluates to %s under M, %s" %  (expr, value, g)
         return value
     except Undefined:
         if trace:
             print
             print "'%s' is undefined under M, %s" %  (expr, g)
         return 'Undefined'

    def __init__(self, meaning, glue, indices=None):
        if not indices:
            indices = set()

        if isinstance(meaning, string_types):
            self.meaning = LogicParser().parse(meaning)
        elif isinstance(meaning, Expression):
            self.meaning = meaning
        else:
            raise RuntimeError('Meaning term neither string or expression: %s, %s' % (meaning, meaning.__class__))

        if isinstance(glue, string_types):
            self.glue = linearlogic.LinearLogicParser().parse(glue)
        elif isinstance(glue, linearlogic.Expression):
            self.glue = glue
        else:
            raise RuntimeError('Glue term neither string or expression: %s, %s' % (glue, glue.__class__))

        self.indices = indices

def print_proof(goal, premises):
    lp = LogicParser()
    prover = Prover9Command(lp.parse(goal), premises)
    command = UniqueNamesProver(ClosedWorldProver(prover))
    print(goal, prover.prove(), command.prove())

def test_clausify():
    lp = LogicParser()

    print(clausify(lp.parse('P(x) | Q(x)')))
    print(clausify(lp.parse('(P(x) & Q(x)) | R(x)')))
    print(clausify(lp.parse('P(x) | (Q(x) & R(x))')))
    print(clausify(lp.parse('(P(x) & Q(x)) | (R(x) & S(x))')))

    print(clausify(lp.parse('P(x) | Q(x) | R(x)')))
    print(clausify(lp.parse('P(x) | (Q(x) & R(x)) | S(x)')))

    print(clausify(lp.parse('exists x.P(x) | Q(x)')))

    print(clausify(lp.parse('-(-P(x) & Q(x))')))
    print(clausify(lp.parse('P(x) <-> Q(x)')))
    print(clausify(lp.parse('-(P(x) <-> Q(x))')))
    print(clausify(lp.parse('-(all x.P(x))')))
    print(clausify(lp.parse('-(some x.P(x))')))

    print(clausify(lp.parse('some x.P(x)')))
    print(clausify(lp.parse('some x.all y.P(x,y)')))
    print(clausify(lp.parse('all y.some x.P(x,y)')))
    print(clausify(lp.parse('all z.all y.some x.P(x,y,z)')))
    print(clausify(lp.parse('all x.(all y.P(x,y) -> -all y.(Q(x,y) -> R(x,y)))')))

def closed_domain_demo():
    lp = LogicParser()

    p1 = lp.parse(r'exists x.walk(x)')
    p2 = lp.parse(r'man(Socrates)')
    c = lp.parse(r'walk(Socrates)')
    prover = Prover9Command(c, [p1,p2])
    print(prover.prove())
    cdp = ClosedDomainProver(prover)
    print('assumptions:')
    for a in cdp.assumptions(): print('   ', a)
    print('goal:', cdp.goal())
    print(cdp.prove())

    p1 = lp.parse(r'exists x.walk(x)')
    p2 = lp.parse(r'man(Socrates)')
    p3 = lp.parse(r'-walk(Bill)')
    c = lp.parse(r'walk(Socrates)')
    prover = Prover9Command(c, [p1,p2,p3])
    print(prover.prove())
    cdp = ClosedDomainProver(prover)
    print('assumptions:')
    for a in cdp.assumptions(): print('   ', a)
    print('goal:', cdp.goal())
    print(cdp.prove())

    p1 = lp.parse(r'exists x.walk(x)')
    p2 = lp.parse(r'man(Socrates)')
    p3 = lp.parse(r'-walk(Bill)')
    c = lp.parse(r'walk(Socrates)')
    prover = Prover9Command(c, [p1,p2,p3])
    print(prover.prove())
    cdp = ClosedDomainProver(prover)
    print('assumptions:')
    for a in cdp.assumptions(): print('   ', a)
    print('goal:', cdp.goal())
    print(cdp.prove())

    p1 = lp.parse(r'walk(Socrates)')
    p2 = lp.parse(r'walk(Bill)')
    c = lp.parse(r'all x.walk(x)')
    prover = Prover9Command(c, [p1,p2])
    print(prover.prove())
    cdp = ClosedDomainProver(prover)
    print('assumptions:')
    for a in cdp.assumptions(): print('   ', a)
    print('goal:', cdp.goal())
    print(cdp.prove())

    p1 = lp.parse(r'girl(mary)')
    p2 = lp.parse(r'dog(rover)')
    p3 = lp.parse(r'all x.(girl(x) -> -dog(x))')
    p4 = lp.parse(r'all x.(dog(x) -> -girl(x))')
    p5 = lp.parse(r'chase(mary, rover)')
    c = lp.parse(r'exists y.(dog(y) & all x.(girl(x) -> chase(x,y)))')
    prover = Prover9Command(c, [p1,p2,p3,p4,p5])
    print(prover.prove())
    cdp = ClosedDomainProver(prover)
    print('assumptions:')
    for a in cdp.assumptions(): print('   ', a)
    print('goal:', cdp.goal())
    print(cdp.prove())

def closed_world_demo():
    lp = LogicParser()

    p1 = lp.parse(r'walk(Socrates)')
    p2 = lp.parse(r'(Socrates != Bill)')
    c = lp.parse(r'-walk(Bill)')
    prover = Prover9Command(c, [p1,p2])
    print(prover.prove())
    cwp = ClosedWorldProver(prover)
    print('assumptions:')
    for a in cwp.assumptions(): print('   ', a)
    print('goal:', cwp.goal())
    print(cwp.prove())

    p1 = lp.parse(r'see(Socrates, John)')
    p2 = lp.parse(r'see(John, Mary)')
    p3 = lp.parse(r'(Socrates != John)')
    p4 = lp.parse(r'(John != Mary)')
    c = lp.parse(r'-see(Socrates, Mary)')
    prover = Prover9Command(c, [p1,p2,p3,p4])
    print(prover.prove())
    cwp = ClosedWorldProver(prover)
    print('assumptions:')
    for a in cwp.assumptions(): print('   ', a)
    print('goal:', cwp.goal())
    print(cwp.prove())

    p1 = lp.parse(r'all x.(ostrich(x) -> bird(x))')
    p2 = lp.parse(r'bird(Tweety)')
    p3 = lp.parse(r'-ostrich(Sam)')
    p4 = lp.parse(r'Sam != Tweety')
    c = lp.parse(r'-bird(Sam)')
    prover = Prover9Command(c, [p1,p2,p3,p4])
    print(prover.prove())
    cwp = ClosedWorldProver(prover)
    print('assumptions:')
    for a in cwp.assumptions(): print('   ', a)
    print('goal:', cwp.goal())
    print(cwp.prove())

    def __init__(self):
        LogicParser.__init__(self)

        self.operator_precedence = {APP: 1, Tokens.IMP: 2, None: 3}
        self.right_associated_operations += [Tokens.IMP]

def default_reasoning_demo():
    lp = LogicParser()

    premises = []

    #define taxonomy
    premises.append(lp.parse(r'all x.(elephant(x)        -> animal(x))'))
    premises.append(lp.parse(r'all x.(bird(x)            -> animal(x))'))
    premises.append(lp.parse(r'all x.(dove(x)            -> bird(x))'))
    premises.append(lp.parse(r'all x.(ostrich(x)         -> bird(x))'))
    premises.append(lp.parse(r'all x.(flying_ostrich(x)  -> ostrich(x))'))

    #default properties
    premises.append(lp.parse(r'all x.((animal(x)  & -Ab1(x)) -> -fly(x))')) #normal animals don't fly
    premises.append(lp.parse(r'all x.((bird(x)    & -Ab2(x)) -> fly(x))')) #normal birds fly
    premises.append(lp.parse(r'all x.((ostrich(x) & -Ab3(x)) -> -fly(x))')) #normal ostriches don't fly

    #specify abnormal entities
    premises.append(lp.parse(r'all x.(bird(x)           -> Ab1(x))')) #flight
    premises.append(lp.parse(r'all x.(ostrich(x)        -> Ab2(x))')) #non-flying bird
    premises.append(lp.parse(r'all x.(flying_ostrich(x) -> Ab3(x))')) #flying ostrich

    #define entities
    premises.append(lp.parse(r'elephant(E)'))
    premises.append(lp.parse(r'dove(D)'))
    premises.append(lp.parse(r'ostrich(O)'))

    #print the assumptions
    prover = Prover9Command(None, premises)
    command = UniqueNamesProver(ClosedWorldProver(prover))
    for a in command.assumptions(): print(a)

    print_proof('-fly(E)', premises)
    print_proof('fly(D)', premises)
    print_proof('-fly(O)', premises)

class GlueFormula(object):
    def __init__(self, meaning, glue, indices=None):
        if not indices:
            indices = set()

        if isinstance(meaning, string_types):
            self.meaning = LogicParser().parse(meaning)
        elif isinstance(meaning, Expression):
            self.meaning = meaning
        else:
            raise RuntimeError('Meaning term neither string or expression: %s, %s' % (meaning, meaning.__class__))

        if isinstance(glue, string_types):
            self.glue = linearlogic.LinearLogicParser().parse(glue)
        elif isinstance(glue, linearlogic.Expression):
            self.glue = glue
        else:
            raise RuntimeError('Glue term neither string or expression: %s, %s' % (glue, glue.__class__))

        self.indices = indices

    def applyto(self, arg):
        """ self = (\\x.(walk x), (subj -o f))
            arg  = (john        ,  subj)
            returns ((walk john),          f)
        """
        if self.indices & arg.indices: # if the sets are NOT disjoint
            raise linearlogic.LinearLogicApplicationException("'%s' applied to '%s'.  Indices are not disjoint." % (self, arg))
        else: # if the sets ARE disjoint
            return_indices = (self.indices | arg.indices)

        try:
            return_glue = linearlogic.ApplicationExpression(self.glue, arg.glue, arg.indices)
        except linearlogic.LinearLogicApplicationException:
            raise linearlogic.LinearLogicApplicationException("'%s' applied to '%s'" % (self.simplify(), arg.simplify()))

        arg_meaning_abstracted = arg.meaning
        if return_indices:
            for dep in self.glue.simplify().antecedent.dependencies[::-1]: # if self.glue is (A -o B), dep is in A.dependencies
                arg_meaning_abstracted = self.make_LambdaExpression(Variable('v%s' % dep),
                                                                    arg_meaning_abstracted)
        return_meaning = self.meaning.applyto(arg_meaning_abstracted)

        return self.__class__(return_meaning, return_glue, return_indices)

    def make_VariableExpression(self, name):
        return VariableExpression(name)

    def make_LambdaExpression(self, variable, term):
        return LambdaExpression(variable, term)

    def lambda_abstract(self, other):
        assert isinstance(other, GlueFormula)
        assert isinstance(other.meaning, AbstractVariableExpression)
        return self.__class__(self.make_LambdaExpression(other.meaning.variable,
                                                         self.meaning),
                              linearlogic.ImpExpression(other.glue, self.glue))

    def compile(self, counter=None):
        """From Iddo Lev's PhD Dissertation p108-109"""
        if not counter:
            counter = Counter()
        (compiled_glue, new_forms) = self.glue.simplify().compile_pos(counter, self.__class__)
        return new_forms + [self.__class__(self.meaning, compiled_glue, set([counter.get()]))]

    def simplify(self):
        return self.__class__(self.meaning.simplify(), self.glue.simplify(), self.indices)

    def __eq__(self, other):
        return self.__class__ == other.__class__ and self.meaning == other.meaning and self.glue == other.glue

    def __ne__(self, other):
        return not self == other

    def __str__(self):
        assert isinstance(self.indices, set)
        accum = '%s : %s' % (self.meaning, self.glue)
        if self.indices:
            accum += ' : {' + ', '.join(str(index) for index in self.indices) + '}'
        return accum

    def __repr__(self):
        return "%s" % self

class Tester(object):
    
    INFERROR = {
    3 : AdmissibilityError,
    2 : InformativityError,
    1 : ConsistencyError           
    }
    
    WORD_SPLIT = re.compile(" |, |,")
    EXCLUDED_NEXT = re.compile("^ha[sd]|is|was|not|will$")
    EXCLUDED = re.compile("^does|h?is|red|[a-z]+ness$")
    SUBSTITUTIONS = [
     (re.compile("^died$"), ("did", "die")),
     (re.compile("^([A-Z][a-z]+)'s?$"), lambda m: (m.group(1), "s")),
     (re.compile("^(?P<stem>[a-z]+)s$"), lambda m: ("does", m.group("stem"))),
     (re.compile("^([a-z]+(?:[^cvklt]|lk|nt))ed|([a-z]+[cvlkt]e)d$"), lambda m: ("did", m.group(1) if m.group(1) else m.group(2))),
     (re.compile("^([A-Z]?[a-z]+)one$"), lambda m: (m.group(1), "one")),
     (re.compile("^([A-Z]?[a-z]+)thing$"), lambda m: (m.group(1), "thing")),
     (re.compile("^bit$"), ("did", "bite")),
     (re.compile("^bought$"), ("did", "buy")),
     (re.compile("^wrote$"), ("did", "write")),
    ]
    
    def __init__(self, grammar, drt_parser):
        assert isinstance(grammar, str) and grammar.endswith('.fcfg'), \
                            "%s is not a grammar name" % grammar
        self.drt_parser = drt_parser()
        self.presupp_parser = PresuppDrtParser()
        self.logic_parser = LogicParser()
        self.parser = load_parser(grammar, logic_parser=self.drt_parser) 

    def _split(self, sentence):
        words = []
        exlude_next = False
        for word in Tester.WORD_SPLIT.split(sentence):
            match = None
            if Tester.EXCLUDED_NEXT.match(word):
                exlude_next = True
                words.append(word)
                continue
            if exlude_next or Tester.EXCLUDED.match(word):
                exlude_next = False
                words.append(word)
                continue
            for pattern, replacement in Tester.SUBSTITUTIONS:
                match = pattern.match(word)
                if match:
                    if isinstance(replacement, LambdaType):
                        words.extend(replacement(match))
                    else:
                        words.extend(replacement)
                    break

            if not match:
                words.append(word)

        return words

    def parse(self, text, **args):
        sentences = text.split('.')
        utter = args.get("utter", True)
        verbose = args.get("verbose", False)
        drs = (utter and self.drt_parser.parse('DRS([n],[])')) or []
        
        for sentence in sentences:
            sentence = sentence.lstrip()
            if sentence:
                words = self._split(sentence)
                if verbose:
                    print words
                trees = self.parser.nbest_parse(words)
                try:
                    new_drs = trees[0].node['SEM'].simplify()
                except IndexError:
                    raise UngrammaticalException()
                if verbose:
                    print(new_drs)
                if drs:
                    drs = (drs + new_drs).simplify()
                else:
                    drs = new_drs
    
        if verbose:
            print drs
        return drs

    def test(self, cases, **args):
        verbose = args.get("verbose", False)
        for number, sentence, expected in cases:
            expected_drs = []
            if expected:
                for item in expected if isinstance(expected, list) else [expected]:
                    expected_drs.append(self.presupp_parser.parse(item, verbose))

            try:
                expression = self.parse(sentence, **args)
                readings, errors = expression.resolve(lambda x: (True, None), verbose)
                if len(expected_drs) == len(readings):
                    for index, pair in enumerate(zip(expected_drs, readings)):
                        if pair[0] == pair[1]:
#.........这里部分代码省略.........