pycheck.py

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

"""
Usage: pycheck.py [options] <proof_file>

This program parses (some) TPTP-3 format proofs (FOF only, no frills -
we reuse the PyRes-Parser) and will try to proofcheck the proof, using
E as a backend for deductive steps, and smart hacks for others (I hope
;-)

Options:

 -h
--help
  Print this help.

 -v
--V
  Be a bit more verbose

 -e<path>
--eprover=<path>
  Provide an explixit path to eprover.


Copyright 2026 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

"""

import sys
import asyncio
import re
from resource import RLIMIT_STACK, setrlimit, getrlimit
import getopt
from version import version, Verbose
from derivations import *
from clauses import Clause
from formulas import Formula, WFormula, clauseToFormula
from formulacnf import formulaVarNormalize, formulasAreAlphaEquiv
from fofspec import FOFSpec
from checkutil import VerificationStatus

EPROVER = "eprover"

def processOptions(options):
    """
    Process the options given
    """
    global Verbose, EPROVER
    for opt, optarg in options:
        if opt in ("-h", "--help"):
            print("pycheck.py "+version)
            print(__doc__)
            sys.exit()
        elif opt in ("-v", "--Verbose"):
            Verbose = True
        elif opt in ("-e", "--eprover"):
            EPROVER = optarg

res_match_re = re.compile("% SZS status (.*)")

class FileCache:
    """
    Provide access to a set of FOF problems potentially to be read
    from the file names provided.
    """
    def __init__(self, refdir = None):
        self.cache = {}
        self.refdir = refdir

    def requestSpec(self, filename):
        """
        Return the FOFSpec corresponding to a given file name."
        """
        if not filename in self.cache:
            spec = FOFSpec()
            spec.parse(filename, self.refdir)
            self.cache[filename] = spec
        return self.cache[filename]

    def getDerivable(self, filename, name):
        """
        Find and return a clause/formula with the given name in the
        spec corresponding to a given file name (or None, if that does
        not exist).
        """
        spec = self.requestSpec(filename)
        return spec.getDerivable(name)

async def run_prover(step, formulas):
    """
    Run E (i.e. EPROVER) and translated the result into a verification
    error (or not).
    """
    job = await asyncio.create_subprocess_shell(
        EPROVER+" --auto-schedule=8 -s --cpu-limit=5 -",
        stdin=asyncio.subprocess.PIPE,
        stdout=asyncio.subprocess.PIPE,
        stderr=asyncio.subprocess.PIPE,
    )
    # print(formulas)
    prob =  "\n".join([repr(f) for f in formulas])+"\n"
    # print("Problem:\n", prob)

    prob = prob.encode('utf-8')
    res_out, res_err = await job.communicate(prob)
    res_out = res_out.decode('utf-8')
    res_err = res_err.decode('utf-8')
    # print(res_out, res_err)
    mo = res_match_re.search(res_out)
    res = mo.groups()[0]
    if res == "ResourceOut":
        VerificationStatus(f"Unknown : Verifying '{step.name}' hit resource limit")
    elif res in ["Satisfiable", "CounterSatisfiable"]:
        VerificationStatus(f"VerifiedBad : '{step.name}' is unsound")
    elif res in ["Theorem", "ContradictoryAxioms"]:
        print(f"% Verified step '{step.name}'")
    else:
        VerificationStatus(f"Unknown : Unexpected resuls {res} for '{step.name}'")


def checkConjectureStructConstraints(step, problem):
    """
    Checks that only plain references of type conjecture and
    negated_conjctures with the appropriate derivation status
    reference a conjecture formula.
    """
    for f in problem.ordered_proof:
        if step in f.getParents():
            if f.type == "conjecture" and f.isSimpleQuotation():
                continue
            if f.type == "negated_conjecture" and f.derivation.status=="status(cth)":
                continue
            VerificationStatus(f"VerifiedBad : Conjecture '{step.name}' is"
                               +f" used weirdly by {f.name}")


def checkInputStep(step, filecache):
    """
    Check a step with justification "file(...)".
    """
    print(f"% Verifying input step '{step.name}'")
    filename, name = step.derivation.parents
    premise = filecache.getDerivable(filename, name)
    if premise is None:
        VerificationStatus(f"VerifiedBad : Step '{step.name}' is not in the input file")
    # print(f"Input: {premise}")
    if isinstance(step, Clause):
        stepf = clauseToFormula(step)
    else:
        stepf = step.formula
    if isinstance(premise, Clause):
        premf = clauseToFormula(premise)
    else:
        premf = premise.formula
    #stepf = formulaVarNormalize(stepf)
    #premf = formulaVarNormalize(premf)
    # print(f"{stepf} == {premf}")
    if not formulasAreAlphaEquiv(stepf, premf):
        VerificationStatus(f"VerifiedBad : Step '{step.name}' is not alpha-equal to {premise.name}")
    print(f"% Verified step '{step.name}'")


