Multiple RHS Support #367
Multiple RHS Support #367
Conversation
|
Note: no support for multiple RHSs dump in souper-check or redis cache for now. |
| @@ -103,7 +104,7 @@ class BaseSolver : public Solver { | |||
| if (EC) | |||
| return EC; | |||
| if (!IsSat) { | |||
| RHS = I; | |||
| RHSs.emplace_back(I); | |||
There was a problem hiding this comment.
do you want to return here, or try to find more RHSs?
There was a problem hiding this comment.
These are both constant synthesis, why we wants to collect multiple RHSs if a constant fit the LHS
There was a problem hiding this comment.
well, it depends on why we want multiple RHSs. for manasij's purposes a constant is always good, but for building a cost model I'd like as many alternatives as possible
There was a problem hiding this comment.
ping me if you need this.
| @@ -142,7 +143,7 @@ class BaseSolver : public Solver { | |||
| if (EC) | |||
| return EC; | |||
| if (!IsSat) { | |||
| RHS = Const; | |||
| RHSs.emplace_back(Const); | |||
| @@ -214,18 +215,21 @@ class BaseSolver : public Solver { | |||
| if(SMTSolver->supportsModels()) { | |||
| if (EnableExhaustiveSynthesis) { | |||
| ExhaustiveSynthesis ES; | |||
| EC = ES.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout); | |||
| if (EC || RHS) | |||
| EC = ES.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHSs, | |||
There was a problem hiding this comment.
did you intend to change this line? was it too long?
There was a problem hiding this comment.
RHS is changed to RHSs, and it is too long so I wrapped.
| if (!EC && RHS) { | ||
| RHSStr = GetReplacementRHSString(RHS, Context); | ||
| if (!EC && !RHSs.empty()) { | ||
| RHSStr = GetReplacementRHSString(RHSs.front(), Context); |
There was a problem hiding this comment.
seems weird to take the first element here, is this a placeholder for something different?
There was a problem hiding this comment.
This PR does not support cache dumping yet, so only print the first RHS in the list. I'll add support for cache dumping soon.
There was a problem hiding this comment.
I'd say don't do the caching part of this yet, until we're sure we want it
There was a problem hiding this comment.
Sounds good, should be possible to prototype without caching.
lib/Infer/ExhaustiveSynthesis.cpp
Outdated
| @@ -438,6 +439,7 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver, | |||
| std::vector<Inst *> Vars; | |||
| findVars(LHS, Vars); | |||
|
|
|||
| unsigned ValidRHS = 0; | |||
There was a problem hiding this comment.
why do you want a separate variable for this? doesn't it work to inspect the length of the vector?
|
overall I'm not sure about this patch |
|
Sure, I'll remove the unnecessary validRHS variable. |
This patch changes the type of the RHS argument of ExhaustiveSynthesis::synthesize() and Solver::infer() from a Inst pointer to a vector of Inst pointers.
Exhaustive Synthesis takes a constant "MaxRHS". This constant is set to 1 for performance. Exhaustive Synthesis generates at most MaxRHS number of RHSs. The original Souper test suite on my machine runs for 282.54s while with MaxRHS set to 3, the test suite runs for 454.83s.
Call sites of infer() function takes the result vector of RHS and extract the first RHS, this preserves the behaviors of these call sites.