Finsih

Cargo.lock

@@ -240,6 +240,12 @@ version = "0.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "df1d3c3b53da64cf5760482273a98e575c651a67eec7f77df96b5b642de8f039"
 
+[[package]]
+name = "litemap"
+version = "0.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77"
+
 [[package]]
 name = "litrs"
 version = "1.0.0"
@@ -286,6 +292,7 @@ dependencies = [
  "corosensei",
  "crossterm",
  "env_logger",
+ "litemap",
  "log",
  "winnow",
 ]

Cargo.toml

@@ -7,5 +7,6 @@ edition = "2024"
 corosensei = "0.3.2"
 crossterm = "0.29.0"
 env_logger = "0.11.8"
+litemap = "0.8.1"
 log = "0.4.29"
 winnow = "0.7.14"

src/main.rs

@@ -32,7 +32,8 @@ fn main()
     // body.prove_in_module(&module).next().next();
     //
 
-    let body: Body = "mult(s(zero), s(s(zero)), X)".into();
+    let body: Body = "mult(s(s(zero)), s(s(s(zero))), X)".into();
+    //let body: Body = "add(X, s(zero), s(s(zero)))".into();
     let mut prover = body.prove_in_module(&module, Constraints::default());
     while let Some(c) = prover.prove()
     {

src/prover.rs

@@ -1,26 +1,22 @@
 use std::cell::Cell;
-use std::collections::HashMap;
 use std::fmt::Display;
-use std::fmt::write;
-use std::ops;
-use std::ops::Rem;
 use std::rc::Rc;
 
 use corosensei::Coroutine;
 use corosensei::Yielder;
-use log::debug;
+use litemap::LiteMap;
 use log::info;
+use std::collections::HashMap;
 
 use crate::ast::Body;
 use crate::ast::Clause;
 use crate::ast::Module;
 use crate::ast::Predicate;
-use crate::prover;
 
 #[derive(Clone, Debug)]
 pub struct Constraints
 {
-    set: HashMap<String, Predicate>,
+    set: LiteMap<String, Predicate>,
 }
 
 struct Context<'a, 'b>
@@ -75,6 +71,16 @@ impl Prover
 impl Body
 {
     pub fn prove_in_module(&self, module: &Module, constraints: Constraints) -> Prover
+    {
+        self.prove_with_counter(module, constraints, Rc::new(Cell::new(0)))
+    }
+
+    fn prove_with_counter(
+        &self,
+        module: &Module,
+        constraints: Constraints,
+        counter: Rc<Cell<usize>>,
+    ) -> Prover
     {
         let cloned_body = self.clone();
         let cloned_module = module.clone();
@@ -84,7 +90,7 @@ impl Body
                     module: &cloned_module,
                     depth: 0,
                     yielder,
-                    global_counter: Rc::new(Cell::new(0)),
+                    global_counter: counter.clone(),
                 },
                 &constraints,
             );
@@ -119,7 +125,11 @@ impl Body
                 {
                     let last = x.last().unwrap();
                     let first = Body::And(Vec::from(&x[..(x.len() - 1)]));
-                    let mut prover = first.prove_in_module(context.module, constraints.clone());
+                    let mut prover = first.prove_with_counter(
+                        context.module,
+                        constraints.clone(),
+                        context.global_counter.clone(),
+                    );
                     while let Some(new_constraints) = prover.prove()
                     {
                         last.clone().prove(context.descend(), &new_constraints);
@@ -344,7 +354,7 @@ impl Constraints
     pub fn new() -> Self
     {
         Constraints {
-            set: HashMap::new(),
+            set: LiteMap::new(),
         }
     }
 
@@ -385,6 +395,7 @@ impl Constraints
         {
             if !new.append(var.clone(), pred.clone())
             {
+                info!(target: "Contradictory", "{} <- {} = {}", new, var, pred);
                 return None;
             };
         }