29class RupInfo:
30
31  '''
32  Information on a failed RUP check.
33
34  **Attributes**:
35    
36    clause (`Clause`): The clause that failed the RUP check.
37
38    chain (`Chain`): A sequence of unit literals that failed to
39      derive an empty clause via propagation, with no further 
40      opportunities to propagate.
41  '''
42
43  def __init__(self, clause : Clause, chain : Chain):
44    self.clause = clause
45    self.chain = chain
46
47  def __str__(self):
48    return f"RupInfo({str(self.clause)}, {str(self.chain)})"

50class RatInfo:
51
52  '''
53  Information on a failed RAT check.
54
55  **Attributes**:
56    clause (`Clause`): The clause that failed the RAT check.
57
58    pivot_clause (`Clause`): A pivot clause that failed a RUP check.
59
60    rup_info (`RupInfo`): Information on the failed RUP check.
61  '''
62
63  def __init__(self, clause : Clause, pivot_clause : Clause, rup_info : RupInfo):
64    self.clause = clause
65    self.pivot_clause = pivot_clause
66    self.rup_info = rup_info
67
68  def __str__(self):
69    return f"RatInfo({str(self.clause)}, {str(self.pivot_clause)}, {str(self.rup_info)})"

 71class CheckerResult:
 72
 73  '''
 74  Result of a proof check.
 75
 76  **Attributes**:
 77
 78    outcome (`Outcome`): The outcome of the check. If the check
 79      succeeded, this will be Outcome.VALID. If the check failed,
 80      this will be Outcome.INVALID.
 81
 82    steps (`Optional[Cnf]`): Completed proof steps prior to an invalid step, 
 83      if the proof was invalid.
 84
 85    rup_info (`Optional[RupInfo]`): Information on a failed RUP check,
 86      if the proof was invalid.
 87
 88    rat_info (`Optional[RatInfo]`): Information on a failed RAT check,
 89      if the proof was invalid. The RAT clause in this object will
 90      be the same as the RUP clause in `rup_info`.
 91  '''
 92
 93  def __init__(self, outcome : Outcome, steps : Optional[Cnf], rup_info : Optional[RupInfo], rat_info : Optional[RatInfo]):
 94    self.outcome = outcome
 95    self.steps = steps
 96    self.rup_info = rup_info
 97    self.rat_info = rat_info
 98
 99  def __str__(self):
100    if self.outcome == Outcome.VALID:
101      return f"CheckerResult({self.outcome})"
102    else:
103      if self.steps is not None and self.rup_info is not None and self.rat_info is not None:
104        steps = " ".join(str(step) for step in self.steps)
105        rup = str(self.rup_info)
106        rat = str(self.rat_info)
107        return f"CheckerResult({self.outcome}, [{steps}], {rup}, {rat})"
108      else:
109        return f"CheckerResult({self.outcome})"

267def check_proof(formula : Cnf, proof : Proof, verbose : bool = False) -> CheckerResult:
268  """Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables
269  of clauses, where each clause is an iterable of signed Python ints.
270
271  **Args:**
272    formula (`Cnf`): Cnf as an iterable of clauses.
273
274    proof (`Proof`): Iterable of RUP or RAT clauses.
275    
276    verbose (bool, optional): Return detailed information
277      if the check fails. Defaults to False.
278
279  **Returns:**
280    `CheckerResult`: CheckerResult struct representing the result of the check.
281  
282  **Raises:**
283    ValueError: If the formula or proof cannot be formatted.
284  """
285  return _check_proof_from_structs(_cnf_to_struct(formula), _cnf_to_struct(proof), verbose)

318def check_proof_from_files(formula_file : str, proof_file : str, verbose : bool = False) -> CheckerResult:
319  """Check a sequence of RUP and RAT clauses against a CNF.
320
321  **Args:**
322    formula_file (str): Path to a file containing a CNF in DIMACS format.
323    proof_file (str): Path to a file containing a sequence of RUP or RAT clauses.
324    verbose (bool, optional): Return detailed information
325      if the check fails. Defaults to False.
326
327  **Returns:**
328    `CheckerResult`: CheckerResult struct representing the result of the check.
329
330  **Raises:**
331    ValueError: If the formula or proof cannot be parsed or formatted.
332    FileNotFoundError: If the formula or proof file cannot be found.
333  """
334  with open(formula_file, 'r') as f:
335    formula = f.read()
336  with open(proof_file, 'r') as f:
337    proof = f.read()
338
339  return check_proof_from_strings(formula, proof, verbose)

