Skip to content

Allow empty theory conflict#19

Open
dewert99 wants to merge 15 commits intoc-cube:masterfrom
dewert99:allow_empty_theory_conflict
Open

Allow empty theory conflict#19
dewert99 wants to merge 15 commits intoc-cube:masterfrom
dewert99:allow_empty_theory_conflict

Conversation

@dewert99
Copy link
Contributor

@dewert99 dewert99 commented Apr 1, 2024

Previously batsat panicked when Theory::raise_conflict was called with an empty clause, but I think it would make sense for the solver to just immediately return unsat

dewert99 added 15 commits March 14, 2024 12:07
@dewert99
Make literal picker independent of theory explanation order
e66c5c9
@dewert99
Move order_heap_data into VarState
cef2379
@dewert99
Cached activity levels in heap.
d2c987e
@dewert99
Switched activity level to use f32
b144218
@dewert99
Don't rebuild order heap
1a0b923
@dewert99
Extracted heap into its own module
2f7b2cf
@dewert99
Fixed activity rescale to also rescale activities cached in heap
796e42b
@dewert99
Merge remote-tracking branch 'origin/master' into deterministic
002f9aa
@dewert99
Switched order_heap to be a quaternary heap
dbe576e
@dewert99
Tried to make heap comparisons less branchy
c3a8b38
@dewert99
Replaced heap comparisons with u64 comparisons by utilizing https://s…
9972854 
…tackoverflow.com/questions/33678827/compare-floating-point-numbers-as-integers
@dewert99
Stored u64s directly in order_heap_data
288548b
@dewert99
Improved order Vars are added to the heap when canceling
f888533
@dewert99
Added more control over assumptions and decision variables
d8e4a4c
@dewert99
Allow theory conflicts to be empty
41aba49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@dewert99