derivations.py

#!/usr/bin/env python3
# ----------------------------------
#
# Module derivations.py

"""
A datatype for representing derivations, i.e. jusifications for
clauses and formulas. Derivations are recursively defined: A
derivation can be the trivial derivation (the clause or formula is
read directly from the input), or it consists of an operator (the
inference rule) and a list of parents.

Copyright 2011-2023 Stephan Schulz, schulz@eprover.org

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program ; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston,
MA  02111-1307 USA

The original copyright holder can be contacted as

Stephan Schulz
Auf der Altenburg 7
70376 Stuttgart
Germany
Email: schulz@eprover.org
"""

from lexer import Token,Lexer
from terms import parseTerm, termIsVar, termArgs, term2String
import unittest
from checkutil import VerificationStatus

class Derivable(object):
    """
    This class represents "derivable" objects. Derivable objects have
    a name and a justification. Names can be generated
    automatically. They are required to be different for different
    objects in the same proof structure, but this is enforced at the
    FOFSpec level. Derivable objects will typically be logical formulas,
    either full FOF formulas, or clauses.
    """
    derivedIdCounter = 0
    """
    Counter for generating new clause names.
    """
    printDerivation = False
    """
    Indicate if derivations should be printed as part of Derivable
    objects. It's up to the concrete classes to support this.
    """
    def __init__(self, name=None, derivation = None):
        """
        Initialize the object..
        """
        self.setName(name)
        self.derivation = derivation
        self.refCount = 0
        self.eqLen = None # How many applications of original axioms
                          # lead to this? Probably only useful in a
                          # purely UEQ setting.
        self.rwSteps = None
        self.number = None

    def __repr__(self):
        return self.name

    def setName(self, name = None):
        """
        Set the name. If no name is given, generate a default name.
        """
        if name:
            self.name = name
        else:
            self.name = "c%d"%(Derivable.derivedIdCounter,)
            Derivable.derivedIdCounter=Derivable.derivedIdCounter+1

    def setNumber(self, number):
        """
        Set the serial number of the step in a linearized derivation.
        """
        self.number = number

    def setDerivation(self, derivation):
        """
        Set the derivation that created this derivable.
        """
        self.derivation = derivation

    def setInputDeriv(self, filename, name):
        """
        Special case: It's an input object.
        """
        self.derivation = Derivation("file", (filename,name))

    def getParents(self):
        """
        Return a list of all parents of this node in the derivation
        graph.
        """
        if self.derivation:
            return self.derivation.getParents()
        else:
            return []

    def getAncestors(self):
        """
        Return a list of all ancestors of this node in the derivation
        graph.
        """
        if self.derivation:
            return self.derivation.getAncestors()
        else:
            return set()

    def incRefCount(self):
        """
        Increase reference counter (counts virtual edges in the
        derivation graph coming from the children).
        """
        self.refCount = self.refCount+1

    def decRefCount(self):
        """
        See above.
        """
        self.refCount = self.refCount-1

    def strDerivation(self):
        """
        If printing of derivations is enabled, return a string
        representartion suitable as part of TPTP-3 output. Otherwise
        return the empty string.
        """
        if not self.derivation:
            return ""
        if Derivable.printDerivation:
            return ","+repr(self.derivation)
        return ""

    def annotateDerivationGraph(self):
        """
        Compute and set the number of virtual edges in all descendents
        of self. The root node has one "virtual" edge.
        """
        self.incRefCount()
        if self.refCount == 1:
            parents = self.getParents()
            for p in parents:
                p.annotateDerivationGraph()

    def linearizeDerivation(self, res = None):
        """
        Return linearized derivation.
        """
        if res == None:
            res = list()
        self.decRefCount()
        if self.refCount==0:
            res.append(self)
            parents = self.getParents()
            for p in parents:
                p.linearizeDerivation(res)
        return res

    def orderedDerivation(self):
        self.annotateDerivationGraph()
        res = self.linearizeDerivation()
        res.reverse()
        return res

    def computeEqLen(self):
        if self.derivation.isInputDeriv() and "conjecture" in self.type:
            self.eqLen = 0
        if self.eqLen == None:
            self.eqLen = self.derivation.computeEqLen()
        return self.eqLen

    def computeRWSteps(self):
        if self.derivation.isInputDeriv() and "conjecture" in self.type:
            self.rwSteps = 0
        if self.rwSteps == None:
            self.rwSteps = self.derivation.computeRWSteps()
        return self.rwSteps

    def checkForwardReferences(self):
        """
        Check if all references point (topologically)
        backwards. Terminate with Verification failure if not.
        """
        for i in self.getParents():
            if i.number > self.number:
                VerificationStatus(f"VerifiedBad: Step {self.name} references topologically later {i.name}")


