#==============================================================================
#  The syntax of the ascii and binary QRP trace/proof formats in EBNF.
#==============================================================================
#
# General notes:
#
# + trace: We do not explicitely distinguish between actual traces (a set of
#          steps that represent a SET of clause AND cube resolution sequences) 
#          and proofs (a set of steps that represents exactly ONE clause OR 
#          cube resolution sequence).
#
# + header: The header statement contains two positive numbers - the number of
#           variables in the input formula (first) and the number of steps in 
#           the trace/proof (second). 
#           Note that in binary format, these two numbers are written in ASCII
#           (rather than being encoded).
#
# + quant_set: As in the QDIMACS format we denote existential quantifiers by 
#              "e" and universal quantifiers by "a". We further require that
#                - each variable in the prefix is unique
#                - consecutive quant_sets are not bound by the same quantifier
#                - the innermost quant_set is existentially quantified
#                - free variables are considered as existentially quantified 
#                  in the outermost quant_set.
#
# + step: A step consists of a unique identifier, a set of literals and a set
#         of antecedents (at most two). Note that a step may represent
#           - an input clause/cube
#           - an application of universal/existential reduction
#             (to its antecedent)
#           - an applicaton of resolution 
#             (to its antecedents)
#           - an empty clause/cube
#
# + antecedents: A set of (unique) step indices (at most two).
#
# + result: The result statement indicates if given proof is a proof of
#           satisfiability or unsatisfiability. Note that in case of "unsat"
#           ("sat"), given proof is a clause (cube) resolution sequence.
#
#------------------------------------------------------------------------------


#==============================================================================
# The Ascii QRP Format
#==============================================================================

trace       = preamble { quant_set } { step } result EOF.

preamble    = { comment } header.
comment     = "#" text EOL.
header      = "p qrp" pnum pnum EOL.

quant_set   = quantifier { var } "0".
quantifier  = "a" | "e".
var         = pnum.

step        = idx literals antecedents.
idx         = pnum.
literals    = { lit } "0".
lit         = ["-"] var.
antecedents = [idx [idx]] "0".

result      = "r " sat EOL.
sat         = "sat" | "unsat".

text        = ? a sequence of non-special ASCII chars ?.
pnum        = ? a 32-bit signed integer > 0 ?.
EOL         = ? end-of-line marker ('\n') ?.
EOF         = ? end-of-file marker ?.


#==============================================================================
# The Binary QRP Format
#==============================================================================
#
# Notes: 
# 
# + header: The marker sequence and both positive numbers in the header
#           statement are given in ASCII (and not binary encoded).
#           
# + bin_(p)num: Is encoded/decoded as shown below (C syntax).
#
# + lit: Must be a binary encoding of an occurrence of var. Note that literals
#        are encoded as a positive number such that e.g. a positive (negative)
#        occurrence of variable "1" is encoded as "2" ("3").
# 
# + var, step: Variable and step indices may not occur negatively, hence we
#              encode them as is (and do not convert them into positive numbers
#              as we do for literals).
#
#------------------------------------------------------------------------------

trace       = preamble { quant_set } { step } result EOF.

preamble    = { comment } header.
comment     = "#" text EOL.
header      = "p bqrp" pnum pnum DELIM.

quant_set   = DELIM quantifier { var } DELIM.
quantifier  = "a" | "e".
var         = bin_pnum.

step        = idx literals antecedents.
idx         = bin_pnum.
literals    = { lit } DELIM.
lit         = bin_num.
antecedents = [idx [idx]] DELIM.

result      = DELIM "r " sat EOL.
sat         = "sat" | "unsat".

text        = ? a sequence of non-special ASCII chars ?.
pnum        = ? a 32-bit signed integer > 0 ?.
bin_num     = ? a binary encoded 32-bit signed integer ?.
bin_pnum    = ? a binary encoded 32-bit signed integer > 0 ?.
DELIM       = ? a null byte (0) ?
EOL         = ? end-of-line marker ('\n') ?.
EOF         = ? end-of-file marker ?.

#------------------------------------------------------------------------------
#
#  unsigned char
#  get_non_eof_ch (FILE *file)
#  { 
#    if (feof (file))
#    {
#      fprintf (stderr, "[ERROR] decode: unexpected EOF\n");
#      exit (EXIT_FAILURE);
#    }
#
#    return getc (file);
#  }
#
#  static int
#  decode_bin_num (void)
#  {
#    unsigned int x = 0, i = 0;
#    unsigned char ch;
#  
#    while ((ch = get_non_eof_ch (file) & 0x80)
#      x |= (ch & 0x7f) << (7 * i++);
#    x = x | (ch << (7 * i));
#    return (x & 1) ? -(x >> 1) : (x >> 1);
#  }
#
#  static int
#  decode_bin_pnum (void)
#  {
#    unsigned int x = 0, i = 0;
#    unsigned char ch;
#  
#    while ((ch = get_non_eof_ch (file) & 0x80)
#      x |= (ch & 0x7f) << (7 * i++);
#
#    return x | (ch << (7 * i));
#  }
#
#------------------------------------------------------------------------------
#
#  void
#  encode_bin_num (FILE *file, int num)
#  {
#    unsigned char ch;
#    unsigned int x = num < 0 ? (-x << 1) | 1 : x << 1;
#  
#    while (x & ~0x7f)
#    {
#      ch = (x & 0x7f) | 0x80;
#      putc (ch, stdout);
#      x >>= 7;
#    }
#
#    ch = x;
#    putc (ch, stdout);
#  }
#
#  void
#  encode_bin_pnum (FILE *file, int num)
#  {
#    unsigned char ch;
#    unsigned x = num;
#  
#    while (x & ~0x7f)
#    {
#      ch = (x & 0x7f) | 0x80;
#      putc (ch, stdout);
#      x >>= 7;
#    }
#
#    ch = x;
#    putc (ch, stdout);
#  }
#
#------------------------------------------------------------------------------