Skip to content
Snippets Groups Projects
Commit 6cdfa722 authored by Romain Ruetschi's avatar Romain Ruetschi :crystal_ball: Committed by Nicolas Voirol
Browse files

Fix always true equality test in Templates

parent eb2c919d
No related branches found
No related tags found
1 merge request!89Fix always true equality test in Templates
......@@ -70,15 +70,17 @@ trait QuantificationTemplates { self: Templates =>
* formula. Positive and negative polarity enable optimizations during
* quantifier instantiation.
*/
sealed abstract class Polarity {
sealed abstract class Polarity(val isPositive: Boolean) {
val isNegative: Boolean = !isPositive
def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): Polarity = this match {
case Positive(subst) => Positive(subst.map(p => p._1 -> p._2.substitute(substituter, msubst)))
case Negative(insts) => Negative(insts._1 -> substituter(insts._2))
}
}
case class Positive(subst: Map[Variable, Arg]) extends Polarity
case class Negative(insts: (Variable, Encoded)) extends Polarity
case class Positive(subst: Map[Variable, Arg]) extends Polarity(true)
case class Negative(insts: (Variable, Encoded)) extends Polarity(false)
class QuantificationTemplate private[QuantificationTemplates] (
val polarity: Polarity,
......
......@@ -770,7 +770,7 @@ trait Templates
// instantiate positive quantifications last to avoid introducing
// extra quantifier instantiations that arise due to empty domains
val (others, positives) = quants.partition(_.polarity != Positive)
val (others, positives) = quants.partition(_.polarity.isNegative)
for (q <- others ++ positives) {
val substMap = subst.mapValues(_.encoded)
val substQuant = q.substitute(mkSubstituter(substMap), matcherSubst)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment