Doz progression

doz/.gitignore

@@ -0,0 +1 @@
+/target

doz/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "doz"
+version = "0.1.0"

doz/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "doz"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

doz/src/constraint.rs

@@ -0,0 +1,103 @@
+pub mod resolution;
+
+use std::collections::{HashMap, VecDeque};
+
+use crate::domain::{Domain, DomainRange};
+
+pub struct Indexical
+{
+    pub variable: usize,
+    pub dependencies: Vec<usize>,
+
+    #[allow(clippy::type_complexity)]
+    pub propagator: Box<dyn Fn(&[DomainRange]) -> DomainRange>,
+}
+
+impl Indexical
+{
+    pub fn new<T>(variable: usize, dependencies: &[usize], propagator: T) -> Indexical
+    where
+        T: Fn(&[DomainRange]) -> DomainRange + 'static,
+    {
+        Indexical {
+            variable,
+            dependencies: dependencies.to_vec(),
+            propagator: Box::new(propagator),
+        }
+    }
+}
+
+pub struct ClpContext
+{
+    pub variables: usize,
+    pub domains: HashMap<usize, Domain>,
+    pub used_by: HashMap<usize, Vec<usize>>,
+    pub constraints: HashMap<usize, Vec<Indexical>>,
+}
+
+impl ClpContext
+{
+    pub fn new() -> Self
+    {
+        ClpContext {
+            variables: 0,
+            domains: HashMap::new(),
+            used_by: HashMap::new(),
+            constraints: HashMap::new(),
+        }
+    }
+
+    pub fn get_var(&mut self) -> usize
+    {
+        let k = self.variables;
+        self.variables += 1;
+        self.domains.insert(k, Domain::from(..));
+        self.used_by.insert(k, vec![]);
+        k
+    }
+
+    pub fn insert_constraint(&mut self, indexical: Indexical)
+    {
+        let vec = self.constraints.entry(indexical.variable).or_insert(vec![]);
+        for x in indexical.dependencies.iter()
+        {
+            self.used_by.get_mut(x).unwrap().push(indexical.variable);
+        }
+        vec.push(indexical);
+    }
+
+    pub fn prune(&mut self) -> bool
+    {
+        let mut queue = VecDeque::from_iter(0..self.variables);
+
+        while !queue.is_empty()
+        {
+            // Apply unary constraints
+            let var = queue.pop_front().unwrap();
+            let constraints = self.constraints.get(&var);
+            if constraints.is_none()
+            {
+                continue;
+            }
+            let constraints = constraints.unwrap();
+
+            for c in constraints.iter()
+            {
+                if c.dependencies.is_empty()
+                {
+                    // Is unary constraint
+                    let domain = self.domains.get(&var).unwrap();
+                }
+            }
+        }
+        todo!();
+    }
+}
+
+impl Default for ClpContext
+{
+    fn default() -> Self
+    {
+        Self::new()
+    }
+}

doz/src/domain.rs

