Skip to content

Commit

Permalink
Cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@zafer-esen
zafer-esen committed Feb 27, 2024
1 parent 22a712e commit 0d21407
Showing 1 changed file with 0 additions and 261 deletions.
261 changes: 0 additions & 261 deletions src/main/scala/lazabs/horn/extendedquantifiers/ClauseInstrumenter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,264 +246,3 @@ class ClauseInstrumenter(instrumentationOperator : InstrumentationOperator) {
instrsFromRewrites
}
}

// A simple instrumenter that works for all extended quantifiers, but is very
// general and thus imprecise.
//class SimpleClauseInstrumenter(extendedQuantifier : ExtendedQuantifier)
// extends ClauseInstrumenter(extendedQuantifier) {
//
// private def pred(o : ITerm, i : ITerm, alienSubstMap : Map[ConstantTerm, ITerm]) = {
// extendedQuantifier.predicate match {
// case Some(p) =>
// // rewrite alien terms in the app to their corresponding ghost variables
// ConstantSubstVisitor(p(o, i), alienSubstMap)
// case None => o
// }
// }
//
// private def getAlienTermsFormulaAndAssertion(headTerms : GhostVariableTerms,
// bodyTerms : GhostVariableTerms,
// alienTermMap : Map[ITerm, ITerm]) :
// (IFormula, IFormula) = {
// val initConjuncts = new ArrayBuffer[IFormula]
// val assertionConjuncts = new ArrayBuffer[IFormula]
// if (bodyTerms.alienTerms isEmpty)
// IBoolLit(true)
// else {
// (for ((AlienGhostVariableTerms(bv, bvSet),
// AlienGhostVariableTerms(hv, hvSet)) <-
// bodyTerms.alienTerms zip headTerms.alienTerms) {
// initConjuncts +=
// ((expr2Formula(bvSet) &&& hv === bv) ||| hv === alienTermMap(bv)) &&& expr2Formula(hvSet)
//// ite(expr2Formula(bvSet),
//// hv === bv &&& hvSet === bvSet, // then
//// expr2Formula(hvSet) &&& hv === alienTermMap(bv)) // else
// assertionConjuncts +=
// (expr2Formula(bvSet) ==> (bv === alienTermMap(bv)))// &&& (expr2Formula(hvSet))
// })
// }
// (initConjuncts.fold(i(true))((c1, c2) => c1 &&& c2),
// assertionConjuncts.fold(i(true))((c1, c2) => c1 &&& c2))
// }
//
// override protected
// def instrumentStore(storeInfo : StoreInfo,
// headTerms : GhostVariableTerms,
// bodyTerms : GhostVariableTerms,
// alienTermMap : Map[ITerm, ITerm]): Seq[InstrumentationResult] = {
// val StoreInfo(a1, a2, i, o, arrayTheory2) = storeInfo
// if (arrayTheory != arrayTheory2)
// Nil
// else {
// import extendedQuantifier._
// import bodyTerms._
// import arrayTheory2._
// val (alienTermInitFormula, alienTermAssertionFormula) =
// getAlienTermsFormulaAndAssertion(headTerms, bodyTerms, alienTermMap)
//
// val standardInstrumentation = {
// val alienSubstMap : Map[ConstantTerm, ITerm] = // todo: incorrect - fix
// (for ((alienC, alienI) <- extendedQuantifier.alienConstantsInPredicate.zipWithIndex) yield {
// alienC -> headTerms.alienTerms(alienI).v
// }).toMap
// val instrConstraint1 =
// (headTerms.arr === a2) &&& alienTermInitFormula &&&
// ite(bodyTerms.lo === bodyTerms.hi,
// (headTerms.lo === i) & (headTerms.hi === i + 1) & (headTerms.res === pred(o, i, alienSubstMap)),
// ite((lo - 1 === i),
// (headTerms.res === reduceOp(res, pred(o, i, alienSubstMap))) & (headTerms.lo === i) & headTerms.hi === hi,
// ite(hi === i,
// (headTerms.res === reduceOp(res, pred(o, i, alienSubstMap))) & (headTerms.hi === i + 1 & headTerms.lo === lo),
// ite(lo <= i & hi > i,
// invReduceOp match {
// case Some(f) =>
// headTerms.res === reduceOp(f(res, select(a1, i)), pred(o, i, alienSubstMap)) &
// headTerms.lo === lo & headTerms.hi === hi
// case _ =>
// (headTerms.lo === i) & (headTerms.hi === i + 1) &
// (headTerms.res === pred(o, i, alienSubstMap))
// },
// (headTerms.lo === i) & (headTerms.hi === i + 1) &
// (headTerms.res === pred(o, i, alienSubstMap)))))) // outside bounds, reset
// val assertion = lo === hi ||| (a1 === arr &&& alienTermAssertionFormula)
//
// InstrumentationResult(newConjunct = instrConstraint1,
// rewriteConjuncts = Map(),
// assertions = Seq(assertion))
// }
// //////////////////////////////////////////////////////////////////////////
// // also add an array pass-through instrumentation for stores
// val arrayPassThroughInstrumentation : InstrumentationResult = {
// val instrConstraint = {
//// ((i < bodyTerms.lo ||| bodyTerms.hi <= i) &&& bodyTerms.arr === a1) ==>
//// (headTerms.arr === a2)
// headTerms.lo === bodyTerms.lo &&& headTerms.hi === bodyTerms.hi &&&
// headTerms.res === bodyTerms.res &&&
// ite(((i < bodyTerms.lo) ||| (bodyTerms.hi <= i)) &&& (bodyTerms.arr === a1),
// headTerms.arr === a2,
// headTerms.arr === bodyTerms.arr)
// }
// InstrumentationResult(newConjunct = instrConstraint,
// rewriteConjuncts = Map(),
// assertions = Nil)
// }
//
// Seq(standardInstrumentation, arrayPassThroughInstrumentation)
// }
// }
//
// override protected
// def instrumentSelect(selectInfo : SelectInfo,
// headTerms : GhostVariableTerms,
// bodyTerms : GhostVariableTerms,
// alienTermMap : Map[ITerm, ITerm]): Seq[InstrumentationResult] = {
// val SelectInfo(a, i, o, arrayTheory2) = selectInfo
// if (arrayTheory != arrayTheory2)
// Nil
// else {
// import extendedQuantifier._
// import bodyTerms._
// val alienSubstMap : Map[ConstantTerm, ITerm] = // todo: incorrect - fix
// (for ((alienC, alienI) <- extendedQuantifier
// .alienConstantsInPredicate.zipWithIndex) yield {
// alienC -> headTerms.alienTerms(alienI).v
// }).toMap
// val (alienTermInitFormula, alienTermAssertionFormula) =
// getAlienTermsFormulaAndAssertion(headTerms, bodyTerms,
// alienTermMap : Map[ITerm, ITerm])
// val instrConstraint1 =
// (headTerms.arr === a) &&& alienTermInitFormula &&&
// ite(lo === hi,
// (headTerms.lo === i) & (headTerms.hi === i + 1) &
// (headTerms.res === pred(o, i, alienSubstMap)),
// ite((lo - 1 === i),
// (headTerms.res === reduceOp(res, pred(o, i, alienSubstMap))) & (headTerms.lo === i) & headTerms.hi === hi,
// ite(hi === i,
// (headTerms.res === reduceOp(res, pred(o, i, alienSubstMap))) & (headTerms.hi === i + 1 & headTerms.lo === lo),
// ite(lo <= i & hi > i,
// headTerms.res === res & headTerms.lo === lo & headTerms.hi === hi, // no change within bounds
// (headTerms.lo === i) & (headTerms.hi === i + 1) &
// (headTerms.res === pred(o, i, alienSubstMap)))))) // outside bounds, reset
// val assertion = lo === hi ||| (a === arr &&& alienTermAssertionFormula)
// Seq(InstrumentationResult(newConjunct = instrConstraint1,
// rewriteConjuncts = Map(),
// assertions = Seq(assertion)))
// }
// }
//
// // todo: instrument const operation
// override protected
// def instrumentConst(constInfo : ConstInfo,
// headTerms : GhostVariableTerms,
// bodyTerms : GhostVariableTerms,
// alienTermMap : Map[ITerm, ITerm]) : Seq[InstrumentationResult] =
// Nil
// // val ConstInfo(a, o, arrayTheory) = constInfo
// // val instr =
// // hhi === 10 &&& hlo === 0 &&& harr === a &&&
// // hres === extendedQuantifier.reduceOp(o, o)
//
// override protected
// def rewriteAggregateFun(exqInfo : ExtendedQuantifierApp,
// ghostVarTerms : Seq[GhostVariableTerms],
// alienVarToPredVar : Map[ITerm, ITerm]) : Seq[InstrumentationResult] = {
// // range1 ? res1 : (range 2 ? res2 : (... : range1+range2 ? res1+res : range2+range1 ? res2+res1 : ... ))
// val combinations: Seq[Seq[GhostVariableTerms]] =
// (for (i <- 1 to ghostVarTerms.length) yield {
// ghostVarTerms.combinations(i)
// }).flatten
//
// val ExtendedQuantifierApp(_, funApp, a, lo, hi, o, conjunct) = exqInfo
// def loExpr = extendedQuantifier.rangeFormulaLo.getOrElse(
// (t1 : ITerm, t2 : ITerm, t3 : ITerm) => t1 === t2)
// def hiExpr = extendedQuantifier.rangeFormulaHi.getOrElse(
// (t1 : ITerm, t2 : ITerm, t3 : ITerm) => t1 === t2)
//
// def buildRangeFormula(combs : Seq[Seq[GhostVariableTerms]]) : IFormula = {
// combs.headOption match {
// case Some(comb) =>
// comb length match {
// case 1 =>
// ((loExpr(comb.head.lo, lo, comb.head.res) &
// hiExpr(comb.head.hi, hi, comb.head.res) &
// comb.head.arr === a) ==> (comb.head.res === o)) &&&
// ((lo >= hi) ==> (extendedQuantifier.identity === o)) &&&
// buildRangeFormula(combs.tail)
// case 2 => //todo: empty range for more than one ghost var range?
// ((loExpr(comb(0).lo, lo, comb(0).res) & hiExpr(comb(0).hi, comb(1).lo, comb(0).res) &
// hiExpr(comb(1).hi, hi, comb(1).res) & comb(0).arr === a & comb(1).arr === a) ==>
// (extendedQuantifier.reduceOp(comb(0).res, comb(1).res) === o) &&&
// ((loExpr(comb(1).lo, lo, comb(1).res) & hiExpr(comb(1).hi, comb(0).lo, comb(1).res) &
// hiExpr(comb(0).hi, hi, comb(0).res) & comb(0).arr === a & comb(1).arr === a) ==>
// (extendedQuantifier.reduceOp(comb(1).res, comb(0).res) === o))) &&&
// buildRangeFormula(combs.tail)
// case _ => ??? // todo: generalize this!
// }
// case None => i(true)
// }
// }
//
// // this builds a formula to be asserted, such that at least one of the
// // branches must be taken
// def buildAssertionFormula(combs : Seq[Seq[GhostVariableTerms]]) : IFormula = {
// // todo: refactor
// combs.headOption match {
// case Some(comb) =>
// comb length match {
// case 1 =>
// // assert that the alien ghost vars are the same as those used
// // in the aggregate
// val alienGuard = {
// for (AlienGhostVariableTerms(v, vSet) <- comb.head.alienTerms)
// yield {
// (expr2Formula(vSet)) &&&
// (v === alienVarToPredVar(v))
// }
// }.fold(i(true))((c1, c2) => c1 &&& c2)
//
// val guard =
// (loExpr(comb.head.lo, lo, comb.head.res) &
// hiExpr(comb.head.hi, hi, comb.head.res) &
// comb.head.arr === a &&& alienGuard) ||| (lo >= hi)
// guard ||| buildAssertionFormula(combs.tail)
// case 2 => //todo: empty range for more than one ghost var range?
// val alienGuard1 = {
// for (AlienGhostVariableTerms(v, vSet) <- comb(0).alienTerms)
// yield {
// expr2Formula(vSet) &&& v === alienVarToPredVar(v)
// }
// }.fold(i(true))((c1, c2) => c1 &&& c2)
// val alienGuard2 = {
// for (AlienGhostVariableTerms(v, vSet) <- comb(1).alienTerms)
// yield {
// expr2Formula(vSet) &&& v === alienVarToPredVar(v)
// }
// }.fold(i(true))((c1, c2) => c1 &&& c2)
// val c1 =
// loExpr(comb(0).lo, lo, comb(0).res) &
// hiExpr(comb(0).hi, comb(1).lo, comb(0).res) &
// hiExpr(comb(1).hi, hi, comb(1).res) & comb(0).arr === a &
// comb(1).arr === a &&& alienGuard1
// val c2 =
// loExpr(comb(1).lo, lo, comb(1).res) &
// hiExpr(comb(1).hi, comb(0).lo, comb(1).res) &
// hiExpr(comb(0).hi, hi, comb(0).res) &
// comb(0).arr === a & comb(1).arr === a &&& alienGuard2
// (c1 ||| c2) ||| buildAssertionFormula(combs.tail)
// case _ => ??? // todo: generalize this!
// }
// case None => IExpression.i(false)
// }
// }
//
// val rewriteConjuncts =
// Map(exqInfo.conjunct -> buildRangeFormula(combinations))
// val assertionFormula = buildAssertionFormula(combinations)
//
// Seq(InstrumentationResult(newConjunct = IExpression.i(true),
// rewriteConjuncts = rewriteConjuncts,
// assertions = Seq(assertionFormula)))
// }
//
//
//}

0 comments on commit 0d21407

Please sign in to comment.