first cut at providing synthesis with 'big components' from the LHS #326
Conversation
…o use in synthesis
|
just for completeness, let me add the rationale for this PR. currently, synthesis often fails because it must recreate the entire RHS from scratch. if the LHS is large, this is just not going to happen. this PR + some followon work in the CEGIS module will let us synthesize only the instructions that are actually new. the hypothesis is that this will let synthesis succeed a lot more often. |
| std::map<Block *, Block *> BlockCache; | ||
| Copies.push_back(getInstCopy(I, IC, InstCache, BlockCache)); | ||
| separateBlockPCs(BPCs, BPCsCopy, InstCache, BlockCache, IC); | ||
| separatePCs(PCs, PCsCopy, InstCache, BlockCache, IC); |
There was a problem hiding this comment.
The synthesis engine doesn't take PCs/BPCs into account that are attached to the component library (RHS). Now, if a candidate from LHS has a PC/PBC, I should consider this during synthesis. This makes things a bit more complex. Maybe we can start without PC/BPC support first.
There was a problem hiding this comment.
Yes, just ignore for now.
I think the correct thing to do with pc/blockpc is to ignore them for almost all purposes (cost functions etc.) but to allow them to put constraints on the LHS, which should make synthesis work more often.
| InstSynthesis IS; | ||
| EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout); | ||
| EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, | ||
| Copies, PCsCopy, BPCsCopy, IC, Timeout); |
There was a problem hiding this comment.
There is no need to make copies, the only thing I need are the LHSComps.
There was a problem hiding this comment.
Wait, really? But we need copies for nop synthesis, what's different here?
There was a problem hiding this comment.
The necessary replacements are performed in the synthesis engine in a special way that is different from the nop synthesis.
|
Duplicate of #327. |
2 participants
Ok, this is a work in progress for Raimondas to look at.
this PR adds parameters to instruction synthesis corresponding to a vector of instructions from the LHS that can be used as components in synthesis. just like in nop synthesis, these have been separated out from each other (and from the RHS) to avoid unsoundness due to component reuse.
also like nop synthesis, these components are found using DFS starting at the root of the LHS, based on the hypothesis that these are the most useful things to use. these should be used instead of vars in synthesis.
the number of big components is currently set to the same value as MaxNops which defaults to 20. of course we can use whatever value we want here.