Copying to list. On Wed, Dec 08, 2010 at 10:14:43PM +0000, Peter Collingbourne wrote: > On Wed, Dec 08, 2010 at 10:30:13PM +0100, Mauro Baluda wrote: > > On Wed, Dec 8, 2010 at 9:20 PM, Peter Collingbourne <peter at pcc.me.uk> > > wrote: > > > Given a constraint solver with an FP theory this would be easy > > > > Wouldn't it be possible to use a software implementation of FP > > arithmetics as a front end to STP? > > http://www.jhauser.us/arithmetic/SoftFloat.html > > I would like to experiment in this direction > > Hi Mauro, > > We have considered using software FP in the past. However, we > decided against it as we see a couple of pitfalls associated with > this technique: > > 1. Software FP implementations (by necessity) use a significant amount > of branching. So with a symbolic FP argument and a relatively > trivial number of operations you would start getting state space > explosions rather quickly. You could try solving this problem by > replacing branches with 'select' instructions: phi-node folding > is one way to do this -- this is discussed in my talk -- but this > technique is still limited. > > 2. Even if you solved this problem then you would still end up with very > large expression trees which would be taxing not only on RAM but on > the constraint solver. Specialised FP solvers can take advantage > of knowledge of FP semantics for optimisation purposes. > > However you are welcome to explore this solution using KLEE-FP and > I would be interested to hear about any progress made. > > Thanks, > -- > Peter
-- Peter
