poly_log/
constraint.rs

1use std::mem;
2use crate::{Polynomial};
3
4#[derive(Clone,Debug,PartialEq)]
5pub struct Constraint {
6    term: Term
7}
8
9impl Constraint {
10    pub const FALSE: Constraint = Constraint{term: Term::Lit(false)};
11    pub const TRUE: Constraint = Constraint{term: Term::Lit(true)};
12
13    pub fn eq_zero(poly: Polynomial) -> Self {
14        Self{term: Term::Eq(poly).simplify()}
15    }
16    pub fn neq_zero(poly: Polynomial) -> Self {
17        Self{term: Term::Neq(poly).simplify()}
18    }
19    pub fn gt_zero(poly: Polynomial) -> Self {
20        Self{term: Term::Gt(poly).simplify()}
21    }
22    pub fn gteq_zero(poly: Polynomial) -> Self {
23        Self{term: Term::GtEq(poly).simplify()}
24    }
25    pub fn and(mut self, cs: Constraint) -> Self {
26	let term = Term::Conjunct(vec![self.term,cs.term]);
27	Self{term: term.simplify()}
28    }
29    pub fn or(mut self, cs: Constraint) -> Self {
30	let term = Term::Disjunct(vec![self.term,cs.term]);
31	Self{term: term.simplify()}
32    }
33    pub fn not(mut self) -> Self {
34        Self{term:self.term.not().simplify()}
35    }
36    pub fn implies(mut self, rhs: Constraint) -> Self {
37        self.not().or(rhs)
38    }
39    pub fn substitute(&mut self, var: usize, val: &Polynomial) {
40        let mut tmp = Term::Lit(false);
41        self.term.substitute(var,val);
42        mem::swap(&mut tmp,&mut self.term);
43        self.term = tmp.simplify();
44    }
45}
46
47impl From<bool> for Constraint {
48    fn from(b: bool) -> Constraint {
49	Constraint{term: Term::Lit(b)}
50    }
51}
52
53// =================================
54
55#[derive(Clone,Debug,PartialEq)]
56enum Term {
57    Conjunct(Vec<Term>),
58    Disjunct(Vec<Term>),
59    // p == 0
60    Eq(Polynomial),
61    Neq(Polynomial),
62    Gt(Polynomial),
63    GtEq(Polynomial),
64    Lit(bool)
65}
66
67impl Term {
68    pub fn substitute(&mut self, var: usize, val: &Polynomial) {
69        match self {
70            Term::Disjunct(cs)|Term::Conjunct(cs) => {
71                for p in cs.iter_mut() {
72                    p.substitute(var,val);
73                }
74            }
75            Term::Eq(p)|Term::Neq(p)|Term::Gt(p)|Term::GtEq(p) => {
76                *p = p.substitute(var,val);
77            }
78            Term::Lit(_) => { }
79        }
80    }
81
82    // Attempt to simplify constraint
83    pub fn simplify(mut self) -> Self {
84	match self {
85	    Term::Disjunct(cs) => { Term::simplify_or(cs) }
86	    Term::Conjunct(cs) => { Term::simplify_and(cs) }
87	    Term::Eq(p) => { Term::simplify_eq(p) }
88	    Term::Neq(p) => { Term::simplify_neq(p) }
89	    Term::Gt(p) => { Term::simplify_gt(p) }
90	    Term::GtEq(p) => { Term::simplify_gteq(p) }
91	    Term::Lit(b) => self
92	}
93    }
94
95    pub fn not(self) -> Self {
96        match self {
97            Term::Eq(p) => Term::Neq(p),
98            Term::Neq(p) => Term::Eq(p),
99            Term::Gt(p) => Term::GtEq(p.negate()),
100            Term::GtEq(p) => Term::Gt(p.negate()),
101            Term::Disjunct(cs) => Term::Conjunct(Self::negate(cs)),
102            Term::Conjunct(cs) => Term::Disjunct(Self::negate(cs)),
103            Term::Lit(b) => Term::Lit(!b)
104        }
105    }
106
107    fn negate(cs: Vec<Term>) -> Vec<Term> {
108        cs.iter().map(|t| t.clone().not()).collect()
109    }
110
111    fn simplify_and(mut cs: Vec<Term>) -> Term {
112	for i in 0..cs.len() {
113            // FIXME: need to fix this :)
114	    let ith = cs[i].clone().simplify();
115	    //
116	    if &ith == &Term::Lit(false) {
117		// Evaluates to false
118		return ith;
119	    } else {
120                cs[i] = ith;
121            }
122	}
123	// Strip anything unnecessary
124	cs.retain(|item| item != &Term::Lit(true));
125        // FIXME: dedup!
126	//
127	if cs.is_empty() {
128	    Term::Lit(true)
129	} else if cs.len() == 1 {
130            // FIXME: get rid of this :)
131            cs[0].clone()
132        } else {
133	    Term::Conjunct(cs)
134	}
135    }
136
137    fn simplify_or(mut cs: Vec<Term>) -> Term {
138	for i in 0..cs.len() {
139            // FIXME: need to fix this :)
140	    let ith = cs[i].clone().simplify();
141	    //
142	    if &ith == &Term::Lit(true) {
143		// Evaluates to false
144		return ith;
145	    } else {
146                cs[i] = ith;
147            }
148	}
149	// Strip anything unnecessary
150	cs.retain(|item| item != &Term::Lit(false));
151        // FIXME: dedup!
152	//
153	if cs.is_empty() {
154	    Term::Lit(false)
155	} else if cs.len() == 1 {
156            // FIXME: get rid of this :)
157            cs[0].clone()
158        } else {
159	    Term::Disjunct(cs)
160	}
161    }
162
163    fn simplify_eq(p: Polynomial) -> Term {
164	match p.is_zero() {
165	    Some(b) => Term::Lit(b),
166	    None => Term::Eq(p)
167	}
168    }
169
170    fn simplify_neq(p: Polynomial) -> Term {
171	match p.is_zero() {
172	    Some(b) => Term::Lit(!b),
173	    None => Term::Neq(p)
174	}
175    }
176
177    fn simplify_gt(p: Polynomial) -> Term {
178	match p.above_zero() {
179	    Some(b) => Term::Lit(b),
180	    None => Term::Gt(p)
181	}
182    }
183    fn simplify_gteq(p: Polynomial) -> Term {
184	match p.below_zero() {
185            Some(b) => Term::Lit(!b),
186            None => Term::GtEq(p)
187	}
188    }
189}
poly_log/constraint.rs

poly_log/
constraint.rs
