Skip to main content

Abstract

elina::ast

Struct Abstract 

Source 
pub struct Abstract { /* private fields */ }
Expand description

An element of the abstract domain lattice.

In ELINA, a single Abstract models mappings from variables to sets of numbers.

Wraps elina_abstract0_t.

Implementations§

Source§

impl Abstract

Source

pub fn top<M: Manager>(man: &M, env: &Environment) -> Abstract

Returns a new Abstract element representing Top (⊤) in the lattice.

Examples found in repository?
examples/bottom_free.rs (line 11)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    std::mem::drop(Abstract::bottom(&man, &env));
9    println!("after ::bottom free");
10
11    let mut top = Abstract::top(&man, &env);
12    top.meet(&man, &Abstract::bottom(&man, &env));
13    println!("after created bottom");
14    std::mem::drop(top);
15    println!("after created bottom free");
16}
More examples
Hide additional examples
examples/showcase.rs (line 15)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn bottom<M: Manager>(man: &M, env: &Environment) -> Abstract

Returns a new Abstract element representing Bottom (⊥) in the lattice.

Examples found in repository?
examples/bottom_free.rs (line 8)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    std::mem::drop(Abstract::bottom(&man, &env));
9    println!("after ::bottom free");
10
11    let mut top = Abstract::top(&man, &env);
12    top.meet(&man, &Abstract::bottom(&man, &env));
13    println!("after created bottom");
14    std::mem::drop(top);
15    println!("after created bottom free");
16}
Source

pub fn satisfy<M: Manager>(&self, man: &M, tcons: &Tcons) -> bool

Returns true if self satisfies tcons, i.e. self ⊆ tcons.

Examples found in repository?
examples/showcase.rs (line 18)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn meet<M: Manager, MT: Meetable + ?Sized>(&mut self, man: &M, other: &MT)

Performs the meet operation on the lattice with self and other, and stores the result in self.

See the copying counterpart at Abstract::meet_copy.

Examples found in repository?
examples/bottom_free.rs (line 12)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    std::mem::drop(Abstract::bottom(&man, &env));
9    println!("after ::bottom free");
10
11    let mut top = Abstract::top(&man, &env);
12    top.meet(&man, &Abstract::bottom(&man, &env));
13    println!("after created bottom");
14    std::mem::drop(top);
15    println!("after created bottom free");
16}
More examples
Hide additional examples
examples/showcase.rs (line 29)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn meet_copy<M: Manager, MT: Meetable + ?Sized>( &self, man: &M, other: &MT, ) -> Abstract

Returns the result of the meet operation on the lattice with self and other.

See the mutating counterpart at Abstract::meet.

Examples found in repository?
examples/showcase.rs (line 21)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn join<M: Manager, JT: Joinable + ?Sized>(&mut self, man: &M, other: &JT)

Performs the join operation on the lattice with self and other, and stores the result in self.

See the copying counterpart at Abstract::join_copy.

Examples found in repository?
examples/showcase.rs (line 125)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn join_copy<M: Manager, JT: Joinable + ?Sized>( &self, man: &M, other: &JT, ) -> Abstract

Returns the result of the join operation on the lattice with self and other.

See the mutating counterpart at Abstract::join.

Examples found in repository?
examples/showcase.rs (line 77)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn assign<M: Manager, S: Borrow<str>>( &mut self, man: &M, env: &Environment, var: S, texpr: &Texpr, )

Assigns var to texpr in self.

This function can be used to model mutable variables.

See the copying counterpart at Abstract::assign_copy.

Examples found in repository?
examples/showcase.rs (line 90)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn assign_copy<M, S>( &self, man: &M, env: &Environment, var: S, texpr: &Texpr, ) -> Abstract
where M: Manager, S: Borrow<str>,

Returns a new Abstract representing self after var has been assigned texpr.

This function can be used to model mutable variables.

See the mutating counterpart at Abstract::assign.

Examples found in repository?
examples/showcase.rs (line 37)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn assign_dim<M: Manager>(&mut self, man: &M, dim: u32, texpr: &Texpr)

Assigns dimension dim to texpr in self.

This function can be used to model mutable variables.

See the copying counterpart at Abstract::assign_copy_dim.

Examples found in repository?
examples/showcase.rs (line 112)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn assign_copy_dim<M: Manager>( &self, man: &M, dim: u32, texpr: &Texpr, ) -> Abstract

Returns a new Abstract representing self after dimension dim has been assigned texpr.

This function can be used to model mutable variables.

See the mutating counterpart at Abstract::assign_dim.

Source

pub fn widen_copy<M: Manager>(&self, man: &M, other: &Abstract) -> Abstract

Returns a new Abstract representing self widened with other.

Specifically, this function applies the widening operator to self and (self JOIN other).

Examples found in repository?
examples/showcase.rs (line 99)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn add_dims<M: Manager>(&mut self, man: &M, dim: u32, n: usize)

