1use std::borrow::Cow;
2use std::collections::HashSet;
3use std::fmt;
4use std::io::{self, Write};
5
6use fixedbitset::FixedBitSet;
7
8use oxidd_core::function::{Function, INodeOfFunc, TermOfFunc};
9use oxidd_core::util::{Borrowed, EdgeHashMap, EdgeVecDropGuard};
10use oxidd_core::{Edge, HasLevel, InnerNode, LevelNo, Manager, Node};
11
12use crate::AsciiDisplay;
13
14use super::{Code, VarInfo};
15
16type FxBuildHasher = std::hash::BuildHasherDefault<rustc_hash::FxHasher>;
21
22#[inline]
23fn is_complemented<E: Edge>(edge: &E) -> bool {
24 edge.tag() != Default::default()
25}
26
27#[derive(
29 Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default, oxidd_derive::Countable, Debug,
30)]
31#[repr(u8)]
32#[non_exhaustive]
33pub enum DDDMPVersion {
34 #[default]
38 V2_0,
39 V3_0,
44}
45
46impl fmt::Display for DDDMPVersion {
47 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
48 f.write_str(match self {
49 DDDMPVersion::V2_0 => "DDDMP-2.0",
50 DDDMPVersion::V3_0 => "DDDMP-3.0",
51 })
52 }
53}
54
55#[derive(Clone, Copy, Debug)]
57pub struct ExportSettings<'a> {
58 version: DDDMPVersion,
59 ascii: bool,
60 strict: bool,
61 diagram_name: &'a str,
62}
63
64impl Default for ExportSettings<'_> {
65 fn default() -> Self {
66 Self {
67 version: DDDMPVersion::default(),
68 ascii: false,
69 strict: true,
70 diagram_name: "",
71 }
72 }
73}
74
75impl<'a> ExportSettings<'a> {
76 #[inline(always)]
78 pub fn version(mut self, version: DDDMPVersion) -> Self {
79 self.version = version;
80 self
81 }
82 #[inline(always)]
84 pub fn get_version(&self) -> DDDMPVersion {
85 self.version
86 }
87
88 #[inline(always)]
91 pub fn binary_supported<M: Manager>(manager: &M) -> bool {
92 M::InnerNode::ARITY == 2 && manager.num_terminals() == 1
95 }
96 #[inline(always)]
101 pub fn ascii(mut self) -> Self {
102 self.ascii = true;
103 self
104 }
105 #[inline(always)]
108 pub fn binary(mut self) -> Self {
109 self.ascii = false;
110 self
111 }
112 #[inline(always)]
115 pub fn is_ascii(&self) -> bool {
116 self.ascii
117 }
118
119 #[inline(always)]
126 pub fn diagram_name(mut self, name: &'a str) -> Self {
127 self.diagram_name = name;
128 self
129 }
130 #[inline(always)]
132 pub fn get_diagram_name(&self) -> &'a str {
133 self.diagram_name
134 }
135
136 #[inline(always)]
163 pub fn strict(mut self, strict: bool) -> Self {
164 self.strict = strict;
165 self
166 }
167 #[inline(always)]
169 pub fn is_strict(&self) -> bool {
170 self.strict
171 }
172
173 pub fn export<'id, FR: std::ops::Deref>(
210 &self,
211 file: impl io::Write,
212 manager: &<FR::Target as Function>::Manager<'id>,
213 functions: impl IntoIterator<Item = FR>,
214 ) -> io::Result<()>
215 where
216 FR::Target: Function,
217 INodeOfFunc<'id, FR::Target>: HasLevel,
218 TermOfFunc<'id, FR::Target>: AsciiDisplay,
219 {
220 let iter = functions.into_iter();
221 let mut roots = EdgeVecDropGuard::new(manager, Vec::with_capacity(iter.size_hint().0));
222 roots.extend(iter.map(|f| manager.clone_edge(f.as_edge(manager))));
223
224 export_common(file, self, manager, &roots, None)
225 }
226
227 pub fn export_with_names<'id, FR: std::ops::Deref, D: fmt::Display>(
269 &self,
270 file: impl io::Write,
271 manager: &<FR::Target as Function>::Manager<'id>,
272 functions: impl IntoIterator<Item = (FR, D)>,
273 ) -> io::Result<()>
274 where
275 FR::Target: Function,
276 INodeOfFunc<'id, FR::Target>: HasLevel,
277 TermOfFunc<'id, FR::Target>: AsciiDisplay,
278 {
279 let iter = functions.into_iter();
280 let mut roots = EdgeVecDropGuard::new(manager, Vec::with_capacity(iter.size_hint().0));
281 let mut root_names = Vec::<u8>::with_capacity(1024);
282
283 let mut res = Ok(());
284
285 for (i, (func, name)) in iter.enumerate() {
286 roots.push(manager.clone_edge(func.as_edge(manager)));
287
288 root_names.push(b' ');
289 let len_before = root_names.len();
290 write!(&mut root_names, "{name}")?;
291
292 let name_bytes = &mut root_names[len_before..];
293 if name_bytes.is_empty() {
294 write!(&mut root_names, "_f{i}")?;
295 if self.strict && res.is_ok() {
296 res = Err(io::Error::new(
297 io::ErrorKind::InvalidInput,
298 "function names must not be empty",
299 ));
300 }
301 continue;
302 }
303
304 for c in name_bytes {
305 if c.is_ascii_control() || *c == b' ' {
306 *c = b'_';
307 if self.strict && res.is_ok() {
308 res = Err(io::Error::new(
309 io::ErrorKind::InvalidInput,
310 "function names must not contain control characters or spaces",
311 ));
312 }
313 }
314 }
315 }
316
317 export_common(file, self, manager, &roots, Some(&root_names))?;
318 res
319 }
320}
321
322fn export_common<M: Manager, W: io::Write>(
323 mut file: W,
324 settings: &ExportSettings,
325 manager: &M,
326 roots: &[M::Edge],
327 root_names: Option<&[u8]>,
328) -> io::Result<()>
329where
330 M::InnerNode: HasLevel,
331 M::Terminal: crate::AsciiDisplay,
332{
333 writeln!(file, ".ver {}", settings.version)?;
334 let ascii = settings.ascii || !ExportSettings::binary_supported(manager);
335 writeln!(file, ".mode {}", if ascii { 'A' } else { 'B' })?;
336
337 writeln!(file, ".varinfo {}", VarInfo::None as u32)?;
339
340 let mut res = Ok(());
341
342 if !settings.diagram_name.is_empty() {
343 write!(file, ".dd ")?;
344 if write_replacing_control(&mut file, settings.diagram_name)? && settings.strict {
345 res = Err(io::Error::new(
346 io::ErrorKind::InvalidInput,
347 "decision diagram name must not contain control characters",
348 ));
349 }
350 writeln!(file)?;
351 }
352
353 let nvars = manager.num_levels();
354
355 let mut node_map: Vec<(LevelNo, _)> =
360 (0..nvars).map(|_| (0, EdgeHashMap::new(manager))).collect();
361 let mut terminal_map = EdgeHashMap::new(manager);
362
363 fn rec_add_map<M: Manager>(
364 manager: &M,
365 node_map: &mut Vec<(u32, EdgeHashMap<M, usize, FxBuildHasher>)>,
366 terminal_map: &mut EdgeHashMap<M, usize, FxBuildHasher>,
367 e: Borrowed<M::Edge>,
368 ) where
369 M::InnerNode: HasLevel,
370 {
371 match manager.get_node(&e) {
372 Node::Inner(node) => {
373 let (_, map) = &mut node_map[node.level() as usize];
374 let res = map.insert(&e.with_tag(Default::default()), 0);
376 if res.is_none() {
377 for e in node.children() {
378 rec_add_map::<M>(manager, node_map, terminal_map, e);
379 }
380 }
381 }
382 Node::Terminal(_) => {
383 terminal_map.insert(&e.with_tag(Default::default()), 0);
384 }
385 }
386 }
387
388 for root in roots.iter() {
389 rec_add_map(manager, &mut node_map, &mut terminal_map, root.borrowed());
390 }
391
392 let mut nnodes = 0;
393 for (_, idx) in &mut terminal_map {
394 nnodes += 1; *idx = nnodes;
396 }
397 let nsuppvars = node_map.iter().filter(|(_, m)| !m.is_empty()).count() as u32;
398 let mut supp_levels = FixedBitSet::with_capacity(nvars as usize);
399 let mut suppvar_idx = nsuppvars;
400 for (i, (var_idx, level)) in node_map.iter_mut().enumerate().rev() {
402 if level.is_empty() {
403 continue;
404 }
405 suppvar_idx -= 1;
406 *var_idx = suppvar_idx;
407 supp_levels.insert(i);
408 for (_, idx) in level.iter_mut() {
409 nnodes += 1; *idx = nnodes;
411 }
412 }
413 writeln!(file, ".nnodes {nnodes}")?;
414 writeln!(file, ".nvars {nvars}")?;
415 writeln!(file, ".nsuppvars {nsuppvars}")?;
416
417 if manager.num_named_vars() == nvars || (!settings.strict && manager.num_named_vars() != 0) {
418 let mut leading_underscores = 1;
419 let mut replaced = 0usize;
420 let var_names: Vec<Cow<str>> = Vec::from_iter((0..nvars).map(|i| {
421 let name = replace_space_and_control(manager.var_name(i));
422 if let Cow::Owned(_) = &name {
423 replaced += 1;
424 }
425 for (i, b) in name.bytes().enumerate() {
426 if b != b'_' {
427 break;
428 }
429 leading_underscores = i + 2;
430 }
431 name
432 }));
433
434 let mut prefix_all_owned = false;
435 if replaced != 0 {
436 let mut replaced_set: HashSet<&str, FxBuildHasher> =
437 HashSet::with_capacity_and_hasher(replaced, FxBuildHasher::default());
438 for name in var_names.iter() {
439 if let Cow::Owned(name) = &name {
440 if manager.name_to_var(name).is_some() || !replaced_set.insert(name) {
441 prefix_all_owned = true;
442 break;
443 }
444 }
445 }
446
447 if settings.strict && res.is_ok() {
448 res = Err(io::Error::new(
449 io::ErrorKind::InvalidInput,
450 "variable names must not contain control characters or spaces",
451 ));
452 }
453 }
454
455 let write_var = |file: &mut W, i: usize| match &var_names[i] {
456 Cow::Borrowed("") => write!(file, " {:_<leading_underscores$}x{i}", ""),
457 Cow::Borrowed(name) => write!(file, " {name}"),
458 Cow::Owned(name) if !prefix_all_owned => write!(file, " {name}"),
459 Cow::Owned(name) => write!(file, " {:_<leading_underscores$}x{i}_{name}", ""),
460 };
461
462 if let DDDMPVersion::V3_0 = settings.version {
463 write!(file, ".varnames")?;
464 for var in 0..nvars {
465 write_var(&mut file, var as usize)?;
466 }
467 writeln!(file)?;
468 }
469
470 write!(file, ".suppvarnames")?;
471 for var in 0..nvars {
472 if supp_levels.contains(manager.var_to_level(var) as usize) {
473 write_var(&mut file, var as usize)?;
474 }
475 }
476 writeln!(file)?;
477
478 write!(file, ".orderedvarnames")?;
479 for level in 0..nvars {
480 write_var(&mut file, manager.level_to_var(level) as usize)?;
481 }
482 writeln!(file)?;
483 }
484
485 write!(file, ".ids")?;
486 for id in 0..nvars {
487 if supp_levels.contains(manager.var_to_level(id) as usize) {
488 write!(file, " {id}")?;
489 }
490 }
491 writeln!(file)?;
492
493 write!(file, ".permids")?;
494 for var in 0..nvars {
495 let level = manager.var_to_level(var);
496 if supp_levels.contains(level as usize) {
497 write!(file, " {level}")?;
498 }
499 }
500 writeln!(file)?;
501
502 let idx = |e: &M::Edge| {
505 let idx = match manager.get_node(e) {
506 Node::Inner(node) => {
507 let (_, map) = &node_map[node.level() as usize];
508 *map.get(&e.with_tag(Default::default())).unwrap() as isize
509 }
510 Node::Terminal(_) => {
511 *terminal_map.get(&e.with_tag(Default::default())).unwrap() as isize
512 }
513 };
514 if is_complemented(e) {
515 -idx
516 } else {
517 idx
518 }
519 };
520 let bin_idx = |e: &M::Edge, node_id: usize| {
521 let idx = match manager.get_node(e) {
522 Node::Inner(node) => {
523 let (_, map) = &node_map[node.level() as usize];
524 *map.get(&e.with_tag(Default::default())).unwrap()
525 }
526 Node::Terminal(_) => return (Code::Terminal, 0),
528 };
529 if idx == node_id - 1 {
530 (Code::Relative1, 0)
531 } else if node_id - idx < idx {
532 (Code::RelativeID, node_id - idx)
533 } else {
534 (Code::AbsoluteID, idx)
535 }
536 };
537
538 writeln!(file, ".nroots {}", roots.len())?;
539 write!(file, ".rootids")?;
540 for root in roots {
541 write!(file, " {}", idx(root))?;
542 }
543 writeln!(file)?;
544 if let Some(root_names) = root_names {
545 write!(file, ".rootnames")?;
546 file.write_all(root_names)?;
547 writeln!(file)?;
548 }
549
550 writeln!(file, ".nodes")?;
551
552 #[inline]
553 const fn node_code(var: Code, t: Code, e_complement: bool, e: Code) -> u8 {
554 ((var as u8) << 5) | ((t as u8) << 3) | ((e_complement as u8) << 2) | e as u8
555 }
556
557 let mut exported_nodes = 0;
558 for (edge, &node_id) in terminal_map.iter() {
559 assert_eq!(exported_nodes + 1, node_id);
563 if ascii {
564 let node = manager.get_node(edge);
567 let desc = Ascii(node.unwrap_terminal());
568 writeln!(file, "{node_id} {desc} 0 0")?;
569 } else {
570 let terminal = node_code(Code::Terminal, Code::Terminal, false, Code::Terminal);
571 write_escaped(&mut file, &[terminal])?;
572 }
573 exported_nodes += 1;
574 }
575 for &(var_idx, ref level) in node_map.iter().rev() {
577 for (e, &node_id) in level.iter() {
578 assert_eq!(exported_nodes + 1, node_id);
579 let node = manager.get_node(e).unwrap_inner();
580 if ascii {
581 write!(file, "{node_id} {var_idx}")?;
584 for child in node.children() {
585 write!(file, " {}", idx(&child))?;
586 }
587 writeln!(file)?;
588 } else {
589 let mut iter = node.children();
590 let t = iter.next().unwrap();
591 let t_lvl = manager.get_node(&t).level();
592 let e = iter.next().unwrap();
593 let e_lvl = manager.get_node(&e).level();
594 debug_assert!(iter.next().is_none());
595
596 let mut var_code = Code::AbsoluteID;
597 let mut var_idx = var_idx;
598 let min_lvl = std::cmp::min(t_lvl, e_lvl);
599 if min_lvl != LevelNo::MAX {
600 let (min_var_idx, _) = node_map[min_lvl as usize];
601 if var_idx == min_var_idx - 1 {
602 var_code = Code::Relative1;
603 } else if min_var_idx - var_idx < var_idx {
604 var_code = Code::RelativeID;
605 var_idx = min_var_idx - var_idx;
606 }
607 }
608
609 let (t_code, t_idx) = bin_idx(&t, node_id);
610 let (e_code, e_idx) = bin_idx(&e, node_id);
611
612 debug_assert!(!is_complemented(&*t));
613 write_escaped(
614 &mut file,
615 &[node_code(var_code, t_code, is_complemented(&*e), e_code)],
616 )?;
617 if var_code == Code::AbsoluteID || var_code == Code::RelativeID {
618 encode_7bit(&mut file, var_idx as usize)?;
619 }
620 if t_code == Code::AbsoluteID || t_code == Code::RelativeID {
621 encode_7bit(&mut file, t_idx)?;
622 }
623 if e_code == Code::AbsoluteID || e_code == Code::RelativeID {
624 encode_7bit(&mut file, e_idx)?;
625 }
626 }
627 exported_nodes += 1;
628 }
629 }
630
631 writeln!(file, ".end")?;
632
633 res
634}
635
636struct Ascii<T>(T);
637impl<T: crate::AsciiDisplay> fmt::Display for Ascii<&T> {
638 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
639 self.0.fmt(f)
640 }
641}
642
643fn write_replacing_control(mut writer: impl io::Write, string: &str) -> io::Result<bool> {
645 let mut bytes = string.as_bytes();
646 let mut did_replace = false;
647 'outer: loop {
648 for (i, &b) in bytes.iter().enumerate() {
649 if b.is_ascii_control() {
650 did_replace = true;
651 writer.write_all(&bytes[..i])?;
652 writer.write_all(b" ")?;
653 bytes = &bytes[i + 1..];
654 continue 'outer;
655 }
656 }
657
658 writer.write_all(bytes)?;
659 return Ok(did_replace);
660 }
661}
662
663fn replace_space_and_control(mut string: &str) -> Cow<'_, str> {
664 let mut result = Cow::Borrowed(string);
665 'outer: loop {
666 for (i, b) in string.bytes().enumerate() {
667 if b.is_ascii_control() {
668 if let Cow::Borrowed(_) = result {
669 result = Cow::Owned(String::with_capacity(string.len()));
670 }
671 let owned = result.to_mut();
672 let (pre, post_with_b) = string.split_at(i);
673 owned.push_str(pre);
674 owned.push('_');
675 string = post_with_b.split_at(1).1;
676 continue 'outer;
677 }
678 }
679
680 if let Cow::Owned(owned) = &mut result {
681 owned.push_str(string);
682 }
683 return result;
684 }
685}
686
687fn encode_7bit(writer: impl io::Write, mut value: usize) -> io::Result<()> {
689 let mut buf = [0u8; (usize::BITS as usize + 8 - 1) / 7];
690 let mut idx = buf.len() - 1;
691 buf[idx] = (value as u8).wrapping_shl(1);
692 value >>= 7;
693 while value != 0 {
694 idx -= 1;
695 buf[idx] = (value as u8).wrapping_shl(1) | 1;
696 value >>= 7;
697 }
698 write_escaped(writer, &buf[idx..])
699}
700
701fn write_escaped(mut writer: impl io::Write, buf: &[u8]) -> io::Result<()> {
703 for c in buf {
704 writer.write_all(match *c {
705 0x00 => &[0x00, 0x00],
706 0x0a => &[0x00, 0x01],
707 0x0d => &[0x00, 0x02],
708 0x1a => &[0x00, 0x03],
709 _ => std::slice::from_ref(c),
710 })?;
711 }
712 Ok(())
713}
714
715#[cfg(test)]
716mod test {
717 use super::*;
718
719 #[test]
720 fn test_encode_7bit() -> io::Result<()> {
721 let mut buf: Vec<u8> = Vec::new();
722
723 if usize::BITS == 64 {
724 encode_7bit(&mut buf, usize::MAX)?;
725 assert_eq!(
726 &buf[..],
727 &[
728 0b0000_0011, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1111, 0b1111_1110, ]
739 );
740 }
741
742 buf.clear();
743 encode_7bit(&mut buf, 0)?;
744 assert_eq!(&buf[..], &[0, 0]); buf.clear();
747 encode_7bit(&mut buf, 1)?;
748 assert_eq!(&buf[..], &[0b10]);
749
750 Ok(())
751 }
752}