Exponential search / Reasoning horizon#37

Open

danielkocher wants to merge 21 commits into

mainfrom

feat/exp-search

Commits on Jan 9, 2023

add: File horizon that implements the horizon extraction when the stride option is enabled
danielkocher
committed
add: Stride option
danielkocher
committed
feat: Exponential search when the stride option is enabled (up to a max unroll depth)
danielkocher
committed

Commits on Jan 12, 2023

Commits on Jan 20, 2023

feat: adds --one-query flag
smml1996
committed
feat: --one-query flag implemented for sat solvers
smml1996
committed
fix: tiny fix sat_solvers
smml1996
committed
feat: --one-query implemented for smt solvers
smml1996
committed
fix: add Node::or handle for smt solvers
smml1996
committed
fix: Node::Bad is now reachable in solvers
smml1996
committed

Commits on Jan 22, 2023

Commits on Jan 23, 2023

Commits on Mar 27, 2023

iter: Fix reasoning horizon functionality (deal with updated order of bad states)
danielkocher
committed