feat: Multithreading (#6)

* refactoring prover in advance of setting up multithreading

* wip making stats,ctx, and prover threadsafe

* wip trying to figure out why perf is terrible...

* finally getting decent performance!

* prepping multithreading code for release

* removing profiling code

* fixing linting

Cargo.toml

@@ -13,6 +13,10 @@ rustc-hash = "1.1.0"
 regex = "1.7.1"
 sugars = "3.0.1"
 lazy_static = "1.4.0"
+rayon = "1.6.1"
+atomic_float = "0.1.0"
+dashmap = "5.4.0"
 
 [package.metadata.maturin]
-name = "tensor_theorem_prover._rust"
+name = "tensor_theorem_prover._rust"
+

README.md

@@ -202,9 +202,17 @@ As a final backstop against the search tree getting too large, you can set a max
 prover = ResolutionProver(knowledge=knowledge, max_resolution_attempts=100_000_000)
 ```
 
+### Multithreading
+
+By default, the ResolutionProver will try to use available CPU cores up to a max of 6, though this may change in future releases. If you want to explicitly control the number of worker threads used for solving, pass `num_workers` when creating the `ResolutionProver`, like below:
+
+```python
+prover = ResolutionProver(knowledge=knowledge, num_workers=1)
+```
+
 ## Acknowledgements
 
-This library borrows code and ideas from the earier library [fuzzy-reasoner](https://github.com/fuzzy-reasoner/fuzzy-reasoner). The main difference between these libraries is that tensor-theorem-prover supports full first-order logic using Resolution, whereas fuzzy-reasoner is restricted to Horn clauses and uses backwards chaining.
+This library borrows code and ideas from the earier library [fuzzy-reasoner](https://github.com/fuzzy-reasoner/fuzzy-reasoner). The main difference between these libraries is that tensor-theorem-prover supports full first-order logic using Resolution, whereas fuzzy-reasoner is restricted to Horn clauses and uses backwards chaining. This library is also much more optimized than the fuzzy-reasoner, as the core of tensor-theorem-prover is written in rust and supports multithreading, while fuzzy-reasoner is pure Python.
 
 Like fuzzy-reasoner, this library also takes inspiration from the following papers for the idea of using vector similarity in theorem proving:
 

docs/usage.rst

@@ -190,4 +190,13 @@ As a final backstop against the search tree getting too large, you can set a max
 
 .. code-block:: python
 
-    prover = ResolutionProver(knowledge=knowledge, max_resolution_attempts=100_000_000)
+    prover = ResolutionProver(knowledge=knowledge, max_resolution_attempts=100_000_000)
+
+Multithreading
+''''''''''''''
+
+By default, the ResolutionProver will try to use available CPU cores up to a max of 6, though this may change in future releases. If you want to explicitly control the number of worker threads used for solving, pass `num_workers` when creating the `ResolutionProver`, like below:
+
+.. code-block:: python
+
+    prover = ResolutionProver(knowledge=knowledge, num_workers=1)

src/prover/mod.rs

@@ -9,14 +9,14 @@ mod resolution_prover;
 mod similarity_cache;
 
 pub use proof::Proof;
-pub use proof_context::ProofContext;
-pub use proof_stats::ProofStats;
+pub use proof_context::{LocalProofContext, SharedProofContext};
+pub use proof_stats::{LocalProofStats, SharedProofStats};
 pub use proof_step::{ProofStep, ProofStepNode, SubstitutionsMap};
 pub use resolution_prover::ResolutionProverBackend;
 
 pub fn register_python_symbols(_py: Python<'_>, module: &PyModule) -> PyResult<()> {
     module.add_class::<ProofStep>()?;
-    module.add_class::<ProofStats>()?;
+    module.add_class::<LocalProofStats>()?;
     module.add_class::<Proof>()?;
     module.add_class::<ResolutionProverBackend>()?;
     Ok(())

src/prover/operations/resolve.rs

@@ -3,7 +3,7 @@ use rustc_hash::{FxHashMap, FxHashSet};
 use std::collections::BTreeSet;
 
 use crate::{
-    prover::{proof_step::ProofStepNode, ProofContext, ProofStep, SubstitutionsMap},
+    prover::{proof_step::ProofStepNode, LocalProofContext, ProofStep, SubstitutionsMap},
     types::{Atom, CNFDisjunction, CNFLiteral, Term, Variable},
     util::PyArcItem,
 };
@@ -25,7 +25,7 @@ lazy_static! {
 pub fn resolve(
     source: &PyArcItem<CNFDisjunction>,
     target: &PyArcItem<CNFDisjunction>,
-    ctx: &mut ProofContext,
+    ctx: &mut LocalProofContext,
     parent_node: Option<&ProofStepNode>,
 ) -> Vec<ProofStepNode> {
     let mut next_steps = Vec::new();
@@ -37,11 +37,8 @@ pub fn resolve(
         if source_literal.item.polarity == target_literal.item.polarity {
             continue;
         }
-        ctx.stats.attempted_unifications += 1;
         let unification = unify(&source_literal.item.atom, &target_literal.item.atom, ctx);
         if let Some(unification) = unification {
-            ctx.stats.successful_unifications += 1;
-
             let resolvent = build_resolvent(
                 source,
                 target,