Skip to content
Snippets Groups Projects
Commit cfbbefbd authored by Ali Sinan Köksal's avatar Ali Sinan Köksal
Browse files

fix for not fetching guards for synthetic L values

parent df28aef2
No related branches found
No related tags found
No related merge requests found
...@@ -217,7 +217,6 @@ object LTrees { ...@@ -217,7 +217,6 @@ object LTrees {
val placeHolders = Seq(FreshIdentifier("placeholder", true).setType(BottomType)) val placeHolders = Seq(FreshIdentifier("placeholder", true).setType(BottomType))
val candidateL = new L[T](handler(), placeHolders) val candidateL = new L[T](handler(), placeHolders)
val instantiatedCnstr = constraint(candidateL) val instantiatedCnstr = constraint(candidateL)
// println("l vars in constraint: " + instantiatedCnstr.lVars)
// now that we have a Constraint, we can perform some actions such as: // now that we have a Constraint, we can perform some actions such as:
GlobalContext.initializeIfNeeded(instantiatedCnstr.program) GlobalContext.initializeIfNeeded(instantiatedCnstr.program)
...@@ -232,7 +231,10 @@ object LTrees { ...@@ -232,7 +231,10 @@ object LTrees {
val subst2 = ((placeHolders map (Variable(_))) zip (typedPlaceHolders map (Variable(_)))).toMap val subst2 = ((placeHolders map (Variable(_))) zip (typedPlaceHolders map (Variable(_)))).toMap
val replacedExpr = replace(subst1 ++ subst2, newExpr) val replacedExpr = replace(subst1 ++ subst2, newExpr)
val otherGuards = instantiatedCnstr.lVars.map(lv => GlobalContext.getGuard(lv.ids)) println("l vars in constraint: " + (instantiatedCnstr.lVars map (_.ids)))
val nonSyntheticLVars = instantiatedCnstr.lVars.map(_.ids) -- Set(placeHolders)
println("non-synthetic l vars: " + nonSyntheticLVars)
val otherGuards = nonSyntheticLVars.map(ids => GlobalContext.getGuard(ids))
if (isStillSat(typedPlaceHolders, replacedExpr, otherGuards)) { if (isStillSat(typedPlaceHolders, replacedExpr, otherGuards)) {
Stream.cons(new L[T](handler(), typedPlaceHolders), underlyingStream()) Stream.cons(new L[T](handler(), typedPlaceHolders), underlyingStream())
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment