rmupdater.py

#! /usr/bin/env python

##################################################################################
#
#   The Reverse Mathematics Zoo Updater
#   by Damir Dzhafarov
#   - Version 1.0 started August, 2010
#   - Version 2.0 started August, 2013
#   Revised by Eric Astor
#   - Version 3.0 - 29 May 2016
#   - Version 4.0 - started 30 May 2016
#   - Version 4.1 - optimizations & refactoring, started 2 July 2016
#   - Version 4.2 - new forms and reasoning, started 12 July 2016
#   - Version 4.3 - changed internal representations, started 21 July 2016
#   - Version 4.4 - moved to a shelf database, started 25 July 2016
#   - Version 5.0 - clean implementation of inference rules, started 1 August 2016
#   - Version 5.1 - reverted from shelf database for cross-platform compatibility, started 16 August 2016
#   Documentation and support: http://rmzoo.uconn.edu
#
##################################################################################

from __future__ import print_function

import itertools
import sys
import 

from io import open
from collections import defaultdict

from version_guard import isString, lru_cache

import zlib
try:
    import cPickle as pickle
except:
    import pickle

def eprint(*args, **kwargs):
    print(*args, file=sys.stderr, **kwargs)

Date = u'16 August 2016'
Version = u'5.1'
DatabaseVersion = u'5.1'

version, versionPoint = sys.version_info[0:2]
if version >= 3 and versionPoint >= 3:
    timekeeper = time.perf_counter
else:
    timekeeper = time.clock

from rmBitmasks import *
from renderJustification import *

RCAprinciple = u'RCA'

principlesList = [RCAprinciple]
principles = set(principlesList)

def addPrinciple(a):
    setA = set(a.split(u'+'))
    a = u'+'.join(sorted(setA))
    principles.add(a)
    principles.update(setA)
    return a

conjunction = {}
def joinPrinciples(a, b):
    try:
        return conjunction[a,b]
    except KeyError:
        p = u'+'.join(sorted(set(a.split(u'+')) | set(b.split(u'+'))))
        if p not in principles:
            p = None
        conjunction[a,b] = p
        conjunction[b,a] = p
        return p

equivalent = defaultdict(noReduction)
implies = defaultdict(noReduction)
notImplies = defaultdict(noReduction)

def addEquivalent(a,reduction,b):
    equivalent[a,b] |= Reduction.weaker(reduction)

def addReduction(a,reduction,b):
    implies[a,b] |= Reduction.weaker(reduction)

def addNonReduction(a,reduction,b):
    notImplies[a,b] |= Reduction.stronger(reduction)

conservative = defaultdict(noForm)
nonConservative = defaultdict(noForm)

def addConservative(a,frm,b):
    conservative[a,b] |= Form.stronger(frm)

def addNonConservative(a,frm,b):
    nonConservative[a,b] |= Form.weaker(frm)

form = defaultdict(noForm)

primary = set()
primaryIndex = []

def addForm(a, frm):
    form[a] |= Form.weaker(frm)

def addPrimary(a):
    primary.add(a)
    primaryIndex.append(a)

justify = {}
justComplexity = {}

def updateJustification(fact, jst, cplx):
    try:
        if cplx >= justComplexity[fact]:
            return False
    except KeyError:
        pass
    justify[fact] = jst
    justComplexity[fact] = cplx
    return True

def unoptimizedJustification(fact, jst, cplx):
    if fact in justify:
        return False
    else:
        justify[fact] = jst
        return True

class UnjustifiedFactError(Exception):
    def __init__(self, a, op, b):
        super(UnjustifiedFactError, self).__init__(u'The fact "{0}" is not justified.'.format(printFact(a, op, b)))

def addUnjustified(a, op, b):
    raise UnjustifiedFactError(a, op, b)

class ContradictionError(Exception):
    def __init__(self, fact1, fact2):
        super(ContradictionError, self).__init__(u'The following facts are contradictory:\n\n' +
                                                 printJustification(fact1, justify) + u'\n\n' +
                                                 printJustification(fact2, justify))

