Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

debug assert is failing #25

Open
sirandreww opened this issue Oct 23, 2024 · 2 comments
Open

debug assert is failing #25

sirandreww opened this issue Oct 23, 2024 · 2 comments

Comments

@sirandreww
Copy link

sirandreww commented Oct 23, 2024 •
edited
Loading 

thread 'tests::a_real_world_test_1' panicked at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:624:9:
assertion failed: id as usize >= TERMINALS
stack backtrace:
   0: rust_begin_unwind
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/std/src/panicking.rs:662:5
   1: core::panicking::panic_fmt
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/panicking.rs:74:14
   2: core::panicking::panic
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/panicking.rs:148:5
   3: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::use_free_slot
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:624:9
   4: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::get_slot_from_shared::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:678:54
   5: std::thread::local::LocalKey<T>::try_with
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/std/src/thread/local.rs:283:12
   6: std::thread::local::LocalKey<T>::with
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/std/src/thread/local.rs:260:9
   7: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::get_slot_from_shared
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:642:9
   8: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::add_node::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:604:13
   9: std::thread::local::LocalKey<T>::try_with
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/std/src/thread/local.rs:283:12
  10: std::thread::local::LocalKey<T>::with
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/std/src/thread/local.rs:260:9
  11: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::add_node
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:572:19
  12: <oxidd_manager_index::manager::LevelView<N,ET,TM,R,MD,_> as oxidd_core::LevelView<oxidd_manager_index::manager::Edge<N,ET>,N>>::get_or_insert::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1455:20
  13: oxidd_manager_index::manager::LevelViewSet<N,ET,TM,R,MD,_>::get_or_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1251:32
  14: <oxidd_manager_index::manager::LevelView<N,ET,TM,R,MD,_> as oxidd_core::LevelView<oxidd_manager_index::manager::Edge<N,ET>,N>>::get_or_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1452:9
  15: oxidd_core::ReducedOrNew<E,N>::then_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/lib.rs:188:28
  16: oxidd_rules_bdd::simple::reduce
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/mod.rs:83:5
  17: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:133:13
  18: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:131:41
  19: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:131:41
  20: oxidd_rules_bdd::simple::apply_rec_mt::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:109:16
  21: <oxidd_rules_bdd::simple::apply_rec_mt::BDDFunctionMT<F> as oxidd_core::function::BooleanFunction>::and_edge
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:618:9
  22: oxidd_core::function::BooleanFunction::and::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/function.rs:325:21
  23: <oxidd_manager_index::manager::Function<NC,ET,TMC,RC,MDC,_> as oxidd_core::function::Function>::with_manager_shared
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:2315:19
  24: <oxidd_rules_bdd::simple::apply_rec_mt::BDDFunctionMT<F> as oxidd_core::function::Function>::with_manager_shared
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:526:55
  25: oxidd_core::function::BooleanFunction::and
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/function.rs:324:9
  26: <oxidd::bdd::index::BDDFunction as oxidd_core::function::BooleanFunction>::and
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-0.7.0/src/bdd.rs:79:9

