#include "xproofs.h"

This page has information from files xproofs.h and xproofs.c.

Contents

Public Routines in File xproofs.c

Index

check_parents_and_uplinks_in_proofexpand_proofproof_id_to_clauserenumber_proof
copy_and_renumber_proofgreatest_id_in_proofproof_to_xproof

Details

void check_parents_and_uplinks_in_proof(Plist proof);

Plist copy_and_renumber_proof(Plist proof, int start);
We assume that every clause occurs after its parents. 
Plist expand_proof(Plist proof, I3list *pmap);
Given a proof, return a more detailed proof, entirely new, leaving the given proof unchanged. Also returned is an I3list mapping new IDs to pairs . The n compnent identifies the sub-steps arising from the expansions, e.g., 66 -> <23,4> means that step 66 in the new proof corresponds to the 4th substep in expanding step 23 of the old proof. Clauses in the new proof that match clauses in the old proof retain the IDs from the old proof, and there is no entry in the map for them. 
int greatest_id_in_proof(Plist proof);

Topform proof_id_to_clause(Plist proof, int id);

Plist proof_to_xproof(Plist proof);

void renumber_proof(Plist proof, int start);
We assume that every clause occurs after its parents.

Public Definitions in File xproofs.h

Introduction