@@ -0,0 +1,241 @@
+pub mod domain_ops;
+pub mod range_ops;
+
+use std::fmt::Display;
+use std::ops::Range;
+use std::ops::RangeFrom;
+use std::ops::RangeFull;
+use std::ops::RangeTo;
+
+pub struct Domain
+{
+    pub ranges: Vec<DomainRange>,
+}
+
+/// Represents the set
+/// $$\{x \in [\text{start}; \text{end}[ | x \equiv \text{congruent} \text{mod} \text{modulo}}$$
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct DomainRange
+{
+    pub start: LowerBound,
+    pub end: HigherBound,
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum LowerBound
+{
+    Infinity,
+    Bounded(i64),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum HigherBound
+{
+    Infinity,
+    Bounded(i64),
+}
+
+pub enum UnionResult<T>
+{
+    Single(T),
+    Union(T, T),
+}
+
+impl Domain
+{
+    pub fn empty(&self) -> Domain
+    {
+        Domain { ranges: vec![] }
+    }
+
+    pub fn is_empty(&self) -> bool
+    {
+        self.ranges.is_empty()
+    }
+}
+
+impl DomainRange
+{
+    pub fn range(from: LowerBound, to: HigherBound) -> DomainRange
+    {
+        DomainRange {
+            start: from,
+            end: to,
+        }
+    }
+}
+
+impl From<Range<i64>> for Domain
+{
+    fn from(value: Range<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeFull> for Domain
+{
+    fn from(value: RangeFull) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeTo<i64>> for Domain
+{
+    fn from(value: RangeTo<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<RangeFrom<i64>> for Domain
+{
+    fn from(value: RangeFrom<i64>) -> Self
+    {
+        Domain {
+            ranges: vec![value.into()],
+        }
+    }
+}
+
+impl From<Range<i64>> for DomainRange
+{
+    fn from(value: Range<i64>) -> Self
+    {
+        DomainRange::range(
+            LowerBound::Bounded(value.start),
+            HigherBound::Bounded(value.end),
+        )
+    }
+}
+
+impl From<RangeTo<i64>> for DomainRange
+{
+    fn from(value: RangeTo<i64>) -> Self
+    {
+        DomainRange::range(LowerBound::Infinity, HigherBound::Bounded(value.end))
+    }
+}
+
+impl From<RangeFrom<i64>> for DomainRange
+{
+    fn from(value: RangeFrom<i64>) -> Self
+    {
+        DomainRange::range(LowerBound::Bounded(value.start), HigherBound::Infinity)
+    }
+}
+
+impl From<RangeFull> for DomainRange
+{
+    fn from(_: RangeFull) -> Self
+    {
+        DomainRange::range(LowerBound::Infinity, HigherBound::Infinity)
+    }
+}
+
+impl Display for LowerBound
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            LowerBound::Infinity => write!(f, "-∞"),
+            LowerBound::Bounded(x) => write!(f, "{}", x),
+        }
+    }
+}
+
+impl Display for HigherBound
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        match self
+        {
+            HigherBound::Infinity => write!(f, "+∞"),
+            HigherBound::Bounded(x) => write!(f, "{}", x),
+        }
+    }
+}
+
+impl Display for DomainRange
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        write!(f, "{}..{}", self.start, self.end)
+    }
+}
+
+impl Display for Domain
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        if self.is_empty()
+        {
+            write!(f, "Ø")
+        }
+        else
+        {
+            let len = self.ranges.len();
+            for (i, r) in self.ranges.iter().enumerate()
+            {
+                write!(f, "{}", r)?;
+                if i != len - 1
+                {
+                    write!(f, " ∪ ")?;
+                }
+            }
+            Ok(())
+        }
+    }
+}
+
+impl PartialOrd for LowerBound
+{
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering>
+    {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for LowerBound
+{
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering
+    {
+        match (self, other)
+        {
+            (LowerBound::Infinity, LowerBound::Infinity) => std::cmp::Ordering::Equal,
+            (LowerBound::Infinity, LowerBound::Bounded(_)) => std::cmp::Ordering::Less,
+            (LowerBound::Bounded(_), LowerBound::Infinity) => std::cmp::Ordering::Greater,
+            (LowerBound::Bounded(a), LowerBound::Bounded(b)) => a.cmp(b),
+        }
+    }
+}
+
+impl PartialOrd for HigherBound
+{
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering>
+    {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for HigherBound
+{
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering
+    {
+        match (self, other)
+        {
+            (HigherBound::Infinity, HigherBound::Infinity) => std::cmp::Ordering::Equal,
+            (HigherBound::Infinity, HigherBound::Bounded(_)) => std::cmp::Ordering::Greater,
+            (HigherBound::Bounded(_), HigherBound::Infinity) => std::cmp::Ordering::Less,
+            (HigherBound::Bounded(a), HigherBound::Bounded(b)) => a.cmp(b),
+        }
+    }
+}

doz/src/domain/domain_ops.rs

@@ -0,0 +1,90 @@
+use crate::domain::{Domain, DomainRange};
+
+impl Domain
+{
+    pub fn intersection(&self, domain: &Domain) -> Domain
+    {
+        let mut i = 0;
+        let mut j = 0;
+        let mut stack = vec![];
+
+        while i < self.ranges.len() || j < domain.ranges.len()
+        {
+            if i < self.ranges.len() && j < domain.ranges.len()
+            {
+                let a = self.ranges[i];
+                let b = domain.ranges[j];
+
+                if a.disjoint(&b)
+                {
+                    if a.start < b.start
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+                else
+                {
+                    let inter = a.intersection(&b);
+                    if let Some(range) = inter
+                    {
+                        stack.push(range);
+                    };
+                    if a.end > b.end
+                    {
+                        i += 1;
+                    }
+                    else
+                    {
+                        j += 1;
+                    }
+                }
+            }
+            else
+            {
+                break;
+            }
+        }
+
+        Domain { ranges: stack }
+    }
+
+    pub fn union(&self, domain: &Domain) -> Domain
+    {
+        let mut stack = self
+            .ranges
+            .iter()
+            .copied()
+            .chain(domain.ranges.iter().copied())
+            .collect::<Vec<DomainRange>>();
+
+        stack.sort_by(|a, b| b.start.cmp(&a.start));
+        let mut ranges = vec![];
+
+        while !stack.is_empty()
+        {
+            if stack.len() >= 2
+            {
+                let (a, b) = (stack.pop().unwrap(), stack.pop().unwrap());
+                match a.union(&b)
+                {
+                    crate::domain::UnionResult::Single(x) => stack.push(x),
+                    crate::domain::UnionResult::Union(x, y) =>
+                    {
+                        ranges.push(x);
+                        stack.push(y);
+                    }
+                }
+            }
+            else if stack.len() == 1
+            {
+                ranges.push(stack.pop().unwrap());
+            }
+        }
+
+        Domain { ranges }
+    }
+}

doz/src/domain/range_ops.rs

@@ -0,0 +1,124 @@
+// Module for computing intersection of domains
+
+use crate::domain::DomainRange;
+use crate::domain::HigherBound;
+use crate::domain::LowerBound;
+use crate::domain::UnionResult;
+
+impl DomainRange
+{
+    pub fn union(&self, range: &DomainRange) -> UnionResult<DomainRange>
+    {
+        let (a, b) = (self.min_by_start(range), self.max_by_start(range));
+        match (a.end, b.start)
+        {
+            (HigherBound::Infinity, LowerBound::Infinity) =>
+            {
+                UnionResult::Single(DomainRange::from(..))
+            }
+            (HigherBound::Infinity, LowerBound::Bounded(_)) => UnionResult::Single(DomainRange {
+                start: a.start,
+                end: HigherBound::Infinity,
+            }),
+            (HigherBound::Bounded(_), LowerBound::Infinity) => UnionResult::Single(DomainRange {
+                start: LowerBound::Infinity,
+                end: b.end,
+            }),
+            (HigherBound::Bounded(c), LowerBound::Bounded(d)) if c < d => UnionResult::Union(a, b),
+            (HigherBound::Bounded(_), LowerBound::Bounded(_)) => UnionResult::Single(DomainRange {
+                start: a.start,
+                end: b.end,
+            }),
+        }
+    }
+
+    pub fn intersection(&self, range: &DomainRange) -> Option<DomainRange>
+    {
+        let (a, b) = (self.min_by_start(range), self.max_by_start(range));
+        match (a.end, b.start)
+        {
+            (HigherBound::Infinity, LowerBound::Infinity) => Some(DomainRange::from(..)),
+            (HigherBound::Infinity, LowerBound::Bounded(a)) => Some(DomainRange::from(a..)),
+            (HigherBound::Bounded(a), LowerBound::Infinity) => Some(DomainRange::from(..a)),
+            (HigherBound::Bounded(a), LowerBound::Bounded(b)) if a <= b => None,
+            (HigherBound::Bounded(a), LowerBound::Bounded(b)) => Some(DomainRange::from(a..b)),
+        }
+    }
+
+    pub fn without(&self, range: &DomainRange) -> DomainRange
+    {
+        match self.intersection(range)
+        {
+            Some(intersecting_part) => match self.union(&intersecting_part)
+            {
+                UnionResult::Single(res) => res,
+                UnionResult::Union(_, _) => unreachable!(),
+            },
+            None => *self,
+        }
+    }
+
+    pub fn symetrical_difference(&self, range: &DomainRange) -> Option<UnionResult<DomainRange>>
+    {
+        match self.intersection(range)
+        {
+            Some(intersecting_part) =>
+            {
+                Some((self.without(&intersecting_part)).union(&range.without(&intersecting_part)))
+            }
+            None => Some(self.union(range)),
+        }
+    }
+
+    pub fn disjoint(&self, range: &DomainRange) -> bool
+    {
+        self.intersection(range).is_none()
+    }
+
+    pub fn included_in(&self, range: &DomainRange) -> bool
+    {
+        if let UnionResult::Single(x) = self.union(range)
+            && x == *range
+        {
+            true
+        }
+        else
+        {
+            false
+        }
+    }
+
+    pub fn min_by_start(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.start < range.start
+        {
+            *self
+        }
+        else
+        {
+            *range
+        }
+    }
+
+    pub fn max_by_start(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.start < range.start
+        {
+            *range
+        }
+        else
+        {
+            *self
+        }
+    }
+
+    pub fn min_by_end(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.end < range.end { *self } else { *range }
+    }
+
+    pub fn max_by_end(&self, range: &DomainRange) -> DomainRange
+    {
+        if self.end < range.end { *range } else { *self }
+    }
+}

doz/src/lib.rs

@@ -0,0 +1,2 @@
+pub mod constraint;
+pub mod domain;

doz/src/main.rs

@@ -0,0 +1,21 @@
+use doz::constraint::Indexical;
+use doz::domain::Domain;
+use doz::domain::DomainRange;
+use doz::indexical;
+
+fn main()
+{
+    let even = Domain {
+        ranges: vec![DomainRange {
+            start: doz::domain::LowerBound::Infinity,
+            end: doz::domain::HigherBound::Infinity,
+        }],
+    };
+
+    //let k = Indexical::new([Box::new(|a, b, c| a), Box::new(|a, b, c| b)]);
+    //
+
+    let k = indexical![|[a, _b]| { a }, |[_a, b]| { b }];
+
+    println!("{}", even);
+}

src/ast.rs

@@ -2,8 +2,6 @@ use owo_colors::{OwoColorize, colors::css::Gray};
 
 use std::fmt::Display;
 
-use crate::domain::Domain;
-
 #[derive(Clone, PartialEq, Eq, Debug, Hash)]
 pub struct Variable(pub String, pub Option<usize>);
 
@@ -33,7 +31,6 @@ pub enum Predicate
 {
     Variable(Variable), // Upercase variable like X
     Fixed(Functor, Vec<Predicate>),
-    Domain(Domain),
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -138,7 +135,6 @@ impl Display for Predicate
                     Ok(())
                 }
             }
-            Predicate::Domain(domain) => write!(f, "{domain}"),
         }
     }
 }
@@ -178,7 +174,6 @@ impl Display for Functor
         }
     }
 }