def enableDerivationOutput():
    Derivable.printDerivation = True

def disableDerivationOutput():
    Derivable.printDerivation = False

def toggleDerivationOutput():
     Derivable.printDerivation = not Derivable.printDerivation



class Derivation(object):
    """
    A derivation object. A derivation is either trivial ("input"), a
    reference to an existing Derivable object ("reference"), or an
    inference with a list of premises.
    """
    def __init__(self, operator, parents=None, status="status(thm)", skolemdata=None):
        """
        Initialize  a derivation object with the operator and a list
        of parents (which can be Derivations or, in the case of
        "reference", Derivables).
        """
        if operator in ["reference", "quasi_ref"]:
            # print(f"Parents: {parents}")
            assert(len(parents)==1)
        self.operator = operator
        self.parents  = parents
        self.status   = status
        self.skolemdata = skolemdata

    def __repr__(self):
        """
        Return a string for the derivation in TPTP-3 format.
        """
        if self.isInputDeriv():
            return f"file('{self.parents[0]}', {self.parents[1]})"
        elif self.operator.startswith("theory("):
            return self.operator
        elif self.operator == "reference":
            # print("reference:", self.parents)
            assert(len(self.parents)==1)
            return self.parents[0].name
        elif self.operator == "quasi_ref":
            assert(len(self.parents)==1)
            return self.parents[0]
        elif self.operator == "skolemize":
            return f"inference({self.operator},[{self.status},"+\
                f"new_symbols(skolem,[{self.skolemdata[0]}])"+\
                f",skolemize({self.skolemdata[1]},"+\
                f"{term2String(self.skolemdata[2])})],{self.parents})"
        else:
            return "inference(%s,[%s],%s)"%\
                   (self.operator, self.status, repr(self.parents))

    def isInputDeriv(self):
        """
        Return true if this derivation corresponds to an input
        clause/formula, i.e. it is justified simply by pointing to its
        origin.
        """
        return self.operator == "file"

    def isSimpleQuotation(self):
        return self.operator == "reference"

    def getInputParts(self):
        """
        Return file and name of an input step.
        """

    def getParents(self):
        """
        Return a list of all derived objects that are used in this
        derivation.
        """
        if self.isInputDeriv():
            return []
        elif self.operator.startswith("theory("):
            return []
        elif self.operator == "reference":
            assert(len(self.parents)==1)
            return self.parents
        elif self.operator == "quasi_ref":
            return []
        else:
            res = list()
            for p in self.parents:
                res.extend(p.getParents())
            return res

    def getAncestors(self):
        parents = self.getParents()
        res = set(parents)
        for p in parents:
            res |= p.getAncestors()
        return res

    def getRecDerivationStatuses(self):
        """
        Return a set of all statuses used in the
        derivation.
        """
        if self.operator.startswith("theory("):
            return set()
        elif self.operator == "reference":
            return set()
        else:
            res = set([self.status])
            for p in self.parents:
                res = res|p.getRecDerivationStatuses()
            return res

    def getDerivationStatuses(self):
        """
        Return a set of all statuses used in the
        derivation.
        """
        if self.isInputDeriv():
            return set()
        if self.isSimpleQuotation():
            return set(["status(thm)"])
        else:
            return self.getRecDerivationStatuses()

    def resolveQuasiReferences(self, index):
        if self.operator == "quasi_ref":
            self.operator = "reference"
            # print("QParents: ", self.parents)
            assert(len(self.parents)==1)
            for p in self.parents:
                if not p in index:
                    VerificationStatus(f"VerifiedBad: Identifier '{p}' cannot be resolved")
            parents = [index[p] for p in self.parents]
            assert(len(parents)==1)
            self.parents = parents
        elif self.isInputDeriv():
            pass
        else:
            # print(self.parents)
            if self.parents:
                for p in self.parents:
                    p.resolveQuasiReferences(index)

    def computeEqLen(self):
        if self.isInputDeriv():
            return 1
        elif self.operator == "reference":
            return self.parents[0].computeEqLen()
        else:
            # print(self.operator, len(self.parents))
            res = 0
            if self.parents:
                for p in self.parents:
                    res += p.computeEqLen()
            return res

    def computeRWSteps(self):
        if self.isInputDeriv():
            return 0
        elif self.operator == "reference":
            return 0
        else:
            res = 0
            if(self.operator in ["rw", "sr"]):
                res = 1
            if self.parents:
                for p in self.parents:
                    res += p.computeRWSteps()
            return res


