FastCexSolver: Start implementing exact value propogation.

 - So far this just propogates obvious equalities and reads. For example,
   FastCexSolver can now prove that:
--
array arr219[3] : w32 -> w8 = symbolic
(query [(Eq 235 N0:(Read w8 0 arr219))]
       (Eq 235 N0))
--
   is valid.

Even though this is very basic, it is good enough to solve ~50% of the valid
queries on pcresymtest-[34].pc (total reduction in # of queries is ~25%).
Unfortunately, this only gives a 1-2% speedup, which is disappointing, but there
is a lot more we can do.

I'm a little surprised the speedup is so low, this may be an indicator that
there are some other things going on, for example perhaps the STP expr
construction cost for arrays is very high, and we inevitably will end up paying
this unless we solve so many queries that some arrays never ever make it to STP.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73058 91177308-0d34-0410-b5e6-96231b3b80d8

0 files changed, 0 insertions, 0 deletions