How about define `Lit` as `(&Var, bool)` to shorten dereference chains?

[shnarazk]

Clauses only refer to properties. We don't need mutual references!

Approach

1. reorganize primitive types
2. move vars from AssignStack to ClauseDB or static mut ❗
3. move out heap of AssignStack
4. change the type of clause.lits from Vec<Lit> to Vec<&Var<'a>>

Let's dive into the unsafe hell

There's no mutable reference!

#![allow(static_mut_refs)]
static mut VECTOR: Vec<usize> = Vec::new();

pub trait VarIF {
    fn push(&self, x: usize);
    fn get(&self) -> usize;
    fn set(&self, x: usize);
    fn increment(&self, offset: usize);
}

struct Var(usize);

impl VarIF for Var {
    fn push(&self, x: usize) {
        unsafe {
            VECTOR.push(x);
        }
    }
    fn get(&self) -> usize {
        unsafe { VECTOR[self.0] }
    }
    fn set(&self, x: usize) {
        unsafe {
            VECTOR[self.0] = x;
        }
    }
    fn increment(&self, offset: usize) {
        unsafe {
            VECTOR[self.0] += offset;
        }
    }
}

fn main() {
    Var(0).push(0);
    println!("{}", Var(0).get());
    Var(0).increment(2);
    println!("{}", Var(0).get());
}