1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
use super::super::node::NodeType::*;
use crate::Ddnnf;
use num::{BigInt, One, Zero};
impl Ddnnf {
#[inline]
// Computes the cardinality of a node according to the rules mentioned at the Nodetypes and saves it in tmp
pub(crate) fn calc_count(&mut self, i: usize) {
match &self.nodes[i].ntype {
And { children } => {
self.nodes[i].temp = children
.iter()
.map(|&indice| &self.nodes[indice].temp)
.product()
}
Or { children } => {
self.nodes[i].temp = children
.iter()
.map(|&indice| &self.nodes[indice].temp)
.sum()
}
False => self.nodes[i].temp.set_zero(),
_ => self.nodes[i].temp.set_one(), // True and Literal
}
}
#[inline]
/// Computes the cardinality of a feature according
/// to the rules mentioned at the Nodetypes and returns the result.
/// The function does not use the marking approach.
/// This function trys to apply optimisations based on core and dead features.
fn _operate_on_single_feature(
&mut self,
feature: i32,
operation: fn(&mut Ddnnf, usize),
) -> BigInt {
if self.has_no_effect_on_query(&feature) {
self.rc()
} else if self.makes_query_unsat(&feature) {
BigInt::ZERO
} else {
for i in 0..self.nodes.len() {
match &mut self.nodes[i].ntype {
// search for the node we want to adjust
Literal { literal } => {
if feature == -*literal {
self.nodes[i].temp.set_zero();
} else {
operation(self, i)
}
}
// all other values stay the same, respectevly get adjusted because the count of the one node got changed
_ => operation(self, i),
}
}
self.rt()
}
}
#[inline]
/// Computes the cardinality of a partial configuration
/// according to the rules mentioned at the Nodetypes and returns the result.
/// The function does not use the marking approach.
/// This function trys to apply optimisations based on core and dead features.
pub(crate) fn operate_on_partial_config_default(
&mut self,
features: &[i32],
operation: fn(&mut Ddnnf, usize),
) -> BigInt {
if self.query_is_not_sat(features) {
BigInt::ZERO
} else {
let features: Vec<i32> = self.reduce_query(features);
for i in 0..self.nodes.len() {
match &self.nodes[i].ntype {
// search for the nodes we want to adjust
Literal { literal } => {
if features.contains(&-literal) {
self.nodes[i].temp.set_zero();
} else {
operation(self, i)
}
}
_ => operation(self, i),
}
}
self.rt()
}
}
}
#[cfg(test)]
mod test {
use crate::parser::build_ddnnf;
use std::path::Path;
use super::*;
#[test]
fn operate_on_single_feature() {
let mut vp9: Ddnnf = build_ddnnf(Path::new("tests/data/VP9_d4.nnf"), Some(42));
let mut auto1: Ddnnf = build_ddnnf(Path::new("tests/data/auto1_d4.nnf"), Some(2513));
for i in 1..=vp9.number_of_variables as i32 {
assert_eq!(
vp9.card_of_feature_with_marker(i),
vp9._operate_on_single_feature(i, Ddnnf::calc_count)
);
assert_eq!(
vp9.card_of_feature_with_marker(-i),
vp9._operate_on_single_feature(-i, Ddnnf::calc_count)
);
}
for i in (1..=auto1.number_of_variables as i32).step_by(100) {
assert_eq!(
auto1.card_of_feature_with_marker(i),
auto1._operate_on_single_feature(i, Ddnnf::calc_count)
);
assert_eq!(
auto1.card_of_feature_with_marker(-i),
auto1._operate_on_single_feature(-i, Ddnnf::calc_count)
);
}
}
}