diff --git a/lit/src/lit.rs b/lit/src/lit.rs
index e55104c..409869c 100644
--- a/lit/src/lit.rs
+++ b/lit/src/lit.rs
@@ -2,6 +2,8 @@ use imctk_derive::{NewtypeCast, SubtypeCast};
 use imctk_ids::{Id, Id32};
 use std::ops;
 
+use crate::pol::{Negate, NegateInPlace};
+
 use super::{pol::Pol, var::Var};
 
 /// Numeric identifier for a Boolean-like literal.
@@ -63,6 +65,28 @@ impl Default for Lit {
     }
 }
 
+impl From<Var> for Lit {
+    #[inline(always)]
+    fn from(var: Var) -> Self {
+        var.as_lit()
+    }
+}
+
+#[derive(Clone, Copy, Debug)]
+pub struct NegativePolarityError(pub Var);
+
+impl TryFrom<Lit> for Var {
+    type Error = NegativePolarityError;
+
+    fn try_from(lit: Lit) -> Result<Self, Self::Error> {
+        if lit.is_pos() {
+            Ok(lit.var())
+        } else {
+            Err(NegativePolarityError(lit.var()))
+        }
+    }
+}
+
 impl Lit {
     /// The literal representing constant false/0/low.
     pub const FALSE: Self = Self::MIN_ID;
@@ -130,10 +154,7 @@ impl Lit {
 
     /// This is equivalent to `f(self.var()) ^ self.pol()`.
     #[inline(always)]
-    pub fn lookup<T, U>(self, f: impl FnOnce(Var) -> T) -> U
-    where
-        T: ops::BitXor<Pol, Output = U>,
-    {
+    pub fn lookup<T: Negate>(self, f: impl FnOnce(Var) -> T) -> T::Negated {
         f(self.var()) ^ self.pol()
     }
 
@@ -159,6 +180,7 @@ impl Lit {
 impl ops::BitXor<Pol> for Lit {
     type Output = Self;
 
+    #[inline(always)]
     fn bitxor(self, rhs: Pol) -> Self::Output {
         // SAFETY: Changing the LSB of the code makes it stay in bounds
         unsafe { Lit::from_code_unchecked(self.code() ^ (rhs as usize)) }
@@ -166,6 +188,7 @@ impl ops::BitXor<Pol> for Lit {
 }
 
 impl ops::BitXorAssign<Pol> for Lit {
+    #[inline(always)]
     fn bitxor_assign(&mut self, rhs: Pol) {
         *self = *self ^ rhs;
     }
@@ -174,6 +197,7 @@ impl ops::BitXorAssign<Pol> for Lit {
 impl ops::BitXor<bool> for Lit {
     type Output = Self;
 
+    #[inline(always)]
     fn bitxor(self, rhs: bool) -> Self::Output {
         // SAFETY: Changing the LSB of the code makes it stay in bounds
         unsafe { Lit::from_code_unchecked(self.code() ^ (rhs as usize)) }
@@ -183,12 +207,14 @@ impl ops::BitXor<bool> for Lit {
 impl ops::BitXor<Pol> for &'_ Lit {
     type Output = Lit;
 
+    #[inline(always)]
     fn bitxor(self, rhs: Pol) -> Self::Output {
         *self ^ rhs
     }
 }
 
 impl ops::BitXorAssign<bool> for Lit {
+    #[inline(always)]
     fn bitxor_assign(&mut self, rhs: bool) {
         *self = *self ^ rhs;
     }
@@ -197,12 +223,37 @@ impl ops::BitXorAssign<bool> for Lit {
 impl ops::Not for Lit {
     type Output = Self;
 
+    #[inline(always)]
     fn not(self) -> Self::Output {
         // SAFETY: Changing the LSB of the code makes it stay in bounds
         unsafe { Lit::from_code_unchecked(self.code() ^ 1) }
     }
 }
 
+impl ops::Not for &'_ Lit {
+    type Output = Lit;
+
+    #[inline(always)]
+    fn not(self) -> Self::Output {
+        !*self
+    }
+}
+
+impl Negate for Lit {
+    type Negated = Lit;
+}
+
+impl NegateInPlace for Lit {
+    #[inline(always)]
+    fn negate_in_place(&mut self) {
+        *self = !*self
+    }
+}
+
+impl Negate for &'_ Lit {
+    type Negated = Lit;
+}
+
 // FIXME optional dependency
 impl flussab_aiger::Lit for Lit {
     const MAX_CODE: usize = <Self as Id>::MAX_ID_INDEX;
diff --git a/lit/src/pol.rs b/lit/src/pol.rs
index 1238d40..e48f534 100644
--- a/lit/src/pol.rs
+++ b/lit/src/pol.rs
@@ -76,6 +76,15 @@ impl ops::BitXor for Pol {
     }
 }
 
+impl ops::BitXor<Pol> for &'_ Pol {
+    type Output = Pol;
+
+    #[inline(always)]
+    fn bitxor(self, rhs: Pol) -> Self::Output {
+        *self ^ rhs
+    }
+}
+
 impl ops::BitXorAssign for Pol {
     #[inline(always)]
     fn bitxor_assign(&mut self, rhs: Self) {
@@ -86,6 +95,7 @@ impl ops::BitXorAssign for Pol {
 impl ops::BitXor<Pol> for bool {
     type Output = bool;
 
+    #[inline(always)]
     fn bitxor(self, rhs: Pol) -> Self::Output {
         self ^ (rhs == Pol::Neg)
     }
@@ -94,12 +104,14 @@ impl ops::BitXor<Pol> for bool {
 impl ops::BitXor<Pol> for &'_ bool {
     type Output = bool;
 
+    #[inline(always)]
     fn bitxor(self, rhs: Pol) -> Self::Output {
         *self ^ rhs
     }
 }
 
 impl ops::BitXorAssign<Pol> for bool {
+    #[inline(always)]
     fn bitxor_assign(&mut self, rhs: Pol) {
         *self ^= rhs == Pol::Neg
     }
@@ -108,6 +120,7 @@ impl ops::BitXorAssign<Pol> for bool {
 impl ops::BitXor<Pol> for u64 {
     type Output = u64;
 
+    #[inline(always)]
     fn bitxor(self, rhs: Pol) -> Self::Output {
         self ^ match rhs {
             Pol::Pos => 0,
@@ -116,10 +129,114 @@ impl ops::BitXor<Pol> for u64 {
     }
 }
 
+impl ops::BitXor<Pol> for &'_ u64 {
+    type Output = u64;
+
+    #[inline(always)]
+    fn bitxor(self, rhs: Pol) -> Self::Output {
+        *self ^ rhs
+    }
+}
+
 impl ops::Not for Pol {
     type Output = Self;
 
+    #[inline(always)]
     fn not(self) -> Self::Output {
         self ^ Pol::Neg
     }
 }
+
+impl ops::Not for &'_ Pol {
+    type Output = Pol;
+
+    #[inline(always)]
+    fn not(self) -> Self::Output {
+        !*self
+    }
+}
+
+pub trait Negate:
+    Sized
+    + ops::Not<Output = <Self as Negate>::Negated>
+    + ops::BitXor<Pol, Output = <Self as Negate>::Negated>
+{
+    // Not called Output as that's ambiguous with the supertrait's Output
+    type Negated;
+
+    #[inline(always)]
+    fn negate(self) -> <Self as Negate>::Negated
+    where
+        Self: Sized,
+    {
+        !self
+    }
+
+    #[inline(always)]
+    fn apply_pol(self, pol: Pol) -> <Self as Negate>::Negated {
+        self ^ pol
+    }
+}
+
+pub trait NegateInPlace: Negate<Negated = Self> + ops::BitXorAssign<Pol> {
+    fn negate_in_place(&mut self);
+    fn apply_pol_in_place(&mut self, pol: Pol) {
+        *self ^= pol;
+    }
+}
+
+impl ops::BitXorAssign<Pol> for u64 {
+    fn bitxor_assign(&mut self, rhs: Pol) {
+        *self = *self ^ rhs
+    }
+}
+
+impl Negate for u64 {
+    type Negated = u64;
+}
+
+impl NegateInPlace for u64 {
+    #[inline(always)]
+    fn negate_in_place(&mut self) {
+        *self = !*self;
+    }
+
+    #[inline(always)]
+    fn apply_pol_in_place(&mut self, pol: Pol) {
+        *self ^= 0 ^ pol;
+    }
+}
+
+impl Negate for &u64 {
+    type Negated = u64;
+}
+
+impl Negate for bool {
+    type Negated = bool;
+}
+
+impl NegateInPlace for bool {
+    #[inline(always)]
+    fn negate_in_place(&mut self) {
+        *self = !*self;
+    }
+}
+
+impl Negate for &bool {
+    type Negated = bool;
+}
+
+impl Negate for Pol {
+    type Negated = Pol;
+}
+
+impl NegateInPlace for Pol {
+    #[inline(always)]
+    fn negate_in_place(&mut self) {
+        *self = !*self;
+    }
+}
+
+impl Negate for &Pol {
+    type Negated = Pol;
+}