-
 impl Display for Operator
 {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result

src/domain.rs

@@ -1,512 +0,0 @@
-use std::{cmp, fmt::Display};
-
-use crate::domain;
-
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
-pub struct Domain
-{
-    pub union: Vec<DomainRange>,
-}
-
-#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
-pub struct DomainRange
-{
-    pub start: DomainBound,
-    pub end: DomainBound,
-}
-
-#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
-pub enum DomainBound
-{
-    Unbounded,
-    Bounded(i64),
-}
-
-impl Domain
-{
-    pub fn all() -> Domain
-    {
-        Domain {
-            union: vec![DomainRange {
-                start: DomainBound::Unbounded,
-                end: DomainBound::Unbounded,
-            }],
-        }
-    }
-
-    pub fn included_in(&self, domain: &Domain) -> bool
-    {
-        self.union(domain) == *domain
-    }
-
-    pub fn empty(&self) -> bool
-    {
-        self.union.len() == 0
-    }
-
-    pub fn disjoint(&self, domain: &Domain) -> bool
-    {
-        self.intersection(domain).union.len() == 0
-    }
-
-    pub fn intersection(&self, domain: &Domain) -> Domain
-    {
-        let mut i = 0;
-        let mut j = 0;
-        let mut stack = vec![];
-
-        while i < self.union.len() || j < domain.union.len()
-        {
-            if i < self.union.len() && j < domain.union.len()
-            {
-                let a = self.union[i];
-                let b = domain.union[j];
-
-                if a.disjoint(&b)
-                {
-                    if a < b
-                    {
-                        i += 1;
-                    }
-                    else
-                    {
-                        j += 1;
-                    }
-                }
-                else
-                {
-                    let inter = a.intersection(&b);
-                    if let Some(range) = inter
-                    {
-                        stack.push(range);
-                    };
-                    if a.ends_furthest(&b)
-                    {
-                        i += 1;
-                    }
-                    else
-                    {
-                        j += 1;
-                    }
-                }
-            }
-            else
-            {
-                break;
-            }
-        }
-
-        Domain { union: stack }
-    }
-
-    pub fn union(&self, domain: &Domain) -> Domain
-    {
-        let mut i = 0;
-        let mut j = 0;
-        let mut stack = vec![];
-
-        while i < self.union.len() || j < domain.union.len()
-        {
-            if i < self.union.len() && j < domain.union.len()
-            {
-                let a = self.union[i];
-                let b = domain.union[j];
-
-                let (min, max) = (a.min(b), a.max(b));
-
-                if let DomainBound::Bounded(end) = min.end
-                    && let DomainBound::Bounded(start) = max.start
-                    && end == start
-                {
-                    let union = a.union(&b);
-                    stack.extend_from_slice(union.union.as_slice());
-                    i += 1;
-                    j += 1;
-                }
-                else if a.disjoint(&b)
-                {
-                    if a < b
-                    {
-                        stack.push(a);
-                        i += 1;
-                    }
-                    else
-                    {
-                        stack.push(b);
-                        j += 1;
-                    }
-                }
-                else
-                {
-                    let union = a.union(&b);
-                    stack.extend_from_slice(union.union.as_slice());
-                    i += 1;
-                    j += 1;
-                }
-            }
-            else if i < self.union.len()
-            {
-                stack.extend_from_slice(&self.union[i..]);
-                i = self.union.len();
-            }
-            else
-            {
-                stack.extend_from_slice(&domain.union[j..]);
-                j = self.union.len();
-            }
-        }
-
-        Domain { union: stack }
-    }
-}
-
-impl From<DomainRange> for Domain
-{
-    fn from(value: DomainRange) -> Self
-    {
-        Domain { union: vec![value] }
-    }
-}
-
-impl DomainBound
-{
-    pub fn min_start(&self, bound: DomainBound) -> DomainBound
-    {
-        match (self, bound)
-        {
-            (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
-            (DomainBound::Bounded(_), DomainBound::Unbounded)
-            | (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.min(&b)),
-        }
-    }
-
-    pub fn max_end(&self, bound: DomainBound) -> DomainBound
-    {
-        match (self, bound)
-        {
-            (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
-            (DomainBound::Bounded(_), DomainBound::Unbounded)
-            | (DomainBound::Unbounded, DomainBound::Bounded(_)) => DomainBound::Unbounded,
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => DomainBound::Bounded(*a.max(&b)),
-        }
-    }
-}
-
-impl PartialOrd for DomainRange
-{
-    fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering>
-    {
-        Some(self.cmp(other))
-    }
-}
-
-impl Ord for DomainRange
-{
-    fn cmp(&self, other: &Self) -> std::cmp::Ordering
-    {
-        match (self.start, other.start)
-        {
-            (DomainBound::Unbounded, DomainBound::Unbounded) => cmp::Ordering::Equal,
-            (DomainBound::Unbounded, DomainBound::Bounded(_)) => cmp::Ordering::Less,
-            (DomainBound::Bounded(_), DomainBound::Unbounded) => cmp::Ordering::Greater,
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => a.cmp(&b),
-        }
-    }
-}
-
-impl DomainRange
-{
-    pub fn intersection(&self, range: &DomainRange) -> Option<DomainRange>
-    {
-        let (min, max) = (self.min(range), self.max(range));
-        match (min.end, max.start)
-        {
-            (DomainBound::Unbounded, DomainBound::Unbounded) => Some(DomainRange {
-                start: DomainBound::Unbounded,
-                end: DomainBound::Unbounded,
-            }),
-            (DomainBound::Unbounded, DomainBound::Bounded(a)) => Some(DomainRange {
-                start: DomainBound::Bounded(a),
-                end: max.end,
-            }),
-            (DomainBound::Bounded(a), DomainBound::Unbounded) => Some(DomainRange {
-                start: max.start,
-                end: DomainBound::Bounded(a),
-            }),
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) if b < a => Some(DomainRange {
-                start: DomainBound::Bounded(b),
-                end: DomainBound::Bounded(a),
-            }),
-            _ => None,
-        }
-    }
-
-    pub fn union(&self, range: &DomainRange) -> Domain
-    {
-        if self.disjoint(range)
-        {
-            let (a, b) = (self.min(range), self.max(range));
-            if let DomainBound::Bounded(end) = a.end
-                && let DomainBound::Bounded(start) = b.start
-                && end == start
-            {
-                Domain {
-                    union: vec![DomainRange {
-                        start: a.start,
-                        end: b.end,
-                    }],
-                }
-            }
-            else
-            {
-                Domain {
-                    union: vec![*self.min(range), *self.max(range)],
-                }
-            }
-        }
-        else
-        {
-            let (a, b) = (self.min(range), self.max(range));
-            let range = DomainRange {
-                start: match (a.start, b.start)
-                {
-                    (DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
-                    {
-                        DomainBound::Bounded(a.min(b))
-                    }
-                    (DomainBound::Unbounded, DomainBound::Bounded(_))
-                    | (DomainBound::Bounded(_), DomainBound::Unbounded)
-                    | (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
-                },
-                end: match (a.end, b.end)
-                {
-                    (DomainBound::Bounded(a), DomainBound::Bounded(b)) =>
-                    {
-                        DomainBound::Bounded(a.max(b))
-                    }
-                    (DomainBound::Unbounded, DomainBound::Bounded(_))
-                    | (DomainBound::Bounded(_), DomainBound::Unbounded)
-                    | (DomainBound::Unbounded, DomainBound::Unbounded) => DomainBound::Unbounded,
-                },
-            };
-
-            Domain { union: vec![range] }
-        }
-    }
-
-    pub fn ends_furthest(&self, end: &DomainRange) -> bool
-    {
-        match (self.end, end.end)
-        {
-            (DomainBound::Unbounded, DomainBound::Unbounded) => true,
-            (DomainBound::Unbounded, DomainBound::Bounded(_)) => true,
-            (DomainBound::Bounded(_), DomainBound::Unbounded) => false,
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) => a >= b,
-        }
-    }
-
-    pub fn disjoint(&self, range: &DomainRange) -> bool
-    {
-        let (a, b) = (self.min(range), self.max(range));
-        matches!((a.end, b.start), (DomainBound::Bounded(a), DomainBound::Bounded(b)) if a <= b)
-    }
-
-    pub fn singleton(value: i64) -> DomainRange
-    {
-        DomainRange {
-            start: DomainBound::Bounded(value),
-            end: DomainBound::Bounded(value + 1),
-        }
-    }
-
-    pub fn from(value: i64) -> DomainRange
-    {
-        DomainRange {
-            start: DomainBound::Bounded(value),
-            end: DomainBound::Unbounded,
-        }
-    }
-
-    pub fn to(value: i64) -> DomainRange
-    {
-        DomainRange {
-            start: DomainBound::Unbounded,
-            end: DomainBound::Bounded(value),
-        }
-    }
-
-    pub fn closed(start: i64, end: i64) -> DomainRange
-    {
-        DomainRange {
-            start: DomainBound::Bounded(start),
-            end: DomainBound::Bounded(end),
-        }
-    }
-}
-
-impl Display for Domain
-{
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
-    {
-        let len = self.union.len();
-        for (i, range) in self.union.iter().enumerate()
-        {
-            write!(f, "{}", range)?;
-            if i != len - 1
-            {
-                write!(f, " ∪ ")?;
-            }
-        }
-        Ok(())
-    }
-}
-
-impl Display for DomainRange
-{
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
-    {
-        match (self.start, self.end)
-        {
-            (DomainBound::Bounded(a), DomainBound::Bounded(b)) if b == a + 1 => write!(f, "{}", a),
-            (a, b) => write!(f, "{}..{}", a, b),
-        }
-    }
-}
-
-impl Display for DomainBound
-{
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
-    {
-        match self
-        {
-            DomainBound::Unbounded => Ok(()),
-            DomainBound::Bounded(n) => write!(f, "{}", n),
-        }
-    }
-}
-
-mod test
-{
-    #[allow(unused_imports)]
-    use crate::domain::{Domain, DomainBound, DomainRange};
-
-    #[test]
-    pub fn domain_range_parse()
-    {
-        let a: DomainRange = "..".into();
-        assert_eq!(
-            a,
-            DomainRange {
-                start: DomainBound::Unbounded,
-                end: DomainBound::Unbounded
-            }
-        );
-
-        let a: DomainRange = "42..".into();
-        assert_eq!(
-            a,
-            DomainRange {
-                start: DomainBound::Bounded(42),
-                end: DomainBound::Unbounded
-            }
-        );
-
-        let a: DomainRange = "..42".into();
-        assert_eq!(
-            a,
-            DomainRange {
-                start: DomainBound::Unbounded,
-                end: DomainBound::Bounded(42),
-            }
-        );
-
-        let a: DomainRange = "0..42".into();
-        assert_eq!(
-            a,
-            DomainRange {
-                start: DomainBound::Bounded(0),
-                end: DomainBound::Bounded(42),
-            }
-        );
-    }
-
-    #[test]
-    pub fn domain_range_union()
-    {
-        let inf: DomainRange = "..".into();
-        let inf_b: DomainRange = "..42".into();
-        let a_inf: DomainRange = "0..".into();
-        let a_b: DomainRange = "10..20".into();
-        let a_b2: DomainRange = "30..50".into();
-        let a_b3: DomainRange = "20..30".into();
-
-        assert_eq!(inf.union(&inf), "..".into());
-        assert_eq!(inf.union(&inf_b), "..".into());
-        assert_eq!(inf.union(&a_inf), "..".into());
-        assert_eq!(inf.union(&a_b), "..".into());
-
-        assert_eq!(inf.union(&inf), "..".into());
-        assert_eq!(inf_b.union(&inf), "..".into());
-        assert_eq!(a_inf.union(&inf), "..".into());
-        assert_eq!(a_b.union(&inf), "..".into());
-
-        assert_eq!(inf.union(&inf), "..".into());
-        assert_eq!(inf_b.union(&inf_b), "..42".into());
-        assert_eq!(a_inf.union(&a_inf), "0..".into());
-        assert_eq!(a_b.union(&a_b), "10..20".into());
-
-        assert_eq!(
-            a_b.union(&a_b2),
-            Domain {
-                union: vec!["10..20".into(), "30..50".into()]
-            }
-        );
-
-        assert_eq!(a_b.union(&a_b3), "10..30".into());
-    }
-
-    #[test]
-    pub fn domain_union()
-    {
-        let k: Domain = "2..5".into();
-        let k2: Domain = "5..10".into();
-        assert_eq!(
-            k.union(&k2),
-            Domain {
-                union: vec![DomainRange {
-                    start: DomainBound::Bounded(2),
-                    end: DomainBound::Bounded(10)
-                }]
-            }
-        );
-    }
-
-    #[test]
-    pub fn domain_intersection()
-    {
-        let k: Domain = "0..5".into();
-        let k2: Domain = "10..15".into();
-
-        let k3: Domain = "3..7".into();
-        let k4: Domain = "13..17".into();
-
-        let a = k.union(&k2);
-        let b = k3.union(&k4);
-        assert_eq!(
-            a.intersection(&b),
-            Domain {
-                union: vec![
-                    DomainRange {
-                        start: DomainBound::Bounded(3),
-                        end: DomainBound::Bounded(5)
-                    },
-                    DomainRange {
-                        start: DomainBound::Bounded(13),
-                        end: DomainBound::Bounded(15)
-                    }
-                ]
-            }
-        );
-    }
-}

src/lib.rs

@@ -1,4 +1,3 @@
 pub mod ast;
-pub mod domain;
 pub mod parsing;
 pub mod prover;

src/main.rs

@@ -1,7 +1,5 @@
 use picolog::ast::Body;
 use picolog::ast::Module;
-use picolog::ast::Predicate;
-use picolog::domain::Domain;
 
 fn main()
 {
@@ -10,67 +8,48 @@ fn main()
         .format_timestamp(None)
         .init();
     //println!("{:#?}", Module::parse_from_file("1.pl"));
-    // let module: Module = "
-    //     integer(zero).
-    //     integer(s(X)) :- integer(X).
-    //
-    //     add(X, zero, X).
-    //     add(X, s(Y), Z) :- add(s(X), Y, Z).
-    //
-    //     mult(zero, X, zero).
-    //     mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
-    //
-    //     op(10, yfx, +).
-    //     op(8, yfx, ^).
-    //     op(6, xfy, ::).
-    //     op(2, fx, [).
-    //     op(2, xf, ]).
-    //     op(3, yfx, |).
-    //
-    //     A + B :- test.
-    //
-    //     A ^ B + C :- test.
-    //     A::B::C :- A.
-    //     [Hd|Tl] :- Hd::Tl.
-    //
-    //     l(X) :- in(X, 3..7).
-    // "
-    // .into();
-
-    let d1: Domain = "5..10".into();
-    let d2: Domain = "7..18".into();
-
     let module: Module = "
-        hello(5..10).
-        world(7..18).
+        integer(zero).
+        integer(s(X)) :- integer(X).
+
+        add(X, zero, X).
+        add(X, s(Y), Z) :- add(s(X), Y, Z).
+
+        mult(zero, X, zero).
+        mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
+
+        op(10, yfx, +).
+        op(8, yfx, ^).
+        op(6, xfy, ::).
+        op(2, fx, [).
+        op(2, xf, ]).
+        op(3, yfx, |).
+
+        A + B :- test.
+
+        A ^ B + C :- test.
+        A::B::C :- A.
+        [Hd|Tl] :- Hd::Tl.
     "
     .into();
 
-    //let pred: Predicate = "hello(0..10).".into();
-    let show: Body = "hello(X), world(X)".into();
-
-    for c in module.prove(&show)
+    // println!("{}", module);
+    // let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
+    //let prop: Body = "integer(s(X))".into();
+    let prop: Body = "mult(X, s(s(zero)), s(s(s(s(zero)))))".into();
+    //let prop: Body = "mult(X, Y, Z)".into();
+    //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into();
+    for c in module.prove(&prop)
     {
         println!("true:");
         println!("{}", c.simplified());
         let _ = std::io::stdin().read_line(&mut String::new());
     }
-    //println!("{}", module.prove(&pred).unwrap());
-    // let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
-    //let prop: Body = "integer(s(X))".into();
-    //let prop: Body = "mult(X, s(s(zero)), s(s(s(s(zero)))))".into();
-    //let prop: Body = "mult(X, Y, Z)".into();
-    //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into();
-    // for c in module.prove(&prop)
-    // {
-    //     println!("true:");
-    //     println!("{}", c.simplified());
-    //     let _ = std::io::stdin().read_line(&mut String::new());
-    // }
-    //
+
     // let p: Predicate = "add(s(zero), zero, Y)".into();
     // let p1: Predicate = "add(X, zero, X)".into();
     // // let p: Predicate = "integer(s(zero))".into();
     // // let p1: Predicate = "integer(s(X))".into();
     // println!("{}", p.matches(&p1).unwrap());
+    //
 }

src/parsing.rs

@@ -1,14 +1,13 @@
 use std::{collections::HashMap, path::Path};
 
 use winnow::{
-    Parser, Result, Stateful,
-    ascii::{self, alphanumeric1, dec_int, multispace0},
+    ascii::{self, alphanumeric1, multispace0},
     combinator::{
-        Infix, Postfix, Prefix, alt, delimited, expression, opt, preceded, repeat, separated, seq,
-        terminated,
+        alt, delimited, expression, opt, preceded, repeat, separated, seq, terminated, Infix,
+        Postfix, Prefix,
     },
     error::ContextError,
-    token::literal,
+    Parser, Result, Stateful,
 };
 
 use crate::ast::Clause;
@@ -16,9 +15,8 @@ use crate::ast::Functor;
 use crate::ast::Module;
 use crate::ast::Operator;
 use crate::ast::Predicate;
-use crate::ast::Variable;
 use crate::ast::{Body, OperatorType};
-use crate::domain::{Domain, DomainBound, DomainRange};
+use crate::ast::Variable;
 
 impl Operator
 {
@@ -108,28 +106,6 @@ impl State
 
 type Stream<'is> = Stateful<&'is str, State>;
 
-pub fn domain_range_parse(input: &mut Stream) -> Result<DomainRange>
-{
-    let start = opt(dec_int.map(DomainBound::Bounded))
-        .map(|v| v.unwrap_or(DomainBound::Unbounded))
-        .parse_next(input)?;
-    literal("..").parse_next(input)?;
-    let end = opt(dec_int.map(DomainBound::Bounded))
-        .map(|v| v.unwrap_or(DomainBound::Unbounded))
-        .parse_next(input)?;
-    Ok(DomainRange { start, end })
-}
-
-pub fn domain_parse(input: &mut Stream) -> Result<Domain>
-{
-    // Domain is either a..b, ..
-    alt((domain_range_parse, dec_int.map(DomainRange::singleton)))
-        .map(|domain| Domain {
-            union: vec![domain],
-        })
-        .parse_next(input)
-}
-
 pub fn operator_parse(input: &mut Stream) -> Result<String>
 {
     delimited(multispace0, repeat(1.., alt(OPERATORS)), multispace0)
@@ -250,7 +226,6 @@ pub fn predicate_parse_recursive(input: &mut Stream) -> Result<Predicate>
 {
     alt((
         delimited("(", predicate_parse, ")"),
-        domain_parse.map(Predicate::Domain),
         predicate_parse_variable_or_functor,
     ))
     .parse_next(input)
@@ -367,35 +342,3 @@ where
             .unwrap()
     }
 }
-
-impl<T> From<T> for Domain
-where
-    T: AsRef<str>,
-{
-    fn from(value: T) -> Self
-    {
-        let str: &str = value.as_ref();
-        domain_parse
-            .parse_next(&mut Stream {
-                input: str,
-                state: State::new(),
-            })
-            .unwrap()
-    }
-}
-
-impl<T> From<T> for DomainRange
-where
-    T: AsRef<str>,
-{
-    fn from(value: T) -> Self
-    {
-        let str: &str = value.as_ref();
-        domain_range_parse
-            .parse_next(&mut Stream {
-                input: str,
-                state: State::new(),
-            })
-            .unwrap()
-    }
-}

src/prover.rs

@@ -135,7 +135,6 @@ impl Predicate
                     .map(|x| x.make_unique(counter.clone(), unique_map))
                     .collect(),
             ),
-            Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
         }
     }
 }

