diff --git a/README.md b/README.md index 532465a..af24c5c 100644 --- a/README.md +++ b/README.md @@ -7,11 +7,6 @@ The core of the checker is written in [Why3](https://why3.lri.fr/), which is ext * The current implementation is not optimized, and will be considerably slower than [DRAT-trim](https://github.com/marijnheule/drat-trim) on large proofs (see [performance](#performance) below). * Accordingly, the frontend does not accept proofs in binary format. -The verification can be checked by running `src/librupchecker/rup_pure.mlw` in Why3. -Most of the verification conditions complete with the `Auto level 0` tactic, and the rest either with a few levels of splitting followed by `Auto 0` or `Auto 1`, or simply with `Auto 2`. -It was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8. -Verification has not been attempted with earlier versions of Why3 or the provers. - ## Installation If you use a recent Linux distribution on x86_64, you should be able to install the compiled wheel from PyPI: @@ -62,52 +57,46 @@ For more information visit https://github.com/cmu-transparency/verified_rup ### As a Python module -See the documentation for details of the API. -The primary function is `drup.check_proof`, or alternatively, `drup.check_derivation` to check each step of the proof, ignoring the absence of an empty clause). -```python -def check_proof(formula : Cnf, proof : Proof, verbose : bool = False) -> CheckerResult: - """Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables - of clauses, where each clause is an iterable of signed Python ints. - - Args: - formula (Cnf): Cnf as an iterable of clauses. - proof (Proof): Iterable of RUP or RAT clauses. - verbose (bool, optional): Return detailed information - if the check fails. Defaults to False. - - Returns: - CheckerResult: CheckerResult struct representing the result of the check. - - Raises: - ValueError: If the formula or proof cannot be formatted. - """ -``` -This takes a CNF and Proof as an iterable of iterables of signed integers, and returns a `CheckerResult`. -```python -class CheckerResult: - - ''' - Result of a proof check. +See the [documentation](http://fairlyaccountable.org/verified_rup/drup.html) for details of the API. +The primary function is `drup.check_proof`, or alternatively, `drup.check_derivation` to check each step of the proof, ignoring the absence of an empty clause). There are corresponding convenience functions `check_proof_from_strings` and `check_proof_from_files`, similarly for `check_derivation`. - Attributes: +The following example uses [CNFgen](https://massimolauria.net/cnfgen/) to generate a PHP instance, +and [PySAT](https://pysathq.github.io/) to solve it and generate a DRUP proof. +To illustrate the verbose output given for failed checks, only the first ten clauses of the proof are checked against the proof. - outcome (`Outcome`): The outcome of the check. If the check - succeeded, this will be Outcome.VALID. If the check failed, - this will be Outcome.INVALID. - - steps (`Optional[Cnf]`): Completed proof steps prior to an invalid step, - if the proof was invalid. +```python +import drup +import cnfgen +from pysat.formula import CNF +from pysat.solvers import Solver + +dimacs = cnfgen.BinaryPigeonholePrinciple(4, 3).dimacs() +cnf = CNF(from_string=dimacs).clauses +g4 = Solver(name='g4', with_proof=True, bootstrap_with=cnf) +g4.solve() +proof = [[int(l) for l in c.split(' ')[:-1]] for c in g4.get_proof()] + +drup.check_proof(cnf[:10], proof, verbose=True) +``` - rup_info (`Optional[RupInfo]`): Information on a failed RUP check, - if the proof was invalid. +This gives a `CheckerResult` object with the following information: - rat_info (`Optional[RatInfo]`): Information on a failed RAT check, - if the proof was invalid. The RAT clause in this object will - be the same as the RUP clause in `rup_info`. - ''' +```python +CheckerResult( + Outcome.INVALID, + [], + RupInfo([4, 6, 7, 8], [-4, -6, -7, -8, 3, 5]), + RatInfo( + [4, 6, 7, 8], + [-4, -3], + RupInfo([6, 7, 8, -3], [-6, -7, -8, 5, 3, -4]) + ) +) ``` -There are corresponding convenience functions `check_proof_from_strings` and `check_proof_from_files`, similarly for `check_derivation`. +The `RupInfo` component relates that RUP verification failed on the first clause of the proof, `4 6 7 8 0`, after propagating the literals `-4, -6, -7, -8, 3, 5`, and failing to find more opposites to propagate. +Likewise, the `RatInfo` component relates that RAT verification on this clause failed when checking the pivot on clause `-4 -3 0`. +The resolvent of these clauses, `6 7 8 -3 0`, failed RUP verification after propagating `-6 -7 -8 5 3 -4`. ## Performance @@ -132,6 +121,82 @@ In the table below, each configuration is run on 10,000 instances, with proofs g [[1]](https://openreview.net/forum?id=HJMC_iA5tm) Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill. *Learning a SAT Solver from Single-Bit Supervision*. International Conference on Learning Representations (ICLR), 2019. +## Verification + +The verification can be examined by running `src/librupchecker/rup_pure.mlw` in Why3, or by checking the Why3 session in `src/librupchecker/rup_pure/why3session.xml`. +The proof was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8. +Verification has not been attempted with earlier versions of Why3 or the provers. + +The primary contract on the proof checker is as follows: +```ocaml +requires { no_redundant_clauses cnf /\ no_trivial_clauses cnf } +requires { no_redundant_clauses pf /\ no_trivial_clauses pf } +ensures { match result with + | Valid -> valid_proof cnf pf + | _ -> proof_failure orig result + end } +``` +The bindings used by this library take care of removing redundant and trivial clauses. +The `valid_proof` predicate is a straightforward translation of DRAT certification requirements. +A `proof_failure` result provides additional assurances about the verbose output of the checker. +```ocaml +predicate proof_failure (cnf : cnf) (result : result) = + match result with + | Valid -> false + | InvalidEmpty steps rup_info -> rup_failure (steps ++ cnf) rup_info + | InvalidStep steps rup_info rat_info -> + rup_failure (steps ++ cnf) rup_info /\ rat_failure (steps ++ cnf) rat_info + end +``` +An `InvalidEmpty` result indicates all of the listed `steps` are valid, but the empty clause was not derived, as witnessed by the provided `rup_info`. +This is only returned when all of the steps in the proof are valid except an empty clause at the end. +The `rup_info` component ensures that the empty clause is not RUP, and that the unit chain used to conclude this is exhaustive. + +```ocaml +predicate rup_failure (cnf : cnf) (info : rup_info) = + not (rup cnf info.rup_clause) /\ + match info.rup_clause with + | Nil -> + let cnf' = bcp cnf info.chain in + is_unit_chain cnf info.chain /\ + forall chain' . is_unit_chain cnf' chain' -> + forall c . mem c (bcp cnf' chain') <-> mem c cnf' + | Cons _ _ -> + let cnf' = bcp (cnf ++ (negate_clause info.rup_clause)) info.chain in + is_unit_chain (cnf ++ (negate_clause info.rup_clause)) info.chain /\ + forall chain' . is_unit_chain cnf' chain' -> + forall c . mem c (bcp cnf' chain') <-> mem c cnf' + end +``` + +An `InvalidStep` result indicates that the `steps` are valid up to some non-empty step. +The next step in the certificate following `steps` is invalid, as witnessed by the provided `rup_info` and `rat_info`. +In addition to the assurances on `rup_info` described above, `rat_info` provides that the identified pivot clause is not RUP. + +```ocaml +predicate rat_failure (cnf : cnf) (info : rat_info) = + not (rat cnf info.rat_clause) /\ + match info.rat_clause with + | Nil -> false + | Cons l _ -> + mem info.pivot_clause (pivot_clauses cnf l) /\ + info.pivot_info.rup_clause = resolve info.rat_clause info.pivot_clause l /\ + rup_failure cnf info.pivot_info + end +``` + +The derivation checker provides a similar contract, but rather than ensuring `valid_proof` on success, it provides `valid_derivation`. + +```ocaml +predicate valid_derivation (cnf : cnf) (pf : proof) = + match pf with + | Nil -> true + | Cons c cs -> (rup cnf c \/ rat cnf c) /\ valid_derivation (Cons c cnf) cs + end +``` + +This is the same condition as `valid_proof`, but in the `Nil` case, the checker does not require that the empty clause is not RUP. + ## Acknowledgements Many thanks to [Frank Pfenning](http://www.cs.cmu.edu/~fp/), [Joseph Reeves](https://www.cs.cmu.edu/~jereeves/), and [Marijn Huele](https://www.cs.cmu.edu/~mheule/) for the ongoing insightful discussions that led to this project. \ No newline at end of file diff --git a/docs/drup.html b/docs/drup.html index a0c68dc..09d8202 100644 --- a/docs/drup.html +++ b/docs/drup.html @@ -26,6 +26,7 @@

Readme

  • Installation
  • Usage
  • Performance
    • +
  • Verification
  • Acknowledgements
    • @@ -133,17 +134,12 @@

  • Accordingly, the frontend does not accept proofs in binary format.
    • -

    The verification can be checked by running src/librupchecker/rup_pure.mlw in Why3. -Most of the verification conditions complete with the Auto level 0 tactic, and the rest either with a few levels of splitting followed by Auto 0 or Auto 1, or simply with Auto 2. -It was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8. -Verification has not been attempted with earlier versions of Why3 or the provers.

    -

    Installation

    If you use a recent Linux distribution on x86_64, you should be able to install the compiled wheel from PyPI:

    -
    $ pip install drup
+
    $ pip install drup
    @@ -151,7 +147,7 @@

    Installation

    The most straightforward way to install these is to use opam, which is available in most package systems, and then install Why3 and Dune (a sufficiently recent version of OCaml should already be installed with Opam):

    -
    $ opam install why3 dune
+
    $ opam install why3 dune
    @@ -160,17 +156,17 @@

    Installation

    Once OCaml and Why3 are installed, make sure that Python build is installed:

    -
    $ pip install build
+
    $ pip install build

    Then, clone this repository, build, and install the package:

    -
    $ git clone https://github.com/cmu-transparency/verified_rup.git
-$ cd verified_rup
-$ python -m build
-$ pip install dist/*.whl
+
    $ git clone https://github.com/cmu-transparency/verified_rup.git
+$ cd verified_rup
+$ python -m build
+$ pip install dist/*.whl
    @@ -181,77 +177,68 @@

    Command line interface

    The package provides a command line interface for checking proofs stored in files:

    -
    $ drup --help
-usage: drup [-h] [-d] [-v] dimacs drup
+
    $ drup --help
+usage: drup [-h] [-d] [-v] dimacs drup
 
-Checks DRUP & DRAT proofs against DIMACS source. Returns 0 if the proof is valid, -1 if not, or a negative error code if the input is invalid.
+Checks DRUP & DRAT proofs against DIMACS source. Returns 0 if the proof is valid, -1 if not, or a negative error code if the input is invalid.
 
-positional arguments:
-  dimacs            Path to a DIMACS CNF formula
-  drup              Path to a DRUP/DRAT proof
+positional arguments:
+  dimacs            Path to a DIMACS CNF formula
+  drup              Path to a DRUP/DRAT proof
 
-optional arguments:
-  -h, --help        show this help message and exit
-  -d, --derivation  Check each step, ignore absence of empty clause
-  -v, --verbose     Print detailed information about failed checks
+optional arguments:
+  -h, --help        show this help message and exit
+  -d, --derivation  Check each step, ignore absence of empty clause
+  -v, --verbose     Print detailed information about failed checks
 
-For more information visit https://github.com/cmu-transparency/verified_rup
+For more information visit https://github.com/cmu-transparency/verified_rup

    As a Python module

    -

    See the documentation for details of the API. -The primary function is drup.check_proof, or alternatively, drup.check_derivation to check each step of the proof, ignoring the absence of an empty clause).

    +

    See the documentation for details of the API. +The primary function is drup.check_proof, or alternatively, drup.check_derivation to check each step of the proof, ignoring the absence of an empty clause). There are corresponding convenience functions check_proof_from_strings and check_proof_from_files, similarly for check_derivation.

    + +

    The following example uses CNFgen to generate a PHP instance, +and PySAT to solve it and generate a DRUP proof. +To illustrate the verbose output given for failed checks, only the first ten clauses of the proof are checked against the proof.

    -
    def check_proof(formula : Cnf, proof : Proof, verbose : bool = False) -> CheckerResult:
-  """Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables
-  of clauses, where each clause is an iterable of signed Python ints.
-
-  Args:
-    formula (Cnf): Cnf as an iterable of clauses.
-    proof (Proof): Iterable of RUP or RAT clauses.
-    verbose (bool, optional): Return detailed information
-      if the check fails. Defaults to False.
-
-  Returns:
-    CheckerResult: CheckerResult struct representing the result of the check.
-
-  Raises:
-    ValueError: If the formula or proof cannot be formatted.
-  """
+
    import drup
+import cnfgen
+from pysat.formula import CNF
+from pysat.solvers import Solver
+
+dimacs = cnfgen.BinaryPigeonholePrinciple(4, 3).dimacs()
+cnf = CNF(from_string=dimacs).clauses
+g4 = Solver(name='g4', with_proof=True, bootstrap_with=cnf)
+g4.solve()
+proof = [[int(l) for l in c.split(' ')[:-1]] for c in g4.get_proof()]
+
+drup.check_proof(cnf[:10], proof, verbose=True)
    -

    This takes a CNF and Proof as an iterable of iterables of signed integers, and returns a CheckerResult.

    +

    This gives a CheckerResult object with the following information:

    -
    class CheckerResult:
-
-  '''
-  Result of a proof check.
-
-  Attributes:
-
-    outcome (`Outcome`): The outcome of the check. If the check
-      succeeded, this will be Outcome.VALID. If the check failed,
-      this will be Outcome.INVALID.
-
-    steps (`Optional[Cnf]`): Completed proof steps prior to an invalid step, 
-      if the proof was invalid.
-
-    rup_info (`Optional[RupInfo]`): Information on a failed RUP check,
-      if the proof was invalid.
-
-    rat_info (`Optional[RatInfo]`): Information on a failed RAT check,
-      if the proof was invalid. The RAT clause in this object will
-      be the same as the RUP clause in `rup_info`.
-  '''
+
    CheckerResult(
+    Outcome.INVALID, 
+    [], 
+    RupInfo([4, 6, 7, 8], [-4, -6, -7, -8, 3, 5]), 
+    RatInfo(
+        [4, 6, 7, 8], 
+        [-4, -3], 
+        RupInfo([6, 7, 8, -3], [-6, -7, -8, 5, 3, -4])
+    )
+)
    -

    There are corresponding convenience functions check_proof_from_strings and check_proof_from_files, similarly for check_derivation.

    +

    The RupInfo component relates that RUP verification failed on the first clause of the proof, 4 6 7 8 0, after propagating the literals -4, -6, -7, -8, 3, 5, and failing to find more opposites to propagate. +Likewise, the RatInfo component relates that RAT verification on this clause failed when checking the pivot on clause -4 -3 0. +The resolvent of these clauses, 6 7 8 -3 0, failed RUP verification after propagating -6 -7 -8 5 3 -4.

    Performance

    @@ -323,6 +310,91 @@

    References

    [1] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill. Learning a SAT Solver from Single-Bit Supervision. International Conference on Learning Representations (ICLR), 2019.

    +

    Verification

    + +

    The verification can be examined by running src/librupchecker/rup_pure.mlw in Why3, or by checking the Why3 session in src/librupchecker/rup_pure/why3session.xml. +The proof was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8. +Verification has not been attempted with earlier versions of Why3 or the provers.

    + +

    The primary contract on the proof checker is as follows:

    + +
    +
    requires { no_redundant_clauses cnf /\ no_trivial_clauses cnf }
+requires { no_redundant_clauses pf /\ no_trivial_clauses pf }
+ensures { match result with
+            | Valid -> valid_proof cnf pf
+            | _ -> proof_failure orig result
+            end }
+
    +
    + +

    The bindings used by this library take care of removing redundant and trivial clauses. +The valid_proof predicate is a straightforward translation of DRAT certification requirements. +A proof_failure result provides additional assurances about the verbose output of the checker.

    + +
    +
    predicate proof_failure (cnf : cnf) (result : result) =
+    match result with
+    | Valid -> false
+    | InvalidEmpty steps rup_info -> rup_failure (steps ++ cnf) rup_info
+    | InvalidStep steps rup_info rat_info -> 
+        rup_failure (steps ++ cnf) rup_info /\ rat_failure (steps ++ cnf) rat_info
+    end
+
    +
    + +

    An InvalidEmpty result indicates all of the listed steps are valid, but the empty clause was not derived, as witnessed by the provided rup_info. +This is only returned when all of the steps in the proof are valid except an empty clause at the end. +The rup_info component ensures that the empty clause is not RUP, and that the unit chain used to conclude this is exhaustive.

    + +
    +
    predicate rup_failure (cnf : cnf) (info : rup_info) =
+    not (rup cnf info.rup_clause) /\
+    match info.rup_clause with
+    | Nil -> 
+        let cnf' = bcp cnf info.chain in
+        is_unit_chain cnf info.chain /\ 
+        forall chain' . is_unit_chain cnf' chain' -> 
+                        forall c . mem c (bcp cnf' chain') <-> mem c cnf'
+    | Cons _ _ -> 
+        let cnf' = bcp (cnf ++ (negate_clause info.rup_clause)) info.chain in
+        is_unit_chain (cnf ++ (negate_clause info.rup_clause)) info.chain /\ 
+        forall chain' . is_unit_chain cnf' chain' -> 
+                        forall c . mem c (bcp cnf' chain') <-> mem c cnf'
+    end
+
    +
    + +

    An InvalidStep result indicates that the steps are valid up to some non-empty step. +The next step in the certificate following steps is invalid, as witnessed by the provided rup_info and rat_info. +In addition to the assurances on rup_info described above, rat_info provides that the identified pivot clause is not RUP.

    + +
    +
    predicate rat_failure (cnf : cnf) (info : rat_info) =
+    not (rat cnf info.rat_clause) /\
+    match info.rat_clause with
+    | Nil -> false
+    | Cons l _ ->
+        mem info.pivot_clause (pivot_clauses cnf l) /\
+        info.pivot_info.rup_clause = resolve info.rat_clause info.pivot_clause l /\
+        rup_failure cnf info.pivot_info
+    end
+
    +
    + +

    The derivation checker provides a similar contract, but rather than ensuring valid_proof on success, it provides valid_derivation.

    + +
    +
    predicate valid_derivation (cnf : cnf) (pf : proof) =
+    match pf with
+    | Nil -> true
+    | Cons c cs -> (rup cnf c \/ rat cnf c) /\ valid_derivation (Cons c cnf) cs
+    end
+
    +
    + +

    This is the same condition as valid_proof, but in the Nil case, the checker does not require that the empty clause is not RUP.

    +

    Acknowledgements

    Many thanks to Frank Pfenning, Joseph Reeves, and Marijn Huele for the ongoing insightful discussions that led to this project.

    @@ -606,7 +678,7 @@
    Inherited Members
    29class RupInfo:
 30
-31  '''
+31  '''
 32  Information on a failed RUP check.
 33
 34  **Attributes**:
@@ -672,7 +744,7 @@ 
    Inherited Members
    
     
             
    50class RatInfo:
 51
-52  '''
+52  '''
 53  Information on a failed RAT check.
 54
 55  **Attributes**:
@@ -738,7 +810,7 @@ 
    Inherited Members
    
     
             
     71class CheckerResult:
  72
- 73  '''
+ 73  '''
  74  Result of a proof check.
  75
  76  **Attributes**:
@@ -832,7 +904,7 @@ 
    Inherited Members
    
     
    
     
             
    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
+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:**
@@ -885,7 +957,7 @@ 
    Inherited Members
    
     
    
     
             
    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.
+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.
@@ -939,7 +1011,7 @@ 
    Inherited Members
    
     
    
     
             
    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.
+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
@@ -1001,7 +1073,7 @@ 
    Inherited Members
    
     
    
     
             
    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
+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:**
@@ -1060,7 +1132,7 @@ 
    Inherited Members
    
     
    
     
             
    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.
+462  """Check a sequence of RUP and RAT clauses against a CNF.
 463
 464  **Args:**
 465    
@@ -1126,7 +1198,7 @@ 
    Inherited Members
    
     
    
     
             
    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.
+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
diff --git a/docs/search.js b/docs/search.js
index 8fc7939..f15f85d 100644
--- a/docs/search.js
+++ b/docs/search.js
@@ -1,6 +1,6 @@
 window.pdocSearch = (function(){
 /** elasticlunr - http://weixsong.github.io * Copyright (C) 2017 Oliver Nightingale * Copyright (C) 2017 Wei Song * MIT Licensed */!function(){function e(e){if(null===e||"object"!=typeof e)return e;var t=e.constructor();for(var n in e)e.hasOwnProperty(n)&&(t[n]=e[n]);return t}var t=function(e){var n=new t.Index;return n.pipeline.add(t.trimmer,t.stopWordFilter,t.stemmer),e&&e.call(n,n),n};t.version="0.9.5",lunr=t,t.utils={},t.utils.warn=function(e){return function(t){e.console&&console.warn&&console.warn(t)}}(this),t.utils.toString=function(e){return void 0===e||null===e?"":e.toString()},t.EventEmitter=function(){this.events={}},t.EventEmitter.prototype.addListener=function(){var e=Array.prototype.slice.call(arguments),t=e.pop(),n=e;if("function"!=typeof t)throw new TypeError("last argument must be a function");n.forEach(function(e){this.hasHandler(e)||(this.events[e]=[]),this.events[e].push(t)},this)},t.EventEmitter.prototype.removeListener=function(e,t){if(this.hasHandler(e)){var n=this.events[e].indexOf(t);-1!==n&&(this.events[e].splice(n,1),0==this.events[e].length&&delete this.events[e])}},t.EventEmitter.prototype.emit=function(e){if(this.hasHandler(e)){var t=Array.prototype.slice.call(arguments,1);this.events[e].forEach(function(e){e.apply(void 0,t)},this)}},t.EventEmitter.prototype.hasHandler=function(e){return e in this.events},t.tokenizer=function(e){if(!arguments.length||null===e||void 0===e)return[];if(Array.isArray(e)){var n=e.filter(function(e){return null===e||void 0===e?!1:!0});n=n.map(function(e){return t.utils.toString(e).toLowerCase()});var i=[];return n.forEach(function(e){var n=e.split(t.tokenizer.seperator);i=i.concat(n)},this),i}return e.toString().trim().toLowerCase().split(t.tokenizer.seperator)},t.tokenizer.defaultSeperator=/[\s\-]+/,t.tokenizer.seperator=t.tokenizer.defaultSeperator,t.tokenizer.setSeperator=function(e){null!==e&&void 0!==e&&"object"==typeof e&&(t.tokenizer.seperator=e)},t.tokenizer.resetSeperator=function(){t.tokenizer.seperator=t.tokenizer.defaultSeperator},t.tokenizer.getSeperator=function(){return t.tokenizer.seperator},t.Pipeline=function(){this._queue=[]},t.Pipeline.registeredFunctions={},t.Pipeline.registerFunction=function(e,n){n in t.Pipeline.registeredFunctions&&t.utils.warn("Overwriting existing registered function: "+n),e.label=n,t.Pipeline.registeredFunctions[n]=e},t.Pipeline.getRegisteredFunction=function(e){return e in t.Pipeline.registeredFunctions!=!0?null:t.Pipeline.registeredFunctions[e]},t.Pipeline.warnIfFunctionNotRegistered=function(e){var n=e.label&&e.label in this.registeredFunctions;n||t.utils.warn("Function is not registered with pipeline. This may cause problems when serialising the index.\n",e)},t.Pipeline.load=function(e){var n=new t.Pipeline;return e.forEach(function(e){var i=t.Pipeline.getRegisteredFunction(e);if(!i)throw new Error("Cannot load un-registered function: "+e);n.add(i)}),n},t.Pipeline.prototype.add=function(){var e=Array.prototype.slice.call(arguments);e.forEach(function(e){t.Pipeline.warnIfFunctionNotRegistered(e),this._queue.push(e)},this)},t.Pipeline.prototype.after=function(e,n){t.Pipeline.warnIfFunctionNotRegistered(n);var i=this._queue.indexOf(e);if(-1===i)throw new Error("Cannot find existingFn");this._queue.splice(i+1,0,n)},t.Pipeline.prototype.before=function(e,n){t.Pipeline.warnIfFunctionNotRegistered(n);var i=this._queue.indexOf(e);if(-1===i)throw new Error("Cannot find existingFn");this._queue.splice(i,0,n)},t.Pipeline.prototype.remove=function(e){var t=this._queue.indexOf(e);-1!==t&&this._queue.splice(t,1)},t.Pipeline.prototype.run=function(e){for(var t=[],n=e.length,i=this._queue.length,o=0;n>o;o++){for(var r=e[o],s=0;i>s&&(r=this._queue[s](r,o,e),void 0!==r&&null!==r);s++);void 0!==r&&null!==r&&t.push(r)}return t},t.Pipeline.prototype.reset=function(){this._queue=[]},t.Pipeline.prototype.get=function(){return this._queue},t.Pipeline.prototype.toJSON=function(){return this._queue.map(function(e){return t.Pipeline.warnIfFunctionNotRegistered(e),e.label})},t.Index=function(){this._fields=[],this._ref="id",this.pipeline=new t.Pipeline,this.documentStore=new t.DocumentStore,this.index={},this.eventEmitter=new t.EventEmitter,this._idfCache={},this.on("add","remove","update",function(){this._idfCache={}}.bind(this))},t.Index.prototype.on=function(){var e=Array.prototype.slice.call(arguments);return this.eventEmitter.addListener.apply(this.eventEmitter,e)},t.Index.prototype.off=function(e,t){return this.eventEmitter.removeListener(e,t)},t.Index.load=function(e){e.version!==t.version&&t.utils.warn("version mismatch: current "+t.version+" importing "+e.version);var n=new this;n._fields=e.fields,n._ref=e.ref,n.documentStore=t.DocumentStore.load(e.documentStore),n.pipeline=t.Pipeline.load(e.pipeline),n.index={};for(var i in e.index)n.index[i]=t.InvertedIndex.load(e.index[i]);return n},t.Index.prototype.addField=function(e){return this._fields.push(e),this.index[e]=new t.InvertedIndex,this},t.Index.prototype.setRef=function(e){return this._ref=e,this},t.Index.prototype.saveDocument=function(e){return this.documentStore=new t.DocumentStore(e),this},t.Index.prototype.addDoc=function(e,n){if(e){var n=void 0===n?!0:n,i=e[this._ref];this.documentStore.addDoc(i,e),this._fields.forEach(function(n){var o=this.pipeline.run(t.tokenizer(e[n]));this.documentStore.addFieldLength(i,n,o.length);var r={};o.forEach(function(e){e in r?r[e]+=1:r[e]=1},this);for(var s in r){var u=r[s];u=Math.sqrt(u),this.index[n].addToken(s,{ref:i,tf:u})}},this),n&&this.eventEmitter.emit("add",e,this)}},t.Index.prototype.removeDocByRef=function(e){if(e&&this.documentStore.isDocStored()!==!1&&this.documentStore.hasDoc(e)){var t=this.documentStore.getDoc(e);this.removeDoc(t,!1)}},t.Index.prototype.removeDoc=function(e,n){if(e){var n=void 0===n?!0:n,i=e[this._ref];this.documentStore.hasDoc(i)&&(this.documentStore.removeDoc(i),this._fields.forEach(function(n){var o=this.pipeline.run(t.tokenizer(e[n]));o.forEach(function(e){this.index[n].removeToken(e,i)},this)},this),n&&this.eventEmitter.emit("remove",e,this))}},t.Index.prototype.updateDoc=function(e,t){var t=void 0===t?!0:t;this.removeDocByRef(e[this._ref],!1),this.addDoc(e,!1),t&&this.eventEmitter.emit("update",e,this)},t.Index.prototype.idf=function(e,t){var n="@"+t+"/"+e;if(Object.prototype.hasOwnProperty.call(this._idfCache,n))return this._idfCache[n];var i=this.index[t].getDocFreq(e),o=1+Math.log(this.documentStore.length/(i+1));return this._idfCache[n]=o,o},t.Index.prototype.getFields=function(){return this._fields.slice()},t.Index.prototype.search=function(e,n){if(!e)return[];e="string"==typeof e?{any:e}:JSON.parse(JSON.stringify(e));var i=null;null!=n&&(i=JSON.stringify(n));for(var o=new t.Configuration(i,this.getFields()).get(),r={},s=Object.keys(e),u=0;u0&&t.push(e);for(var i in n)"docs"!==i&&"df"!==i&&this.expandToken(e+i,t,n[i]);return t},t.InvertedIndex.prototype.toJSON=function(){return{root:this.root}},t.Configuration=function(e,n){var e=e||"";if(void 0==n||null==n)throw new Error("fields should not be null");this.config={};var i;try{i=JSON.parse(e),this.buildUserConfig(i,n)}catch(o){t.utils.warn("user configuration parse failed, will use default configuration"),this.buildDefaultConfig(n)}},t.Configuration.prototype.buildDefaultConfig=function(e){this.reset(),e.forEach(function(e){this.config[e]={boost:1,bool:"OR",expand:!1}},this)},t.Configuration.prototype.buildUserConfig=function(e,n){var i="OR",o=!1;if(this.reset(),"bool"in e&&(i=e.bool||i),"expand"in e&&(o=e.expand||o),"fields"in e)for(var r in e.fields)if(n.indexOf(r)>-1){var s=e.fields[r],u=o;void 0!=s.expand&&(u=s.expand),this.config[r]={boost:s.boost||0===s.boost?s.boost:1,bool:s.bool||i,expand:u}}else t.utils.warn("field name in user configuration not found in index instance fields");else this.addAllFields2UserConfig(i,o,n)},t.Configuration.prototype.addAllFields2UserConfig=function(e,t,n){n.forEach(function(n){this.config[n]={boost:1,bool:e,expand:t}},this)},t.Configuration.prototype.get=function(){return this.config},t.Configuration.prototype.reset=function(){this.config={}},lunr.SortedSet=function(){this.length=0,this.elements=[]},lunr.SortedSet.load=function(e){var t=new this;return t.elements=e,t.length=e.length,t},lunr.SortedSet.prototype.add=function(){var e,t;for(e=0;e1;){if(r===e)return o;e>r&&(t=o),r>e&&(n=o),i=n-t,o=t+Math.floor(i/2),r=this.elements[o]}return r===e?o:-1},lunr.SortedSet.prototype.locationFor=function(e){for(var t=0,n=this.elements.length,i=n-t,o=t+Math.floor(i/2),r=this.elements[o];i>1;)e>r&&(t=o),r>e&&(n=o),i=n-t,o=t+Math.floor(i/2),r=this.elements[o];return r>e?o:e>r?o+1:void 0},lunr.SortedSet.prototype.intersect=function(e){for(var t=new lunr.SortedSet,n=0,i=0,o=this.length,r=e.length,s=this.elements,u=e.elements;;){if(n>o-1||i>r-1)break;s[n]!==u[i]?s[n]u[i]&&i++:(t.add(s[n]),n++,i++)}return t},lunr.SortedSet.prototype.clone=function(){var e=new lunr.SortedSet;return e.elements=this.toArray(),e.length=e.elements.length,e},lunr.SortedSet.prototype.union=function(e){var t,n,i;this.length>=e.length?(t=this,n=e):(t=e,n=this),i=t.clone();for(var o=0,r=n.toArray();oA Verified DRUP Proof Checker\n\n
    As the title suggests, a verified implementation of a checker for propositional unsatisfiability proofs in the  DRUP format that is produced by many solvers.\nThe core of the checker is written in Why3, which is extracted to OCaml, compiled natively, and exported as a C library with Python bindings.
    \n\n
      \n
    • The checker also supports RAT clauses, so DRAT proofs are accepted.
      • \n
    • The current implementation is not optimized, and will be considerably slower than DRAT-trim on large proofs (see performance below).
      • \n
    • Accordingly, the frontend does not accept proofs in binary format.
      • \n
    \n\n
    The verification can be checked by running src/librupchecker/rup_pure.mlw in Why3. \nMost of the verification conditions complete with the Auto level 0 tactic, and the rest either with a few levels of splitting followed by Auto 0 or Auto 1, or simply with Auto 2.\nIt was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8.\nVerification has not been attempted with earlier versions of Why3 or the provers.
    \n\n
    Installation
    \n\n
    If you use a recent Linux distribution on x86_64, you should be able to install the compiled wheel from PyPI:
    \n\n
    \n
    $ pip install drup\n
    \n
    \n\n
    Otherwise, you need to have OCaml (>= 4.12), Ctypes (>=0.20), Why3 (>= 1.5.1), and Dune (>=2.9.3) installed.\nThe most straightforward way to install these is to use opam, which is available in most package systems, and then install Why3 and Dune (a sufficiently recent version of OCaml should already be installed with Opam): 
    \n\n
    \n
    $ opam install why3 dune\n
    \n
    \n\n
    If you do not intend to check the verification of the library or develop it further, then you do not need to install Why3's IDE or any of the solvers that it supports.
    \n\n
    Once OCaml and Why3 are installed, make sure that Python build is installed:
    \n\n
    \n
    $ pip install build\n
    \n
    \n\n
    Then, clone this repository, build, and install the package:
    \n\n
    \n
    $ git clone https://github.com/cmu-transparency/verified_rup.git\n$ cd verified_rup\n$ python -m build\n$ pip install dist/*.whl\n
    \n
    \n\n
    Usage
    \n\n
    Command line interface
    \n\n
    The package provides a command line interface for checking proofs stored in files:
    \n\n
    \n
    $ drup --help\nusage: drup [-h] [-d] [-v] dimacs drup\n\nChecks DRUP & DRAT proofs against DIMACS source. Returns 0 if the proof is valid, -1 if not, or a negative error code if the input is invalid.\n\npositional arguments:\n  dimacs            Path to a DIMACS CNF formula\n  drup              Path to a DRUP/DRAT proof\n\noptional arguments:\n  -h, --help        show this help message and exit\n  -d, --derivation  Check each step, ignore absence of empty clause\n  -v, --verbose     Print detailed information about failed checks\n\nFor more information visit https://github.com/cmu-transparency/verified_rup\n
    \n
    \n\n
    As a Python module
    \n\n
    See the documentation for details of the API.\nThe primary function is drup.check_proof, or alternatively, drup.check_derivation to check each step of the proof, ignoring the absence of an empty clause).
    \n\n
    \n
    def check_proof(formula : Cnf, proof : Proof, verbose : bool = False) -> CheckerResult:\n  """Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables\n  of clauses, where each clause is an iterable of signed Python ints.\n\n  Args:\n    formula (Cnf): Cnf as an iterable of clauses.\n    proof (Proof): Iterable of RUP or RAT clauses.\n    verbose (bool, optional): Return detailed information\n      if the check fails. Defaults to False.\n\n  Returns:\n    CheckerResult: CheckerResult struct representing the result of the check.\n\n  Raises:\n    ValueError: If the formula or proof cannot be formatted.\n  """\n
    \n
    \n\n
    This takes a CNF and Proof as an iterable of iterables of signed integers, and returns a CheckerResult.
    \n\n
    \n
    class CheckerResult:\n\n  '''\n  Result of a proof check.\n\n  Attributes:\n\n    outcome (`Outcome`): The outcome of the check. If the check\n      succeeded, this will be Outcome.VALID. If the check failed,\n      this will be Outcome.INVALID.\n\n    steps (`Optional[Cnf]`): Completed proof steps prior to an invalid step, \n      if the proof was invalid.\n\n    rup_info (`Optional[RupInfo]`): Information on a failed RUP check,\n      if the proof was invalid.\n\n    rat_info (`Optional[RatInfo]`): Information on a failed RAT check,\n      if the proof was invalid. The RAT clause in this object will\n      be the same as the RUP clause in `rup_info`.\n  '''\n
    \n
    \n\n
    There are corresponding convenience functions check_proof_from_strings and check_proof_from_files, similarly for check_derivation.
    \n\n
    Performance
    \n\n
    At present, the implementation of RUP checking is not optimized, and drop lines are ignored.\nUnit propagation does not take advantage of watched literals, and does not use mutable data structures.\nNonetheless, the performance compares well to that of DRAT-trim on small proofs (<200 variables, a few hundred clauses).
    \n\n
    We measure this on random unsatisfiable instances generated by the procedure described in [1].\nTo evaluate the performance of DRAT-trim without the overhead of creating and tearing down a new process for each instance, we compiled it into a library with the same check_from_strings interface as the C library, and called it using ctypes.\nIn the table below, each configuration is run on 10,000 instances, with proofs generated by Glucose 4.
    \n\n\n\n\n  \n  \n  \n  \n  \n\n\n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n
    # vars# clauses (avg)pf len (avg)drup (sec, avg)drat-trim (sec, avg)
    25147.77.30.0010.085
    50280.514.20.0060.179
    75413.526.30.0220.217
    100548.240.60.0680.172
    150811.8102.70.4070.326
    2001079.5227.91.9160.292
    \n\n
    References
    \n\n
    [1] Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, David L. Dill. Learning a SAT Solver from Single-Bit Supervision. International Conference on Learning Representations (ICLR), 2019.
    \n\n
    Acknowledgements
    \n\n
    Many thanks to Frank Pfenning, Joseph Reeves, and Marijn Huele for the ongoing insightful discussions that led to this project.
    \n"}, {"fullname": "drup.Lit", "modulename": "drup", "qualname": "Lit", "kind": "variable", "doc": "
    A signed integer representing a literal.
    \n", "default_value": "<class 'int'>"}, {"fullname": "drup.Clause", "modulename": "drup", "qualname": "Clause", "kind": "variable", "doc": "
    A sequence of literals.
    \n", "default_value": "typing.Iterable[int]"}, {"fullname": "drup.Chain", "modulename": "drup", "qualname": "Chain", "kind": "variable", "doc": "
    A sequence of clauses.
    \n", "default_value": "typing.Iterable[int]"}, {"fullname": "drup.Cnf", "modulename": "drup", "qualname": "Cnf", "kind": "variable", "doc": "
    A sequence of literals.
    \n", "default_value": "typing.Iterable[typing.Iterable[int]]"}, {"fullname": "drup.Proof", "modulename": "drup", "qualname": "Proof", "kind": "variable", "doc": "
    A sequence of clauses.
    \n", "default_value": "typing.Iterable[typing.Iterable[int]]"}, {"fullname": "drup.Outcome", "modulename": "drup", "qualname": "Outcome", "kind": "class", "doc": "
    An enumeration.
    \n", "bases": "enum.Enum"}, {"fullname": "drup.Outcome.VALID", "modulename": "drup", "qualname": "Outcome.VALID", "kind": "variable", "doc": "
    \n", "default_value": "<Outcome.VALID: 1>"}, {"fullname": "drup.Outcome.INVALID", "modulename": "drup", "qualname": "Outcome.INVALID", "kind": "variable", "doc": "
    \n", "default_value": "<Outcome.INVALID: 2>"}, {"fullname": "drup.RupInfo", "modulename": "drup", "qualname": "RupInfo", "kind": "class", "doc": "
    Information on a failed RUP check.
    \n\n
    Attributes:
    \n\n
    clause (Clause): The clause that failed the RUP check.
    \n\n
    chain (Chain): A sequence of unit literals that failed to\n    derive an empty clause via propagation, with no further \n    opportunities to propagate.
    \n"}, {"fullname": "drup.RupInfo.__init__", "modulename": "drup", "qualname": "RupInfo.__init__", "kind": "function", "doc": "
    \n", "signature": "(clause: Iterable[int], chain: Iterable[int])"}, {"fullname": "drup.RatInfo", "modulename": "drup", "qualname": "RatInfo", "kind": "class", "doc": "
    Information on a failed RAT check.
    \n\n
    Attributes:\n  clause (Clause): The clause that failed the RAT check.
    \n\n
    pivot_clause (Clause): A pivot clause that failed a RUP check.
    \n\n
    rup_info (RupInfo): Information on the failed RUP check.
    \n"}, {"fullname": "drup.RatInfo.__init__", "modulename": "drup", "qualname": "RatInfo.__init__", "kind": "function", "doc": "
    \n", "signature": "(\tclause: Iterable[int],\tpivot_clause: Iterable[int],\trup_info: drup.wrappers.RupInfo)"}, {"fullname": "drup.CheckerResult", "modulename": "drup", "qualname": "CheckerResult", "kind": "class", "doc": "
    Result of a proof check.
    \n\n
    Attributes:
    \n\n
    outcome (Outcome): The outcome of the check. If the check\n    succeeded, this will be Outcome.VALID. If the check failed,\n    this will be Outcome.INVALID.
    \n\n
    steps (Optional[Cnf]): Completed proof steps prior to an invalid step, \n    if the proof was invalid.
    \n\n
    rup_info (Optional[RupInfo]): Information on a failed RUP check,\n    if the proof was invalid.
    \n\n
    rat_info (Optional[RatInfo]): Information on a failed RAT check,\n    if the proof was invalid. The RAT clause in this object will\n    be the same as the RUP clause in rup_info.
    \n"}, {"fullname": "drup.CheckerResult.__init__", "modulename": "drup", "qualname": "CheckerResult.__init__", "kind": "function", "doc": "
    \n", "signature": "(\toutcome: drup.wrappers.Outcome,\tsteps: Optional[Iterable[Iterable[int]]],\trup_info: Optional[drup.wrappers.RupInfo],\trat_info: Optional[drup.wrappers.RatInfo])"}, {"fullname": "drup.check_proof", "modulename": "drup", "qualname": "check_proof", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables\nof clauses, where each clause is an iterable of signed Python ints.
    \n\n
    Args:\n  formula (Cnf): Cnf as an iterable of clauses.
    \n\n
    proof (Proof): Iterable of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be formatted.
    \n", "signature": "(\tformula: Iterable[Iterable[int]],\tproof: Iterable[Iterable[int]],\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_proof_from_files", "modulename": "drup", "qualname": "check_proof_from_files", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula_file (str): Path to a file containing a CNF in DIMACS format.\n  proof_file (str): Path to a file containing a sequence of RUP or RAT clauses.\n  verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.\n  FileNotFoundError: If the formula or proof file cannot be found.
    \n", "signature": "(\tformula_file: str,\tproof_file: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_proof_from_strings", "modulename": "drup", "qualname": "check_proof_from_strings", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula (str): Cnf as a string in DIMACS format. The header\n    is ignored if present.\n  proof (str): Sequence of RUP or RAT clauses format.\n  verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.
    \n", "signature": "(\tformula: str,\tproof: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation", "modulename": "drup", "qualname": "check_derivation", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables\nof clauses, where each clause is an iterable of signed Python ints.
    \n\n
    Args:\n  formula (Cnf): Cnf as an iterable of clauses.
    \n\n
    derivation (Proof): Iterable of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or derivation cannot be formatted.
    \n", "signature": "(\tformula: Iterable[Iterable[int]],\tderivation: Iterable[Iterable[int]],\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation_from_files", "modulename": "drup", "qualname": "check_derivation_from_files", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:
    \n\n
    formula_file (str): Path to a file containing a CNF in DIMACS format.
    \n\n
    derivation_file (str): Path to a file containing a sequence of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.\n  FileNotFoundError: If the formula or proof file cannot be found.
    \n", "signature": "(\tformula_file: str,\tderivation_file: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation_from_strings", "modulename": "drup", "qualname": "check_derivation_from_strings", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula (str): Cnf as a string in DIMACS format. The header\n    is ignored if present.
    \n\n
    proof (str): Sequence of RUP or RAT clauses format.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.
    \n", "signature": "(\tformula: str,\tderivation: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}];
+    /** pdoc search index */const docs = [{"fullname": "drup", "modulename": "drup", "kind": "module", "doc": "
    A Verified DRUP Proof Checker
    \n\n
    As the title suggests, a verified implementation of a checker for propositional unsatisfiability proofs in the  DRUP format that is produced by many solvers.\nThe core of the checker is written in Why3, which is extracted to OCaml, compiled natively, and exported as a C library with Python bindings.
    \n\n
      \n
    • The checker also supports RAT clauses, so DRAT proofs are accepted.
      • \n
    • The current implementation is not optimized, and will be considerably slower than DRAT-trim on large proofs (see performance below).
      • \n
    • Accordingly, the frontend does not accept proofs in binary format.
      • \n
    \n\n
    Installation
    \n\n
    If you use a recent Linux distribution on x86_64, you should be able to install the compiled wheel from PyPI:
    \n\n
    \n
    $ pip install drup\n
    \n
    \n\n
    Otherwise, you need to have OCaml (>= 4.12), Ctypes (>=0.20), Why3 (>= 1.5.1), and Dune (>=2.9.3) installed.\nThe most straightforward way to install these is to use opam, which is available in most package systems, and then install Why3 and Dune (a sufficiently recent version of OCaml should already be installed with Opam): 
    \n\n
    \n
    $ opam install why3 dune\n
    \n
    \n\n
    If you do not intend to check the verification of the library or develop it further, then you do not need to install Why3's IDE or any of the solvers that it supports.
    \n\n
    Once OCaml and Why3 are installed, make sure that Python build is installed:
    \n\n
    \n
    $ pip install build\n
    \n
    \n\n
    Then, clone this repository, build, and install the package:
    \n\n
    \n
    $ git clone https://github.com/cmu-transparency/verified_rup.git\n$ cd verified_rup\n$ python -m build\n$ pip install dist/*.whl\n
    \n
    \n\n
    Usage
    \n\n
    Command line interface
    \n\n
    The package provides a command line interface for checking proofs stored in files:
    \n\n
    \n
    $ drup --help\nusage: drup [-h] [-d] [-v] dimacs drup\n\nChecks DRUP & DRAT proofs against DIMACS source. Returns 0 if the proof is valid, -1 if not, or a negative error code if the input is invalid.\n\npositional arguments:\n  dimacs            Path to a DIMACS CNF formula\n  drup              Path to a DRUP/DRAT proof\n\noptional arguments:\n  -h, --help        show this help message and exit\n  -d, --derivation  Check each step, ignore absence of empty clause\n  -v, --verbose     Print detailed information about failed checks\n\nFor more information visit https://github.com/cmu-transparency/verified_rup\n
    \n
    \n\n
    As a Python module
    \n\n
    See the documentation for details of the API.\nThe primary function is drup.check_proof, or alternatively, drup.check_derivation to check each step of the proof, ignoring the absence of an empty clause). There are corresponding convenience functions check_proof_from_strings and check_proof_from_files, similarly for check_derivation.
    \n\n
    The following example uses CNFgen to generate a PHP instance,\nand PySAT to solve it and generate a DRUP proof.\nTo illustrate the verbose output given for failed checks, only the first ten clauses of the proof are checked against the proof.
    \n\n
    \n
    import drup\nimport cnfgen\nfrom pysat.formula import CNF\nfrom pysat.solvers import Solver\n\ndimacs = cnfgen.BinaryPigeonholePrinciple(4, 3).dimacs()\ncnf = CNF(from_string=dimacs).clauses\ng4 = Solver(name='g4', with_proof=True, bootstrap_with=cnf)\ng4.solve()\nproof = [[int(l) for l in c.split(' ')[:-1]] for c in g4.get_proof()]\n\ndrup.check_proof(cnf[:10], proof, verbose=True)\n
    \n
    \n\n
    This gives a CheckerResult object with the following information:
    \n\n
    \n
    CheckerResult(\n    Outcome.INVALID, \n    [], \n    RupInfo([4, 6, 7, 8], [-4, -6, -7, -8, 3, 5]), \n    RatInfo(\n        [4, 6, 7, 8], \n        [-4, -3], \n        RupInfo([6, 7, 8, -3], [-6, -7, -8, 5, 3, -4])\n    )\n)\n
    \n
    \n\n
    The RupInfo component relates that RUP verification failed on the first clause of the proof, 4 6 7 8 0, after propagating the literals -4, -6, -7, -8, 3, 5, and failing to find more opposites to propagate.\nLikewise, the RatInfo component relates that RAT verification on this clause failed when checking the pivot on clause -4 -3 0.\nThe resolvent of these clauses, 6 7 8 -3 0, failed RUP verification after propagating -6 -7 -8 5 3 -4.
    \n\n
    Performance
    \n\n
    At present, the implementation of RUP checking is not optimized, and drop lines are ignored.\nUnit propagation does not take advantage of watched literals, and does not use mutable data structures.\nNonetheless, the performance compares well to that of DRAT-trim on small proofs (<200 variables, a few hundred clauses).
    \n\n
    We measure this on random unsatisfiable instances generated by the procedure described in [1].\nTo evaluate the performance of DRAT-trim without the overhead of creating and tearing down a new process for each instance, we compiled it into a library with the same check_from_strings interface as the C library, and called it using ctypes.\nIn the table below, each configuration is run on 10,000 instances, with proofs generated by Glucose 4.
    \n\n\n\n\n  \n  \n  \n  \n  \n\n\n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n  \n  \n  \n  \n  \n\n\n
    # vars# clauses (avg)pf len (avg)drup (sec, avg)drat-trim (sec, avg)
    25147.77.30.0010.085
    50280.514.20.0060.179
    75413.526.30.0220.217
    100548.240.60.0680.172
    150811.8102.70.4070.326
    2001079.5227.91.9160.292
    \n\n
    References
    \n\n
    [1] Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, David L. Dill. Learning a SAT Solver from Single-Bit Supervision. International Conference on Learning Representations (ICLR), 2019.
    \n\n
    Verification
    \n\n
    The verification can be examined by running src/librupchecker/rup_pure.mlw in Why3, or by checking the Why3 session in src/librupchecker/rup_pure/why3session.xml. \nThe proof was developed using Why3 1.5.1, Alt-Ergo 2.4.0, Z3 4.8.6, and CVC4 1.8.\nVerification has not been attempted with earlier versions of Why3 or the provers.
    \n\n
    The primary contract on the proof checker is as follows:
    \n\n
    \n
    requires { no_redundant_clauses cnf /\\ no_trivial_clauses cnf }\nrequires { no_redundant_clauses pf /\\ no_trivial_clauses pf }\nensures { match result with\n            | Valid -> valid_proof cnf pf\n            | _ -> proof_failure orig result\n            end }\n
    \n
    \n\n
    The bindings used by this library take care of removing redundant and trivial clauses.\nThe valid_proof predicate is a straightforward translation of DRAT certification requirements.\nA proof_failure result provides additional assurances about the verbose output of the checker.
    \n\n
    \n
    predicate proof_failure (cnf : cnf) (result : result) =\n    match result with\n    | Valid -> false\n    | InvalidEmpty steps rup_info -> rup_failure (steps ++ cnf) rup_info\n    | InvalidStep steps rup_info rat_info -> \n        rup_failure (steps ++ cnf) rup_info /\\ rat_failure (steps ++ cnf) rat_info\n    end\n
    \n
    \n\n
    An InvalidEmpty result indicates all of the listed steps are valid, but the empty clause was not derived, as witnessed by the provided rup_info.\nThis is only returned when all of the steps in the proof are valid except an empty clause at the end.\nThe rup_info component ensures that the empty clause is not RUP, and that the unit chain used to conclude this is exhaustive.
    \n\n
    \n
    predicate rup_failure (cnf : cnf) (info : rup_info) =\n    not (rup cnf info.rup_clause) /\\\n    match info.rup_clause with\n    | Nil -> \n        let cnf' = bcp cnf info.chain in\n        is_unit_chain cnf info.chain /\\ \n        forall chain' . is_unit_chain cnf' chain' -> \n                        forall c . mem c (bcp cnf' chain') <-> mem c cnf'\n    | Cons _ _ -> \n        let cnf' = bcp (cnf ++ (negate_clause info.rup_clause)) info.chain in\n        is_unit_chain (cnf ++ (negate_clause info.rup_clause)) info.chain /\\ \n        forall chain' . is_unit_chain cnf' chain' -> \n                        forall c . mem c (bcp cnf' chain') <-> mem c cnf'\n    end\n
    \n
    \n\n
    An InvalidStep result indicates that the steps are valid up to some non-empty step.\nThe next step in the certificate following steps is invalid, as witnessed by the provided rup_info and rat_info.\nIn addition to the assurances on rup_info described above, rat_info provides that the identified pivot clause is not RUP.
    \n\n
    \n
    predicate rat_failure (cnf : cnf) (info : rat_info) =\n    not (rat cnf info.rat_clause) /\\\n    match info.rat_clause with\n    | Nil -> false\n    | Cons l _ ->\n        mem info.pivot_clause (pivot_clauses cnf l) /\\\n        info.pivot_info.rup_clause = resolve info.rat_clause info.pivot_clause l /\\\n        rup_failure cnf info.pivot_info\n    end\n
    \n
    \n\n
    The derivation checker provides a similar contract, but rather than ensuring valid_proof on success, it provides valid_derivation.
    \n\n
    \n
    predicate valid_derivation (cnf : cnf) (pf : proof) =\n    match pf with\n    | Nil -> true\n    | Cons c cs -> (rup cnf c \\/ rat cnf c) /\\ valid_derivation (Cons c cnf) cs\n    end\n
    \n
    \n\n
    This is the same condition as valid_proof, but in the Nil case, the checker does not require that the empty clause is not RUP.
    \n\n
    Acknowledgements
    \n\n
    Many thanks to Frank Pfenning, Joseph Reeves, and Marijn Huele for the ongoing insightful discussions that led to this project.
    \n"}, {"fullname": "drup.Lit", "modulename": "drup", "qualname": "Lit", "kind": "variable", "doc": "
    A signed integer representing a literal.
    \n", "default_value": "<class 'int'>"}, {"fullname": "drup.Clause", "modulename": "drup", "qualname": "Clause", "kind": "variable", "doc": "
    A sequence of literals.
    \n", "default_value": "typing.Iterable[int]"}, {"fullname": "drup.Chain", "modulename": "drup", "qualname": "Chain", "kind": "variable", "doc": "
    A sequence of clauses.
    \n", "default_value": "typing.Iterable[int]"}, {"fullname": "drup.Cnf", "modulename": "drup", "qualname": "Cnf", "kind": "variable", "doc": "
    A sequence of literals.
    \n", "default_value": "typing.Iterable[typing.Iterable[int]]"}, {"fullname": "drup.Proof", "modulename": "drup", "qualname": "Proof", "kind": "variable", "doc": "
    A sequence of clauses.
    \n", "default_value": "typing.Iterable[typing.Iterable[int]]"}, {"fullname": "drup.Outcome", "modulename": "drup", "qualname": "Outcome", "kind": "class", "doc": "
    An enumeration.
    \n", "bases": "enum.Enum"}, {"fullname": "drup.Outcome.VALID", "modulename": "drup", "qualname": "Outcome.VALID", "kind": "variable", "doc": "
    \n", "default_value": "<Outcome.VALID: 1>"}, {"fullname": "drup.Outcome.INVALID", "modulename": "drup", "qualname": "Outcome.INVALID", "kind": "variable", "doc": "
    \n", "default_value": "<Outcome.INVALID: 2>"}, {"fullname": "drup.RupInfo", "modulename": "drup", "qualname": "RupInfo", "kind": "class", "doc": "
    Information on a failed RUP check.
    \n\n
    Attributes:
    \n\n
    clause (Clause): The clause that failed the RUP check.
    \n\n
    chain (Chain): A sequence of unit literals that failed to\n    derive an empty clause via propagation, with no further \n    opportunities to propagate.
    \n"}, {"fullname": "drup.RupInfo.__init__", "modulename": "drup", "qualname": "RupInfo.__init__", "kind": "function", "doc": "
    \n", "signature": "(clause: Iterable[int], chain: Iterable[int])"}, {"fullname": "drup.RatInfo", "modulename": "drup", "qualname": "RatInfo", "kind": "class", "doc": "
    Information on a failed RAT check.
    \n\n
    Attributes:\n  clause (Clause): The clause that failed the RAT check.
    \n\n
    pivot_clause (Clause): A pivot clause that failed a RUP check.
    \n\n
    rup_info (RupInfo): Information on the failed RUP check.
    \n"}, {"fullname": "drup.RatInfo.__init__", "modulename": "drup", "qualname": "RatInfo.__init__", "kind": "function", "doc": "
    \n", "signature": "(\tclause: Iterable[int],\tpivot_clause: Iterable[int],\trup_info: drup.wrappers.RupInfo)"}, {"fullname": "drup.CheckerResult", "modulename": "drup", "qualname": "CheckerResult", "kind": "class", "doc": "
    Result of a proof check.
    \n\n
    Attributes:
    \n\n
    outcome (Outcome): The outcome of the check. If the check\n    succeeded, this will be Outcome.VALID. If the check failed,\n    this will be Outcome.INVALID.
    \n\n
    steps (Optional[Cnf]): Completed proof steps prior to an invalid step, \n    if the proof was invalid.
    \n\n
    rup_info (Optional[RupInfo]): Information on a failed RUP check,\n    if the proof was invalid.
    \n\n
    rat_info (Optional[RatInfo]): Information on a failed RAT check,\n    if the proof was invalid. The RAT clause in this object will\n    be the same as the RUP clause in rup_info.
    \n"}, {"fullname": "drup.CheckerResult.__init__", "modulename": "drup", "qualname": "CheckerResult.__init__", "kind": "function", "doc": "
    \n", "signature": "(\toutcome: drup.wrappers.Outcome,\tsteps: Optional[Iterable[Iterable[int]]],\trup_info: Optional[drup.wrappers.RupInfo],\trat_info: Optional[drup.wrappers.RatInfo])"}, {"fullname": "drup.check_proof", "modulename": "drup", "qualname": "check_proof", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables\nof clauses, where each clause is an iterable of signed Python ints.
    \n\n
    Args:\n  formula (Cnf): Cnf as an iterable of clauses.
    \n\n
    proof (Proof): Iterable of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be formatted.
    \n", "signature": "(\tformula: Iterable[Iterable[int]],\tproof: Iterable[Iterable[int]],\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_proof_from_files", "modulename": "drup", "qualname": "check_proof_from_files", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula_file (str): Path to a file containing a CNF in DIMACS format.\n  proof_file (str): Path to a file containing a sequence of RUP or RAT clauses.\n  verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.\n  FileNotFoundError: If the formula or proof file cannot be found.
    \n", "signature": "(\tformula_file: str,\tproof_file: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_proof_from_strings", "modulename": "drup", "qualname": "check_proof_from_strings", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula (str): Cnf as a string in DIMACS format. The header\n    is ignored if present.\n  proof (str): Sequence of RUP or RAT clauses format.\n  verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.
    \n", "signature": "(\tformula: str,\tproof: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation", "modulename": "drup", "qualname": "check_derivation", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF. Inputs are Python iterables\nof clauses, where each clause is an iterable of signed Python ints.
    \n\n
    Args:\n  formula (Cnf): Cnf as an iterable of clauses.
    \n\n
    derivation (Proof): Iterable of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or derivation cannot be formatted.
    \n", "signature": "(\tformula: Iterable[Iterable[int]],\tderivation: Iterable[Iterable[int]],\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation_from_files", "modulename": "drup", "qualname": "check_derivation_from_files", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:
    \n\n
    formula_file (str): Path to a file containing a CNF in DIMACS format.
    \n\n
    derivation_file (str): Path to a file containing a sequence of RUP or RAT clauses.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.\n  FileNotFoundError: If the formula or proof file cannot be found.
    \n", "signature": "(\tformula_file: str,\tderivation_file: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}, {"fullname": "drup.check_derivation_from_strings", "modulename": "drup", "qualname": "check_derivation_from_strings", "kind": "function", "doc": "
    Check a sequence of RUP and RAT clauses against a CNF.
    \n\n
    Args:\n  formula (str): Cnf as a string in DIMACS format. The header\n    is ignored if present.
    \n\n
    proof (str): Sequence of RUP or RAT clauses format.
    \n\n
    verbose (bool, optional): Return detailed information\n    if the check fails. Defaults to False.
    \n\n
    Returns:\n  CheckerResult: CheckerResult struct representing the result of the check.\n    If each step in the derivation is either RUP or RAT, then the result will\n    be Outcome.VALID. Otherwise, the result will be Outcome.INVALID.\n    The derivation does not need to contain the empty clause.
    \n\n
    Raises:\n  ValueError: If the formula or proof cannot be parsed or formatted.
    \n", "signature": "(\tformula: str,\tderivation: str,\tverbose: bool = False) -> drup.wrappers.CheckerResult:", "funcdef": "def"}];
 
     // mirrored in build-search-index.js (part 1)
     // Also split on html tags. this is a cheap heuristic, but good enough.