search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

fix(bmc, basic, parse): fix jumpmap #70

Closed wweic closed 9 years ago

wweic commented 9 years ago
  1. In order to support jump to same target under different condition, use list instead of map to store the jump edges. The logic in heuristics need to be rewritten.

in issue #68

soonhokong commented 9 years ago

@kquine, could you test this patch?

kquine commented 9 years ago

I tested a few examples, and it now generates a "or" brach including all corresponding jumps. I think it looks OK (note that some extra text is added in the generated smt2 file). However, --visualize seems not to work well here. I do not know whether it's the problem caused by this or not, though. Using the json files by the test cases for this, the visualization tool only shows the traces for the first mode change.

soonhokong commented 9 years ago

Great. Could you give us the smt2 file that you have a problem with visualization? I will take a look at.

Wei, thanks a lot. I'll merge this one soon.

Soonho Kong soonhok@cs.cmu.edu

kquine commented 9 years ago

Please find attached. The visualization tool only shows one mode changes, even though k > 3.

Kyungmin

On Fri, Jan 23, 2015 at 11:25 AM, Soonho Kong notifications@github.com wrote:

Great. Could you give us the smt2 file that you have a problem with visualization? I will take a look at.

Wei, thanks a lot. I'll merge this one soon.

Soonho Kong soonhok@cs.cmu.edu

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/pull/70#issuecomment-71219262.

Kyungmin Bae, Postdoctoral Fellow School of Computer Science Carnegie Mellon University