src/prover/constraints.rs

@@ -4,15 +4,11 @@ use std::fmt::Display;
 use crate::ast::Body;
 use crate::ast::Predicate;
 use crate::ast::Variable;
-use crate::domain;
-use crate::domain::Domain;
-use crate::prover::predicate;
 
 #[derive(Clone, Debug)]
 pub struct Constraints
 {
-    pub(crate) predicates: HashMap<Variable, Predicate>,
-    pub(crate) domains: HashMap<Variable, Domain>,
+    pub(crate) set: HashMap<Variable, Predicate>,
 }
 
 impl Constraints
@@ -20,33 +16,20 @@ impl Constraints
     pub fn none() -> Self
     {
         Constraints {
-            predicates: HashMap::new(),
-            domains: HashMap::new(),
+            set: HashMap::new(),
         }
     }
 
-    pub fn with(variable: Variable, predicate: Option<Predicate>, domain: Option<Domain>) -> Self
+    pub fn with(variable: Variable, predicate: Predicate) -> Self
     {
         let mut c = Constraints::none();
-        if let Some(predicate) = predicate
-        {
-            c.predicates.insert(variable.clone(), predicate);
-        }
-        if let Some(domain) = domain
-        {
-            c.domains.insert(variable, domain);
-        }
+        c.set.insert(variable, predicate);
         c
     }
 