# Noted side-effects:
#     Changing '<->' can affect '->'
#     Changing '->' can affect 'c' and '<->'
#     Changing 'c' can affect '->'
#     Changing '-|>' can affect 'nc'
#     Changing 'nc' can affect '-|>'
def addFact(a, op, b, jst, cplx):
    fact = (a, op, b)
    if not updateJustification(fact, jst, cplx):
        return False
    opCtx,opCore = op
    
    ref = (fact,)
    refCplx = 1 + cplx
    
    if opCore == u'<->': # equivalence
        # Symmetry:
        #     IF (a X<-> b), THEN (b X<-> a).
        updateJustification((b, op, a), jst, cplx)
        
        for x in Reduction.list(Reduction.weaker(opCtx)):
            newOp = (x, u'<->')
            
            addEquivalent(a, x, b)
            updateJustification((a, newOp, b), ref, refCplx)
            
            # Symmetry:
            #     IF (a X<-> b), THEN (b X<-> a).
            addEquivalent(b, x, a)
            updateJustification((b, newOp, a), ref, refCplx)
        
        # Definition of equivalence:
        #     IF (a X<-> b), THEN (a X-> b) AND (b X-> a).
        impliesOp = (opCtx, u'->')
        addFact(a, impliesOp, b, (fact,), refCplx)
        addFact(b, impliesOp, a, (fact,), refCplx)
    elif opCore == u'->': # implication
        for x in Reduction.list(Reduction.weaker(opCtx)):
            addReduction(a, x, b)
            updateJustification((a, (x, u'->'), b), ref, refCplx)
            
            if Reduction.isPresent(x, notImplies[a,b]):
                raise ContradictionError((a, (x, u'->'), b), (a, (x, u'-|>'), b))
        
            if x == Reduction.RCA:
                if x == opCtx:
                    newRef = ref
                    newRefCplx = refCplx
                else:
                    newRef = ((a, (x, u'->'), b),)
                    newRefCplx = 1 + refCplx
                
                # Trivial conservation:
                #     IF (a RCA-> b), THEN (b Fc a).
                for f in Form:
                    if f != Form.none:
                        addFact(b, (f, u'c'), a, newRef, newRefCplx)
        
        # Definition of conjunction (special case):
        #     IF (a X-> b), THEN (a X<-> a+b).
        ab = joinPrinciples(a,b)
        if ab is not None:
            addFact(a, (opCtx, u'<->'), ab, ref, refCplx)
    elif opCore == u'-|>': # non-implication
        for x in Reduction.list(Reduction.stronger(opCtx)):
            addNonReduction(a, x, b)
            updateJustification((a, (x, u'-|>'), b), ref, refCplx)
            
            if Reduction.isPresent(x, implies[a,b]):
                raise ContradictionError((a, (x, u'-|>'), b), (a, (x, u'->'), b))
        
            if x == Reduction.RCA:
                if x == opCtx:
                    newFact = fact
                    newCplx = 1 + refCplx
                else:
                    newFact = (a, (x, u'-|>'), b)
                    newCplx = 2 + refCplx
                
                # Definition of non-conservation (special case):
                #     IF (a RCA-|> b) AND (b form F), THEN (b nFc a).
                for f in Form.list(form[b]):
                    addFact(b, (f, u'nc'), a, (newFact, (b, u'form', f)), newCplx)
    elif opCore == u'c': # conservation
        for f in Form.list(Form.stronger(opCtx)):
            newFact = (a, (f, u'c'), b)
            
            addConservative(a, f, b)
            updateJustification(newFact, ref, refCplx)
            
            if Form.isPresent(f, nonConservative[a,b]):
                raise ContradictionError((a, (f, u'c'), b), (a, (f, u'nc'), b))
            
            # Definition of conservation (special case):
            #     IF (a Fc b) AND (a form F), THEN (b RCA-> a).
            if Form.isPresent(f, form[a]):
                if f == opCtx:
                    newCplx = 1 + refCplx
                else:
                    newCplx = 2 + refCplx
                
                addFact(b, (Reduction.RCA, u'->'), a, (newFact, (a, u'form', f)), newCplx)
    elif opCore == u'nc': # non-conservation
        for f in Form.list(Form.weaker(opCtx)):
            addNonConservative(a, f, b)
            updateJustification((a, (f, u'nc'), b), ref, refCplx)
            
            if Form.isPresent(f, conservative[a,b]):
                raise ContradictionError((a, (f, u'nc'), b), (a, (f, u'c'), b))
        
        # Trivial conservation (contrapositive):
        #     IF (a nFc b), THEN (b RCA-|> a).
        addFact(b, (Reduction.RCA, u'-|>'), a, ref, refCplx)
    else:
        raise ValueError(u'Unrecognized operator: ' + opCore)
    
    return True

