Parser for Certificates #
This file contains a parser for parsing certificates for the proof system.
Try to read the file at the given path, and try to parse it into a certificate for the planing
task pt. Each line of the certificate is expected to either be an action set expression,
a state set expression, a piece of knowledge or a comment (starting with #).
Action set expressions have the following formats, where <AID> stands for action set ID.
The action set ID after a is the ID of the action set itself, it should start at 0 and
increase by one for each action set expression.
a <AID> b <amount of actions> <list of action IDs> (list of actions)
a <AID> u <AID left> <AID right> (union of actions)
a <AID> a (set of all actions)
State set expressions have the following formats, where <SID> stands for state set ID.
The state set ID after e is the ID of the state set itself, it should start at 0 and
increase by one for each state set expression.
e <SID> c e (constant empty set)
e <SID> c i (constant initial state set)
e <SID> c g (constant goal set)
e <SID> b <bdd_filename> <bdd_index> (bdd set)
e <SID> h <discription in DIMACS> (horn set)
e <SID> e <TODO> (MODS set)
e <SID> n <ID of negated state set> (negation)
e <SID> i <SID left> <SID right> (intersection)
e <SID> u <SID left> <SID right> (union)
e <SID> p <SID> <AID> (progression)
e <SID> r <SID> <AID> (regression)
Knowledge expressions have the following formats, where <KID> stands for knowledge ID.
The knowledge ID after k is the ID of the knowledge itself, it should start at 0 and
increase by one for each piece of knowledge. For dead knowledge, the ID after d is the
ID of state set that is dead, and for subset knowledge the IDs after s are the IDs
corresponding to the left and right state set. The knowledge IDs after the rule are the IDs
of the premises.
k <KID> d <SID> ed (empty set dead)
k <KID> d <SID> ud <KID> <KID> (union dead)
k <KID> d <SID> sd <KID> <KID> (subset dead)
k <KID> d <SID> pg <KID> <KID> <KID> (progression goal)
k <KID> d <SID> pi <KID> <KID> <KID> (progression initial)
k <KID> d <SID> sd <KID> <KID> <KID> (regression goal)
k <KID> d <SID> pg <KID> <KID> <KID> (regression initial)
k <KID> u ci <KID> (conclusion initial)
k <KID> u cg <KID> (conclusion goal)
k <KID> s <SID> <SID> urs (union right state)
k <KID> s <AID> <AID> ura (union right action)
k <KID> s <SID> <SID> uls (union left state)
k <KID> s <AID> <AID> ula (union left action)
k <KID> s <SID> <SID> irs (intersection right state)
k <KID> s <SID> <SID> ils (intersection left state)
k <KID> s <SID> <SID> dis (distributivity state)
k <KID> s <SID> <SID> sus <KID> <KID> (subset union state)
k <KID> s <AID> <AID> sua <KID> <KID> (subset union action)
k <KID> s <SID> <SID> sis <KID> <KID> (subset intersection state)
k <KID> s <SID> <SID> sts <KID> <KID> (subset transitivity state)
k <KID> s <AID> <AID> sta <KID> <KID> (subset transitivity action)
k <KID> s <SID> <SID> at <KID> <KID> (action transitivity)
k <KID> s <SID> <SID> au <KID> <KID> (action union)
k <KID> s <SID> <SID> pt <KID> <KID> (progression transitivity)
k <KID> s <SID> <SID> pu <KID> <KID> (progression union)
k <KID> s <SID> <SID> pr <KID> (progression regression)
k <KID> s <SID> <SID> rp <KID> (regression progression)
k <KID> s <SID> <SID> b1 (basic statement 1)
k <KID> s <SID> <SID> b2 (basic statement 2)
k <KID> s <SID> <SID> b3 (basic statement 3)
k <KID> s <SID> <SID> b4 (basic statement 4)
k <KID> s <AID> <AID> b5 (basic statement 5)
Equations
- One or more equations did not get rendered due to their size.