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

Add Theory::explain_propagation_final for use in analyze_final #20

Open
wants to merge 16 commits into
base: master
Choose a base branch
from
Open

Add Theory::explain_propagation_final for use in analyze_final #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
e66c5c9
Make literal picker independent of theory explanation order
dewert99 Mar 14, 2024
cef2379
Move `order_heap_data` into `VarState`
dewert99 Mar 15, 2024
d2c987e
Cached activity levels in heap.
dewert99 Mar 15, 2024
b144218
Switched activity level to use `f32`
dewert99 Mar 15, 2024
1a0b923
Don't rebuild order heap
dewert99 Mar 16, 2024
2f7b2cf
Extracted heap into its own module
dewert99 Mar 16, 2024
796e42b
Fixed activity rescale to also rescale activities cached in heap
dewert99 Mar 18, 2024
002f9aa
Merge remote-tracking branch 'origin/master' into deterministic
dewert99 Mar 18, 2024
dbe576e
Switched `order_heap` to be a quaternary heap
dewert99 Mar 18, 2024
c3a8b38
Tried to make heap comparisons less branchy
dewert99 Mar 18, 2024
9972854
Replaced heap comparisons with u64 comparisons by utilizing https://s…
dewert99 Mar 19, 2024
288548b
Stored `u64`s directly in order_heap_data
dewert99 Mar 19, 2024
f888533
Improved order `Var`s are added to the heap when canceling
dewert99 Mar 19, 2024
d8e4a4c
Added more control over assumptions and decision variables
dewert99 Mar 26, 2024
41aba49
Allow theory conflicts to be empty
dewert99 Apr 1, 2024
517f3ee
Add `Theory::explain_propagation_final` for use in `analyze_final`
dewert99 Apr 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

[workspace]
resolver = "2"

members = [
"src/batsat",
Expand Down
2 changes: 1 addition & 1 deletion src/batsat/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ readme = "../../README.md"
keywords = ["sat", "minisat"]
categories = ["algorithms"]
license = "MIT"
edition = "2018"
edition = "2021"

publish = true

Expand Down
4 changes: 2 additions & 2 deletions src/batsat/src/clause.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ use {
alloc::{self, RegionAllocator},
intmap::{AsIndex, IntMap, IntMapBool, IntSet},
},
std::{fmt, iter::DoubleEndedIterator, ops, slice, u32},
std::{fmt, iter::DoubleEndedIterator, ops, slice},
};

#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
Expand All @@ -42,7 +42,7 @@ impl fmt::Debug for Var {
}

impl Var {
pub const UNDEF: Var = Var(!0);
pub const UNDEF: Var = Var(u32::MAX / 2);
#[inline(always)]
pub(crate) fn from_idx(idx: u32) -> Self {
debug_assert!(idx < u32::MAX / 2, "Var::from_idx: index too large");
Expand Down
Loading
Loading