def standardizePrinciple(a):
    return u'+'.join(sorted(set(a.split(u'+'))))
def standardizeFact(a, op, b):
    a = standardizePrinciple(a)
    if op != u'form':
        b = standardizePrinciple(b)
        if op[1] == u'<=':
            op = (op[0], u'->')
            a,b = b,a
        elif op[1] == u'</=':
            op = (op[0], u'-|>')
            a,b = b,a
    return a, op, b

from pyparsing import *
def parseResults(resultsString, quiet=False):
    start = timekeeper()
    if not quiet: eprint(u'Parsing results...')
    # Name parsed strings
    name = Word( alphas+"_+^{}\\$", alphanums+"_+^{}$\\").setParseAction(lambda s,l,t: addPrinciple(t[0]))
    
    parenth = Literal('"')
    justification = QuotedString('"""',multiline=True) | quotedString.setParseAction(removeQuotes)
    
    _reductionName = NoMatch()
    for r in Reduction:
        if r != Reduction.none:
            _reductionName |= Literal(r.name)
    for r in Reduction.alias:
        if r != u'':
            _reductionName |= Literal(r)
    _reductionType = _reductionName.setParseAction(lambda s,l,t: [Reduction.fromString(t[0])])
    reductionType = Optional(_reductionType, default=Reduction.RCA)
    postfixReductionType = Optional(Suppress(Literal("_")) + _reductionType, default=Reduction.RCA)
    
    implication = (reductionType + Literal("->")) | (Literal("=>") + postfixReductionType).setParseAction(lambda s,l,t: [t[1], "->"])
    nonImplication = (reductionType + Literal("-|>")) | (Literal("=/>") + postfixReductionType).setParseAction(lambda s,l,t: [t[1], "-|>"])
    equivalence = (reductionType + Literal("<->")) | (Literal("<=>") + postfixReductionType).setParseAction(lambda s,l,t: [t[1], "<->"])
    
    reduction = (Literal("<=") + postfixReductionType).setParseAction(lambda s,l,t: [t[1], "<="])
    nonReduction = (Literal("</=") + postfixReductionType).setParseAction(lambda s,l,t: [t[1], "</="])
    
    _formName = NoMatch()
    for f in Form:
        if f != Form.none:
            _formName |= Literal(f.name)
    formType = _formName.setParseAction(lambda s,l,t: [Form.fromString(t[0])])
    
    conservation = formType + Literal("c")
    nonConservation = (Literal("n") + formType + Literal("c")).setParseAction(lambda s,l,t: [t[1], "nc"])
    
    operator = implication | nonImplication | reduction | nonReduction | equivalence | conservation | nonConservation
    
    # Results file lines
    unjustified = (name + Group(operator) + name + ~justification).setParseAction(lambda s,l,t: addUnjustified(*standardizeFact(t[0], tuple(t[1]), t[2])))
    
    factsToAdd = []
    def _addFactParseAction(s,l,t):
        a,op,b = standardizeFact(t[0], tuple(t[1]), t[2])
        factsToAdd.append(((a, op, b), t[3]))
    fact = (name + Group(operator) + name + justification).setParseAction(_addFactParseAction)

    formDef = (name + Literal("form") + formType).setParseAction(lambda s,l,t: addForm(t[0], t[2]))
    primary = (name + Literal("is primary")).setParseAction(lambda s,l,t: addPrimary(t[0]))
    
    comments = Suppress(Literal( "#" ) + SkipTo(LineEnd()))
    
    # Represent and parse results file
    entry = fact | formDef | primary | unjustified | comments
    results = ZeroOrMore( entry ) + StringEnd()
    
    results.parseString(resultsString)
    
    global principlesList
    principlesList = sorted(principles)
    
    for (a, op, b), jst in factsToAdd:
        addFact(a, op, b, jst, 1)
    
    if not quiet: eprint(u'Principles found: {0:,d}'.format(len(principlesList)))
    if not quiet: eprint(u'Elapsed: {0:.6f} s\n'.format(timekeeper() - start))