def checkSkolemizationStep(step, problem):
    """
    Check a skolemization step by trying to reconstruct it, checking
    for variable skope and symbol freshness.
    """
    print(f"% Verifying Skolemization step '{step.name}'")
    skolem,var,skolemterm,varlist = step.derivation.skolemdata
    if problem.sig.isFun(skolem):
        VerificationStatus(f"VerifiedBad : Skolem symbol '{skolem}' is"
                           +f" not new in '{step.name}'")
    problem.sig.addFun(skolem, len(termArgs(skolemterm)))
    parents = step.getParents()
    if len(parents)!=1:
        VerificationStatus("VerifiedBad : Skolemization step "
                           +f"'{step.name}' has more than one parent")
    parent = parents[0]
    pform = parent.formula
    if not pform.quantifiedVarsAreUnique():
        VerificationStatus("VerifiedBad : Skolemization step "
                           +f"'{step.name}' source '{parent.name}' "
                           +"is not variable-normalized")

    scope = pform.findQuantifierScope("?", var)
    if scope is None:
        VerificationStatus("VerifiedBad : Skolemization step "
                           +f"'{step.name}' source '{parent.name}' "
                           +f"does not contain ?[{var}]")
    newvars = []
    for (q,v) in scope:
        if q!="!":
            VerificationStatus("VerifiedBad : Skolemization step "
                               +f"'{step.name}' does not Skolemize"
                               +"outermost existential variable")
        newvars.append(v)
    if set(varlist)!=set(newvars):
        VerificationStatus("VerifiedBad : Skolemization step "
                           +f"'{step.name}' does not use exactly the "
                           "variables in scope")

    skform = pform.applySkolem(var, skolemterm)
    print("Before:", pform, "Skolemized:", skform, "Step: ", step.formula)
    if not formulasAreAlphaEquiv(step.formula,skform):
        VerificationStatus(f"VerifiedBad : Skolemization of '{step.name}'"
                           +f" does not correspond to '{skform}'")
    print(f"% Verified Skolemization step '{step.name}'")




async def checkProofStep(step, problem, filecache):
    """
    Check step (
    """
    print(f"% Performing local checks on '{step.name}'")

    if step.type not in ["axiom",
                         "conjecture",
                         "negated_conjecture",
                         "plain",
                         "definition"]:
        VerificationStatus(f"VerifiedBad : Step '{step.name}' has unknown role {step.type}")
    if step.type == "conjecture":
        checkConjectureStructConstraints(step, problem)

    if not step.derivation:
        VerificationStatus(f"VerifiedBad : Step '{step.name}' has no justification")

    if step.derivation.operator == "file":
        checkInputStep(step, filecache)
    else:
        statuses = step.derivation.getDerivationStatuses()
        if len(statuses) > 1:
            VerificationStatus(f"VerifiedBad : Step '{step.name}''s "
                               +f"derivation has multiple statuses: {statuses}")
        premises = step.getParents()
        if isinstance(step, Clause):
            concl = clauseToFormula(step)
        else:
            concl = step.formula
        # print("Premises: ", [p.name for p in premises])
        #for p in premises:
        #    try:
        #        print(p.name, p)
        #    except AssertionError:
        #        print(p.name, p.derivation.parents)
        # print("Conclusion:\n", concl)
        if "status(cth)" in statuses:
            print(f"# Verifying cth step '{step.name}'")
            # new_prem = WFormula(premises[0].formula, "plain", premises[0].name)
            # premises = [new_prem]
            # concl = Formula("~", concl)
            # conclf = WFormula(concl, "conjecture", "prove_to_verify")
            # premises.append(conclf)
            lhs  = premises[0].formula
            rhs = Formula("~", concl)
            concl = Formula("<=>", lhs, rhs)
            conclf = WFormula(concl, "conjecture", "prove_to_verify")
            await run_prover(step, [conclf])
        elif "status(thm)" in statuses:
            print(f"# Verifying thm step '{step.name}'")
            conclf = WFormula(concl, "conjecture", "prove_to_verify")
            premises.append(conclf)
            await run_prover(step, premises)
        elif "status(esa)" in statuses:
            print(f"# Verifying esa/skolemize step '{step.name}'")
            if not step.derivation.operator == "skolemize":
                VerificationStatus(f"Unknown : Cannot handle {step.operator} "
                                   + "with status(esa) in '{step.name}'")
            checkSkolemizationStep(step, problem)


async def checkProofSteps(problem):
    """
    Go through the (necessary) proof steps and check them.
    """
    filecache = FileCache(problem.refdir)
    for step in problem.ordered_proof:
        await checkProofStep(step, problem, filecache)




if __name__ == '__main__':
    # We try to increase stack space, since we use a lot of
    # recursion. This works differentially well on different OSes, so
    # it is a bit more complex than I would hope for.
    try:
        soft, hard = getrlimit(RLIMIT_STACK)
        soft = 10*soft
        if  soft > hard > 0:
            soft = hard
        setrlimit(RLIMIT_STACK, (soft, hard))
    except ValueError:
        # For reasons nobody understands, this seems to fail on
        # OS-X. In that case, we just do our best...
        pass

    sys.setrecursionlimit(10000)

    try:
        opts, args = getopt.gnu_getopt(sys.argv[1:],
                                       "hve:",
                                       ["help", "Verbose", "eprover="])
    except getopt.GetoptError as err:
        print(sys.argv[0],":", err)
        sys.exit(1)

    processOptions(opts)

    Derivable.printDerivation = True
    for file in args:
        proof = FOFSpec()
        proof.parse(file)
        proof.resolveQuasiReferences()
        proof.checkStructure()

        # print(proof)

        asyncio.run(checkProofSteps(proof))

        VerificationStatus(f"VerifiedGood : No problems found with '{file}'")