dreal
let + forall
From https://github.com/dreal/dreal4/pull/78#issuecomment-380218590
Input:
(set-logic QF_NRA)
(assert
(forall ((x Real [0.0, 7.0]))
(let ((y (+ x 1)))
(>= y (* x 2)))))
(check-sat)
(exit)
Output:
Running local dreal
terminate called after throwing an instance of 'std::runtime_error'
what(): dreal/util/ibex_converter.cc:90 Variable x is not appeared in L0\y .
Aborted (core dumped)
/cc @martinjos
This is because we process a let_binding_list and add the temporary terms (i.e. L0\y = x + 1) at the top-level. This strategy works for the exist-case but does not work when let is embedded inside of forall (which is this case).
https://github.com/dreal/dreal4/blob/8fbce2e029c05f4fd95d7299dfd69bec8b400fb2/dreal/smt2/parser.yy#L360-L362
https://github.com/dreal/dreal4/blob/8fbce2e029c05f4fd95d7299dfd69bec8b400fb2/dreal/smt2/parser.yy#L501-L519
I'll change the parser so that let_binding_list: returns a formula (a conjunction of bindings) so that we can combine it with the term in let. This will make sure that nothing is leaked outside of the scope.