287def check_proof_from_strings(formula : str, proof : str, verbose : bool = False) -> CheckerResult:
288  """Check a sequence of RUP and RAT clauses against a CNF.
289
290  **Args:**
291    formula (str): Cnf as a string in DIMACS format. The header
292      is ignored if present.
293    proof (str): Sequence of RUP or RAT clauses format.
294    verbose (bool, optional): Return detailed information
295      if the check fails. Defaults to False.
296  
297  **Returns:**
298    `CheckerResult`: CheckerResult struct representing the result of the check.
299
300  **Raises:**
301    ValueError: If the formula or proof cannot be parsed or formatted.
302  """
303  try:
304    formula = re.sub(' +', ' ', formula)
305    if '\n' in formula and formula.split('\n')[0].strip().startswith('p'):
306      formula = '\n'.join(formula.split('\n')[1:])
307    formula = _read_clauses(formula)
308  except:
309    raise ValueError("Error parsing formula. Check that the input is properly formatted.")
310  try:
311    proof = re.sub(' +', ' ', proof)
312    proof = _read_clauses(proof)
313  except:
314    raise ValueError("Error parsing proof. Check that the input is properly formatted.")
315
316  return check_proof(formula, proof, verbose)

402def check_derivation(formula : Cnf, derivation : Proof, verbose : bool = False) -> CheckerResult:
403  """Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables
404  of clauses, where each clause is an iterable of signed Python ints.
405
406  **Args:**
407    formula (`Cnf`): Cnf as an iterable of clauses.
408
409    derivation (`Proof`): Iterable of RUP or RAT clauses.
410    
411    verbose (bool, optional): Return detailed information
412      if the check fails. Defaults to False.
413
414  **Returns:**
415    `CheckerResult`: CheckerResult struct representing the result of the check.
416      If each step in the derivation is either RUP or RAT, then the result will
417      be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.
418      The derivation does not need to contain the empty clause.
419  
420  **Raises:**
421    ValueError: If the formula or derivation cannot be formatted.
422  """
423  return _check_derivation_from_structs(_cnf_to_struct(formula), _cnf_to_struct(derivation), verbose)

461def check_derivation_from_files(formula_file : str, derivation_file : str, verbose : bool = False) -> CheckerResult:
462  """Check a sequence of RUP and RAT clauses against a CNF.
463
464  **Args:**
465    
466    formula_file (str): Path to a file containing a CNF in DIMACS format.
467    
468    derivation_file (str): Path to a file containing a sequence of RUP or RAT clauses.
469    
470    verbose (bool, optional): Return detailed information
471      if the check fails. Defaults to False.
472
473  **Returns:**
474    `CheckerResult`: CheckerResult struct representing the result of the check.
475      If each step in the derivation is either RUP or RAT, then the result will
476      be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.
477      The derivation does not need to contain the empty clause.
478
479  **Raises:**
480    ValueError: If the formula or proof cannot be parsed or formatted.
481    FileNotFoundError: If the formula or proof file cannot be found.
482  """
483  with open(formula_file, 'r') as f:
484    formula = f.read()
485  with open(derivation_file, 'r') as f:
486    derivation = f.read()
487
488  return check_derivation_from_strings(formula, derivation, verbose)

425def check_derivation_from_strings(formula : str, derivation : str, verbose : bool = False) -> CheckerResult:
426  """Check a sequence of RUP and RAT clauses against a CNF.
427
428  **Args:**
429    formula (str): Cnf as a string in DIMACS format. The header
430      is ignored if present.
431    
432    proof (str): Sequence of RUP or RAT clauses format.
433    
434    verbose (bool, optional): Return detailed information
435      if the check fails. Defaults to False.
436  
437  **Returns:**
438    `CheckerResult`: CheckerResult struct representing the result of the check.
439      If each step in the derivation is either RUP or RAT, then the result will
440      be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.
441      The derivation does not need to contain the empty clause.
442
443  **Raises:**
444    ValueError: If the formula or proof cannot be parsed or formatted.
445  """
446  try:
447    formula = re.sub(' +', ' ', formula)
448    if '\n' in formula and formula.split('\n')[0].strip().startswith('p'):
449      formula = '\n'.join(formula.split('\n')[1:])
450    formula = _read_clauses(formula)
451  except:
452    raise ValueError("Error parsing formula. Check that the input is properly formatted.")
453  try:
454    derivation = re.sub(' +', ' ', derivation)
455    derivation = _read_clauses(derivation)
456  except:
457    raise ValueError("Error parsing derivation. Check that the input is properly formatted.")
458
459  return check_derivation(formula, derivation, verbose)