bcsat 0.1.0

A parser, printer and related utilities for BCSAT (http://users.ics.aalto.fi/tjunttil/bcsat/)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

use ast::*;

pub mod join_assoc;

impl BCSAT {
    pub fn transform<F>(&mut self, f: &F)
        where F: Fn(Formula) -> Formula
    {
        use self::Statement::*;
        for stm in self.statements.iter_mut() {
            match *stm {
                Assigned(ref mut form) |
                Defined(_, ref mut form) => transform_box(form, f),
                _ => (),
            }
        }
    }
}
impl Formula {
    pub fn transform<F>(&mut self, f: &F)
        where F: Fn(Formula) -> Formula
    {
        let form = ::std::mem::replace(self, Formula::Constant(Constant::False));
        let form = f(form);
        ::std::mem::replace(self, form);
    }
    pub fn t<F>(self, f: &F) -> Self
        where F: Fn(Formula) -> Formula
    {
        f(self)
    }
    pub fn tb<F>(mut self: Box<Self>, f: &F) -> Box<Self>
        where F: Fn(Formula) -> Formula
    {
        self.transform(f);
        self
    }
}

pub fn transform_box<F>(b: &mut Box<Formula>, f: &F)
    where F: Fn(Formula) -> Formula
{
    b.transform(f)
}