def parseSkolemData(lexer):
    lexer.AcceptTok(Token.OpenSquare)
    lexer.AcceptLit("status")
    lexer.AcceptTok(Token.OpenPar)
    lexer.CheckLit("esa")
    status = "status(%s)"%(lexer.LookLit(),)
    lexer.AcceptTok(Token.IdentLower)
    lexer.AcceptTok(Token.ClosePar)
    lexer.AcceptTok(Token.Comma)
    lexer.AcceptLit("new_symbols")
    lexer.AcceptTok(Token.OpenPar)
    lexer.AcceptLit("skolem")
    lexer.AcceptTok(Token.Comma)
    lexer.AcceptTok(Token.OpenSquare)
    skolem = lexer.LookLit()
    lexer.AcceptTok(Token.IdentLower)
    lexer.AcceptTok(Token.CloseSquare)
    lexer.AcceptTok(Token.ClosePar)
    lexer.AcceptTok(Token.Comma)
    lexer.AcceptLit("skolemize")
    lexer.AcceptTok(Token.OpenPar)
    lexer.CheckTok(Token.IdentUpper)
    var = parseTerm(lexer)
    lexer.AcceptTok(Token.Comma)
    lexer.CheckLit(skolem)
    skolemterm = parseTerm(lexer)
    varlist = termArgs(skolemterm)
    for t in varlist:
        if not termIsVar(t):
            raise ScannerError(f"All arguments of a Skolem term must be variables, {term2String(t)} is not")
    lexer.AcceptTok(Token.ClosePar)
    lexer.AcceptTok(Token.CloseSquare)
    return status,skolem,var,skolemterm,varlist

def parsePrologishTermList(lexer):
    """
    Parse (and ignore) something that seems to be a (non-empty)
    Prolog-term list.
    """
    parsePrologishTerm(lexer)
    while lexer.TestTok(Token.Comma):
        lexer.AcceptTok(Token,Comma)
        parsePrologishTerm(lexer)


def parsePrologishTerm(lexer):
    """
    Parse (and ignore) something that seems to be a Prolog-term.
    """
    if lexer.TestTok(Token.OpenSquare):
        lexer.AcceptTok(Token.OpenSquare)
        parsePrologishTermList(lexer)
        lexer.AcceptTok(Token.CloseSquare)
    else:
        lexer.AcceptTok([Token.IdentUpper, Token.IdentLower])
        if lexer.TestTok(Token.OpenPar):
            lexer.AcceptTok(Token.OpenPar)
            if not lexer.TestTok(Token.ClosePar):
                parsePrologishTermList(lexer)
            lexer.AcceptTok(Token.ClosePar)


