[klee-dev] Experssion Rewriter

[Cristian Cadar]

Hi, there is some overlap between those two options, and in general 
things are not that well documented, so the best reference is the code. 
  I'll try to take a closer look at this once I have some time.  In the 
meantime, you may want to open a new issue on GitHub.

Best,
Cristian

On 12/05/15 06:53, Zhiyi Zhang wrote:
> Hi, Rizzi
>
> Thank you for your reply.
>
> I have read the file in
> https://github.com/klee/klee/commit/f0de5e4ea4f1bed2e698ae99a19f1f0b96770f9c,
> but I am confused that this file seems also to be used for constraint
> set simplification optimization. Does expression rewrite
> optimization and constraint set simplification optimization have
> combined in the new version? And the option is --rewrite-equalities and
> --equality-substitution?
>
> Best wishes.
> Zhiyi Zhang
>
> On Mon, May 11, 2015 at 7:54 PM, Eric Rizzi <eric.rizzi at gmail.com
> <mailto:eric.rizzi at gmail.com>> wrote:
>
>     There should be a --rewrite-equalities option per the following commit
>
>     https://github.com/klee/klee/commit/f0de5e4ea4f1bed2e698ae99a19f1f0b96770f9c
>
>     The default behavior is on anyways, though.
>
>     On Mon, May 11, 2015 at 3:02 AM, Zhiyi Zhang
>     <xianlingzibiying at gmail.com <mailto:xianlingzibiying at gmail.com>> wrote:
>
>         Hi all,
>
>         When I used klee with llvm3.4, I found that there is no
>         "--rewrite" option in klee orders. So how could I use expression
>           rewrite optimization  when I use klee running a program?
>
>         Thank you.
>         Zhiyi Zhang
>
>         _______________________________________________
>         klee-dev mailing list
>         klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>