# General fact; uses nothing, affects '<->', '->', and 'c'
def addReflexivities():
    for a in principlesList:
        for x in Reduction:
            if x == Reduction.none: continue
            
            # (a X-> a)
            addFact(a, (x, u'->'), a, u'reflexivity', 1)
            
            # (a X<-> a)
            addFact(a, (x, u'<->'), a, u'reflexivity', 1)
        
        for f in Form:
            if f == Form.none: continue
            
            # (a Fc a)
            addFact(a, (f, u'c'), a, u'reflexivity', 1)

# General fact; uses nothing, affects '->'
def addRCABottom():
    # (a X-> RCA)
    for a in principlesList:
        for x in Reduction:
            if x == Reduction.none: continue
            
            addFact(a, (x, u'->'), RCAprinciple, u'', 1)

# General fact; uses nothing, affects '->'
def definitionOfConjunction():
    # IF (a == b+...), THEN (a X-> b).
    for a in principlesList:
        splitA = set(a.split(u'+'))
        if len(splitA) == 1: continue
        
        for b in principlesList:
            if b == a: continue
            
            splitB = set(b.split(u'+'))
            if splitB <= splitA:
                for x in Reduction:
                    if x == Reduction.none: continue
                    
                    addFact(a, (x, u'->'), b, u'', 1)

# Uses '->', affects '<->'
def definitionOfEquivalence():
    #a X<-> b
    #WHEN
    #    (a X-> b) AND (b X-> a)
    
    r = False
    for a,b in itertools.combinations(principlesList, 2):
        equiv = implies[a,b] & implies[b,a]
        
        if equiv != Reduction.none:
            for x in Reduction.list(equiv):
                imp = (x, u'->')
                aImpB = (a, imp, b)
                bImpA = (b, imp, a)
                
                r |= addFact(a, (x, u'<->'), b,
                             (aImpB, bImpA), 1 + justComplexity[aImpB] + justComplexity[bImpA])
    return r

# Uses array, affects array
def transitiveClosure(array, opName, clsCtx):
    # Complete (current) transitive closure of array, using Floyd-Warshall
    
    r = False
    for c in principlesList:
        for a in principlesList:
            if a == c: continue
            
            acRelation = array[a,c]
            if acRelation == clsCtx.none: continue
            
            for b in principlesList:
                if b == a or b == c: continue
                
                transitive = acRelation & array[c,b]
                if transitive == clsCtx.none: continue
                
                for x in clsCtx.list(transitive):
                    op = (x, opName)
                    aOpC = (a, op, c)
                    cOpB = (c, op, b)
                    
                    r |= addFact(a, op, b,
                                 (aOpC, cOpB), 1 + justComplexity[aOpC] + justComplexity[cOpB])
    return r

# Uses '->', affects '->'
def unifyOverConjunctions():
    #a X-> b
    #WHEN
    #    (b == c+d) AND (a X-> c) AND (a X-> d) "Definition of conjunction"
    
    r = False
    for b in principlesList:
        splitB = b.split(u'+')
        if len(splitB) == 1: continue # b is not a conjunction
        
        for a in principlesList:
            aImpliesAll = ~Reduction.none
            for p in splitB:
                aImpliesAll &= implies[a,p]
            if aImpliesAll == Reduction.none: continue
            
            for x in Reduction.list(aImpliesAll):
                aImpConjuncts = tuple([(a, (x, u'->'), t) for t in splitB])
                r |= addFact(a, (x, u'->'), b,
                             aImpConjuncts, 1 + sum(justComplexity[aImpX] for aImpX in aImpConjuncts))
    return r

#REDUNDANT
# Uses 'c' and '->', affects '->'
def definitionOfConservation():
    #a RCA-> b
    #WHEN
    #    (c Fc a) AND (c RCA-> b) AND (b has form F) "Definition of conservation"
    
    r = False
    for c in principlesList:
        for b in principlesList:
            if b == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[c,b]):
                formB = form[b]
                if formB == Form.none: continue
                
                cImpB = (c, (Reduction.RCA, u'->'), b)
                refCplxCB = 2 + justComplexity[cImpB]
                
                for a in principlesList:
                    if a == b or a == c: continue
                    
                    frms = formB & conservative[c,a]
                    if frms == Form.none: continue
                    
                    for f in Form.list(frms):
                        cConsA = (c, (f, u'c'), a)
                        
                        r |= addFact(a, (Reduction.RCA, u'->'), b,
                                     (cConsA, cImpB, (b, u'form', f)), refCplxCB + justComplexity[cConsA])
    return r