Adds n dimensions after dimension dim to self.

Examples found in repository?
examples/showcase.rs (line 111)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn add_dims_copy<M: Manager>(&self, man: &M, dim: u32, n: usize) -> Abstract

Returns a new Abstract representing self after n dimensions have been added after dimension dim.

Source

pub fn is_top<M: Manager>(&self, man: &M) -> bool

Returns true if self is Top.

Source

pub fn is_bottom<M: Manager>(&self, man: &M) -> bool

Returns true if self is Bottom.

Source

pub fn get_bounds_texpr<M: Manager>(&self, man: &M, texpr: &Texpr) -> Interval

Returns the bounds of the Texpr in self.

Examples found in repository?
examples/showcase.rs (line 114)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn get_bounds_dim<M: Manager>(&self, man: &M, dim: u32) -> Interval

Returns the bounds of dimension dim in self.

Examples found in repository?
examples/showcase.rs (line 113)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn get_bounds<M, S>(&self, man: &M, env: &Environment, var: S) -> Interval
where M: Manager, S: Borrow<str>,

Returns the bounds of variable var in self.

Examples found in repository?
examples/showcase.rs (line 54)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn to_string<M: Manager>(&self, man: &M, env: &Environment) -> String

Returns a String representation of self.

Examples found in repository?
examples/showcase.rs (line 40)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}
Source

pub fn print<M: Manager>(&self, man: &M, env: &Environment)

Prints self to stdout.

