feat: Make Literal wrapper of Predicate

pumpkin-crates/constraints/src/constraints/arithmetic/equality.rs

@@ -3,9 +3,9 @@ use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
 use pumpkin_core::options::ReifiedPropagatorArgs;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
-use pumpkin_core::variables::Literal;
 use pumpkin_core::variables::TransformableVariable;
 use pumpkin_propagators::arithmetic::BinaryEqualsPropagatorArgs;
 use pumpkin_propagators::arithmetic::BinaryNotEqualsPropagatorArgs;
@@ -109,7 +109,7 @@ where
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         if self.terms.len() == 2 && !solver.is_logging_proof() {
             let _ = solver.add_propagator(ReifiedPropagatorArgs {
@@ -184,7 +184,7 @@ where
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         let NotEqualConstraint {
             terms,

pumpkin-crates/constraints/src/constraints/arithmetic/inequality.rs

@@ -2,9 +2,9 @@ use pumpkin_core::ConstraintOperationError;
 use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
-use pumpkin_core::variables::Literal;
 use pumpkin_propagators::arithmetic::LinearLessOrEqualPropagatorArgs;
 
 /// Create the [`NegatableConstraint`] `∑ terms_i <= rhs`.
@@ -119,7 +119,7 @@ impl<Var: IntegerVariable + 'static> Constraint for Inequality<Var> {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         LinearLessOrEqualPropagatorArgs {
             x: self.terms,

pumpkin-crates/constraints/src/constraints/boolean.rs

@@ -1,19 +1,20 @@
 use pumpkin_core::ConstraintOperationError;
 use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::AffineView;
+use pumpkin_core::variables::AnyInteger;
 use pumpkin_core::variables::DomainId;
-use pumpkin_core::variables::Literal;
 use pumpkin_core::variables::TransformableVariable;
 
-use super::equals;
 use super::less_than_or_equals;
+use crate::equals;
 
 /// Creates the [`Constraint`] `∑ weights_i * bools_i <= rhs`.
 pub fn boolean_less_than_or_equals(
     weights: impl Into<Box<[i32]>>,
-    bools: impl Into<Box<[Literal]>>,
+    bools: impl Into<Box<[Predicate]>>,
     rhs: i32,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
@@ -28,7 +29,7 @@ pub fn boolean_less_than_or_equals(
 /// Creates the [`Constraint`] `∑ weights_i * bools_i == rhs`.
 pub fn boolean_equals(
     weights: impl Into<Box<[i32]>>,
-    bools: impl Into<Box<[Literal]>>,
+    bools: impl Into<Box<[Predicate]>>,
     rhs: DomainId,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
@@ -42,7 +43,7 @@ pub fn boolean_equals(
 
 struct BooleanLessThanOrEqual {
     weights: Box<[i32]>,
-    bools: Box<[Literal]>,
+    bools: Box<[Predicate]>,
     rhs: i32,
     constraint_tag: ConstraintTag,
 }
@@ -57,7 +58,7 @@ impl Constraint for BooleanLessThanOrEqual {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         let domains = self.create_domains();
 
@@ -67,18 +68,18 @@ impl Constraint for BooleanLessThanOrEqual {
 }
 
 impl BooleanLessThanOrEqual {
-    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
+    fn create_domains(&self) -> Vec<AffineView<Predicate>> {
         self.bools
             .iter()
             .enumerate()
-            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
+            .map(|(index, bool)| bool.scaled(self.weights[index]))
             .collect()
     }
 }
 
 struct BooleanEqual {
     weights: Box<[i32]>,
-    bools: Box<[Literal]>,
+    bools: Box<[Predicate]>,
     rhs: DomainId,
     constraint_tag: ConstraintTag,
 }
@@ -93,7 +94,7 @@ impl Constraint for BooleanEqual {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         let domains = self.create_domains();
 
@@ -102,12 +103,12 @@ impl Constraint for BooleanEqual {
 }
 
 impl BooleanEqual {
-    fn create_domains(&self) -> Vec<AffineView<DomainId>> {
+    fn create_domains(&self) -> Vec<AffineView<AnyInteger>> {
         self.bools
             .iter()
             .enumerate()
-            .map(|(index, bool)| bool.get_integer_variable().scaled(self.weights[index]))
-            .chain(std::iter::once(self.rhs.scaled(-1)))
+            .map(|(index, bool)| bool.scaled(self.weights[index]).into())
+            .chain(std::iter::once(self.rhs.scaled(-1).into()))
             .collect()
     }
 }

pumpkin-crates/constraints/src/constraints/clause.rs

@@ -2,14 +2,14 @@ use pumpkin_core::ConstraintOperationError;
 use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
-use pumpkin_core::variables::Literal;
 
 /// Creates the [`NegatableConstraint`] `\/ literal`
 ///
 /// Its negation is `/\ !literal`
 pub fn clause(
-    literals: impl Into<Vec<Literal>>,
+    literals: impl Into<Vec<Predicate>>,
     constraint_tag: ConstraintTag,
 ) -> impl NegatableConstraint {
     Clause(literals.into(), constraint_tag)
@@ -19,36 +19,32 @@ pub fn clause(
 ///
 /// Its negation is `\/ !literal`
 pub fn conjunction(
-    literals: impl Into<Vec<Literal>>,
+    literals: impl Into<Vec<Predicate>>,
     constraint_tag: ConstraintTag,
 ) -> impl NegatableConstraint {
     Conjunction(literals.into(), constraint_tag)
 }
 
-struct Clause(Vec<Literal>, ConstraintTag);
+struct Clause(Vec<Predicate>, ConstraintTag);
 
 impl Constraint for Clause {
     fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
         let Clause(clause, constraint_tag) = self;
 
-        solver.add_clause(
-            clause.iter().map(|literal| literal.get_true_predicate()),
-            constraint_tag,
-        )
+        solver.add_clause(clause.iter().copied(), constraint_tag)
     }
 
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         let Clause(clause, constraint_tag) = self;
 
         solver.add_clause(
             clause
                 .into_iter()
-                .chain(std::iter::once(!reification_literal))
-                .map(|literal| literal.get_true_predicate()),
+                .chain(std::iter::once(!reification_literal)),
             constraint_tag,
         )
     }
@@ -64,33 +60,27 @@ impl NegatableConstraint for Clause {
     }
 }
 
-struct Conjunction(Vec<Literal>, ConstraintTag);
+struct Conjunction(Vec<Predicate>, ConstraintTag);
 
 impl Constraint for Conjunction {
     fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
         let Conjunction(conjunction, constraint_tag) = self;
 
         conjunction
             .into_iter()
-            .try_for_each(|lit| solver.add_clause([lit.get_true_predicate()], constraint_tag))
+            .try_for_each(|lit| solver.add_clause([lit], constraint_tag))
     }
 
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         let Conjunction(conjunction, constraint_tag) = self;
 
-        conjunction.into_iter().try_for_each(|lit| {
-            solver.add_clause(
-                [
-                    (!(reification_literal)).get_true_predicate(),
-                    lit.get_true_predicate(),
-                ],
-                constraint_tag,
-            )
-        })
+        conjunction
+            .into_iter()
+            .try_for_each(|lit| solver.add_clause([(!(reification_literal)), lit], constraint_tag))
     }
 }
 

pumpkin-crates/constraints/src/constraints/cumulative.rs

@@ -4,9 +4,9 @@ use pumpkin_core::ConstraintOperationError;
 use pumpkin_core::Solver;
 use pumpkin_core::asserts::pumpkin_assert_simple;
 use pumpkin_core::constraints::Constraint;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
-use pumpkin_core::variables::Literal;
 use pumpkin_propagators::cumulative::ArgTask;
 use pumpkin_propagators::cumulative::options::CumulativeOptions;
 use pumpkin_propagators::cumulative::options::CumulativePropagationMethod;
@@ -235,7 +235,7 @@ impl<Var: IntegerVariable + 'static + Debug> Constraint for CumulativeConstraint
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         match self.options.propagation_method {
             CumulativePropagationMethod::TimeTablePerPoint => TimeTablePerPointPropagator::new(

pumpkin-crates/constraints/src/constraints/disjunctive_strict.rs

@@ -1,9 +1,9 @@
 use pumpkin_core::ConstraintOperationError;
 use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
+use pumpkin_core::predicates::Predicate;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
-use pumpkin_core::variables::Literal;
 use pumpkin_core::variables::TransformableVariable;
 use pumpkin_propagators::disjunctive::ArgDisjunctiveTask;
 use pumpkin_propagators::disjunctive::DisjunctiveConstructor;
@@ -58,7 +58,7 @@ impl<Var: IntegerVariable + 'static> Constraint for DisjunctiveConstraint<Var> {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         // We post both the propagator on the lower-bound and the propagator on the upper-bound.
         DisjunctiveConstructor::new(self.tasks.clone(), self.constraint_tag)

pumpkin-crates/constraints/src/constraints/table.rs

@@ -5,9 +5,10 @@ use pumpkin_core::Solver;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::constraints::NegatableConstraint;
 use pumpkin_core::predicate;
+use pumpkin_core::predicates::Predicate;
+use pumpkin_core::predicates::PredicateConstructor;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
-use pumpkin_core::variables::Literal;
 
 /// Create the [table](https://sofdem.github.io/gccat/gccat/Cin_relation.html#uid22830) [`NegatableConstraint`].
 ///
@@ -65,11 +66,11 @@ impl<Var: IntegerVariable> Table<Var> {
     fn encode(
         self,
         solver: &mut Solver,
-        reification_literal: Option<Literal>,
+        reification_literal: Option<Predicate>,
     ) -> Result<(), ConstraintOperationError> {
         // 1. Create a variable `y_i` that selects the row from the table which is chosen.
         let ys: Vec<_> = (0..self.table.len())
-            .map(|_| solver.new_literal())
+            .map(|_| solver.new_bounded_integer(0, 1).lower_bound_predicate(1))
             .collect();
 
         // 2. Setup the implications between values and `ys`.
@@ -92,20 +93,20 @@ impl<Var: IntegerVariable> Table<Var> {
 
                 // For every `support in supports`: `support -> condition`
                 for support in supports.iter() {
-                    let mut clause = vec![support.get_false_predicate(), condition];
+                    let mut clause = vec![!*support, condition];
 
                     // Account for possible reification.
                     // l -> clause
-                    clause.extend(reification_literal.iter().map(|l| l.get_false_predicate()));
+                    clause.extend(reification_literal.iter().map(|l| !*l));
 
                     solver.add_clause(clause, self.constraint_tag)?;
                 }
 
                 // `condition -> (\/ supports)`
                 let mut clause = vec![!condition];
-                clause.extend(supports.iter().map(|l| l.get_true_predicate()));
+                clause.extend(supports.iter());
                 // Account for possible reification.
-                clause.extend(reification_literal.iter().map(|l| l.get_false_predicate()));
+                clause.extend(reification_literal.iter().map(|l| !*l));
             }
         }
 
@@ -129,7 +130,7 @@ impl<Var: IntegerVariable> Constraint for Table<Var> {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         self.encode(solver, Some(reification_literal))
     }
@@ -176,15 +177,15 @@ impl<Var: IntegerVariable> Constraint for NegativeTable<Var> {
     fn implied_by(
         self,
         solver: &mut Solver,
-        reification_literal: Literal,
+        reification_literal: Predicate,
     ) -> Result<(), ConstraintOperationError> {
         for row in self.table {
             let clause: Vec<_> = self
                 .xs
                 .iter()
                 .zip(row)
                 .map(|(x, value)| predicate![x != value])
-                .chain(std::iter::once(reification_literal.get_false_predicate()))
+                .chain(std::iter::once(!reification_literal))
                 .collect();
 
             solver.add_clause(clause, self.constraint_tag)?;