1 unstable release
0.1.0 | Jan 26, 2023 |
---|
#1103 in Algorithms
Used in fgr-rs
54KB
1.5K
SLoC
nnf
Negation Normal Form manipulation library
Macro & bit operations
fn sample() {
let a = Nnf::Var("a", true);
let b = var!("b", false);
let or = or!(a.clone(), b.clone());
}
Simple operations optimization
assert_eq!(and!("a") & and!("b"), and!("a", "b"));
assert_eq!(and!("a") | and!("b"), or!("a", "b"));
Tseitin Transform (NNF -> CNF)
fn transform(sentence: Nnf<&'static str>) -> Nnf<&'static str> {
let mut counter = 0;
let transformer = TseitinTransform::new(|_| {
let name: &'static str = Box::leak(Box::new(format!("aux_{}", counter)));
counter += 1;
var!(name)
});
transformer.transform(sentence)
}
fn test() {
let sentence = or!(
and!(
var!("a"),
and!("b", "c")
),
and!(
or!("!d", "e"),
and!("f", "!g")
)
);
assert!(!sentence.is_cnf(), "Expression is not a cnf yet");
let sentence = transform(sentence);
assert!(sentence.is_cnf(), "Expression must be in the cnf form after transformation");
assert_eq!(
sentence,
and!(
or!("a", "!aux_1"),
or!("aux_0", "!aux_1"),
or!("aux_1", "aux_4"),
or!("aux_2", "!aux_4"),
or!("aux_3", "!aux_4"),
or!("!aux_0", "b"),
or!("!aux_0", "c"),
or!("aux_3", "d"),
or!("aux_3", "!e"),
or!("!aux_2", "f"),
or!("!aux_2", "!g"),
or!("!a", "!aux_0", "aux_1"),
or!("!aux_2", "!aux_3", "aux_4"),
or!("aux_0", "!b", "!c"),
or!("!aux_3", "!d", "e"),
or!("aux_2", "!f", "g")
)
);
}
Parse Tree
Macro support
fn test() {
let root = ExpressionNode::Not(
ExpressionNode::And(
ExpressionNode::Or(
ExpressionNode::Leaf(1).into(),
ExpressionNode::Leaf(2).into(),
).into(),
ExpressionNode::And(
ExpressionNode::Leaf(3).into(),
ExpressionNode::Leaf(4).into(),
).into(),
).into());
let root = e_not!(
e_and!(
e_or!(
e_leaf!(1),
e_leaf!(2)
),
e_and!(
e_leaf!(3),
e_leaf!(4)
)
)
);
}
Expression Tree to NNF conversion (De Morgan's Law, double negation, etc.)
assert_eq!(
e_not!(e_leaf!(true) & e_leaf!(true)).to_nnf(),
e_or!(e_leaf!(false), e_leaf!(false))
);
assert_eq!(
e_not!(e_leaf!(true) | e_leaf!(true)).to_nnf(),
e_and!(e_leaf!(false), e_leaf!(false))
);
assert_eq!(
!ExpressionNode::Not(e_or!(e_leaf!(true), e_leaf!(true)).into()),
e_or!(e_leaf!(true), e_leaf!(true))
);
(Optional) Render / Graphviz
fn test() {
let sentence = or!(
and!(
var!("a"),
and!("b", "c")
),
and!(
or!("!d", "e"),
and!("f", "!g")
)
);
assert!(!sentence.render().is_empty());
}