note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
`Edge`s must not be dropped. Use `Manager::drop_edge()`. Backtrace:
   0: <oxidd_manager_index::manager::Edge<N,ET> as core::ops::drop::Drop>::drop
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:444:13
   1: core::ptr::drop_in_place<oxidd_manager_index::manager::Edge<oxidd_manager_index::node::fixed_arity::NodeWithLevel<(),2_usize>,()>>
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/ptr/mod.rs:574:1
   2: core::ptr::drop_in_place<[oxidd_manager_index::manager::Edge<oxidd_manager_index::node::fixed_arity::NodeWithLevel<(),2_usize>,()>; 2]>
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/ptr/mod.rs:574:1
   3: core::ptr::drop_in_place<core::cell::UnsafeCell<[oxidd_manager_index::manager::Edge<oxidd_manager_index::node::fixed_arity::NodeWithLevel<(),2_usize>,()>; 2]>>
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/ptr/mod.rs:574:1
   4: core::ptr::drop_in_place<oxidd_manager_index::node::fixed_arity::NodeWithLevel<(),2_usize>>
             at /rustc/f6e511eec7342f59a25f7c0534f1dbea00d01b14/library/core/src/ptr/mod.rs:574:1
   5: oxidd_manager_index::manager::Store<N,ET,TM,R,MD,_>::add_node
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:616:5
   6: <oxidd_manager_index::manager::LevelView<N,ET,TM,R,MD,_> as oxidd_core::LevelView<oxidd_manager_index::manager::Edge<N,ET>,N>>::get_or_insert::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1455:20
   7: oxidd_manager_index::manager::LevelViewSet<N,ET,TM,R,MD,_>::get_or_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1251:32
   8: <oxidd_manager_index::manager::LevelView<N,ET,TM,R,MD,_> as oxidd_core::LevelView<oxidd_manager_index::manager::Edge<N,ET>,N>>::get_or_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:1452:9
   9: oxidd_core::ReducedOrNew<E,N>::then_insert
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/lib.rs:188:28
  10: oxidd_rules_bdd::simple::reduce
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/mod.rs:83:5
  11: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:133:13
  12: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:131:41
  13: oxidd_rules_bdd::simple::apply_rec_st::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_st.rs:131:41
  14: oxidd_rules_bdd::simple::apply_rec_mt::apply_bin
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:109:16
  15: <oxidd_rules_bdd::simple::apply_rec_mt::BDDFunctionMT<F> as oxidd_core::function::BooleanFunction>::and_edge
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:618:9
  16: oxidd_core::function::BooleanFunction::and::{{closure}}
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/function.rs:325:21
  17: <oxidd_manager_index::manager::Function<NC,ET,TMC,RC,MDC,_> as oxidd_core::function::Function>::with_manager_shared
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-manager-index-0.7.0/src/manager.rs:2315:19
  18: <oxidd_rules_bdd::simple::apply_rec_mt::BDDFunctionMT<F> as oxidd_core::function::Function>::with_manager_shared
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-rules-bdd-0.7.0/src/simple/apply_rec_mt.rs:526:55
  19: oxidd_core::function::BooleanFunction::and
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-core-0.7.0/src/function.rs:324:9
  20: <oxidd::bdd::index::BDDFunction as oxidd_core::function::BooleanFunction>::and
             at /home/andrew/.cargo/registry/src/index.crates.io-6f17d22bba15001f/oxidd-0.7.0/src/bdd.rs:79:9

I'm getting this assert failure during debug mode. Do you have an idea why this might be happening? I'm initializing the BDD manager using this function:

fn allocate_bdd_manager(x: usize) -> BDDManager {
      let cap = if x <= 10 {
          1 << 5
      } else if x <= 100 {
          1 << 10
      } else if x <= 1000 {
          1 << 20
      } else {
          1 << 23
      };
      let inner_node_capacity = cap;
      let apply_cache_capacity = cap;
      let threads = 1;

      let manager_ref =
          oxidd::bdd::new_manager(inner_node_capacity, apply_cache_capacity, threads);
      let var_to_bdd: FxHashMap<Variable, Bdd> = FxHashMap::default();
      let bdd_true = manager_ref.with_manager_exclusive(|manager| Bdd::t(manager));
      let bdd_false = manager_ref.with_manager_exclusive(|manager| Bdd::f(manager));
      debug_assert!(bdd_true.valid());
      debug_assert!(bdd_true.satisfiable());
      debug_assert!(!bdd_false.valid());
      debug_assert!(!bdd_false.satisfiable());
      let cache = FxHashMap::default();

      BDDManager {
          var_to_bdd,
          manager_ref,
          bdd_false,
          bdd_true,
          clause_cache: cache.clone(),
          not_clause_cache: cache,
      }
  }

This function might be called multiple times during the run.
@sirandreww
Copy link
Author

I think this issue is correlated with calling new_manager multiple times in the same thread. Is static memory used? Could it be the issue?

@nhusung
Copy link
Member

nhusung commented Feb 25, 2025

Sorry for the delay. Does the issue still persist with more recent versions of OxiDD? The manager implementation uses thread-local storage, but it should still be possible to have multiple managers in the same thread. Is it possible for you to share your entire test case? So far I have not been able to reproduce the issue …

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nhusung @sirandreww