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
//! d-DNNF compilation substrate consumer (P-PRIM-6).
//!
//! Wires `vyre_primitives::dnnf::compile_dnnf` and `model_count`
//! into the dispatch path so the pass scheduler can compile each
//! pass-precondition CNF to a d-DNNF DAG once at startup, then
//! evaluate it in linear time per Program at dispatch time.
//!
//! The substrate exposes the compile + count steps as separate
//! entry points so callers that only need the SAT-style decision
//! can skip the (potentially saturating) model count.
use vyre_primitives::dnnf::{
compile_dnnf as primitive_compile, model_count as primitive_count, DnnfDag,
};
/// Compile a CNF formula to a d-DNNF DAG. Bumps the
/// dataflow-fixpoint substrate counter so observability dashboards
/// register every compilation event.
#[must_use]
pub fn compile_precondition(
clauses: &[Vec<(u32, bool)>],
num_vars: u32,
max_depth: u32,
) -> DnnfDag {
use crate::observability::{bump, dataflow_fixpoint_calls};
bump(&dataflow_fixpoint_calls);
primitive_compile(clauses, num_vars, max_depth)
}
/// Count satisfying assignments of a previously-compiled d-DNNF
/// DAG. Linear in the gate count; saturating at u64::MAX.
#[must_use]
pub fn count_models(dag: &DnnfDag) -> u64 {
use crate::observability::{bump, dataflow_fixpoint_calls};
bump(&dataflow_fixpoint_calls);
primitive_count(dag)
}
/// Convenience: returns true iff the formula is satisfiable
/// (model_count > 0). The pass scheduler uses this as a fast
/// "would this pass ever be applicable?" check during pre-flight.
#[must_use]
pub fn is_satisfiable(dag: &DnnfDag) -> bool {
count_models(dag) > 0
}
/// Convenience: returns true iff the formula is a tautology over
/// `num_vars` (model count == 2^num_vars).
#[must_use]
pub fn is_tautology(dag: &DnnfDag, num_vars: u32) -> bool {
if num_vars >= 64 {
return false; // 2^64 saturates; conservative reject.
}
count_models(dag) == 1u64 << num_vars
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn empty_formula_is_tautology() {
let dag = compile_precondition(&[], 3, 4);
assert!(is_tautology(&dag, 3));
assert!(is_satisfiable(&dag));
}
#[test]
fn contradiction_is_unsatisfiable() {
let clauses = vec![vec![(0u32, true)], vec![(0, false)]];
let dag = compile_precondition(&clauses, 1, 4);
assert!(!is_satisfiable(&dag));
assert!(!is_tautology(&dag, 1));
}
#[test]
fn single_literal_satisfiable_not_tautology() {
let dag = compile_precondition(&[vec![(0u32, true)]], 2, 4);
assert!(is_satisfiable(&dag));
assert!(!is_tautology(&dag, 2));
// (x0) over 2 vars: x1 free → 2 models.
assert_eq!(count_models(&dag), 2);
}
/// Closure-bar: substrate output equals primitive output exactly.
#[test]
fn matches_primitive_directly() {
let clauses = vec![vec![(0u32, true), (1, false)], vec![(1, true), (2, true)]];
let via_substrate = compile_precondition(&clauses, 3, 8);
let via_primitive = primitive_compile(&clauses, 3, 8);
assert_eq!(via_substrate, via_primitive);
assert_eq!(
count_models(&via_substrate),
primitive_count(&via_primitive)
);
}
/// Adversarial: max_depth budget terminates even on a wide
/// formula that would otherwise diverge.
#[test]
fn depth_budget_terminates() {
let clauses = vec![vec![(0u32, true), (1, true)], vec![(2, true), (3, true)]];
let dag = compile_precondition(&clauses, 4, 1);
// No assertion on the count — only that compile + count
// both terminate (via the saturating arithmetic + depth
// budget contract).
let _ = count_models(&dag);
}
/// Adversarial: tautology check is conservative for num_vars >= 64.
#[test]
fn tautology_conservative_at_64_vars() {
let dag = compile_precondition(&[], 64, 4);
// 2^64 saturates u64::MAX which is != 2^64; we conservatively
// reject here.
assert!(!is_tautology(&dag, 64));
}
}