-    pub fn try_append(
-        &mut self,
-        variable: &Variable,
-        predicate: &Predicate,
-        domain: &Domain,
-    ) -> bool
+    pub fn try_append(&mut self, variable: &Variable, predicate: &Predicate) -> bool
     {
-        let predicates = if let Some(other_predicate) = self.predicates.get(variable)
+        if let Some(other_predicate) = self.set.get(variable)
         {
             if predicate == other_predicate
             {
@@ -63,7 +46,7 @@ impl Constraints
                 // We can try adding the unification contraints which is implicitely the same
                 if self.try_merge(&unification_contraints)
                 {
-                    self.predicates.insert(variable.clone(), predicate.clone());
+                    self.set.insert(variable.clone(), predicate.clone());
                     true
                 }
                 else
@@ -80,40 +63,18 @@ impl Constraints
         else
         {
             // No constraint
-            self.predicates
-                .insert(variable.clone(), (predicate.clone(), domain.clone()));
+            self.set.insert(variable.clone(), predicate.clone());
             true
-        };
-
-        // Check if domains are compatible
-        let domains = if let Some((_, other_domain)) = self.predicates.get_mut(variable)
-        {
-            let intersection = domain.intersection(other_domain);
-            if intersection.empty()
-            {
-                false
-            }
-            else
-            {
-                *other_domain = intersection;
-                true
-            }
         }
-        else
-        {
-            true
-        };
-
-        domains && predicates
     }
 
     pub fn try_merge(&mut self, constraints: &Constraints) -> bool
     {
         // Trying to merge, is just trying to add all of the constraints into self
         let mut ok = self.clone();
-        for (var, (pred, domain)) in constraints.predicates.iter()
+        for (var, pred) in constraints.set.iter()
         {
-            if !ok.try_append(var, pred, domain)
+            if !ok.try_append(var, pred)
             {
                 return false;
             }
@@ -132,26 +93,24 @@ impl Constraints
     pub fn simplified(&self) -> Constraints
     {
         let mut max_sub = Constraints::none();
-        for (var, (pred, domain)) in self.predicates.iter()
+        for (var, pred) in self.set.iter()
         {
-            max_sub
-                .predicates
-                .insert(var.clone(), (pred.substitute(self), domain.clone()));
+            max_sub.set.insert(var.clone(), pred.substitute(self));
         }
 
         let mut stripped = max_sub.clone();
-        'outer: for (var, _) in max_sub.predicates.iter()
+        'outer: for (var, _) in max_sub.set.iter()
         {
             if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some()
             {
-                for (_, (other_pred, _)) in max_sub.predicates.iter()
+                for (_, other_pred) in max_sub.set.iter()
                 {
                     if other_pred.contains_variable(var)
                     {
                         continue 'outer;
                     }
                 }
-                stripped.predicates.remove(var);
+                stripped.set.remove(var);
             }
         }
 
@@ -167,7 +126,7 @@ impl Predicate
         {
             Predicate::Variable(name) =>
             {
-                if let Some((pred, _)) = constraints.predicates.get(name)
+                if let Some(pred) = constraints.set.get(name)
                 {
                     pred.substitute(constraints)
                 }
@@ -183,7 +142,6 @@ impl Predicate
                     .map(|x| x.substitute(constraints))
                     .collect(),
             ),
-            Predicate::Domain(domain) => Predicate::Domain(domain.clone()),
         }
     }
 
@@ -193,7 +151,6 @@ impl Predicate
         {
             Predicate::Variable(var_name) => name == var_name,
             Predicate::Fixed(_, predicates) => predicates.iter().any(|x| x.contains_variable(name)),
-            Predicate::Domain(_) => false,
         }
     }
 }
@@ -226,8 +183,8 @@ impl Display for Constraints
 {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
     {
-        let len = self.predicates.len();
-        for (i, (var, (pred, _))) in self.predicates.iter().enumerate()
+        let len = self.set.len();
+        for (i, (var, pred)) in self.set.iter().enumerate()
         {
             write!(f, "{} = {}", var, pred)?;
             if i != len - 1
@@ -235,15 +192,6 @@ impl Display for Constraints
                 write!(f, ", ")?;
             }
         }
-        write!(f, " ;; ")?;
-        for (i, (var, (_, domain))) in self.predicates.iter().enumerate()
-        {
-            write!(f, "{} in {}", var, domain)?;
-            if i != len - 1
-            {
-                write!(f, ", ")?;
-            }
-        }
         Ok(())
     }
 }

src/prover/internal_operators.rs

@@ -1,50 +0,0 @@
-use crate::{ast::Predicate, prover::constraints::Constraints};
-
-impl Constraints
-{
-    pub fn collapsed_operators(&self) -> Constraints
-    {
-        let mut new_constraints = Constraints::none();
-        for (var, pred) in self.set.iter()
-        {
-            new_constraints
-                .set
-                .insert(var.clone(), pred.substitute(self).collapsed_operators());
-        }
-        new_constraints
-    }
-}
-
-impl Predicate
-{
-    pub fn collapsed_operators(&self) -> Predicate
-    {
-        match self
-        {
-            Predicate::Variable(variable) => Predicate::Variable(variable.clone()),
-            Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
-                if op.op == "+" && predicates.len() == 2 =>
-            {
-                match (predicates[0].clone(), predicates[1].clone())
-                {
-                    (Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a + b),
-                    _ => self.clone(),
-                }
-            }
-            Predicate::Fixed(crate::ast::Functor::Operator(op), predicates)
-                if op.op == "-" && predicates.len() == 2 =>
-            {
-                match (predicates[0].clone(), predicates[1].clone())
-                {
-                    (Predicate::Number(a), Predicate::Number(b)) => Predicate::Number(a - b),
-                    _ => self.clone(),
-                }
-            }
-            Predicate::Fixed(functor, predicates) => Predicate::Fixed(
-                functor.clone(),
-                predicates.iter().map(|x| x.collapsed_operators()).collect(),
-            ),
-            Predicate::Number(n) => Predicate::Number(*n),
-        }
-    }
-}

src/prover/unification.rs

@@ -1,7 +1,4 @@
-use std::clone;
-
 use crate::ast::Predicate;
-use crate::domain::{self, Domain};
 use crate::prover::constraints::Constraints;
 
 impl Predicate
@@ -19,20 +16,9 @@ impl Predicate
                 //debug!("Unifying var {} against {}", self, other);
                 // We are trying to see if X (any) matches the other Predicate.
                 // This is always true if X = other_predicate
-                match other
-                {
-                    Predicate::Domain(domain) => Some(Constraints::with(
-                        variable.clone(),
-                        other.clone(),
-                        domain.clone(),
-                    )),
-                    _ => Some(Constraints::with(
-                        variable.clone(),
-                        other.clone(),
-                        Domain::all(),
-                    )),
-                }
+                Some(Constraints::with(variable.clone(), other.clone()))
             }
+
             Predicate::Fixed(name, arguments) =>
             {
                 match other
@@ -43,7 +29,7 @@ impl Predicate
                         // (any)
                         // This is always true
                         //debug!("Unifying pred {} against var {}", self, other);
-                        Some(Constraints::with(var.clone(), self.clone(), Domain::all()))
+                        Some(Constraints::with(var.clone(), self.clone()))
                     }
                     // Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...)
                     Predicate::Fixed(other_name, other_arguments)
@@ -72,20 +58,6 @@ impl Predicate
                     _ => None,
                 }
             }
-            Predicate::Domain(domain) => match other
-            {
-                Predicate::Variable(variable) => Some(Constraints::with(
-                    variable.clone(),
-                    other.clone(),
-                    domain.clone(),
-                )),
-                Predicate::Fixed(_, _) => None,
-                Predicate::Domain(other_domain) if !domain.intersection(other_domain).empty() =>
-                {
-                    Some(Constraints::none())
-                }
-                Predicate::Domain(_) => None,
-            },
         }
     }
 }