# Uses posArray and negArray, affects negArray
def contrapositiveTransitivity(posArray, posOpName, negArray, negOpName, clsCtx):
    r = False
    for c in principlesList:
        for a in principlesList:
            if a == c: continue
            
            #a nop b
            #WHEN
            #    (c op a) AND (c nop b)
            caRelation = posArray[c,a]
            if caRelation != clsCtx.none:
                for b in principlesList:
                    if b == a or b == c: continue
                    
                    contexts = caRelation & negArray[c,b]
                    if contexts == clsCtx.none: continue
                    
                    for ctx in clsCtx.list(contexts):
                        nop = (ctx, negOpName)
                        
                        cOpA = (c, (ctx, posOpName), a)
                        cNOpB = (c, nop, b)
                        
                        r |= addFact(a, nop, b,
                                     (cOpA, cNOpB), 1 + justComplexity[cOpA] + justComplexity[cNOpB])
            
            #a nop b
            #WHEN
            #    (a nop c) AND (b op c)
            acNRelation = negArray[a,c]
            if acNRelation != clsCtx.none:
                for b in principlesList:
                    if b == a or b == c: continue
                    
                    contexts = acNRelation & posArray[b,c]
                    if contexts == clsCtx.none: continue
                    
                    for ctx in clsCtx.list(contexts):
                        nop = (ctx, negOpName)
                        
                        aNOpC = (a, nop, c)
                        bOpC = (b, (ctx, posOpName), c)
                        
                        r |= addFact(a, nop, b,
                                     (aNOpC, bOpC), 1 + justComplexity[aNOpC] + justComplexity[bOpC])
    return r

# Uses '->' and '-|>', affects '-|>'
def contrapositiveConjunction():
    #a X-|> b
    #WHEN
    #    (a X-> c) AND (a X-|> b+c)
    
    r = False
    for c in principlesList:
        for b in principlesList:
            if b == c: continue
            
            bc = joinPrinciples(b,c)
            if bc is None: continue
            
            for a in principlesList:
                if a == b: continue
                
                if a == c: # Special-case
                    reds = notImplies[a,bc]
                    if reds == Reduction.none: continue
                    
                    for x in Reduction.list(reds):
                        notImp = (x, u'-|>')
                        
                        aNotImpBC = (a, notImp, bc)
                        
                        r |= addFact(a, notImp, b,
                                     (aNotImpBC,), 1 + justComplexity[aNotImpBC])
                else:
                    reds = implies[a,c] & notImplies[a,bc]
                    if reds == Reduction.none: continue
                    
                    for x in Reduction.list(reds):
                        notImp = (x, u'-|>')
                        
                        aImpC = (a, (x, u'->'), c)
                        aNotImpBC = (a, notImp, bc)
                        
                        r |= addFact(a, notImp, b,
                                     (aImpC, aNotImpBC), 1 + justComplexity[aImpC] + justComplexity[aNotImpBC])
    return r

#REDUNDANT
# Uses 'c' and '-|>', affects '-|>'
def contrapositiveConservation():    
    #a RCA-|> b
    #WHEN
    #    (a Fc c) AND (c RCA-|> b) AND (b has form F)
    notImp = (Reduction.RCA, u'-|>')
    
    r = False
    for c in principlesList:
        for b in principlesList:
            if b == c: continue
            
            if Reduction.isPresent(Reduction.RCA, notImplies[c,b]):
                formB = form[b]
                if formB == Form.none: continue
                
                cNotImpB = (c, notImp, b)
                refCplxCB = 2 + justComplexity[cNotImpB]
                
                for a in principlesList:
                    if a == b or a == c: continue
                    
                    frms = conservative[a,c] & formB
                    if frms == Form.none: continue
                    
                    for f in Form.list(frms):
                        aConsC = (a, (f, u'c'), c)
                        
                        r |= addFact(a, notImp, b,
                                     (aConsC, cNotImpB, (b, u'form', f)), justComplexity[aConsC] + refCplxCB)
    return r

