extern crate rsdd;
use rsdd::builder::bdd::RobddBuilder;
use rsdd::builder::cache::LruIteTable;
use rsdd::builder::BottomUpBuilder;
use rsdd::repr::{BddPtr, VarLabel};
fn main() {
let builder = RobddBuilder::<LruIteTable<BddPtr>>::new_with_linear_order(0);
let vars: Vec<VarLabel> = std::iter::repeat_with(|| builder.new_var(true).0)
.take(15)
.collect();
let acc = builder.ite(
builder.var(vars[8], true),
builder.var(vars[9], true),
builder.true_ptr(),
);
dbg!(acc);
let c = (VarLabel::new(8), builder.var(vars[0], true)); // FIRST
dbg!(c);
let acc = builder.compose(acc, c.0, c.1);
dbg!(acc);
let c = (VarLabel::new(9), builder.var(vars[1], true)); // SECOND
dbg!(c);
let acc = builder.compose(acc, c.0, c.1);
dbg!(acc);
}
It crashes. If you swap lines FIRST
and SECOND
it doesn't crash.
thread 'main' panicked at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:196:34:
index out of bounds: the len is 0 but the index is 0
stack backtrace:
0: 0x1025ce754 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::he395ae20fca1ef41
1: 0x1025dc620 - core::fmt::write::haacaf63c647e4106
2: 0x1025d02b8 - std::io::Write::write_fmt::hcc90f2571dcb9970
3: 0x1025ce5a8 - std::sys_common::backtrace::print::ha2445e687f87d0f3
4: 0x1025cf08c - std::panicking::default_hook::{{closure}}::hc7b880a562e56458
5: 0x1025cede8 - std::panicking::default_hook::h8fd7f383a85001a1
6: 0x1025cf804 - std::panicking::rust_panic_with_hook::h99baae440a1a295b
7: 0x1025cf5cc - std::panicking::begin_panic_handler::{{closure}}::hea77d56975627739
8: 0x1025ce974 - std::sys_common::backtrace::__rust_end_short_backtrace::h7afafd01e3c2d80e
9: 0x1025cf344 - _rust_begin_unwind
10: 0x1025e2d58 - core::panicking::panic_fmt::h5e7349beebf2ad6e
11: 0x1025e2eb0 - core::panicking::panic_bounds_check::h3de19823c79388aa
12: 0x10258a214 - <usize as core::slice::index::SliceIndex<[T]>>::index::h73df678068e5c4a5
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/slice/index.rs:264:10
13: 0x10258aad8 - core::slice::index::<impl core::ops::index::Index<I> for [T]>::index::h2438b636c7ee056b
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/slice/index.rs:18:9
14: 0x10258aad8 - <alloc::vec::Vec<T,A> as core::ops::index::Index<I>>::index::hcd13fd21b7b5374e
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/alloc/src/vec/mod.rs:2829:9
15: 0x10258e3d4 - rsdd::builder::bdd::robdd::RobddBuilder<T>::cond_with_alloc::he6233a6ad090a152
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:196:34
16: 0x10258e134 - rsdd::builder::bdd::robdd::RobddBuilder<T>::cond_with_alloc::he6233a6ad090a152
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:202:25
17: 0x10258dabc - <rsdd::builder::bdd::robdd::RobddBuilder<T> as rsdd::builder::bdd::builder::BddBuilder>::cond_helper::hdb6771a9ea4823dd
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:86:9
18: 0x10258eb58 - rsdd::builder::bdd::builder::<impl rsdd::builder::BottomUpBuilder<rsdd::repr::bdd::BddPtr> for T>::condition::h7b258a965d65240a
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/builder.rs:167:17
19: 0x10258eaa0 - rsdd::builder::bdd::builder::<impl rsdd::builder::BottomUpBuilder<rsdd::repr::bdd::BddPtr> for T>::exists::h1bda9750aeff7d45
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/builder.rs:161:18
20: 0x10258decc - rsdd::builder::BottomUpBuilder::compose::h800650db86284d83
at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/mod.rs:60:9
21: 0x10258c60c - mu_calculus_bdd_mc::test_bug::h8b55024bae65aa0a
at /Users/denbuen/DontTouch/work/inprogress/proj/src/main.rs:601:15
22: 0x10258c788 - mu_calculus_bdd_mc::main::hab7bd1394f490286
at /Users/denbuen/DontTouch/work/inprogress/proj/src/main.rs:612:5
23: 0x102588ee0 - core::ops::function::FnOnce::call_once::h9598a2e15e6eeeeb
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/ops/function.rs:250:5
24: 0x102596864 - std::sys_common::backtrace::__rust_begin_short_backtrace::ha7dbbf5c76d19971
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/sys_common/backtrace.rs:155:18
25: 0x10258bc30 - std::rt::lang_start::{{closure}}::hacd6ff232f341af4
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/rt.rs:166:18
26: 0x1025cf21c - std::panicking::try::h930b3e414b1d9cbc
27: 0x1025c8ca8 - std::rt::lang_start_internal::he9a392d3f16eaee8
28: 0x10258bbfc - std::rt::lang_start::h4d4d5e1e8f8d49b8
at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/rt.rs:165:17
29: 0x10258c7b4 - _main