Exponential search / Reasoning horizon #37
Conversation
…ide option is enabled
src/main.rs
Outdated
| let mut model_copy = model.clone(); | ||
|
|
||
| for m in 0..n { | ||
| unroll_model(&mut model_copy, m); |
There was a problem hiding this comment.
The second parameter to unroll_model (i.e. the m) is only used to construct the names of bad-state nodes and input nodes in the current unrolling step. Would it make the algorithm simpler if we were to pass the correct absolute depth at this point already? I think this could make print_reasoning_horizon simpler.
There was a problem hiding this comment.
Good pointer, thanks.
I adapted the implementation accordingly and print_reasoning_horizon did simplify significantly (as expected).
src/unicorn/mod.rs
Outdated
|
|
||
| pub type Nid = u64; | ||
| pub type NodeRef = Rc<RefCell<Node>>; | ||
|
|
||
| #[derive(Debug)] | ||
| #[derive(Clone,Debug)] |
There was a problem hiding this comment.
I understand that we need to clone Model for now. But from what I can tell we are not cloning Node objects. I might very well be missing something. Could you double-check whether deriving Clone on Node is still necessary here?
There was a problem hiding this comment.
True, this is a leftover that I will fix - thanks!
…earch + binary search)
…called (i.e., panic only if stride is disabled)
Implements the stride option
-l,--stride, which performs an exponential search until the first bad state is encountered - we called this the reasoning horizon.Outline
2^0,2^1,2^2, ...bad_states_initialusing a helper functionprint_reasoning_horizonin constant time. Since the final search step subsumes previous search steps, we do not need a binary search between the last and second to last step. However, it should be easy to extend the implementation with a binary search if required.-uoption) is specified. The max. unrolling depth is used as an upper bound for the exponential search. This seems reasonable but I can also change this to work without unrolling if desired. In addition, we discussed that we want specify a time budget, which would be the max. unrolling depth (assuming that the time budget are number of steps and not real time). I am happy to discuss (and change) this before we merge intomain.Tested with the gcc-compiled RISC-V binary of
lion/factorize_35.c:n=189adivision-by-zerois satisfiable):n=62adivision-by-zerois satisfiable, which is correct because it is encountered during the 7-th search step2^7 = 128, i.e.,2^0 + 2^1 + 2^2 + 2^3 + 2^4 + 2^5 + 2^6 = 127 + 62 = 189; the final warning prints the derived depth:189):n=62):