#REDUNDANT
# Uses 'c' and '->', affects 'c'
def liftConservation():
    r = False
    for c in principlesList:
        #a Fc b
        #WHEN
        #    (c RCA-> a) AND (c Fc b) [aka "Weaker principles prove less"]
        for a in principlesList:
            if a == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[c,a]):
                cImpA = (c, (Reduction.RCA, u'->'), a)
                refCplxCA = 1 + justComplexity[cImpA]
                
                for b in principlesList:
                    if b == a or b == c: continue
                    
                    for f in Form.list(conservative[c,b]):
                        fc = (f, u'c')
                        cConsB = (c, fc, b)
                        
                        r |= addFact(a, fc, b,
                                     (cImpA, cConsB), refCplxCA + justComplexity[cConsB])
        
        #a Fc b
        #WHEN
        #    (a Fc c) AND (b RCA-> c) [aka "Stronger principles prove more"]
        for b in principlesList:
            if b == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[b,c]):
                bImpC = (b, (Reduction.RCA, u'->'), c)
                refCplxBC = 1 + justComplexity[bImpC]
                
                for a in principlesList:
                    if a == b or a == c: continue
                    
                    for f in Form.list(conservative[a,c]):
                        fc = (f, u'c')
                        aConsC = (a, fc, c)
                        
                        r |= addFact(a, fc, b,
                                     (aConsC, bImpC), justComplexity[aConsC] + refCplxBC)
    return r

#REDUNDANT
# Uses '->' and '-|>', affects 'nc'
def definitionOfNonConservation():
    #a nFc b
    #WHEN
    #    (a RCA-> c) AND (b RCA-|> c) AND (c has form F)
    r = False
    for c in principlesList:
        formC = form[c]
        if formC == Form.none: continue
        cForms = Form.list(formC)
        
        for a in principlesList:
            if a == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[a,c]):
                aImpC = (a, (Reduction.RCA, u'->'), c)
                refCplxAC = 2 + justComplexity[aImpC]
                
                for b in principlesList:
                    if b == a or b == c: continue
                    
                    if Reduction.isPresent(Reduction.RCA, notImplies[b,c]):
                        bNotImpC = (b, (Reduction.RCA, u'-|>'), c)
                        
                        cplx = refCplxAC + justComplexity[bNotImpC]
                        
                        for f in cForms:
                            r |= addFact(a, (f, u'nc'), b,
                                         (aImpC, bNotImpC, (c, u'form', f)), cplx)
    return r

#REDUNDANT
# Uses 'nc' and '->', affects 'nc'
def liftNonConservation():
    imp = (Reduction.RCA, u'->')
    
    r = False
    for c in principlesList:
        #a nFc b
        #WHEN
        #    (a nFc c) AND (c RCA-> b) [aka "Weaker principles prove less (contrapositive)"]
        for b in principlesList:
            if b == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[c,b]):
                cImpB = (c, imp, b)
                refCplxCB = 1 + justComplexity[cImpB]
                
                for a in principlesList:
                    if a == b or a == c: continue
                    
                    for f in Form.list(nonConservative[a,c]):
                        nFc = (f, u'nc')
                        aNonConsC = (a, nFc, c)
                        
                        r |= addFact(a, nFc, b,
                                     (aNonConsC, cImpB), justComplexity[aNonConsC] + refCplxCB)
        
        #a nFc b
        #WHEN
        #    (a RCA-> c) AND (c nFc b) [aka "Stronger principles prove more (contrapositive)"]
        for a in principlesList:
            if a == c: continue
            
            if Reduction.isPresent(Reduction.RCA, implies[a,c]):
                aImpC = (a, imp, c)
                refCplxAC = 1 + justComplexity[aImpC]
                
                for b in principlesList:
                    if b == a or b == c: continue
                    
                    for f in Form.list(nonConservative[c,b]):
                        nFc = (f, u'nc')
                        cNonConsB = (c, (f, u'nc'), b)
                        
                        r |= addFact(a, nFc, b,
                                     (aImpC, cNonConsB), refCplxAC + justComplexity[cNonConsB])
    return r

