Skip to content

Commit 1c849d7

Browse files
robby-phdrobby-phd
committed
Refactored utility methods.
1 parent 8670796 commit 1c849d7

File tree

1 file changed

+9
-84
lines changed

1 file changed

+9
-84
lines changed

‎shared/src/main/scala/org/sireum/logika/Util.scala

+9-84
Original file line numberDiff line numberDiff line change
@@ -544,8 +544,6 @@ object Util {
544544
val eqMap: HashMap[Z, HashSSet[State.Claim.Eq]],
545545
var atPossMap: HashMap[ClaimsToExps.AtPossKey, HashMap[ISZ[Position], HashMap[Z, (Z, State.Value.Sym)]]]) {
546546

547-
val trueLit: AST.Exp.LitB = AST.Exp.LitB(T, AST.Attr(Some(pos)))
548-
val falseLit: AST.Exp = AST.Exp.LitB(F, trueLit.attr)
549547
val posOpt: Option[Position] = Some(pos)
550548
val mulSymDefs: HashSet[Z] = {
551549
var r = HashSet.empty[Z]
@@ -616,79 +614,6 @@ object Util {
616614
return r
617615
}
618616

619-
@pure def bigAndExp(exps: ISZ[AST.Exp]): AST.Exp = {
620-
var set = HashSSet.empty[AST.Exp]
621-
for (exp <- exps) {
622-
if (exp == trueLit) {
623-
// skip
624-
} else if (exp == falseLit) {
625-
return falseLit
626-
} else {
627-
set = set + exp
628-
}
629-
}
630-
return esToBinaryExp(set.elements, trueLit, AST.Exp.BinaryOp.And,
631-
AST.Typed.bOpt, AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryAnd))
632-
}
633-
634-
@pure def bigOrExp(exps: ISZ[AST.Exp]): AST.Exp = {
635-
var set = HashSSet.empty[AST.Exp]
636-
for (exp <- exps) {
637-
if (exp == trueLit) {
638-
return trueLit
639-
} else if (exp == falseLit) {
640-
// skip
641-
} else {
642-
set = set + exp
643-
}
644-
}
645-
return esToBinaryExp(set.elements, falseLit, AST.Exp.BinaryOp.Or,
646-
AST.Typed.bOpt, AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryOr))
647-
}
648-
649-
@pure def bigImplyExp(isCond: B, exps: ISZ[AST.Exp]): AST.Exp = {
650-
var es = ISZ[AST.Exp]()
651-
for (i <- 0 until exps.size - 1) {
652-
val exp = exps(i)
653-
if (exp == falseLit) {
654-
return trueLit
655-
} else {
656-
es = es :+ exp
657-
}
658-
}
659-
es = es :+ exps(exps.size - 1)
660-
assert(es.size >= 2)
661-
var r = es(es.size - 1)
662-
val op: String = if (isCond) AST.Exp.BinaryOp.CondImply else AST.Exp.BinaryOp.Imply
663-
val res = AST.ResolvedInfo.BuiltIn(if (isCond) AST.ResolvedInfo.BuiltIn.Kind.BinaryCondImply else
664-
AST.ResolvedInfo.BuiltIn.Kind.BinaryImply)
665-
var i = es.size - 2
666-
while (i >= 0) {
667-
if (r != trueLit) {
668-
r = AST.Exp.Binary(es(i), op, r, AST.ResolvedAttr(None(), Some(res), AST.Typed.bOpt), None())
669-
}
670-
i = i - 1
671-
}
672-
return r
673-
}
674-
675-
@pure def constructIf(cond: AST.Exp, left: AST.Exp, right: AST.Exp, pOpt: Option[Position], tOpt: Option[AST.Typed]): AST.Exp = {
676-
if (right == trueLit) {
677-
if (left == trueLit) {
678-
return trueLit
679-
}
680-
return AST.Exp.Binary(cond, AST.Exp.BinaryOp.CondImply, left, AST.ResolvedAttr(pOpt,
681-
Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryCondImply)), AST.Typed.bOpt), pOpt)
682-
} else if (right == falseLit) {
683-
return AST.Exp.Binary(cond, AST.Exp.BinaryOp.CondAnd, left, AST.ResolvedAttr(pOpt,
684-
Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryCondAnd)), AST.Typed.bOpt), pOpt)
685-
} else if (left == trueLit) {
686-
return AST.Exp.Binary(cond, AST.Exp.BinaryOp.CondOr, right, AST.ResolvedAttr(pOpt,
687-
Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryCondOr)), AST.Typed.bOpt), pOpt)
688-
}
689-
return AST.Exp.If(cond, left, right, AST.TypedAttr(pOpt, tOpt))
690-
}
691-
692617
@pure def rcvOptIdent(v: State.Value, symPosOpt: Option[Position]): Option[(Option[AST.Exp], AST.Exp.Ident)] = {
693618
valueToExp(v) match {
694619
case Some(o) =>
@@ -1017,7 +942,7 @@ object Util {
1017942
case _ =>
1018943
}
1019944
}
1020-
return Some(bigAndExp(es))
945+
return Some(AST.Util.bigAnd(es, posOpt))
1021946
case let: State.Claim.Let.Or =>
1022947
var es = ISZ[AST.Exp]()
1023948
for (v <- let.args) {
@@ -1026,7 +951,7 @@ object Util {
1026951
case _ => return None()
1027952
}
1028953
}
1029-
return Some(bigOrExp(es))
954+
return Some(AST.Util.bigOr(es, posOpt))
1030955
case let: State.Claim.Let.Imply =>
1031956
var es = ISZ[AST.Exp]()
1032957
for (i <- 0 until let.args.size - 1) {
@@ -1043,11 +968,11 @@ object Util {
1043968
es = es :+ e
1044969
case _ => return None()
1045970
}
1046-
return Some(bigImplyExp(F, es))
971+
return Some(AST.Util.bigImply(F, es, posOpt))
1047972
case let: State.Claim.Let.Ite =>
1048973
(valueToExp(let.cond), valueToExp(let.left), valueToExp(let.right)) match {
1049974
case (Some(cond), Some(left), Some(right)) =>
1050-
return Some(constructIf(cond, left, right, symPosOpt, Some(sym.tipe)))
975+
return Some(AST.Util.ite(cond, left, right, symPosOpt, Some(sym.tipe)))
1051976
case (_, _, _) => return None()
1052977
}
1053978
case let: State.Claim.Let.TupleLit =>
@@ -1647,7 +1572,7 @@ object Util {
16471572
case _ =>
16481573
}
16491574
}
1650-
return Some(bigAndExp(es))
1575+
return Some(AST.Util.bigAnd(es, posOpt))
16511576
case claim: State.Claim.Or =>
16521577
var es = ISZ[AST.Exp]()
16531578
for (c <- defsToEqs(claim.claims)) {
@@ -1656,7 +1581,7 @@ object Util {
16561581
case _ => return None()
16571582
}
16581583
}
1659-
return Some(bigOrExp(es))
1584+
return Some(AST.Util.bigOr(es, posOpt))
16601585
case claim: State.Claim.Imply =>
16611586
var es = ISZ[AST.Exp]()
16621587
val cs = defsToEqs(claim.claims)
@@ -1673,7 +1598,7 @@ object Util {
16731598
case Some(e) => es = es :+ e
16741599
case _ => return None()
16751600
}
1676-
return Some(bigImplyExp(claim.isCond, es))
1601+
return Some(AST.Util.bigImply(claim.isCond, es, posOpt))
16771602
case claim: State.Claim.Prop =>
16781603
valueToExp(claim.value) match {
16791604
case Some(e) =>
@@ -1689,7 +1614,7 @@ object Util {
16891614
val leftOpt = toExp(State.Claim.And(claim.tClaims))
16901615
val rightOpt = toExp(State.Claim.And(claim.fClaims))
16911616
(condOpt, leftOpt, rightOpt) match {
1692-
case (Some(cond), Some(left), Some(right)) => return Some(constructIf(cond, left, right, posOpt, AST.Typed.bOpt))
1617+
case (Some(cond), Some(left), Some(right)) => return Some(AST.Util.ite(cond, left, right, posOpt, AST.Typed.bOpt))
16931618
case (_, _, _) => return None()
16941619
}
16951620
case claim: State.Claim.Let.CurrentId =>
@@ -1748,7 +1673,7 @@ object Util {
17481673

17491674
for (i <- 0 until claims.size if !ignore(claims(i))) {
17501675
toExp(claims(i)) match {
1751-
case Some(`trueLit`) =>
1676+
case Some(AST.Util.trueLit) =>
17521677
case Some(exp: AST.Exp.Binary) if isEquivLeftRight(exp) =>
17531678
case Some(exp) =>
17541679
r = r :+ exp

0 commit comments

Comments
 (0)