Examples found in repository?
examples/showcase.rs (line 17)
4fn main() {
5    let env = Environment::new(vec!["x", "y", "z", "i"]);
6    let man = OptPkManager::default();
7
8    let x = Texpr::var(&env, "x");
9    let y = Texpr::var(&env, "y");
10    let z = Texpr::var(&env, "z");
11
12    let upper = x.clone().lt(Texpr::int(20));
13    let lower = x.clone().ge(Texpr::int(-10));
14
15    let top = Abstract::top(&man, &env);
16    println!("top:");
17    top.print(&man, &env);
18    println!("top satisfies x < 20: {}", top.satisfy(&man, &upper));
19    println!();
20
21    let mut meet = top.meet_copy(&man, &[&upper, &lower]);
22    println!("meet:");
23    meet.print(&man, &env);
24    println!("meet satisfies x < 20: {}", meet.satisfy(&man, &upper));
25    // println!("meet satisfies x2 < 400: {}", meet.satisfy(&man, &(x.clone() * x.clone()).lt(Texpr::int(400))));
26    println!();
27
28    let inter = y.clone().lt(x.clone());
29    meet.meet(&man, &inter);
30    println!("meet with `inter` constraint:");
31    meet.print(&man, &env);
32    println!("meet satisfies y < 20: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(20))));
33    println!("meet satisfies y < 19: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(19))));
34    println!("meet satisfies y < 18: {}", meet.satisfy(&man, &y.clone().lt(Texpr::int(18))));
35    println!();
36
37    let meet_assn = meet.assign_copy(&man, &env, "z", &(y.clone() + Texpr::int(2)));
38    println!("meet_assn (z = y + 2):");
39    meet_assn.print(&man, &env);
40    println!("meet_assn string: {}", meet_assn.to_string(&man, &env));
41    println!("meet_assn satisfies z < 21: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(21))));
42    println!("meet_assn satisfies z < 20: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(20))));
43    println!("meet_assn satisfies z < 19: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(19))));
44    println!("meet_assn satisfies z < 18: {}", meet_assn.satisfy(&man, &z.clone().lt(Texpr::int(18))));
45
46    // meeting meet_assn with x < Texpr::top should change nothing
47    let meet_assn2 = meet_assn.meet_copy(&man, &x.clone().lt(Texpr::top()));
48    println!("meet_assn (with x < top): {}", meet_assn2.to_string(&man, &env));
49
50    // neither should Hcons::top
51    println!("meet_assn (meet with  top): {}", meet_assn.meet_copy(&man, &Hcons::Top).to_string(&man, &env));
52    println!("meet_assn (meet with !top): {}", meet_assn.meet_copy(&man, &Hcons::Top.not()).to_string(&man, &env));
53
54    let x_bounds = meet_assn.get_bounds(&man, &env, "x");
55    println!("x's bounds: {:?}", x_bounds);
56
57
58
59    
60
61    let x_gt_10 = Texpr::var(&env, "x").gt(Texpr::int(10));
62    let x_lt_0 = Texpr::var(&env, "x").lt(Texpr::int(0));
63
64    let top = Abstract::top(&man, &env);
65
66    let hc_unsat = x_gt_10.clone().into_hcons().and(x_lt_0.clone().into());
67    println!("Prev meet");
68    let hc_unsat_meet = top.meet_copy(&man, &hc_unsat);
69    println!("hc_unsat_meet:");
70    hc_unsat_meet.print(&man, &env);
71
72    let hc_or = hc_unsat.or(x.clone().lt(Texpr::int(1)).into());
73    let hc_or_meet = top.meet_copy(&man, &hc_or);
74    println!("hc_or_meet:");
75    hc_or_meet.print(&man, &env);
76
77    let hc_or_meet_joined = hc_or_meet.join_copy(&man, &meet_assn);
78    println!("hc_or_meet_joined:");
79    hc_or_meet_joined.print(&man, &env);
80
81    let hc_or_meet_joined_string = hc_or_meet_joined.to_string(&man, &env);
82    println!("hc_or_meet_joined string: {}", hc_or_meet_joined_string);
83
84    // Widen stuff
85    let x = x;
86    let i = Texpr::var(&env, "i");
87    let i_lt_x: Hcons = i.clone().lt(x.clone()).into();
88
89    let mut top = Abstract::top(&man, &env);
90    top.assign(&man, &env, "i", &y);
91    top.meet(&man, &i_lt_x);
92
93    let i0 = top.clone();
94    top.assign(&man, &env, "i", &Texpr::int(1).add(y.clone()));
95    top.meet(&man, &i_lt_x);
96    let i1 = top.clone();
97    println!("i0: {}", i0.to_string(&man, &env));
98    println!("i1: {}", i1.to_string(&man, &env));
99    println!("i0 widen i1: {}", (i0.widen_copy(&man, &i1)).to_string(&man, &env));
100
101
102    let mut state = Abstract::top(&man, &env);
103    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
104    state.meet(&man, &(y.clone() + x.clone()).lt(Texpr::int(9)));
105    println!("3x < 9: {}", state.to_string(&man, &env));
106    println!("x bounds: {:?}", state.get_bounds(&man, &env, "x"));
107
108    let mut state = Abstract::top(&man, &env);
109    state.assign(&man, &env, "y", &Texpr::int(2).mul(x.clone()));
110    println!("y = 2x: {}", state.to_string(&man, &env));
111    state.add_dims(&man, 3, 1);
112    state.assign_dim(&man, 4, &Texpr::int(5));
113    println!("bounds of new state: {:?}", state.get_bounds_dim(&man, 4));
114    println!("bounds of new state: {:?}", state.get_bounds_texpr(&man, &Texpr::int(100)));
115
116    // Testing segfault
117    // When one joins BOTTOM with something, where BOTTOM was obtained with unsat meet, segfault happens.
118    // Segfault does not happen when Bottom is obtained with ::bottom()
119    let mut state = hc_or_meet_joined.clone();
120    let mut bot = state.clone();
121    // let mut bot = Abstract::bottom(&man, &env);
122    println!("bottom = state MEET false");
123    bot.meet(&man, &Texpr::int(1).lt(Texpr::int(0)));
124    println!("bottom JOIN state");
125    bot.join(&man, &state);
126    println!("{}", bot.to_string(&man, &env));
127    // 'Testing' memory leaks
128
129    // let mut meet_assn = meet_assn.clone();
130    // let mut i = 0;
131    // loop {
132    //     i += 1;
133    //
134    //     meet_assn.meet(&man, &[&upper, &lower]);
135    //     if i % 10000 == 0 {
136    //         println!("iter: {}", i);
137    //         meet_assn.print(&man, &env);
138    //     }
139    // }
140}

Trait Implementations§

Source§

impl Clone for Abstract

Source§

fn clone(&self) -> Self

Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl Drop for Abstract

Source§

fn drop(&mut self)

Executes the destructor for this type. Read more
Source§

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)
Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned. Read more
Source§

impl Eq for Abstract

Source§

impl Joinable for Abstract

Source§

unsafe fn join_internal<M: Manager>( &self, man: &M, other: *mut elina_abstract0_t, destructive: bool, ) -> *mut elina_abstract0_t

Returns a pointer to the internal join result of self with other. Read more
Source§

fn join_with<M: Manager>(&self, man: &M, other: &mut Abstract)

Source§

fn join_with_copy<M: Manager>(&self, man: &M, other: &Abstract) -> Abstract

Source§

impl Meetable for Abstract

Source§

unsafe fn meet_internal<M: Manager>( &self, man: &M, other: *mut elina_abstract0_t, destructive: bool, ) -> *mut elina_abstract0_t

Returns a pointer to the internal meet result of self with other. Read more
Source§

fn meet_with<M: Manager>(&self, man: &M, other: &mut Abstract)

Source§

fn meet_with_copy<M: Manager>(&self, man: &M, other: &Abstract) -> Abstract

Source§

impl PartialEq for Abstract

Source§

fn eq(&self, other: &Self) -> bool

Equality operator ==. Read more
1.0.0 (const: unstable) · Source§

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=. Read more

Auto Trait Implementations§

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.