def deriveInferences(quiet=False, verbose=False):
    start = timekeeper()
    if not quiet: eprint(u'Adding reflexivity facts..')
    addReflexivities()
    if not quiet: eprint(u'Making RCA trivial..')
    addRCABottom()
    if not quiet: eprint(u'Recording conjunctions...')
    definitionOfConjunction()
    if not quiet: eprint(u'Elapsed: {0:.6f} s\n'.format(timekeeper() - start))
    
    start = timekeeper()
    if not quiet: eprint(u'Deriving positive facts:')
    n = 0
    eUpdated, iUpdated, cUpdated = True, True, True
    while eUpdated or iUpdated or cUpdated:
        n += 1
        eChanged, iChanged, cChanged = False, False, False
        
        if iUpdated or iChanged:
            if not quiet: eprint(u'\tExtracting equivalences...')
            eChanged |= definitionOfEquivalence() # Uses '->', affects '<->'
        if eUpdated or eChanged:
            if not quiet: eprint(u'\tTaking the transitive closure of equivalence...')
            eChanged |= transitiveClosure(equivalent, u'<->', Reduction) # Uses '<->', affects '<->'
        
        if iUpdated or iChanged:
            if not quiet: eprint(u'\tTaking the transitive closure of implication...')
            iChanged |= transitiveClosure(implies, u'->', Reduction) # Uses '->', affects '->'
            if not quiet: eprint(u'\tReverse-engineering implications of conjunctions...')
            iChanged |= unifyOverConjunctions() # Uses '->', affects '->'
        if (cUpdated or cChanged) or (iUpdated or iChanged):
            if not quiet: eprint(u'\tImplementing conservativity for implication...')
            iChanged |= definitionOfConservation() # Uses 'c' and '->', affects '->'
        
        if cUpdated or cChanged:
            if not quiet: eprint(u'\tTaking the transitive closure of conservation facts...')
            cChanged |= transitiveClosure(conservative, u'c', Form) # Uses 'c', affects 'c'
        if (cUpdated or cChanged) or (iUpdated or iChanged):
            if not quiet: eprint(u'\tLifting conservation facts over implications...')
            cChanged |= liftConservation() # Uses 'c' and '->', affects 'c'
        
        if verbose:
            eprint(u'\t\tDuring iteration {0}:'.format(n))
            if eChanged: eprint(u'\t\t\tEquivalences updated.')
            if iChanged: eprint(u'\t\t\tImplications updated.')
            if cChanged: eprint(u'\t\t\tConservation facts updated.')
            if not eChanged and not iChanged and not cChanged: eprint(u'\t\t\tNothing updated.')
        
        eUpdated = eChanged
        iUpdated = iChanged
        cUpdated = cChanged
    if not quiet:
        eprint(u'Finished with positive facts.')
        eprint(u'Elapsed: {0:.6f} s (with {1} repeats)\n'.format(timekeeper() - start, n))
    
    start = timekeeper()
    if not quiet: eprint(u'Deriving negative facts:')
    n = 0
    niUpdated, ncUpdated = True, True
    while niUpdated or ncUpdated:
        n += 1
        niChanged, ncChanged = False, False
        
        if niUpdated or niChanged:
            if not quiet: eprint(u'\tApplying transivitity to non-implications...')
            niChanged |= contrapositiveTransitivity(implies, u'->', notImplies, u'-|>', Reduction) # Uses '->' and '-|>', affects '-|>'
            if not quiet: eprint(u'\tSplitting non-implications over conjunctions...')
            niChanged |= contrapositiveConjunction() # Uses '->' and '-|>', affects '-|>'
            if not quiet: eprint(u'\tImplementing conservativity for non-implication...')
            niChanged |= contrapositiveConservation() # Uses 'c' and '-|>', affects '-|>'
        
        if ncUpdated or ncChanged:
            if not quiet: eprint(u'\tApplying transivitity to non-conservation facts...')
            ncChanged |= contrapositiveTransitivity(conservative, u'c', nonConservative, u'nc', Form) # Uses 'c' and 'nc', affects 'nc'
        if niUpdated or niChanged:
            if not quiet: eprint(u'\tExtracting non-conservation facts from non-implications...')
            ncChanged |= definitionOfNonConservation() # Uses '->' and '-|>', affects 'nc'
        if ncUpdated or ncChanged:
            if not quiet: eprint(u'\tLifting non-conservation facts over implications...')
            ncChanged |= liftNonConservation() # Uses 'nc' and '->', affects 'nc'
        
        if verbose:
            eprint(u'\t\tDuring iteration {0}:'.format(n))
            if niChanged: eprint(u'\t\t\tNon-implications updated.')
            if ncChanged: eprint(u'\t\t\tNon-conservation facts updated.')
            if not niChanged and not ncChanged: eprint(u'\t\t\tNothing updated.')
        
        niUpdated = niChanged
        ncUpdated = ncChanged
    if not quiet:
        eprint(u'Finished with negative facts.')
        eprint(u'Elapsed: {0:.6f} s (with {1} repeats)\n'.format(timekeeper() - start, n))