def parseInfDataItem(lexer):
    """
    Parse one annotation item of an inference step. This can be
    status(<status>), new_symbols(<bla>, [<symbols>],
    skolemize(<Var>,<term>), or a random nested something.
    We return a tuple with the recognized components != None.
    """
    status = None
    skolem = None
    var    = None
    skolemterm = None
    varlist = None

    if lexer.TestLit("status"):
        lexer.AcceptLit("status")
        lexer.AcceptTok(Token.OpenPar)
        status = "status(%s)"%(lexer.LookLit(),)
        lexer.AcceptTok(Token.IdentLower)
        lexer.AcceptTok(Token.ClosePar)
    elif lexer.TestLit("new_symbols"):
        lexer.AcceptLit("new_symbols")
        lexer.AcceptTok(Token.OpenPar)
        lexer.AcceptTok(Token.IdentLower)
        lexer.AcceptTok(Token.Comma)
        lexer.AcceptTok(Token.OpenSquare)
        skolem = lexer.LookLit()
        lexer.AcceptTok(Token.IdentLower)
        lexer.AcceptTok(Token.CloseSquare)
        lexer.AcceptTok(Token.ClosePar)
    elif lexer.TestLit("skolemize"):
        lexer.AcceptLit("skolemize")
        lexer.AcceptTok(Token.OpenPar)
        lexer.CheckTok(Token.IdentUpper)
        var = parseTerm(lexer)
        lexer.AcceptTok(Token.Comma)
        # lexer.CheckLit(skolem)
        skolemterm = parseTerm(lexer)
        varlist = termArgs(skolemterm)
        for t in varlist:
            if not termIsVar(t):
                raise ScannerError(f"All arguments of a Skolem term must be variables, {term2String(t)} is not")
        lexer.AcceptTok(Token.ClosePar)
    else:
        parsePrologishTerm()


    return status,skolem,var,skolemterm,varlist

def parseInfData(lexer):
    status = None
    skolem = None
    var    = None
    skolemterm = None
    varlist = None
    first = True

    lexer.AcceptTok(Token.OpenSquare)
    while not lexer.TestTok(Token.CloseSquare):
        if first:
            first = False
        else:
            lexer.AcceptTok(Token.Comma)

        lstatus,lskolem,lvar,lskolemterm,lvarlist = parseInfDataItem(lexer)
        if lstatus != None:
            status = lstatus
        if lskolem != None:
            skolem = lskolem
        if lvar != None:
            var = lvar
        if lskolemterm != None:
            skolemterm = lskolemterm
        if lvarlist != None:
            varlist = lvarlist
    lexer.AcceptTok(Token.CloseSquare)

    return status,skolem,var,skolemterm,varlist


def parseRecDerivation(lexer):
    if lexer.TestLit("inference"):
        lexer.AcceptLit("inference")
        lexer.AcceptTok(Token.OpenPar)
        operator = lexer.LookLit()
        lexer.AcceptTok(Token.IdentLower)
        lexer.AcceptTok(Token.Comma)

        tmp = parseInfData(lexer)
        status = tmp[0]
        skolemdata = tmp[1:]

        if operator == "skolemize":
            if None in skolemdata:
                raise IncompleteDataError("Skolem informatiom incomplete")
            skolem,var,skolemterm,varlist = skolemdata
            if skolem!=skolemterm[0]:
                raise InconsistentDataError(f"Skolem symbol {skolem} not heading skolem term {term2String(skolemterm)}")

        if not status:
            raise IncompleteDataError("Inference record has no status")
        lexer.AcceptTok(Token.Comma)
        lexer.AcceptTok(Token.OpenSquare)
        parents = list()
        if not lexer.TestTok(Token.CloseSquare):
            parent = parseRecDerivation(lexer)
            parents.append(parent)
            while lexer.TestTok(Token.Comma):
                lexer.AcceptTok(Token.Comma)
                parent = parseRecDerivation(lexer)
                parents.append(parent)
        lexer.AcceptTok(Token.CloseSquare)
        lexer.AcceptTok(Token.ClosePar)
        return Derivation(operator, parents, status, skolemdata)
    elif lexer.TestTok([Token.IdentLower, Token.Integer]):
        name = lexer.LookLit()
        lexer.AcceptTok([Token.IdentLower,Token.Integer])
        return Derivation("quasi_ref", [name])