def getDatabase():
    return {'version': DatabaseVersion,
            'principles': principles,
            'implication': (implies, notImplies),
            'conservation': (conservative, nonConservative),
            'form': form,
            'primary': (primary, primaryIndex),
            'justify': justify}

def setDatabase(database):
    if database['version'] != DatabaseVersion:
        raise VersionError(database['version'], DatabaseVersion)
    
    global principles, principlesList
    principles = database['principles']
    principlesList = sorted(principles)
    
    global implies, notImplies
    implies, notImplies = database['implication']
    
    global conservative, nonConservative
    conservative, nonConservative = database['conservation']
    
    global form
    form = database['form']
    
    global primary, primaryIndex
    primary, primaryIndex = database['primary']
    
    global justify
    justify = database['justify']
    
    global justComplexity
    justComplexity = {}
    def rebuildComplexity(fact):
        try:
            return justComplexity[fact]
        except KeyError:
            r = 1
            
            a,op,b = fact
            if op != u'form':
                jst = justify[fact]
                if not isString(jst):
                    r += sum(rebuildComplexity(f) for f in jst)
            
            justComplexity[fact] = r
            return r
    for fact in justify:
        rebuildComplexity(fact)

def dumpDatabase(databaseName, quiet=False):
    if not quiet: eprint(u'Facts known: {0:,d}\n'.format(len(justify)))
    
    start = timekeeper()
    if not quiet: eprint(u'Dumping updated database to binary file...')
    with open(databaseName, mode='wb') as databaseFile:
        pickledDatabase = pickle.dumps(getDatabase(), protocol=2)
        compressedDatabase = zlib.compress(pickledDatabase)
        databaseFile.write(compressedDatabase)
    
    if not quiet: eprint(u'Elapsed: {0:.6f} s\n'.format(timekeeper() - start))

def loadDatabase(databaseName, quiet=False):
    with open(databaseName, mode='rb') as databaseFile:
        compressedDatabase = databaseFile.read()
        pickledDatabase = zlib.decompress(compressedDatabase)
        setDatabase(pickle.loads(pickledDatabase))

from optparse import OptionParser, OptionGroup
def main():
    absoluteStart = timekeeper()
    eprint(u'\nRM Zoo (v{0})\n'.format(Version))
    
    parser = OptionParser(u'Usage: %prog [options] results [database_title]', version=u'%prog {0} ({1})'.format(Version, Date))
    
    parser.set_defaults(quiet=False, verbose=False)
    
    parser.add_option('-q', action='store_true', dest='quiet',
        help = u'Suppress progress/timing indicators.')
    parser.add_option('-v', action='store_true', dest='verbose',
        help = u'Report additional execution information.')
    
    (options, args) = parser.parse_args()
    if len(args)>2:
        parser.error(u'Too many arguments provided.')
    if len(args)<1:
        parser.error(u'No results file specified.')
    
    if options.quiet and options.verbose:
        parser.error(u'Options -q and -v are incompatible.')
    
    import os
    resultsFile = args[0]
    if len(args) > 1:
        databaseTitle = args[1]
    else:
        eprint(u'No database title specified; defaulting to "database".')
        databaseTitle = 'database.dat'
    
    if os.path.splitext(databaseTitle)[1] == '':
        databaseName = databaseTitle + os.extsep + 'dat'
    else:
        databaseName = databaseTitle
    
    if not os.path.exists(resultsFile):
        parser.error(u'Results file "{0}" does not exist.'.format(resultsFile))
    
    with open(resultsFile, encoding='utf-8') as f:
        parseResults(f.read(), options.quiet)
    deriveInferences(quiet=options.quiet, verbose=options.verbose)
    dumpDatabase(databaseName, options.quiet)
    if not options.quiet: eprint(u'Total elapsed time: {0:.6f} s'.format(timekeeper() - absoluteStart))
    
    if options.verbose:
        try:
            report = []
            report.append(u'\tReduction.list: {0}'.format(Reduction.list.cache_info()))
            report.append(u'\tForm.list: {0}'.format(Form.list.cache_info()))
            eprint(u'\nCache report: ')
            eprint('\n'.join(report))
        except AttributeError:
            pass
if __name__ == '__main__':
    main()