def parseDerivation(lexer):
    if lexer.TestLit("file"):
        lexer.AcceptLit("file")
        lexer.AcceptTok(Token.OpenPar)
        filename = lexer.LookLit().strip("'")
        lexer.AcceptTok(Token.SQString)
        lexer.AcceptTok(Token.Comma)
        name = lexer.LookLit()
        lexer.AcceptTok([Token.IdentLower,Token.SQString])
        lexer.AcceptTok(Token.ClosePar)
        return Derivation("file", (filename,name))
    else:
        return parseRecDerivation(lexer)


def flatDerivation(operator, parents, status="status(thm)"):
    """
    Simple convenience function: Create a derivation which directly
    references all parents.
    """
    parentlist = [Derivation("reference", [p]) for p in parents]
    return Derivation(operator, parentlist, status)



class TestDerivations(unittest.TestCase):
    """
    """
    def setUp(self):
        print()

    def testDerivable(self):
        """
        Test basic properties of derivations.
        """
        o1 = Derivable()
        o2 = Derivable()
        o3 = Derivable()
        o3.setDerivation(flatDerivation("resolution", [o1, o2]))
        self.assertEqual(o1.getParents(),[])
        self.assertEqual(o2.getParents(),[])
        self.assertEqual(len(o3.getParents()), 2)
        print(o3)
        print(o3.derivation)
        o3.setDerivation(flatDerivation("factor", [o1]))
        print(o3.derivation)
        self.assertEqual(len(o3.getParents()), 1)

    def testProofExtraction(self):
        """
        Test basic proof extraction.
        """
        o1 = Derivable()
        o2 = Derivable()
        o3 = Derivable()
        o4 = Derivable()
        o5 = Derivable()
        o6 = Derivable()
        o7 = Derivable()
        o1.setDerivation(Derivation("theory(equality)"))
        print(repr(o1.derivation))
        o2.setDerivation(Derivation("file", ('\'fake\'', 'fake')))
        o3.setDerivation(flatDerivation("factor", [o1]))
        o4.setDerivation(flatDerivation("factor", [o3]))
        o5.setDerivation(flatDerivation("resolution", [o1,o2]))
        o6.setDerivation(Derivation("reference", [o5]))
        o7.setDerivation(flatDerivation("resolution", [o5,o1]))
        proof = o7.orderedDerivation()
        print(proof)
        self.assertEqual(len(proof),4)
        self.assertTrue(o1 in proof)
        self.assertTrue(o2 in proof)
        self.assertTrue(o5 in proof)
        self.assertTrue(o7 in proof)

    def testOutput(self):
        """
        Test derivation output functions.
        """
        o1 = Derivable()
        o2 = Derivable()
        o3 = Derivable()
        o4 = Derivable()
        o1.setDerivation(Derivation("theory(equality)"))
        o2.setDerivation(Derivation("input"))
        o3.setDerivation(flatDerivation("resolution", [o1, o2]))
        enableDerivationOutput()
        self.assertTrue(o2.strDerivation()!="")
        self.assertTrue(o3.strDerivation()!="")
        self.assertTrue(o4.strDerivation()=="")
        disableDerivationOutput()
        self.assertTrue(o3.strDerivation()=="")
        self.assertTrue(o4.strDerivation()=="")
        toggleDerivationOutput()
        self.assertTrue(o3.strDerivation()!="")
        self.assertTrue(o4.strDerivation()=="")



if __name__ == '__main__':
    unittest.main()