diff --git a/src/multisets/ASTMapaFun.scala b/src/multisets/ASTMapaFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..74ed0240a1d0e69b8c704af374b30960329cb122
--- /dev/null
+++ b/src/multisets/ASTMapaFun.scala
@@ -0,0 +1,43 @@
+package mapaFun
+
+ sealed abstract class MAPAFunInt
+ case class MFIntVar(val i: String) extends MAPAFunInt
+ case class MFIntConst (val c: Int) extends MAPAFunInt
+ case class MFIPlus(val i1: MAPAFunInt, val i2: MAPAFunInt) extends MAPAFunInt
+ case class MFITimes(val c: Int, val i2: MAPAFunInt) extends MAPAFunInt
+ case class MFSCard(val s: MAPAFunSet) extends MAPAFunInt
+ case class MFMCard(val m: MAPAFunMultiset) extends MAPAFunInt
+
+ sealed abstract class MAPAFunMultiset
+ case class MFMSetVar(val m: String) extends MAPAFunMultiset
+ case object MFEmptyMSet extends MAPAFunMultiset
+ case class MFMUnion(val m1: MAPAFunMultiset, val m2: MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFMIntersec(val m1: MAPAFunMultiset, val m2: MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFMPlus(val m1: MAPAFunMultiset, val m2: MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFMMinus(val m1: MAPAFunMultiset, val m2: MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFSetMinus(val m1: MAPAFunMultiset, val m2: MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFSSetOf(val m:MAPAFunMultiset) extends MAPAFunMultiset
+ case class MFFunction(val f: String, val s: MAPAFunSet) extends MAPAFunMultiset
+
+ sealed abstract class MAPAFunSet
+ case class MFSetVar(val s:String) extends MAPAFunSet
+ case object MFEmptySet extends MAPAFunSet
+ case object MFUnivSet extends MAPAFunSet
+ case class MFSUnion(val s1:MAPAFunSet, val s2:MAPAFunSet) extends MAPAFunSet
+ case class MFSIntersec(val s1:MAPAFunSet, val s2:MAPAFunSet) extends MAPAFunSet
+ case class MFSCompl(val s:MAPAFunSet) extends MAPAFunSet
+
+ sealed abstract class MAPAFunAtom
+ case class MFSetEqual(val s1:MAPAFunSet, val s2:MAPAFunSet) extends MAPAFunAtom
+ case class MFSetSubset(val s1:MAPAFunSet, val s2:MAPAFunSet) extends MAPAFunAtom
+ case class MFMSetEqual(val m1:MAPAFunMultiset, val m2:MAPAFunMultiset) extends MAPAFunAtom
+ case class MFMSetSubset(val m1:MAPAFunMultiset, val m2:MAPAFunMultiset) extends MAPAFunAtom
+ case class MFIntEqual(val i1:MAPAFunInt, val i2:MAPAFunInt) extends MAPAFunAtom
+ case class MFIntLessEqual(val i1:MAPAFunInt, val i2:MAPAFunInt) extends MAPAFunAtom
+ case class MFIntDivides(val c:Int, val i:MAPAFunInt) extends MAPAFunAtom
+
+ sealed abstract class MAPAFunFormula
+ case class MFAnd(val f1: MAPAFunFormula, val f2: MAPAFunFormula) extends MAPAFunFormula
+ case class MFOr(val f1: MAPAFunFormula, val f2: MAPAFunFormula) extends MAPAFunFormula
+ case class MFNot(val f: MAPAFunFormula) extends MAPAFunFormula
+ case class MFAtom(val a: MAPAFunAtom) extends MAPAFunFormula
diff --git a/src/multisets/ASTMultisets.scala b/src/multisets/ASTMultisets.scala
new file mode 100644
index 0000000000000000000000000000000000000000..891961b5002ee39598cc038c19edc9005f1a7d3c
--- /dev/null
+++ b/src/multisets/ASTMultisets.scala
@@ -0,0 +1,66 @@
+package multisets
+
+ sealed abstract class Multiset
+ case class MVariable(val v: String) extends Multiset
+ case object MEmpty extends Multiset
+ case class MUnion(val m1: Multiset, val m2: Multiset) extends Multiset
+ case class MIntersection(val m1: Multiset, val m2: Multiset) extends Multiset
+ case class MPlus(val m1: Multiset, val m2: Multiset) extends Multiset
+ case class MMinus(val m1: Multiset, val m2: Multiset) extends Multiset
+ case class MSetMinus(val m1: Multiset, val m2: Multiset) extends Multiset
+ case class MSetOf(val m: Multiset) extends Multiset
+
+ sealed abstract class TermIn
+ case class TIMultiplicity(val v: String) extends TermIn
+ case class TIConstant(val c: Int) extends TermIn
+ case class TIPlus(val t1: TermIn, val t2: TermIn) extends TermIn
+ case class TITimes(val c: Int, val t: TermIn) extends TermIn
+ case class TIIte(val f: FormulaIn, val t1: TermIn, val t2: TermIn) extends TermIn
+
+ sealed abstract class AtomIn
+ case class AILeq(val t1: TermIn, t2: TermIn) extends AtomIn
+ case class AIEq(val t1: TermIn, t2: TermIn) extends AtomIn
+
+ sealed abstract class FormulaIn
+ case class FIAtom(val a: AtomIn) extends FormulaIn
+ case class FIAnd(val f1: FormulaIn, val f2: FormulaIn) extends FormulaIn
+ case class FIOr(val f1: FormulaIn, val f2: FormulaIn) extends FormulaIn
+ case class FINot(val f: FormulaIn) extends FormulaIn
+ case object FITrue extends FormulaIn
+ case object FIFalse extends FormulaIn
+
+
+ sealed abstract class TermOut
+ case class TOConstant(val c: Int) extends TermOut
+ case class TOVariable(val v: String) extends TermOut
+ case class TOCard(val m: Multiset) extends TermOut
+ case class TOPlus(val t1: TermOut, val t2: TermOut) extends TermOut
+ case class TOTimes(val c: Int, val t: TermOut) extends TermOut
+ case class TOIte(val f: FormulaOut, val t1: TermOut, val t2: TermOut) extends TermOut
+
+ sealed abstract class AtomOut
+ case class AOLeq(val t1: TermOut, t2: TermOut) extends AtomOut
+ case class AOEq(val t1: TermOut, t2: TermOut) extends AtomOut
+ case class AOSum(val v1: List[TermOut], val f: FormulaIn, val v2: List[TermIn]) extends AtomOut
+
+ sealed abstract class FormulaOut
+ case class FOAtom(val a: AtomOut) extends FormulaOut
+ case class FOAnd(val f1: FormulaOut, val f2: FormulaOut) extends FormulaOut
+ case class FOOr(val f1: FormulaOut, val f2: FormulaOut) extends FormulaOut
+ case class FONot(val f: FormulaOut) extends FormulaOut
+ case object FOTrue extends FormulaOut
+ case object FOFalse extends FormulaOut
+
+ sealed abstract class Atom
+ case class AEqual(val m1:Multiset, val m2:Multiset) extends Atom
+ case class ASubset(val m1:Multiset, val m2:Multiset) extends Atom
+ case class AForAllElem(val f:FormulaIn) extends Atom
+ case class AAtomOut(val a:AtomOut) extends Atom
+
+ sealed abstract class Formula
+ case class FAnd(val f1: Formula, val f2: Formula) extends Formula
+ case class FOr(val f1: Formula, val f2: Formula) extends Formula
+ case class FNot(val f: Formula) extends Formula
+ case class FAtom(val a: Atom) extends Formula
+ case object FTrue extends Formula
+ case object FFalse extends Formula
diff --git a/src/multisets/ASTStars.scala b/src/multisets/ASTStars.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81fcd4be953d81942099be0b4f9e285945c072d2
--- /dev/null
+++ b/src/multisets/ASTStars.scala
@@ -0,0 +1,23 @@
+package multisets
+
+ sealed abstract class TermQFPA
+ case class TVariable(val v: String) extends TermQFPA
+ case class TConstant(val c: Int) extends TermQFPA
+ case class TPlus(val t1: TermQFPA, val t2: TermQFPA) extends TermQFPA
+ case class TTimes(val c: Int, val t: TermQFPA) extends TermQFPA
+ case class TIte(val f: QFPAFormula, val t1: TermQFPA, val t2: TermQFPA) extends TermQFPA
+
+ sealed abstract class AtomQFPA
+ case class ALeq(val t1: TermQFPA, val t2: TermQFPA) extends AtomQFPA
+ case class AEq(val t1: TermQFPA, val t2: TermQFPA) extends AtomQFPA
+
+ sealed abstract class QFPAFormula
+ case class QFPAAnd(val f1: QFPAFormula, val f2: QFPAFormula) extends QFPAFormula
+ case class QFPAOr(val f1: QFPAFormula, val f2: QFPAFormula) extends QFPAFormula
+ case class QFPANot(val f: QFPAFormula) extends QFPAFormula
+ case class QFPAAtom(val a: AtomQFPA) extends QFPAFormula
+ case object QFPAFalse extends QFPAFormula
+ case object QFPATrue extends QFPAFormula
+
+ // f1 & l1 \in {l2 | f2}*
+ case class StarFormula(val f1: QFPAFormula, val l1: List[TermQFPA], val l2: List[TermQFPA], val f2: QFPAFormula)
diff --git a/src/multisets/BuildingModels.scala b/src/multisets/BuildingModels.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b9e050953f4151127dc4203f6c888ceeca35ce8f
--- /dev/null
+++ b/src/multisets/BuildingModels.scala
@@ -0,0 +1,355 @@
+package multisets
+
+
+import scala.collection.mutable.Map
+import java.lang.Integer
+
+
+
+object reconstructingModels {
+
+ def addNewValuestoMap(l:List[String], i: Int, m: Map[String, Int]): Map[String, Int] = {
+ var mt = m
+ l.foreach(s => mt += (s -> i))
+ mt
+ }
+
+ def getIntValueFromString(s: String): Int = {
+ val s1 = s.replaceAll(":int", "")
+ val n = Integer.parseInt(s1)
+ n
+ }
+
+ def getAllVariablesFromString(s: String): List[String] = {
+ val i1 = s.indexOf('{')
+ val i2 = s.indexOf('}')
+ val s1 = s.substring(i1 + 1, i2)
+ val vars = s1.split(" ")
+ val l1 = vars.toList
+ l1
+ }
+
+
+ def extractModelAndAddtoMap(s: String, m: Map[String, Int]): Map[String, Int] = {
+ if (s.startsWith("*")) {
+ val strings = s.split (" -> ");
+ val l = getAllVariablesFromString(strings(0))
+ val n = getIntValueFromString(strings(1))
+ val m1 = addNewValuestoMap(l, n, m)
+ m1
+ } else m
+ }
+
+ def createSatisfyingAssignmentforQFPA(ls: List[String]): Map[String, Int] = {
+ var tm = Map[String, Int]()
+ ls.foreach(s => {
+ tm = extractModelAndAddtoMap(s, tm)
+ })
+ tm
+ }
+
+// ======================
+
+
+ def replaceVectorsStartingWithSomeStringWithValuesinTerm(t: TermQFPA, m: Map[String, Int], s: String): TermQFPA = t match {
+ case TConstant(c) => t
+ case TVariable(v) => {
+ if (v.contains(s)) {
+ val nv = m(v)
+ TConstant(nv)
+ } else t
+ }
+ case TPlus(t1, t2) => {
+ val t1n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t1, m, s)
+ val t2n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t2, m, s)
+ TPlus(t1n, t2n)
+ }
+ case TTimes(c, t1) => {
+ val t1n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t1, m, s)
+ TTimes(c, t1n)
+ }
+ case TIte(f, t1, t2) => {
+ val fn = replaceVectorsStartingWithSomeStringWithValues(f, m, s)
+ val t1n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t1, m, s)
+ val t2n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t2, m, s)
+ TIte(fn, t1n, t2n)
+ }
+ }
+
+
+ def replaceVectorsStartingWithSomeStringWithValuesinAtom(a: AtomQFPA, m: Map[String, Int], s: String): AtomQFPA = a match {
+ case ALeq(t1,t2) => {
+ val t1n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t1, m, s)
+ val t2n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t2, m, s)
+ ALeq(t1n, t2n)
+ }
+ case AEq(t1,t2) => {
+ val t1n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t1, m, s)
+ val t2n = replaceVectorsStartingWithSomeStringWithValuesinTerm(t2, m, s)
+ AEq(t1n, t2n)
+ }
+ }
+
+ def replaceVectorsStartingWithSomeStringWithValues(f: QFPAFormula, m: Map[String, Int], s: String): QFPAFormula = f match {
+ case QFPAAnd(f1,f2) => {
+ val f1n = replaceVectorsStartingWithSomeStringWithValues(f1, m, s)
+ val f2n = replaceVectorsStartingWithSomeStringWithValues(f2, m, s)
+ QFPAAnd(f1n, f2n)
+ }
+ case QFPAOr(f1,f2) => {
+ val f1n = replaceVectorsStartingWithSomeStringWithValues(f1, m, s)
+ val f2n = replaceVectorsStartingWithSomeStringWithValues(f2, m, s)
+ QFPAOr(f1n, f2n)
+ }
+ case QFPANot(f1) => {
+ val f1n = replaceVectorsStartingWithSomeStringWithValues(f1, m, s)
+ QFPANot(f1n)
+ }
+ case QFPAAtom(a) => {
+ val a1 = replaceVectorsStartingWithSomeStringWithValuesinAtom(a, m, s)
+ QFPAAtom(a1)
+ }
+ case QFPAFalse => f
+ case QFPATrue => f
+ }
+
+ def isNumericalTerm(t: TermQFPA): (Boolean, Int) = t match {
+ case TConstant(c) => (true, c)
+ case TVariable(v) => (false, 0)
+ case TPlus(t1, t2) => {
+ val (b1, c1) = isNumericalTerm(t1)
+ val (b2, c2) = isNumericalTerm(t2)
+ (b1 && b2, c1 + c2)
+ }
+ case TTimes(c, t1) => {
+ val (b1, c1) = isNumericalTerm(t1)
+ (b1, c * c1)
+ }
+ case TIte(f, t1, t2) => {
+ val f1 = evaluatePureNumericalExpressions(f)
+ val (b1, c1) = isNumericalTerm(t1)
+ val (b2, c2) = isNumericalTerm(t2)
+ val f2 = evaluatePureBooleanExpressions(f1)
+ if (f2 == QFPATrue) (b1, c1) else
+ if (f2 == QFPANot(QFPATrue)) (b2, c2) else
+ (false, 0)
+ }
+ }
+
+ def evaluatePureNumericalExpressioninTerm(t: TermQFPA): TermQFPA = t match {
+ case TConstant(c) => t
+ case TVariable(v) => t
+ case TPlus(t1, t2) => {
+ val t1n = evaluatePureNumericalExpressioninTerm(t1)
+ val t2n = evaluatePureNumericalExpressioninTerm(t2)
+ val (b1, c1) = isNumericalTerm(t1n)
+ val (b2, c2) = isNumericalTerm(t2n)
+ if (b1 && b2) {
+ val c = c1 + c2
+ TConstant(c)
+ } else { if (b1 && c1 == 0) t2n
+ else if (b2 && c2 == 0) t1n else TPlus(t1n, t2n)
+ }
+ }
+ case TTimes(c, t1) => {
+ val t1n = evaluatePureNumericalExpressioninTerm(t1)
+ val (b1, c1) = isNumericalTerm(t1n)
+ if (b1) {
+ val cf = c * c1
+ TConstant(cf)
+ } else TTimes(c, t1n)
+ }
+ case TIte(f, t1, t2) => {
+ val f1 = evaluatePureNumericalExpressions(f)
+ val t1n = evaluatePureNumericalExpressioninTerm(t1)
+ val t2n = evaluatePureNumericalExpressioninTerm(t2)
+ val f2 = evaluatePureBooleanExpressions(f1)
+ if (f2 == QFPATrue) t1n else
+ if (f2 == QFPANot(QFPATrue)) t2n else
+ TIte(f2, t1n, t2n)
+ }
+ }
+
+ def evaluatePureNumericalExpressioninAtom(a: AtomQFPA): AtomQFPA = a match {
+ case ALeq(t1,t2) => {
+ val t1n = evaluatePureNumericalExpressioninTerm(t1)
+ val t2n = evaluatePureNumericalExpressioninTerm(t2)
+ ALeq(t1n, t2n)
+ }
+ case AEq(t1,t2) => {
+ val t1n = evaluatePureNumericalExpressioninTerm(t1)
+ val t2n = evaluatePureNumericalExpressioninTerm(t2)
+ AEq(t1n, t2n)
+ }
+ }
+
+ def evaluatePureNumericalExpressions(f: QFPAFormula): QFPAFormula = f match {
+ case QFPAAnd(f1,f2) => {
+ val f1n = evaluatePureNumericalExpressions(f1)
+ val f2n = evaluatePureNumericalExpressions(f2)
+ QFPAAnd(f1n, f2n)
+ }
+ case QFPAOr(f1,f2) => {
+ val f1n = evaluatePureNumericalExpressions(f1)
+ val f2n = evaluatePureNumericalExpressions(f2)
+ QFPAOr(f1n, f2n)
+ }
+ case QFPANot(f1) => {
+ val f1n = evaluatePureNumericalExpressions(f1)
+ QFPANot(f1n)
+ }
+ case QFPAAtom(a) => {
+ val a1 = evaluatePureNumericalExpressioninAtom(a)
+ QFPAAtom(a1)
+ }
+ case QFPAFalse => f
+ case QFPATrue => f
+ }
+
+
+
+ def evaluatePureBooleanExpressionsinAtom(a: AtomQFPA): QFPAFormula = a match {
+ case ALeq(t1, t2) => {
+ if (t1 == t2) QFPATrue else {
+ val (b1, c1) = isNumericalTerm(t1)
+ val (b2, c2) = isNumericalTerm(t2)
+ if (b1 && b2) {
+ if (c1 <= c2) QFPATrue else QFPANot(QFPATrue)
+ } else QFPAAtom(a)
+ }
+ }
+ case AEq(t1,t2) => {
+ if (t1 == t2) QFPATrue else {
+ val (b1, c1) = isNumericalTerm(t1)
+ val (b2, c2) = isNumericalTerm(t2)
+ if (b1 && b2) {
+ if (c1 == c2) QFPATrue else QFPANot(QFPATrue)
+ } else QFPAAtom(a)
+ }
+ }
+ }
+
+
+ def evaluatePureBooleanExpressions(f: QFPAFormula): QFPAFormula = f match {
+ case QFPAAnd(f1,f2) => {
+ val f1n = evaluatePureBooleanExpressions(f1)
+ val f2n = evaluatePureBooleanExpressions(f2)
+ if (f1n == QFPANot(QFPATrue) || f2n == QFPANot(QFPATrue)) QFPANot(QFPATrue) else
+ if (f1n == QFPATrue) f2n else
+ if (f2n == QFPATrue) f1n else
+ QFPAAnd(f1n, f2n)
+ }
+ case QFPAOr(f1,f2) => {
+ val f1n = evaluatePureBooleanExpressions(f1)
+ val f2n = evaluatePureBooleanExpressions(f2)
+ if (f1n == QFPATrue || f2n == QFPATrue) QFPATrue else
+ if (f1n == QFPANot(QFPATrue)) f2n else
+ if (f2n == QFPANot(QFPATrue)) f1n else
+ QFPAOr(f1n, f2n)
+ }
+ case QFPANot(f1) => {
+ val f1n = evaluatePureBooleanExpressions(f1)
+ val f2n = f1n match {
+ case QFPANot(f3n) => f3n
+ case _ => QFPANot(f1n)
+ }
+ f2n
+ }
+ case QFPAAtom(a) => evaluatePureBooleanExpressionsinAtom(a)
+ case QFPAFalse => f
+ case QFPATrue => f
+ }
+
+
+ def simplifyArithmeticExpressionsInQFPA(f: QFPAFormula): QFPAFormula = {
+ val f1 = evaluatePureNumericalExpressions(f)
+ val f2 = evaluatePureBooleanExpressions(f1)
+ f2
+ }
+
+
+ def evaluateFormulaForVariablesStartingWith(f: QFPAFormula, m: Map[String, Int], s: String): QFPAFormula = {
+ val f1 = replaceVectorsStartingWithSomeStringWithValues(f, m, s)
+ val f2 = simplifyArithmeticExpressionsInQFPA(f1)
+ f2
+ }
+
+
+// ===========================
+
+ def deriveValueofVarTermInModel(t: TermQFPA, m: Map[String, Int]): Int = t match {
+ case TConstant(c) => c
+ case TVariable(v) => m(v)
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def isNulVectorinGivenModel(t: List[TermQFPA], m: Map[String, Int]): Boolean = {
+ val t1 = t.map(tm => deriveValueofVarTermInModel(tm, m))
+ t1.forall(tm => (tm == 0))
+ }
+
+
+
+ def replaceAllTermsWithZeroinTerm(t: TermQFPA, l: List[TermQFPA]): TermQFPA = t match {
+ case TConstant(c) => t
+ case TVariable(v) => if (l.contains(t)) TConstant(0) else t
+ case TPlus(t1, t2) => {
+ val t1n = replaceAllTermsWithZeroinTerm(t1, l)
+ val t2n = replaceAllTermsWithZeroinTerm(t2, l)
+ TPlus(t1n, t2n)
+ }
+ case TTimes(c, t1) => {
+ val t1n = replaceAllTermsWithZeroinTerm(t1, l)
+ TTimes(c, t1n)
+ }
+ case TIte(f, t1, t2) => {
+ val fn = replaceAllTermsWithZero(f, l)
+ val t1n = replaceAllTermsWithZeroinTerm(t1, l)
+ val t2n = replaceAllTermsWithZeroinTerm(t2, l)
+ TIte(fn, t1n, t2n)
+ }
+ }
+
+ def replaceAllTermsWithZeroinAtom(a: AtomQFPA, t: List[TermQFPA]): AtomQFPA = a match {
+ case ALeq(t1,t2) => {
+ val t1n = replaceAllTermsWithZeroinTerm(t1, t)
+ val t2n = replaceAllTermsWithZeroinTerm(t2, t)
+ ALeq(t1n, t2n)
+ }
+ case AEq(t1,t2) => {
+ val t1n = replaceAllTermsWithZeroinTerm(t1, t)
+ val t2n = replaceAllTermsWithZeroinTerm(t2, t)
+ AEq(t1n, t2n)
+ }
+ }
+
+ def replaceAllTermsWithZero(f: QFPAFormula, t: List[TermQFPA]): QFPAFormula = f match {
+ case QFPAAnd(f1,f2) => {
+ val f1n = replaceAllTermsWithZero(f1, t)
+ val f2n = replaceAllTermsWithZero(f2, t)
+ QFPAAnd(f1n, f2n)
+ }
+ case QFPAOr(f1,f2) => {
+ val f1n = replaceAllTermsWithZero(f1, t)
+ val f2n = replaceAllTermsWithZero(f2, t)
+ QFPAOr(f1n, f2n)
+ }
+ case QFPANot(f1) => {
+ val f1n = replaceAllTermsWithZero(f1, t)
+ QFPANot(f1n)
+ }
+ case QFPAAtom(a) => {
+ val a1 = replaceAllTermsWithZeroinAtom(a, t)
+ QFPAAtom(a1)
+ }
+ case QFPAFalse => f
+ case QFPATrue => f
+ }
+
+ def removeZeroVectorInFormula(f: QFPAFormula, t: List[TermQFPA]): QFPAFormula = {
+ val f1 = replaceAllTermsWithZero(f, t)
+ val f2 = simplifyArithmeticExpressionsInQFPA(f1)
+ f2
+ }
+}
+
diff --git a/src/multisets/CheckingConsistency.scala b/src/multisets/CheckingConsistency.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da91e6457bb711fbdddce42ff0de6a3ba906d351
--- /dev/null
+++ b/src/multisets/CheckingConsistency.scala
@@ -0,0 +1,357 @@
+package multisets
+import scala.collection.mutable.Map
+import scala.collection.mutable.Set
+//import java.io._
+
+import z3.scala._
+
+object CheckingConsistency {
+
+
+
+
+/*
+
+
+
+ def createVariableString(va:Array[String]):String = {
+ var s = ""
+ va.foreach(v => s = s + "(" + v + " Int) ")
+ s
+ }
+
+
+ def createSMTRepresentationOfTerm(t:TermQFPA):String = t match {
+ case TVariable(v) => v
+ case TConstant(c) => c.toString
+ case TPlus(t1, t2) => {
+ val s1 = createSMTRepresentationOfTerm(t1)
+ val s2 = createSMTRepresentationOfTerm(t2)
+ "(+ " + s1 + " " + s2 + ")"
+ }
+ case TTimes(c, t1) => {
+ val s1 = createSMTRepresentationOfTerm(t1)
+ "(* " + c.toString + " " + s1 + ")"
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def createSMTRepresentationOfAtom(a:AtomQFPA):String = a match {
+ case ALeq(t1, t2) => {
+ val s1 = createSMTRepresentationOfTerm(t1)
+ val s2 = createSMTRepresentationOfTerm(t2)
+ "(<= " + s1 + " " + s2 + ")"
+ }
+ case AEq(t1, t2) => {
+ val s1 = createSMTRepresentationOfTerm(t1)
+ val s2 = createSMTRepresentationOfTerm(t2)
+ "(= " + s1 + " " + s2 + ")"
+ }
+ }
+
+ def createSMTRepresentationOfFormula(f:QFPAFormula):String = {
+ val s = f match {
+ case QFPAAnd(f1, f2) => {
+ val s1 = createSMTRepresentationOfFormula(f1)
+ val s2 = createSMTRepresentationOfFormula(f2)
+ "and " + s1 + " " + s2
+ }
+ case QFPAOr(f1, f2) => {
+ val s1 = createSMTRepresentationOfFormula(f1)
+ val s2 = createSMTRepresentationOfFormula(f2)
+ "or " + s1 + " " + s2
+ }
+ case QFPANot(f1) => {
+ val s1 = createSMTRepresentationOfFormula(f1)
+ "not " + s1
+ }
+ case QFPAAtom(a) => createSMTRepresentationOfAtom(a)
+ case _ => " "
+ }
+ "( " + s + " )"
+ }
+
+
+ def callZ3toDetermineConsistency(c:List[QFPAFormula]):String = {
+ val smtfile = File.createTempFile("iteremove", ".smt");
+ val smtfileName = smtfile.getAbsolutePath
+
+ val vars = getAllVariablesFromListofFormulas(c)
+ val s1 = createVariableString(vars)
+
+ val out = new BufferedWriter(new FileWriter(smtfile))
+ out.write("(benchmark example")
+ out.newLine()
+ out.write(":logic QF_LIA")
+ out.newLine()
+ out.write(":extrafuns (")
+ out.write(s1)
+ out.write(")")
+ out.newLine()
+ out.write(":formula (and")
+ out.newLine()
+ vars.foreach (v => {
+ out.write("(<= 0 " + v + " )" )
+ out.newLine()
+ })
+ c.foreach(g => {
+ val sg = createSMTRepresentationOfFormula(g)
+ out.write(sg)
+ out.newLine()
+ })
+ out.write(")")
+ out.newLine()
+ out.write(")")
+ out.newLine()
+ out.close
+
+ val cmd = Array("z3.exe.linux", smtfileName)
+ val p: Process = Runtime.getRuntime.exec(cmd)
+ val input: BufferedReader = new BufferedReader(new InputStreamReader(p.getInputStream()))
+ val line: String = input.readLine
+ p.waitFor
+ input.close
+
+ smtfile.deleteOnExit
+ line
+ }
+
+
+ def checkConsistencyofOneFormula(f:QFPAFormula): List[String] = {
+ val smtfile = File.createTempFile("finalFormula", ".smt");
+ val smtfileName = smtfile.getAbsolutePath
+
+ val vars = getAllVariablesFromOneFormula(f)
+ val s1 = createVariableString(vars)
+
+ val out = new BufferedWriter(new FileWriter(smtfile))
+ out.write("(benchmark example")
+ out.newLine()
+ out.write(":logic QF_LIA")
+ out.newLine()
+ out.write(":extrafuns (")
+ out.write(s1)
+ out.write(")")
+ out.newLine()
+ out.write(":formula (and")
+ out.newLine()
+ vars.foreach (v => {
+ out.write("(<= 0 " + v + " )" )
+ out.newLine()
+ })
+ val sg = createSMTRepresentationOfFormula(f)
+ out.write(sg)
+ out.newLine()
+ out.write(")")
+ out.newLine()
+ out.write(")")
+ out.newLine()
+ out.close
+
+ val cmd = Array("z3", "-m", smtfileName)
+ val p: Process = Runtime.getRuntime.exec(cmd)
+ val input: BufferedReader = new BufferedReader(new InputStreamReader(p.getInputStream()))
+ var line = input.readLine()
+ var l: List[String] = Nil
+ while (line != null) {
+ l = line :: l
+ line = input.readLine()
+ }
+ p.waitFor
+ input.close
+
+ smtfile.deleteOnExit
+ l
+ } */
+
+
+// start: getting out all variables
+
+ def getAllVariablesAndConstsFromTerm(t:TermQFPA):(Set[String], Set[Int]) = t match {
+ case TVariable(v) => (Set(v), Set[Int]())
+ case TConstant(c) => (Set[String](), Set(c))
+ case TPlus(t1, t2) => {
+ val p1 = getAllVariablesAndConstsFromTerm(t1)
+ val p2 = getAllVariablesAndConstsFromTerm(t2)
+ (p1._1 ++ p2._1, p1._2 ++ p2._2)
+ }
+ case TTimes(c, t1) => {
+ val p1 = getAllVariablesAndConstsFromTerm(t1)
+ (p1._1, p1._2 ++ Set(c))
+ }
+ case TIte(f, t1, t2) => {
+ val p0 = getAllVariablesAndConstsFromFormula(f)
+ val p1 = getAllVariablesAndConstsFromTerm(t1)
+ val p2 = getAllVariablesAndConstsFromTerm(t2)
+ (p0._1 ++ p1._1 ++ p2._1, p0._2 ++ p1._2 ++ p2._2)
+ }
+ }
+
+ def getAllVariablesAndConstsFromAtom(a:AtomQFPA):(Set[String], Set[Int]) = a match {
+ case ALeq(t1, t2) => {
+ val p1 = getAllVariablesAndConstsFromTerm(t1)
+ val p2 = getAllVariablesAndConstsFromTerm(t2)
+ (p1._1 ++ p2._1, p1._2 ++ p2._2)
+ }
+ case AEq(t1, t2) => {
+ val p1 = getAllVariablesAndConstsFromTerm(t1)
+ val p2 = getAllVariablesAndConstsFromTerm(t2)
+ (p1._1 ++ p2._1, p1._2 ++ p2._2)
+ }
+ }
+
+ def getAllVariablesAndConstsFromFormula(f:QFPAFormula):(Set[String], Set[Int]) = f match {
+ case QFPAAnd(f1, f2) => {
+ val p1 = getAllVariablesAndConstsFromFormula(f1)
+ val p2 = getAllVariablesAndConstsFromFormula(f2)
+ (p1._1 ++ p2._1, p1._2 ++ p2._2)
+ }
+ case QFPAOr(f1, f2) => {
+ val p1 = getAllVariablesAndConstsFromFormula(f1)
+ val p2 = getAllVariablesAndConstsFromFormula(f2)
+ (p1._1 ++ p2._1, p1._2 ++ p2._2)
+ }
+ case QFPANot(f1) => getAllVariablesAndConstsFromFormula(f1)
+ case QFPAAtom(a) => getAllVariablesAndConstsFromAtom(a)
+ case QFPAFalse => (Set[String](), Set[Int]())
+ case QFPATrue => (Set[String](), Set[Int]())
+ }
+
+
+ def getAllVariablesAndConstsFromListofFormulas(c:List[QFPAFormula]): (Set[String], Set[Int]) = {
+ var p = (Set[String](), Set[Int]())
+ c.foreach(g => {
+ val p1 = getAllVariablesAndConstsFromFormula(g)
+ p = (p._1 ++ p1._1, p._2 ++ p1._2)
+ })
+ p
+ }
+
+// end
+
+
+
+ def mkASTTerm(t:TermQFPA, s: Z3Sort, z3: Z3Context): (Z3AST, Z3Sort, Z3Context) = t match {
+ case TConstant(c) => (z3.mkInt(c, s), s, z3)
+ case TVariable(v) => (z3.mkConst(z3.mkStringSymbol(v), s), s, z3)
+ case TPlus(t1, t2) => {
+ val t1N = mkASTTerm(t1, s, z3)._1
+ val t2N = mkASTTerm(t2, s, z3)._1
+ (z3.mkAdd(t1N, t2N), s, z3)
+ }
+ case TTimes(c, t1)=> {
+ val cN = z3.mkInt(c, s)
+ val t1N = mkASTTerm(t1, s, z3)._1
+ (z3.mkMul(cN, t1N), s, z3)
+ }
+ case TIte(f, t1, t2)=> {
+ val fN = mkAST(f, s, z3)._1
+ val t1N = mkASTTerm(t1, s, z3)._1
+ val t2N = mkASTTerm(t2, s, z3)._1
+ (z3.mkITE(fN, t1N, t2N), s, z3)
+ }
+ }
+
+ def mkASTAtom(a:AtomQFPA, s: Z3Sort, z3: Z3Context): (Z3AST, Z3Sort, Z3Context) = a match {
+ case ALeq(t1,t2) => {
+ val t1N = mkASTTerm(t1, s, z3)._1
+ val t2N = mkASTTerm(t2, s, z3)._1
+ (z3.mkLE(t1N, t2N), s, z3)
+ }
+ case AEq(t1,t2) => {
+ val t1N = mkASTTerm(t1, s, z3)._1
+ val t2N = mkASTTerm(t2, s, z3)._1
+ (z3.mkEq(t1N, t2N), s, z3)
+ }
+ }
+
+ def mkAST(f: QFPAFormula, s: Z3Sort, z3: Z3Context): (Z3AST, Z3Sort, Z3Context) = f match {
+ case QFPAAnd(f1,f2) => {
+ val f1N = mkAST(f1, s, z3)._1
+ val f2N = mkAST(f2, s, z3)._1
+ (z3.mkAnd(f1N, f2N), s, z3)
+ }
+ case QFPAOr(f1,f2) => {
+ val f1N = mkAST(f1, s, z3)._1
+ val f2N = mkAST(f2, s, z3)._1
+ (z3.mkOr(f1N, f2N), s, z3)
+ }
+ case QFPANot(f1) => (z3.mkNot(mkAST(f1, s, z3)._1), s, z3)
+ case QFPAAtom(a) => mkASTAtom(a, s, z3)
+ case QFPAFalse => (z3.mkFalse, s, z3)
+ case QFPATrue => (z3.mkTrue, s, z3)
+ }
+
+
+ def callZ3NewWaytoDetermineConsistency(c:List[QFPAFormula]): Boolean = {
+ val z3 = new Z3Context((new Z3Config).setParamValue("MODEL", "false"))
+ val i = z3.mkIntSort
+
+ val z3formulasPairs = c.map(f => mkAST(f, i, z3))
+ val z3formulas = z3formulasPairs.map(f => f._1)
+ z3formulas.foreach(f => z3.assertCnstr(f))
+
+ val b = z3.check() match {
+ case Some(x) => x
+ case None => error("There was an error with Z3.")
+ }
+ z3.delete
+ b
+ }
+
+
+/////////
+
+
+ def callZ3NewWaytoCheckConsistencyofOneFormula(f:QFPAFormula):(Boolean, Map[String, Int]) = {
+ val z3 = new Z3Context((new Z3Config).setParamValue("MODEL", "true"))
+ val i = z3.mkIntSort
+
+ val vars = getAllVariablesAndConstsFromFormula(f)._1
+ val varMap = Map.empty[String,Z3AST]
+
+ vars.foreach(v => {
+ if(!varMap.keySet.contains(v)) {
+ val ast = z3.mkConst(z3.mkStringSymbol(v), i)
+ varMap(v) = ast
+ }
+ })
+
+ val z3formulaTuple = mkAST(f, i, z3)
+ val z3formula = z3formulaTuple._1
+ z3.assertCnstr(z3formula)
+
+ val (res, model) = z3.checkAndGetModel()
+
+ val out = res match {
+ case Some(false) => (false, Map.empty[String,Int])
+ case Some(true) => (true, Map.empty[String,Int] ++ varMap.map(p => (p._1, model.evalAsInt(p._2).get)))
+ case None => error("There was an error with Z3.")
+ }
+ out
+ }
+
+
+
+
+//------------------------------------------
+// old names keep consistency with old calls
+//------------------------------------------
+
+
+// calls Z3 on list of formulas and returns "sat" or "unsat"
+ def callZ3toDetermineConsistency(c:List[QFPAFormula]):String = {
+ val b = callZ3NewWaytoDetermineConsistency(c)
+ val s = if (b == true) "sat" else "unsat"
+ s
+ }
+
+
+// calls z3 on One formula and return a model and "sat" or "unsat"
+ def checkConsistencyofOneFormula(f:QFPAFormula): (String, Map[String, Int]) = {
+ val p = callZ3NewWaytoCheckConsistencyofOneFormula(f)
+ val res = if (p._1 == true) ("sat", p._2) else ("unsat", p._2)
+ res
+ }
+
+}
diff --git a/src/multisets/CreateDisjunctions.scala b/src/multisets/CreateDisjunctions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..444de613ffa8a877e5a70a38f0baa5ad38fe4ee3
--- /dev/null
+++ b/src/multisets/CreateDisjunctions.scala
@@ -0,0 +1,729 @@
+package multisets
+
+
+import scala.collection.mutable.Set
+
+
+object CreateDisjunctions {
+
+// start: input formula
+// output: formula without ITE Expresssions and formula denoting ITE experssions
+
+ def flattenITEExpressionsTerm(t:TermQFPA, vc:Int, il:List[(String,TermQFPA)]):(TermQFPA,Int,List[(String,TermQFPA)]) = t match {
+ case TPlus(t1, t2) => {
+ val (t1N, vc1, il1) = flattenITEExpressionsTerm(t1, vc, il)
+ val (t2N, vc2, il2) = flattenITEExpressionsTerm(t2, vc1, il1)
+ (TPlus(t1N, t2N), vc2, il2)
+ }
+ case TTimes(c, t1) => {
+ val (t1N, vc1, il1) = flattenITEExpressionsTerm(t1, vc, il)
+ (TTimes(c, t1N), vc1, il1)
+ }
+ case TIte(f, t1, t2) => {
+ val newITEVar = "FRESHv" + vc
+ var il1 = (newITEVar, t) :: il
+ (TVariable(newITEVar), vc + 1, il1)
+ }
+ case _ => (t, vc, il)
+ }
+
+ def flattenITEExpressionsAtom(a:AtomQFPA, vc:Int, il:List[(String,TermQFPA)]):(QFPAFormula,Int,List[(String,TermQFPA)]) = a match {
+ case ALeq(t1, t2) => {
+ val (t1N, vc1, il1) = flattenITEExpressionsTerm(t1, vc, il)
+ val (t2N, vc2, il2) = flattenITEExpressionsTerm(t2, vc1, il1)
+ (QFPAAtom(ALeq(t1N, t2N)), vc2, il2)
+ }
+ case AEq(t1, t2) => {
+ val (t1N, vc1, il1) = flattenITEExpressionsTerm(t1, vc, il)
+ val (t2N, vc2, il2) = flattenITEExpressionsTerm(t2, vc1, il1)
+ (QFPAAtom(AEq(t1N, t2N)), vc2, il2)
+ }
+ }
+
+ def flattenITEExpressionsFormula(f:QFPAFormula, vc:Int, il:List[(String,TermQFPA)]):(QFPAFormula,Int,List[(String,TermQFPA)]) = f match {
+ case QFPAAnd(f1, f2) => {
+ val (f1N, vc1, il1) = flattenITEExpressionsFormula(f1, vc, il)
+ val (f2N, vc2, il2) = flattenITEExpressionsFormula(f2, vc1, il1)
+ (QFPAAnd(f1N, f2N), vc2, il2)
+ }
+ case QFPAOr(f1, f2) => {
+ val (f1N, vc1, il1) = flattenITEExpressionsFormula(f1, vc, il)
+ val (f2N, vc2, il2) = flattenITEExpressionsFormula(f2, vc1, il1)
+ (QFPAOr(f1N, f2N), vc2, il2)
+ }
+ case QFPANot(f1) => {
+ val (f1N, vc1, il1) = flattenITEExpressionsFormula(f1, vc, il)
+ (QFPANot(f1N), vc1, il1)
+ }
+ case QFPAAtom(a) => flattenITEExpressionsAtom(a, vc, il)
+ case _ => (f, vc, il)
+ }
+
+ def flatten_ITEList(il:List[(String,TermQFPA)],ic:Int, toBeFlattened: Boolean):List[(String,TermQFPA)] = {
+ var addedFreshITEs = false
+ var ilN:List[(String,TermQFPA)] = Nil
+ var icN = ic
+ if (toBeFlattened) {
+ il.foreach(p => p._2 match {
+ case TIte(f, t1, t2) => {
+ var iltmp:List[(String,TermQFPA)] = Nil
+ val (fF, ic1, il1) = flattenITEExpressionsFormula(f, icN, iltmp)
+ val (t1F, ic2, il2) = flattenITEExpressionsTerm(t1, ic1, il1)
+ val (t2F, ic3, il3) = flattenITEExpressionsTerm(t2, ic2, il2)
+ if (il3.isEmpty) {
+ ilN = p :: ilN
+ } else {
+ val newITEVar = "FRESHv" + ic3
+ icN = ic3 + 1
+ ilN = il3 ::: ilN
+ ilN = (newITEVar, TIte(fF, t1F, t2F)) :: ilN
+ addedFreshITEs = true
+ }
+ }
+ case _ => error("Impossible case ")
+ })
+ flatten_ITEList(ilN, icN, addedFreshITEs)
+ } else il
+ }
+
+
+ def flattenITEExpressions(f:QFPAFormula):(QFPAFormula, List[(String,TermQFPA)]) = {
+ var variableCount = 0
+ var iteList:List[(String,TermQFPA)] = Nil
+ val (f1, vc1, iteList1) = flattenITEExpressionsFormula(f, variableCount, iteList)
+ // every ITE is pulled out
+ val toBeFlattened = true
+ val iteListFinal = flatten_ITEList(iteList1, vc1, toBeFlattened)
+ (f1, iteListFinal)
+ }
+
+// end
+
+//--------------
+
+//start: v - list of (complex) terms
+// output: $1 - formula describing freshly introduced terms
+ def flattenComplexTerms(v:List[TermQFPA]):(QFPAFormula,List[TermQFPA]) = {
+ var tc = 0
+ var tempForm:QFPAFormula = QFPATrue
+ var tempVector:List[TermQFPA] = Nil
+ v.foreach(t => t match {
+ case TVariable(v) => tempVector = t :: tempVector
+ case TConstant(c) => tempVector = t :: tempVector
+ case _ => {
+ val newTermVar = "FRESHt" + tc
+ val fTemp = QFPAAtom(AEq(TVariable(newTermVar), t))
+ tempForm = QFPAAnd(tempForm, fTemp)
+ tempVector = TVariable(newTermVar) :: tempVector
+ tc = tc + 1
+ }
+ })
+ val fN = multisets.Multiset2StarsTranslator.removeTrueAndFalse(tempForm)
+ val tN = tempVector.reverse
+ (fN, tN)
+ }
+//end
+
+
+// ------------
+// start: input f AND l (l = list of conjunction of equlities about ITE)
+//output: DNF of f AND f1 in form List[List[formula]]
+ def nnform(f:QFPAFormula):QFPAFormula = f match {
+ case QFPANot(QFPANot(f1)) => nnform(f1)
+ case QFPANot(QFPAAnd(f1, f2)) => QFPAOr(QFPANot(nnform(f1)), QFPANot(nnform(f2)))
+ case QFPANot(QFPAOr(f1, f2)) => QFPAAnd(QFPANot(nnform(f1)), QFPANot(nnform(f2)))
+ case QFPAAnd(f1, f2) => QFPAAnd(nnform(f1), nnform(f2))
+ case QFPAOr(f1, f2) => QFPAOr(nnform(f1), nnform(f2))
+ case QFPANot(f1) => QFPANot(nnform(f1))
+ case _ => f
+ }
+
+ def removeNegationFromNegatedAtom(a:AtomQFPA):QFPAFormula = a match {
+ case ALeq(t1, t2) => QFPAAtom(ALeq(TPlus(t2, TConstant(1)), t1))
+ case AEq(t1, t2) => QFPAOr(
+ QFPAAtom(ALeq(TPlus(t1, TConstant(1)), t2)),
+ QFPAAtom(ALeq(TPlus(t2, TConstant(1)), t1))
+ )
+ }
+
+ def removeNegationCompletely(f:QFPAFormula):QFPAFormula = f match {
+ case QFPAAnd(f1, f2) => QFPAAnd(removeNegationCompletely(f1), removeNegationCompletely(f2))
+ case QFPAOr(f1, f2) => QFPAOr(removeNegationCompletely(f1), removeNegationCompletely(f2))
+ case QFPANot(QFPAAtom(a)) => removeNegationFromNegatedAtom(a)
+ case QFPANot(QFPATrue) => QFPAFalse
+ case QFPANot(QFPAFalse) => QFPATrue
+ case _ => f
+ }
+
+
+ def mergeTwoConjuntions(d1:List[QFPAFormula], d2:List[QFPAFormula]): List[List[QFPAFormula]] = {
+ val ln = d1 ::: d2
+ List(ln)
+ }
+
+ def addOneDisjuntToWholeFormula(l:List[List[QFPAFormula]], c:List[QFPAFormula]): List[List[QFPAFormula]] = {
+ var lt: List[List[QFPAFormula]] = Nil
+ l.foreach(s => {
+ val fn = mergeTwoConjuntions(s, c)
+ lt = fn ::: lt
+ })
+ lt
+ }
+
+ def mergeTwoDisjunctions(l1: List[List[QFPAFormula]], l2: List[List[QFPAFormula]]): List[List[QFPAFormula]] = {
+ var lt: List[List[QFPAFormula]] = Nil
+ l2.foreach(s => {
+ val ln = addOneDisjuntToWholeFormula(l1, s)
+ lt = ln ::: lt
+ })
+ lt
+ }
+
+
+ def disjuntiveNormalForm(f:QFPAFormula): List[List[QFPAFormula]] = {
+ val f1 = nnform(f)
+ val f2 = removeNegationCompletely(f1)
+ val f3 = f2 match {
+ case QFPAAnd(fa, fb) => {
+ val f1N = disjuntiveNormalForm(fa)
+ val f2N = disjuntiveNormalForm(fb)
+ mergeTwoDisjunctions(f1N, f2N)
+ }
+ case QFPAOr(fa, fb) => {
+ val f1N = disjuntiveNormalForm(fa)
+ val f2N = disjuntiveNormalForm(fb)
+ f1N ::: f2N
+ }
+ case _ => List(List(f2))
+ }
+ f3
+ }
+
+
+// -------------------------
+
+
+ def mergeTogether(c:List[QFPAFormula],f:List[List[QFPAFormula]]):List[List[QFPAFormula]] = {
+ val list1 = f.map(d => c ::: d)
+ list1
+ }
+
+ def addITEExpressionToOneDisjunct(c:List[QFPAFormula], p:(String,TermQFPA)): List[List[QFPAFormula]] = {
+ val lN = p._2 match {
+ case TIte(f, t1, t2) => {
+ val f1 = disjuntiveNormalForm(f)
+ val f2 = disjuntiveNormalForm(QFPANot(f))
+ val c1 = QFPAAtom(AEq(TVariable(p._1), t1)) :: c
+ val c2 = QFPAAtom(AEq(TVariable(p._1), t2)) :: c
+ val l1 = mergeTogether(c1, f1)
+ val l2 = mergeTogether(c2, f2)
+ l1 ::: l2
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+ lN
+ }
+
+ def evaluateITEExpressionInListOfDisjunctions(l: List[List[QFPAFormula]], t:(String,TermQFPA)): List[List[QFPAFormula]] = {
+ var lt: List[List[QFPAFormula]] = Nil
+ l.foreach(s => {
+ val ln = addITEExpressionToOneDisjunct(s, t)
+ lt = ln ::: lt
+ })
+ lt
+ }
+
+ def unrollITEExpressions(f:QFPAFormula,lITE: List[(String,TermQFPA)]): List[List[QFPAFormula]] = {
+ val fN = disjuntiveNormalForm(f)
+ var lTemp = fN
+ lITE.foreach(t => {
+ val lNew = evaluateITEExpressionInListOfDisjunctions(lTemp, t)
+ lTemp = lNew
+ })
+ lTemp
+ }
+
+// end
+
+
+
+
+
+// ------------------
+
+/// STRT: to be considered!
+
+ def replaceInequalitiesWithEqualitiesinAtom(a:AtomQFPA, lc:Int):(AtomQFPA,Int) = a match {
+ case ALeq(t1, t2) => {
+ val newTermVar = "FRESHl" + lc
+ val newRHS = TPlus(t1, TVariable(newTermVar))
+ (AEq(t2, newRHS), lc + 1)
+ }
+ case AEq(t1, t2) => (a, lc)
+ }
+
+ def replaceInequalitiesWithEqualitiesinOneSingleFormula(f:QFPAFormula, lc:Int):(QFPAFormula,Int) = f match {
+ case QFPAAtom(a) => {
+ val (a1, lc1) = replaceInequalitiesWithEqualitiesinAtom(a, lc)
+ (QFPAAtom(a1), lc1)
+ }
+ case QFPATrue => (f, lc)
+ case _ => error("Impossible case ")
+ }
+
+ def replaceInequalitiesWithEqualitiesinConjunct(l:List[QFPAFormula], lc:Int):(List[QFPAFormula],Int) = {
+ var lc1 = lc
+ var lTemp: List[QFPAFormula] = Nil
+ l.foreach(f => {
+ val (fT, lcT) = replaceInequalitiesWithEqualitiesinOneSingleFormula(f, lc1)
+ lc1 = lcT
+ lTemp = fT :: lTemp
+ })
+ (lTemp, lc1)
+ }
+
+
+ def replaceInequalitiesWithEqualities(l:List[List[QFPAFormula]]):List[List[QFPAFormula]] = {
+ var lTemp: List[List[QFPAFormula]] = Nil
+ var lc = 0
+ l.foreach(c => {
+ val (cT, lcT) = replaceInequalitiesWithEqualitiesinConjunct(c, lc)
+ lc = lcT
+ lTemp = cT :: lTemp
+ })
+ lTemp
+ }
+
+//// END
+
+ def consistentConjunctUsingZ3(c:List[QFPAFormula]):Boolean = {
+ val out = multisets.CheckingConsistency.callZ3toDetermineConsistency(c)
+ val res = if (out == "sat") true else false
+ res
+ }
+
+ def removeRedundantUsingZ3(c:List[QFPAFormula]):List[QFPAFormula] = {
+ var l1: List[QFPAFormula] = Nil
+ var l2 = c
+ while (! l2.isEmpty) {
+ val f = l2.head
+ l2 = l2.tail
+ if (consistentConjunctUsingZ3((QFPANot(f) :: l2) ::: l1) ) l1 = f :: l1
+ }
+ l1
+ }
+
+ def useAntisymmetryToDeriveEq(c:List[QFPAFormula]): List[QFPAFormula] = {
+ var l1: List[QFPAFormula] = Nil
+ var ltemp: List[QFPAFormula] = Nil
+ var l2 = c
+ while (! l2.isEmpty) {
+ val f = l2.head
+ l2 = l2.tail
+ f match {
+ case QFPAAtom(ALeq(t1, t2)) => {
+ if (l2.exists(fl => fl == QFPAAtom(ALeq(t2, t1)))) ltemp = f :: ltemp
+ else if (ltemp.exists(fl => fl == QFPAAtom(ALeq(t2, t1)))) l1 = QFPAAtom(AEq(t1, t2)) :: l1
+ else l1 = f :: l1
+ }
+ case _ => l1 = f :: l1
+ }
+ }
+ l1
+ }
+
+ def checkConsistencyAndRemoveRedundantUsingZ3(l:List[List[QFPAFormula]]): List[List[QFPAFormula]] = {
+ var lTemp: List[List[QFPAFormula]] = Nil
+ l.foreach(c => if (consistentConjunctUsingZ3(c)) {
+ val c1 = removeRedundantUsingZ3(c)
+ val c2 = useAntisymmetryToDeriveEq(c1)
+ // a <= b & b <= a ===> a = b
+ lTemp = c2 :: lTemp
+ })
+ lTemp
+ }
+
+// ----------------------
+
+/*
+
+ def checkIfTermIsAboutTempVVariable(t:TermQFPA):Boolean = t match {
+ case TVariable(v) => v.startsWith("FRESHv")
+ case TConstant(c) => false
+ case TPlus(t1, t2) => false
+ case TTimes(c, t1) => false
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def isAtomAboutTempVVariable(a:AtomQFPA):Boolean = a match {
+ case AEq(t1, t2) => checkIfTermIsAboutTempVVariable(t1)
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def isFormulaAboutTempVVariable(f:QFPAFormula):Boolean = f match {
+ case QFPAAtom(a) => isAtomAboutTempVVariable(a)
+ case QFPAEmpty => false
+ case QFPATrue => false
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def separateEqualitiesIntoTwoListsDepandingOnTempVarV(c:List[QFPAFormula]):(List[QFPAFormula],List[QFPAFormula]) = {
+ var l1T: List[QFPAFormula] = Nil
+ var l2T: List[QFPAFormula] = Nil
+ c.foreach(f => {
+ if (isFormulaAboutTempVVariable(f)) {
+ l2T = f :: l2T
+ } else l1T = f :: l1T
+ })
+ (l1T, l2T)
+ }
+
+
+ def getStringValueofTempVarV(t:TermQFPA):String = t match {
+ case TVariable(v) => v
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def createValueOfTempVarVAtom(a:AtomQFPA):(String,TermQFPA) = a match {
+ case AEq(t1, t2) => {
+ val s = getStringValueofTempVarV(t1)
+ (s, t2)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def createValueOfTempVarV(f:QFPAFormula):(String,TermQFPA) = f match {
+ case QFPAAtom(a) => createValueOfTempVarVAtom(a)
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def updateValuesWitnNewVValueTerm(tt:TermQFPA, vu:String, tu: TermQFPA):TermQFPA = tt match {
+ case TVariable(v) => if (v == vu) tu else tt
+ case TConstant(c) => tt
+ case TPlus(t1, t2) => {
+ val t1N = updateValuesWitnNewVValueTerm(t1, vu, tu)
+ val t2N = updateValuesWitnNewVValueTerm(t2, vu, tu)
+ TPlus(t1N, t2N)
+ }
+ case TTimes(c, t1) => {
+ val t1N = updateValuesWitnNewVValueTerm(t1, vu, tu)
+ TTimes(c, t1N)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def updateValuesWitnNewVValueAtom(a:AtomQFPA, v:String, t: TermQFPA):AtomQFPA = a match {
+ case AEq(t1, t2) => {
+ val t1N = updateValuesWitnNewVValueTerm(t1, v, t)
+ val t2N = updateValuesWitnNewVValueTerm(t2, v, t)
+ AEq(t1N, t2N)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def updateValuesWitnNewVValueFormula(f:QFPAFormula, v:String, t: TermQFPA):QFPAFormula = f match {
+ case QFPAAtom(a) => QFPAAtom(updateValuesWitnNewVValueAtom(a, v, t))
+ case QFPAEmpty => f
+ case QFPATrue => f
+ case x@_ => error("Impossible case :" + x)
+ }
+
+
+ def updateValuesWitnNewVValue(l:List[QFPAFormula], v:String, t: TermQFPA):List[QFPAFormula] = {
+ var lTemp: List[QFPAFormula] = Nil
+ l.foreach(f => {
+ val fN = updateValuesWitnNewVValueFormula(f, v, t)
+ lTemp = fN :: lTemp
+ })
+ lTemp
+ }
+
+
+ def getRidOfTempVVariablesFromConjuntion(c:List[QFPAFormula]):List[QFPAFormula] = {
+ val (l1, l2) = separateEqualitiesIntoTwoListsDepandingOnTempVarV(c)
+ var l1T = l1
+ var l2T = l2
+ while (! l2T.isEmpty) {
+ val (v, t) = createValueOfTempVarV(l2T.head)
+ val lT = l2T.tail
+ l1T = updateValuesWitnNewVValue(l1T, v, t)
+ l2T = updateValuesWitnNewVValue(lT, v, t)
+ }
+ l1T
+ }
+
+ def orientEqualities(c:List[QFPAFormula]):List[QFPAFormula] = {
+ var l1: List[QFPAFormula] = Nil
+ var l2 = c
+ while (! l2.isEmpty) {
+ val f = l2.head
+ l2 = l2.tail
+ f match {
+ case QFPAAtom(AEq(t1, TVariable(v))) => l1 = QFPAAtom(AEq(TVariable(v), t1)) :: l1
+ case _ => l1 = f :: l1
+ }
+ }
+ l1
+ }
+
+ def getRidOfTempVVariablesandOrientEqualities(l:List[List[QFPAFormula]]):List[List[QFPAFormula]] = {
+ var lTemp: List[List[QFPAFormula]] = Nil
+ l.foreach(c => {
+ val c1 = getRidOfTempVVariablesFromConjuntion(c)
+ val c2 = orientEqualities(c1)
+ lTemp = c2 :: lTemp
+ })
+ lTemp
+ }
+
+*/
+
+ def getVariablesfromFormula(f:QFPAFormula):Set[String] = {
+ val l1 = multisets.CheckingConsistency.getAllVariablesAndConstsFromFormula(f)
+ l1._1
+ }
+
+ def getvariablesFromVector(l:List[TermQFPA]):Set[String] = {
+ var s1 = Set.empty[String]
+ l.foreach(t => s1 = s1 ++ multisets.RemoveStars.getAllVariablesFromTerm(t))
+ s1
+ }
+
+// start
+
+ def createZeroMap(vars:Set[String]):Map[String,Int] = {
+ var m = Map.empty[String,Int]
+ vars.foreach(v => m += (v -> 0))
+ m += ("CONST" -> 0)
+ m
+ }
+
+
+ def addVariableinMap(v:String,vars:Set[String]):Map[String,Int] = {
+ var m = createZeroMap(vars)
+ m += (v -> 1)
+ m
+ }
+
+ def addConstantInMap(c:Int,vars:Set[String]):Map[String,Int] = {
+ var m = createZeroMap(vars)
+ m += ("CONST" -> c)
+ m
+ }
+
+ def sumTwoMaps(m1:Map[String,Int],m2:Map[String,Int],vars:Set[String]):Map[String,Int] = {
+ var m3 = Map.empty[String,Int]
+ vars.foreach(v => {
+ val l = m1(v) + m2(v)
+ m3 += (v -> l)
+ })
+ val c = m1("CONST") + m2("CONST")
+ m3 += ("CONST" -> c)
+ m3
+ }
+
+
+ def multiplyMap(c:Int,m:Map[String,Int],vars:Set[String]):Map[String,Int] = {
+ var mN = Map.empty[String,Int]
+ vars.foreach(v => {
+ val l = c * m(v)
+ mN += (v -> l)
+ })
+ val cn = c * m("CONST")
+ mN += ("CONST" -> cn)
+ mN
+ }
+
+
+ def createMapRepresentingTerm(t:TermQFPA,vars:Set[String]):Map[String,Int] = t match {
+ case TVariable(v) => addVariableinMap(v,vars)
+ case TConstant(c) => addConstantInMap(c,vars)
+ case TPlus(t1, t2) => {
+ val m1 = createMapRepresentingTerm(t1, vars)
+ val m2 = createMapRepresentingTerm(t2, vars)
+ sumTwoMaps(m1, m2, vars)
+ }
+ case TTimes(c, t1) => {
+ val m1 = createMapRepresentingTerm(t1, vars)
+ multiplyMap(c, m1, vars)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def createMapRepresentingFormula(f:QFPAFormula,vars:Set[String]):(String,Map[String,Int]) = {
+ val p = f match {
+ case QFPAAtom(ALeq(t1, t2)) => {
+ val s = "i"
+ val m1 = createMapRepresentingTerm(t1, vars)
+ val m2 = createMapRepresentingTerm(t2, vars)
+ val m3 = multiplyMap(-1, m1, vars)
+ val m = sumTwoMaps(m2, m3, vars)
+ (s, m)
+ }
+ case QFPAAtom(AEq(t1, t2)) => {
+ val s = "e"
+ val m1 = createMapRepresentingTerm(t1, vars)
+ val m2 = createMapRepresentingTerm(t2, vars)
+ val m3 = multiplyMap(-1, m1, vars)
+ val m = sumTwoMaps(m2, m3, vars)
+ (s, m)
+ }
+ case QFPATrue => {
+ val s = "t"
+ val m = createZeroMap(vars)
+ (s, m)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+ p
+ }
+
+// end
+
+
+ def updateOneMapWithOther(mTU:Map[String,Int],m:Map[String,Int],v:String):Map[String,Int] = {
+ val c = mTU(v)
+ val j = m(v)
+ val mT1 = mTU - v
+ val m1 = m - v
+// val vars = m.keySet
+// hell:
+ var vars = Set.empty[String]
+ vars = vars ++ m1.keySet
+ val m2 = if (j == 1) multiplyMap(-1,m1,vars) else m1
+ val m3 = multiplyMap(c,m2,vars)
+ sumTwoMaps(mT1, m3, vars)
+ }
+
+ def updateMapwhileQE(l:List[(String,Map[String,Int])],m:Map[String,Int],v:String):List[(String,Map[String,Int])] = {
+ var lt = List.empty[(String,Map[String,Int])]
+ l.foreach(p => {
+ if (p._2 != m) {
+ val m1 = updateOneMapWithOther(p._2, m, v)
+ lt = (p._1, m1) :: lt
+ }
+ })
+ lt
+ }
+
+ def eliminateVariable(v:String,l:List[(String,Map[String,Int])]):(List[(String,Map[String,Int])],Boolean) = {
+ val lf = l.filter(p => p._1 == "e" && (p._2(v) == 1 || p._2(v) == -1))
+ val res = if (lf.isEmpty) (l, false) else (updateMapwhileQE(l, lf.head._2, v), true)
+ res
+ }
+
+
+ def createOneTermFromMap(i:Int,v:String,m:Map[String,Int]):TermQFPA = {
+ val c = i * m(v)
+ val t = if (v == "CONST") TConstant(c) else
+ if (c == 1) TVariable(v) else TTimes(c, TVariable(v))
+ t
+ }
+
+ def constructTermFromMap(i:Int,vars:Set[String],m:Map[String,Int]):TermQFPA = {
+ val t = if (vars.isEmpty) TConstant(0) else {
+ val l = vars.toList
+ var term = createOneTermFromMap(i, l.head, m)
+ val ltail = l.tail
+ ltail.foreach(v => {
+ val t1 = createOneTermFromMap(i, v, m)
+ term = TPlus(t1, term)
+ })
+ term
+ }
+ t
+ }
+
+ def constructPositiveTermFromMap(pVars:Set[String],m:Map[String,Int]):TermQFPA =
+ constructTermFromMap(1, pVars, m)
+
+ def constructNegativeTermFromMap(nVars:Set[String],m:Map[String,Int]):TermQFPA =
+ constructTermFromMap(-1, nVars, m)
+
+
+ def getPositiveAndNegativeVarsandConstFromMap(m:Map[String,Int],vars:Set[String]):(Set[String],Set[String]) = {
+ var sp = Set.empty[String]
+ var sn = Set.empty[String]
+ vars.foreach(v => {
+ if (m(v) > 0) sp = sp + v
+ if (m(v) < 0) sn = sn + v
+ })
+ if (m("CONST") > 0) sp = sp + "CONST"
+ if (m("CONST") < 0) sn = sn + "CONST"
+ (sp, sn)
+ }
+
+
+ def reconstructEqualityFromMap(m:Map[String,Int],vars:Set[String]):QFPAFormula = {
+ val (pVars, nVars) = getPositiveAndNegativeVarsandConstFromMap(m, vars)
+ val tp = constructPositiveTermFromMap(pVars, m)
+ val tn = constructNegativeTermFromMap(nVars, m)
+ QFPAAtom(AEq(tp, tn))
+ }
+
+ def reconstructInequalityFromMap(m:Map[String,Int],vars:Set[String]):QFPAFormula = {
+ val (pVars, nVars) = getPositiveAndNegativeVarsandConstFromMap(m, vars)
+ val tp = constructPositiveTermFromMap(pVars, m)
+ val tn = constructNegativeTermFromMap(nVars, m)
+ QFPAAtom(ALeq(tn, tp))
+ }
+
+
+ def reconstructFormulaFromMaps(t:(String,Map[String,Int]),vars:Set[String]):QFPAFormula = {
+ val f = if (t._1 == "t") QFPATrue else
+ if (t._1 == "e") reconstructEqualityFromMap(t._2,vars)
+ else reconstructInequalityFromMap(t._2,vars)
+ f
+ }
+
+ def reconstructFormulasFromMaps(l:List[(String,Map[String,Int])],vars:Set[String]):List[QFPAFormula] = {
+ val list1 = l.map(e => reconstructFormulaFromMaps(e,vars))
+ list1
+ }
+
+
+
+ def doSimpleQE(v:List[TermQFPA],l:List[QFPAFormula]):List[QFPAFormula] = {
+ val inVars = getvariablesFromVector(v)
+ var allVars = Set.empty[String]
+ l.foreach(f => allVars = allVars ++ getVariablesfromFormula(f))
+ val varsForQE = allVars -- inVars
+ val listOfMaps = l.map(f => createMapRepresentingFormula(f, allVars))
+ var fmla = listOfMaps
+ var eliminated = Set.empty[String]
+ varsForQE.foreach(v => {
+ val p = eliminateVariable(v, fmla)
+ fmla = p._1
+ if (p._2) eliminated = eliminated + v
+ })
+ val l1 = reconstructFormulasFromMaps(fmla,allVars -- eliminated)
+ l1
+ }
+
+
+ // def doEliminationOfConstants(v:List[TermQFPA],List[
+
+
+
+// -----------------------
+
+ def main(v:List[TermQFPA],f:QFPAFormula): (List[TermQFPA], List[List[QFPAFormula]]) = {
+ val (fTemp1, vN) = flattenComplexTerms(v)
+ val fNew1 = if (fTemp1 == QFPATrue) f else QFPAAnd(f, fTemp1)
+ val (fNew2, fl) = flattenITEExpressions(fNew1)
+ // fNew2 is a formula that doesn't contain ITE expressions,
+ //fl is a list of a type (v, ITE(...)) no nested ITE expressions
+ val listDNFNoITEs = unrollITEExpressions(fNew2, fl)
+ // no more ITE expressions and listDNFNoITs is in DNF, does not contain ITEs
+ // listDNFNoITEs is a list of lists of formulas
+ val list1 = checkConsistencyAndRemoveRedundantUsingZ3(listDNFNoITEs)
+ // list1 contains only satisfiable constraints
+ val list2 = list1.map(f => doSimpleQE(vN,f))
+ val list3 = replaceInequalitiesWithEqualities(list2)
+/* val list3 = getRidOfTempVVariablesandOrientEqualities(list2) */
+ // a + b = c ===> c = a + b
+ (vN, list3)
+ // vN is a term that contains only variables and list1 is a list of lists of formulas
+ }
+
+}
diff --git a/src/multisets/FormulaConstructor.scala b/src/multisets/FormulaConstructor.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4c72b3c6962778f1e83b126a65d9fa2d5603a0b3
--- /dev/null
+++ b/src/multisets/FormulaConstructor.scala
@@ -0,0 +1,536 @@
+package multisets
+
+import scala.collection.mutable.Map
+import scala.collection.mutable.Set
+import java.util.NoSuchElementException
+import multisets.MultisetFormulaPrinter._
+
+
+
+object FormulaConstructor {
+
+
+// start: exists the execution with a message
+ def abort(msg: String) {
+ println(msg)
+ System.exit(-1)
+ }
+
+// start: parsing of NoSuchElementException message
+ def whichVarIsMissing(s: String): String = {
+ val strings = s.split (":");
+ strings(1)
+ }
+// end
+
+
+// Start: we check for atoms of a type a = b, whether it is about msets or integers
+ def checkTypesOfAtom(s: String, m: Map[String, String], a: Atom): Atom = {
+ try {
+ val af = a match {
+ case AEqual(MVariable(m1), MVariable(m2)) => {
+ val aN = if (m(m1) == "INT" && m(m2) == "INT") AAtomOut(AOEq(TOVariable(m1), TOVariable(m2)))
+ else a
+ aN
+ }
+ case AAtomOut(AOEq(TOVariable(v1), TOVariable(v2))) => {
+ val aN = if (m(v1) == "INT" && m(v2) == "INT") a
+ else AEqual(MVariable(v1), MVariable(v2))
+ aN
+ }
+ case _ => a
+ }
+ af
+ } catch {
+ case ex: NoSuchElementException => {
+ val v = whichVarIsMissing(ex.getMessage)
+ abort("Program abort: in the problem " + s + " the variable " + v + " is not declared!")
+ AEqual(MEmpty, MEmpty)
+ }
+ }
+ }
+
+ def checkAtomsInFormula(s: String, p: (Map[String, String], Formula)): Formula = p._2 match {
+ case FAnd(f1, f2) => {
+ val f1N = checkAtomsInFormula(s, (p._1, f1))
+ val f2N = checkAtomsInFormula(s, (p._1, f2))
+ FAnd(f1N, f2N)
+ }
+ case FOr(f1, f2) => {
+ val f1N = checkAtomsInFormula(s, (p._1, f1))
+ val f2N = checkAtomsInFormula(s, (p._1, f2))
+ FOr(f1N, f2N)
+ }
+ case FNot(f1) => {
+ val f1N = checkAtomsInFormula(s, (p._1, f1))
+ FNot(f1N)
+ }
+ case FAtom(a) => {
+ val aN = checkTypesOfAtom(s, p._1, a)
+ FAtom(aN)
+ }
+ case FTrue => p._2
+ case FFalse => p._2
+ }
+// end
+
+// start: given a formula we derive two sets of variables: integer variables and set veriables
+ def getVariablesfromMultiset(m: Multiset): (Set[String], Set[String]) = m match {
+ case MVariable(v) => (Set[String](), Set(v))
+ case MEmpty => (Set[String](), Set[String]())
+ case MUnion(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (p1, p2) = getVariablesfromMultiset(m2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case MIntersection(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (p1, p2) = getVariablesfromMultiset(m2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case MPlus(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (p1, p2) = getVariablesfromMultiset(m2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case MMinus(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (p1, p2) = getVariablesfromMultiset(m2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case MSetMinus(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (p1, p2) = getVariablesfromMultiset(m2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case MSetOf(m1) => getVariablesfromMultiset(m1)
+ }
+
+ def getVariablesfromTermIn(t: TermIn): (Set[String], Set[String]) = t match {
+ case TIMultiplicity(v) => (Set[String](), Set(v))
+ case TIConstant(c) => (Set[String](), Set[String]())
+ case TIPlus(t1, t2) => {
+ val (s1, s2) = getVariablesfromTermIn(t1)
+ val (p1, p2) = getVariablesfromTermIn(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case TITimes(c, t1)=> getVariablesfromTermIn(t1)
+ case TIIte(f, t1, t2)=> {
+ val (s1, s2) = getVariablesfromTermIn(t1)
+ val (p1, p2) = getVariablesfromTermIn(t2)
+ val (st, tt) = (s1 ++ p1, s2 ++ p2)
+ val (sf, tf) = getVariablesfromFormulaIn(f)
+ (sf ++ st, tf ++ tt)
+ }
+ }
+
+ def getVariablesfromAtomIn(a: AtomIn): (Set[String], Set[String]) = a match {
+ case AILeq(t1, t2) => {
+ val (s1, s2) = getVariablesfromTermIn(t1)
+ val (p1, p2) = getVariablesfromTermIn(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case AIEq(t1,t2) => {
+ val (s1, s2) = getVariablesfromTermIn(t1)
+ val (p1, p2) = getVariablesfromTermIn(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ }
+
+ def getVariablesfromFormulaIn(f: FormulaIn): (Set[String], Set[String]) = f match {
+ case FIAnd(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormulaIn(f1)
+ val (t1, t2) = getVariablesfromFormulaIn(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FIOr(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormulaIn(f1)
+ val (t1, t2) = getVariablesfromFormulaIn(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FINot(f1) => getVariablesfromFormulaIn(f1)
+ case FIAtom(a) => getVariablesfromAtomIn(a)
+ case FITrue => (Set[String](), Set[String]())
+ case FIFalse => (Set[String](), Set[String]())
+ }
+
+ def getVariablesfromTermOut(t: TermOut): (Set[String], Set[String]) = t match {
+ case TOConstant(c) => (Set[String](), Set[String]())
+ case TOVariable(v) => (Set(v), Set[String]())
+ case TOCard(m) => getVariablesfromMultiset(m)
+ case TOPlus(t1, t2) => {
+ val (s1, s2) = getVariablesfromTermOut(t1)
+ val (p1, p2) = getVariablesfromTermOut(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case TOTimes(c, t1)=> getVariablesfromTermOut(t1)
+ case TOIte(f, t1, t2)=> {
+ val (s1, s2) = getVariablesfromTermOut(t1)
+ val (p1, p2) = getVariablesfromTermOut(t2)
+ val (st, tt) = (s1 ++ p1, s2 ++ p2)
+ val (sf, tf) = getVariablesfromFormulaOut(f)
+ (sf ++ st, tf ++ tt)
+ }
+ }
+
+ def getVariablesfromAtomOut(a: AtomOut): (Set[String], Set[String]) = a match {
+ case AOLeq(t1, t2) => {
+ val (s1, s2) = getVariablesfromTermOut(t1)
+ val (p1, p2) = getVariablesfromTermOut(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case AOEq(t1,t2) => {
+ val (s1, s2) = getVariablesfromTermOut(t1)
+ val (p1, p2) = getVariablesfromTermOut(t2)
+ (s1 ++ p1, s2 ++ p2)
+ }
+ case AOSum(l1, f, l2) => {
+ var s = Set[String]()
+ var t = Set[String]()
+ l1.foreach(v => {
+ val (st, tt) = getVariablesfromTermOut(v)
+ s = s ++ st
+ t = t ++ tt
+ })
+ l2.foreach(v => {
+ val (st, tt) = getVariablesfromTermIn(v)
+ s = s ++ st
+ t = t ++ tt
+ })
+ val (sf, tf) = getVariablesfromFormulaIn(f)
+ (s ++ sf, t ++ tf)
+ }
+ }
+
+ def getVariablesfromFormulaOut(f: FormulaOut): (Set[String], Set[String]) = f match {
+ case FOAnd(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormulaOut(f1)
+ val (t1, t2) = getVariablesfromFormulaOut(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FOOr(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormulaOut(f1)
+ val (t1, t2) = getVariablesfromFormulaOut(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FONot(f1) => getVariablesfromFormulaOut(f1)
+ case FOAtom(a) => getVariablesfromAtomOut(a)
+ case FOTrue => (Set[String](), Set[String]())
+ case FOFalse => (Set[String](), Set[String]())
+ }
+
+ def getVariablesfromAtom(a: Atom): (Set[String], Set[String]) = a match {
+ case AEqual(m1, m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (t1, t2) = getVariablesfromMultiset(m2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case ASubset(m1,m2) => {
+ val (s1, s2) = getVariablesfromMultiset(m1)
+ val (t1, t2) = getVariablesfromMultiset(m2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case AForAllElem(f1) => getVariablesfromFormulaIn(f1)
+ case AAtomOut(a1) => getVariablesfromAtomOut(a1)
+ }
+
+ def getVariablesfromFormula(f: Formula): (Set[String], Set[String]) = f match {
+ case FAnd(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormula(f1)
+ val (t1, t2) = getVariablesfromFormula(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FOr(f1, f2) => {
+ val (s1, s2) = getVariablesfromFormula(f1)
+ val (t1, t2) = getVariablesfromFormula(f2)
+ (s1 ++ t1, s2 ++ t2)
+ }
+ case FNot(f1) => getVariablesfromFormula(f1)
+ case FAtom(a) => getVariablesfromAtom(a)
+ case FTrue => (Set[String](), Set[String]())
+ case FFalse => (Set[String](), Set[String]())
+ }
+// end
+
+
+// start: checking that all types are correct
+ def checkTypesOfIntVariables(name: String, m: Map[String, String], ints: List[String]): Unit = {
+ try {
+ ints.foreach(v => if (m(v) != "INT")
+ abort("Program abort: in the problem " + name + " the INT variable " + v + " is declared as" + m(v) + "!")
+ )
+ } catch {
+ case ex: NoSuchElementException => {
+ val v = whichVarIsMissing(ex.getMessage)
+ abort("Program abort: in the problem " + name + " the variable " + v + " is not declared!")
+ AEqual(MEmpty, MEmpty)
+ }
+ }
+ }
+
+ def checkTypesOfMSetVariables(name: String, m: Map[String, String], msets: List[String]): Unit = {
+ try {
+ msets.foreach(v => if (m(v) == "INT")
+ abort("Program abort: in the problem " + name + " the collection variable " + v + " is declared as INT!")
+ )
+ } catch {
+ case ex: NoSuchElementException => {
+ val v = whichVarIsMissing(ex.getMessage)
+ abort("Program abort: in the problem " + name + " the variable " + v + " is not declared!")
+ AEqual(MEmpty, MEmpty)
+ }
+ }
+ }
+
+ def simpleTypeChecking(name: String, m: Map[String, String], ints: List[String], msets: List[String]): Unit = {
+ checkTypesOfIntVariables(name, m, ints)
+ checkTypesOfMSetVariables(name, m, msets)
+ }
+// end
+
+
+// start: here we construct formulas describing that S is a SET or e is an ELEM
+ def createConstraintAboutOneVar(t: String, v:String): Formula = {
+ val f = if (t == "SET") {
+ val f1in = FIAtom(AIEq(TIMultiplicity(v), TIConstant(0)))
+ val f2in = FIAtom(AIEq(TIMultiplicity(v), TIConstant(1)))
+ FAtom(AForAllElem(FIOr(f1in, f2in)))
+ } else FAtom(AAtomOut(AOEq(TOCard(MVariable(v)), TOConstant(1))))
+ f
+ }
+
+ def getAdditionalConstraints(m: Map[String, String], l: List[String]): Formula = {
+ val ln = l.filter(v => m(v) != "MSET")
+ val f = if (ln.isEmpty) FTrue else {
+ var ft = createConstraintAboutOneVar(m(ln.head), ln.head)
+ val lnt = ln.tail
+ lnt.foreach(v => {
+ val fn = createConstraintAboutOneVar(m(v), v)
+ ft = FAnd(ft, fn)
+ })
+ ft
+ }
+ f
+ }
+// end
+
+
+// start: translation to NNF
+ def nnfTermIn(t: TermIn): TermIn = t match {
+ case TIPlus(t1, t2) => {
+ val t1n = nnfTermIn(t1)
+ val t2n = nnfTermIn(t2)
+ TIPlus(t1n, t2n)
+ }
+ case TITimes(c, t1)=> {
+ val t1n = nnfTermIn(t1)
+ TITimes(c, t1n)
+ }
+ case TIIte(f, t1, t2) => {
+ val t1n = nnfTermIn(t1)
+ val t2n = nnfTermIn(t2)
+ val f1 = nnfFormulaIn(f)
+ TIIte(f1, t1n, t2n)
+ }
+ case _ => t
+ }
+
+ def nnfAtomIn(a: AtomIn): AtomIn = a match {
+ case AILeq(t1, t2) => {
+ val t1n = nnfTermIn(t1)
+ val t2n = nnfTermIn(t2)
+ AILeq(t1n, t2n)
+ }
+ case AIEq(t1,t2) => {
+ val t1n = nnfTermIn(t1)
+ val t2n = nnfTermIn(t2)
+ AIEq(t1n, t2n)
+ }
+ }
+
+ def nnfFormulaIn(f: FormulaIn): FormulaIn = f match {
+ case FIAnd(f1, f2) => {
+ val f1n = nnfFormulaIn(f1)
+ val f2n = nnfFormulaIn(f2)
+ FIAnd(f1n, f2n)
+ }
+ case FIOr(f1, f2) => {
+ val f1n = nnfFormulaIn(f1)
+ val f2n = nnfFormulaIn(f2)
+ FIOr(f1n, f2n)
+ }
+ case FINot(FIAnd(f1, f2)) => {
+ val f1n = nnfFormulaIn(FINot(f1))
+ val f2n = nnfFormulaIn(FINot(f2))
+ FIOr(f1n, f2n)
+ }
+ case FINot(FIOr(f1, f2)) => {
+ val f1n = nnfFormulaIn(FINot(f1))
+ val f2n = nnfFormulaIn(FINot(f2))
+ FIAnd(f1n, f2n)
+ }
+ case FINot(FINot(f1)) => nnfFormulaIn(f1)
+ case FINot(FIAtom(a)) => {
+ val a1 = nnfAtomIn(a)
+ FINot(FIAtom(a1))
+ }
+ case FINot(FITrue) => FIFalse
+ case FINot(FIFalse) => FITrue
+ case FIAtom(a) => {
+ val a1 = nnfAtomIn(a)
+ FIAtom(a1)
+ }
+ case _ => f
+ }
+
+
+ def nnfTermOut(t: TermOut): TermOut = t match {
+ case TOPlus(t1, t2) => {
+ val t1n = nnfTermOut(t1)
+ val t2n = nnfTermOut(t2)
+ TOPlus(t1n, t2n)
+ }
+ case TOTimes(c, t1)=> {
+ val t1n = nnfTermOut(t1)
+ TOTimes(c, t1n)
+ }
+ case TOIte(f, t1, t2) => {
+ val t1n = nnfTermOut(t1)
+ val t2n = nnfTermOut(t2)
+ val f1 = nnfFormulaOut(f)
+ TOIte(f1, t1n, t2n)
+ }
+ case _ => t
+ }
+
+ def nnfAtomOut(a: AtomOut): AtomOut = a match {
+ case AOLeq(t1, t2) => {
+ val t1n = nnfTermOut(t1)
+ val t2n = nnfTermOut(t2)
+ AOLeq(t1n, t2n)
+ }
+ case AOEq(t1,t2) => {
+ val t1n = nnfTermOut(t1)
+ val t2n = nnfTermOut(t2)
+ AOEq(t1n, t2n)
+ }
+ case AOSum(l1, f, l2) => {
+ val l1n = l1.map(v => nnfTermOut(v))
+ val l2n = l2.map(v => nnfTermIn(v))
+ val f1 = nnfFormulaIn(f)
+ AOSum(l1n, f1, l2n)
+ }
+ }
+
+ def nnfFormulaOut(f: FormulaOut): FormulaOut = f match {
+ case FOAnd(f1, f2) => {
+ val f1n = nnfFormulaOut(f1)
+ val f2n = nnfFormulaOut(f2)
+ FOAnd(f1n, f2n)
+ }
+ case FOOr(f1, f2) => {
+ val f1n = nnfFormulaOut(f1)
+ val f2n = nnfFormulaOut(f2)
+ FOOr(f1n, f2n)
+ }
+ case FONot(FOAnd(f1, f2)) => {
+ val f1n = nnfFormulaOut(FONot(f1))
+ val f2n = nnfFormulaOut(FONot(f2))
+ FOOr(f1n, f2n)
+ }
+ case FONot(FOOr(f1, f2)) => {
+ val f1n = nnfFormulaOut(FONot(f1))
+ val f2n = nnfFormulaOut(FONot(f2))
+ FOAnd(f1n, f2n)
+ }
+ case FONot(FONot(f1)) => nnfFormulaOut(f1)
+ case FONot(FOAtom(a)) => {
+ val a1 = nnfAtomOut(a)
+ FONot(FOAtom(a1))
+ }
+ case FONot(FOTrue) => FOFalse
+ case FONot(FOFalse) => FOTrue
+ case FOAtom(a) => {
+ val a1 = nnfAtomOut(a)
+ FOAtom(a1)
+ }
+ case _ => f
+ }
+
+ def nnfAtom(a: Atom): Atom = a match {
+ case AForAllElem(f1) => {
+ val f1n = nnfFormulaIn(f1)
+ AForAllElem(f1n)
+ }
+ case AAtomOut(a1) => {
+ val a1n = nnfAtomOut(a1)
+ AAtomOut(a1n)
+ }
+ case _ => a
+ }
+
+ def nnf(f: Formula): Formula = f match {
+ case FAnd(f1, f2) => {
+ val f1n = nnf(f1)
+ val f2n = nnf(f2)
+ FAnd(f1n, f2n)
+ }
+ case FOr(f1, f2) => {
+ val f1n = nnf(f1)
+ val f2n = nnf(f2)
+ FOr(f1n, f2n)
+ }
+ case FNot(FAnd(f1, f2)) => {
+ val f1n = nnf(FNot(f1))
+ val f2n = nnf(FNot(f2))
+ FOr(f1n, f2n)
+ }
+ case FNot(FOr(f1, f2)) => {
+ val f1n = nnf(FNot(f1))
+ val f2n = nnf(FNot(f2))
+ FAnd(f1n, f2n)
+ }
+ case FNot(FNot(f1)) => nnf(f1)
+ case FNot(FAtom(a)) => {
+ val a1 = nnfAtom(a)
+ FNot(FAtom(a1))
+ }
+ case FNot(FTrue) => FFalse
+ case FNot(FFalse) => FTrue
+ case FAtom(a) => {
+ val a1 = nnfAtom(a)
+ FAtom(a1)
+ }
+ case _ => f
+ }
+// end
+
+
+// start: input problem, output: (name, created-formula, negated-created-formula, constraints)
+// all output formulas are in NNF
+ def processOneProblem(p: (String, (Map[String, String], Formula))): (String, (Formula, Formula, Formula)) = {
+ val mf = p._2
+ val f1 = checkAtomsInFormula(p._1, mf)
+ val f1f = nnf(f1)
+ val (sInt, sMsets) = getVariablesfromFormula(f1)
+ val lInt = sInt.toList
+ val lMsets = sMsets.toList
+ val m = mf._1
+ simpleTypeChecking(p._1, m, lInt, lMsets)
+ val fc = getAdditionalConstraints(m, lMsets)
+ val fcf = nnf(fc)
+ val fN = nnf(FNot(f1))
+ (p._1, (f1f, fN, fcf))
+ }
+// end
+
+
+
+//------------------------------------------------
+
+ def main(problemList: List[(String, (Map[String, String], Formula))]) : List[(String, (Formula, Formula, Formula))] = {
+ val formulaList = problemList.map(p => processOneProblem(p))
+ formulaList
+ }
+}
+
diff --git a/src/multisets/MAPA-FunExamples.scala b/src/multisets/MAPA-FunExamples.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f7b651575049e95dbeac0e683b0a885fc94aa7e
--- /dev/null
+++ b/src/multisets/MAPA-FunExamples.scala
@@ -0,0 +1,65 @@
+package mapaFun
+
+import mapaFun.MAPAFunFormulaPrinter._
+import multisets.MultisetFormulaPrinter._
+
+
+object MAPAFunExamples {
+
+// val m1 = MFMPlus(MFFunction("f", MFSetVar("D")), MFFunction("f", MFSetVar("F")))
+ val m1 = MFMPlus(MFFunction("f", MFSetVar("A")), MFFunction("f", MFSetVar("E")))
+ val a1 = MFMSetEqual(MFFunction("f", MFSUnion(MFSetVar("A"), MFSetVar("E"))), m1)
+ val s1 = MFSIntersec(MFSetVar("A"), MFSetVar("E"))
+ val f1 = MFAnd(MFAtom(MFSetEqual(s1, MFEmptySet)), MFNot(MFAtom(a1)))
+
+//---------------
+// the one from the VMCAI submission
+
+ val f21 = MFAtom(MFSetSubset(MFSetVar("N"), MFSetVar("A")))
+ val f22 = MFAtom(MFIntEqual(MFSCard(MFSetVar("T")), MFIntConst (1)))
+ val f23 = MFAtom(MFSetEqual(MFSIntersec(MFSetVar("T"), MFSetVar("A")), MFEmptySet))
+ val f24 = MFAtom(MFMSetEqual(MFFunction("d", MFSetVar("T")), MFMSetVar("E")))
+ val f25 = MFAtom(MFMSetEqual(MFFunction("d", MFSetVar("N")), MFMSetVar("C")))
+ val f26 = MFAtom(MFSetEqual(MFSUnion(MFSetVar("N"), MFSetVar("T")), MFSetVar("N1")))
+ val f27 = MFAtom(MFMSetEqual(MFFunction("d", MFSetVar("N1")), MFMSetVar("C1")))
+ val f28 = MFNot(MFAtom(MFIntLessEqual(MFMCard(MFMSetVar("C1")), MFIPlus(MFMCard(MFMSetVar("C")), MFIntConst (1)))))
+ val f2 = MFAnd(MFAnd(MFAnd(f21, f22), MFAnd(f23, f24)), MFAnd(MFAnd(f25, f26), MFAnd(f27, f28)))
+
+//---------------
+
+
+ def run (name: String, f: MAPAFunFormula): Unit = {
+ println("Formula " + name + ":")
+ print_MAPAFunFormula(f)
+ println("")
+ println("---------------------")
+ val f1n = mapaFun.SetExpansionAndCNF.noMoreSets(f)
+ print_MAPAFunFormula(f1n)
+ println("")
+ println("---------------------")
+ val f2n = mapaFun.FunctionElimination.noMoreFunctions(f1n)
+ print_MAPAFunFormula(f2n)
+ println("")
+ println("---------------------")
+ val f3n = mapaFun.MapaFunConversion.mapaFun2standardMAPA(f2n)
+ print_multisetFormula(f3n)
+ println("")
+ println("---------------------")
+ println("And now the original decision procedure:")
+ println("---------------------")
+// guru.multisets.Examples.run("f", f3n)
+ println("---------------------")
+ }
+
+
+// -----
+
+ def runExamples() {
+ run("f1", f1)
+// run("f2", f2)
+ }
+
+
+}
+
+
diff --git a/src/multisets/MAPA-FunFunctionEliminations.scala b/src/multisets/MAPA-FunFunctionEliminations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..877da2fc5af6cd763d536bb3f4f780c023d652f6
--- /dev/null
+++ b/src/multisets/MAPA-FunFunctionEliminations.scala
@@ -0,0 +1,210 @@
+package mapaFun
+
+import scala.collection.mutable.Map
+
+
+object FunctionElimination {
+
+
+ def createSumOfMultisets(l: List[String]): MAPAFunMultiset = {
+ var mm = MFMSetVar(l.head): MAPAFunMultiset
+ val t = l.tail
+ t.foreach(s => mm = MFMPlus(MFMSetVar(s), mm))
+ mm
+ }
+
+
+ def createMultisetVariableOutofSet(s: String): String = {
+ val s1 = s.replace('S', 'M')
+ s1
+ }
+
+
+ def createListOfFreshMultisetsAndSetMultisetEqualitySet(l: List[String]): (List[String], Set[(String, String)]) = {
+ var sn = Set[(String, String)]()
+ var ln: List[String] = Nil
+ l.foreach(e => {
+ val st = createMultisetVariableOutofSet(e)
+ ln = st :: ln
+ sn = sn ++ Set((e, st))
+ })
+ (ln, sn)
+ }
+
+
+
+ def listOfSetsInUnion(s: MAPAFunSet): List[String] = s match {
+ case MFSetVar(v) => List(v)
+ case MFSUnion(MFSetVar(v), s1) => {
+ val l1 = listOfSetsInUnion(s1)
+ val l2 = v :: l1
+ l2
+ }
+ case MFSUnion(s1, MFSetVar(v)) => {
+ val l1 = listOfSetsInUnion(s1)
+ val l2 = v :: l1
+ l2
+ }
+ case MFSUnion(s1, s2) => {
+ val l1 = listOfSetsInUnion(s1)
+ val l2 = listOfSetsInUnion(s2)
+ val l3 = l1 ::: l2
+ l3
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+
+
+
+ def pullOutAllFunctionsFromMultiset(m: MAPAFunMultiset): (MAPAFunMultiset, Set[(String, String)]) = m match {
+ case MFMSetVar(v) => (m, Set[(String, String)]())
+ case MFEmptyMSet => (m, Set[(String, String)]())
+ case MFMUnion(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ (MFMUnion(m1n, m2n), s1 ++ s2)
+ }
+ case MFMIntersec(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ (MFMIntersec(m1n, m2n), s1 ++ s2)
+ }
+ case MFMPlus(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ (MFMPlus(m1n, m2n), s1 ++ s2)
+ }
+ case MFMMinus(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ (MFMMinus(m1n, m2n), s1 ++ s2)
+ }
+ case MFSetMinus(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ (MFSetMinus(m1n, m2n), s1 ++ s2)
+ }
+ case MFSSetOf(m1) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ (MFSSetOf(m1n), s1)
+ }
+ case MFFunction(f, s) => {
+ val l = listOfSetsInUnion(s)
+ val (ml, smes) = createListOfFreshMultisetsAndSetMultisetEqualitySet(l)
+ val mf = createSumOfMultisets(ml)
+ (mf, smes)
+ }
+ }
+
+
+ def pullOutAllFunctionsFromInteger(i: MAPAFunInt): (MAPAFunInt, Set[(String, String)]) = i match {
+ case MFIntVar(v) => (i, Set[(String, String)]())
+ case MFIntConst(c) => (i, Set[(String, String)]())
+ case MFIPlus(i1, i2) => {
+ val (i1n, s1) = pullOutAllFunctionsFromInteger(i1)
+ val (i2n, s2) = pullOutAllFunctionsFromInteger(i2)
+ (MFIPlus(i1n, i2n), s1 ++ s2)
+ }
+ case MFITimes(c, i1) => {
+ val (i1n, s1) = pullOutAllFunctionsFromInteger(i1)
+ (MFITimes(c, i1n), s1)
+ }
+ case MFSCard(s) => (i, Set[(String, String)]())
+ case MFMCard(m) => {
+ val (m1, s1) = pullOutAllFunctionsFromMultiset(m)
+ (MFMCard(m1), s1)
+ }
+ }
+
+
+ def pullOutAllFunctionsFromAtom(a: MAPAFunAtom): (MAPAFunFormula, Set[(String, String)]) = a match {
+ case MFSetEqual(s1, s2) => (MFAtom(a), Set[(String, String)]())
+ case MFSetSubset(s1, s2) => (MFAtom(a), Set[(String, String)]())
+ case MFMSetEqual(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ val an = MFMSetEqual(m1n, m2n)
+ (MFAtom(an), s1 ++ s2)
+ }
+ case MFMSetSubset(m1, m2) => {
+ val (m1n, s1) = pullOutAllFunctionsFromMultiset(m1)
+ val (m2n, s2) = pullOutAllFunctionsFromMultiset(m2)
+ val an = MFMSetSubset(m1n, m2n)
+ (MFAtom(an), s1 ++ s2)
+ }
+ case MFIntEqual(i1, i2) => {
+ val (i1n, s1) = pullOutAllFunctionsFromInteger(i1)
+ val (i2n, s2) = pullOutAllFunctionsFromInteger(i2)
+ val an = MFIntEqual(i1n, i2n)
+ (MFAtom(an), s1 ++ s2)
+ }
+ case MFIntLessEqual(i1, i2) => {
+ val (i1n, s1) = pullOutAllFunctionsFromInteger(i1)
+ val (i2n, s2) = pullOutAllFunctionsFromInteger(i2)
+ val an = MFIntLessEqual(i1n, i2n)
+ (MFAtom(an), s1 ++ s2)
+ }
+ case MFIntDivides(c, i) => {
+ val (in, s1) = pullOutAllFunctionsFromInteger(i)
+ val an = MFIntDivides(c, in)
+ (MFAtom(an), s1)
+ }
+ }
+
+
+ def pullOutAllFunctionsFromFormula(f: MAPAFunFormula): (MAPAFunFormula, Set[(String, String)]) = f match {
+ case MFAnd(f1, f2) => {
+ val (f1n, s1) = pullOutAllFunctionsFromFormula(f1)
+ val (f2n, s2) = pullOutAllFunctionsFromFormula(f2)
+ (MFAnd(f1n, f2n), s1 ++ s2)
+ }
+ case MFOr(f1, f2) => {
+ val (f1n, s1) = pullOutAllFunctionsFromFormula(f1)
+ val (f2n, s2) = pullOutAllFunctionsFromFormula(f2)
+ (MFOr(f1n, f2n), s1 ++ s2)
+ }
+ case MFNot(f1) => {
+ val (f1n, s1) = pullOutAllFunctionsFromFormula(f1)
+ (MFNot(f1n), s1)
+ }
+ case MFAtom(a) => pullOutAllFunctionsFromAtom(a)
+ }
+
+
+
+ def createOneCardinalityFormula(p: (String, String)): MAPAFunFormula = {
+ val s = p._1
+ val m = p._2
+ val f = MFAtom(MFIntEqual(MFSCard(MFSetVar(s)), MFMCard(MFMSetVar(m))))
+ f
+ }
+
+
+ def createCardinalityFormulas(l: List[(String, String)]): MAPAFunFormula = {
+ var ft = createOneCardinalityFormula(l.head)
+ val t = l.tail
+ val ff = if (t.isEmpty) ft else {
+ t.foreach(p => {
+ val fp = createOneCardinalityFormula(p)
+ ft = MFAnd(fp, ft)
+ })
+ ft
+ }
+ ff
+ }
+
+
+
+
+//--------------------------------------
+
+
+ def noMoreFunctions(f: MAPAFunFormula): MAPAFunFormula = {
+ val (f1, s) = pullOutAllFunctionsFromFormula(f)
+ val l = s.toList
+ val f2 = createCardinalityFormulas(l)
+ MFAnd(f1, f2)
+ }
+}
+
diff --git a/src/multisets/MAPA-FunPrinter.scala b/src/multisets/MAPA-FunPrinter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3cb7b593109c20f7a5624fd25e7df91c416a43d1
--- /dev/null
+++ b/src/multisets/MAPA-FunPrinter.scala
@@ -0,0 +1,153 @@
+package mapaFun
+
+
+object MAPAFunFormulaPrinter {
+
+ def print_MAPAFunInt(i: MAPAFunInt): Unit = i match {
+ case MFIntVar(v) => Console.print(v)
+ case MFIntConst(c) => Console.print(c)
+ case MFIPlus(i1, i2) => {
+ print_MAPAFunInt(i1)
+ Console.print(" + ")
+ print_MAPAFunInt(i2)
+ }
+ case MFITimes(c, i1) => {
+ Console.print(c + "*")
+ print_MAPAFunInt(i1)
+ }
+ case MFSCard(s) => {
+ Console.print("| ")
+ print_MAPAFunSet(s)
+ print(" |")
+ }
+ case MFMCard(m) => {
+ Console.print("| ")
+ print_MAPAFunMultiset(m)
+ print(" |")
+ }
+ }
+
+ def print_MAPAFunMultiset(m: MAPAFunMultiset):Unit = m match {
+ case MFMSetVar(v) => Console.print(v)
+ case MFEmptyMSet => Console.print("EMPTY MULTISET")
+ case MFMUnion(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" UNION ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFMIntersec(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" INTERSEC ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFMPlus(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" PLUS ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFMMinus(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" MINUS ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFSetMinus(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" SET MINUS ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFSSetOf(m1) => {
+ Console.print(" SETOf ( ")
+ print_MAPAFunMultiset(m1)
+ print(" )")
+ }
+ case MFFunction(f, s) => {
+ Console.print(f + "[ ")
+ print_MAPAFunSet(s)
+ print(" ]")
+ }
+ }
+
+ def print_MAPAFunSet(s: MAPAFunSet):Unit = s match {
+ case MFSetVar(v) => Console.print(v)
+ case MFEmptySet => Console.print("EMPTY SET")
+ case MFUnivSet => Console.print("UNIVERSAL SET")
+ case MFSUnion(s1, s2) => {
+ print_MAPAFunSet(s1)
+ Console.print(" UNION ")
+ print_MAPAFunSet(s2)
+ }
+ case MFSIntersec(s1, s2) => {
+ print_MAPAFunSet(s1)
+ Console.print(" INTERSEC ")
+ print_MAPAFunSet(s2)
+ }
+ case MFSCompl(s1) => {
+ Console.print("( ")
+ print_MAPAFunSet(s1)
+ print(" )^c ")
+ }
+ }
+
+
+ def print_MAPAFunAtom(a: MAPAFunAtom):Unit = a match {
+ case MFSetEqual(s1, s2) => {
+ print_MAPAFunSet(s1)
+ Console.print(" = ")
+ print_MAPAFunSet(s2)
+ }
+ case MFSetSubset(s1, s2) => {
+ print_MAPAFunSet(s1)
+ Console.print(" SUBSET ")
+ print_MAPAFunSet(s2)
+ }
+ case MFMSetEqual(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" = ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFMSetSubset(m1, m2) => {
+ print_MAPAFunMultiset(m1)
+ Console.print(" SUBSET ")
+ print_MAPAFunMultiset(m2)
+ }
+ case MFIntEqual(i1, i2) => {
+ print_MAPAFunInt(i1)
+ Console.print(" = ")
+ print_MAPAFunInt(i2)
+ }
+ case MFIntLessEqual(i1, i2) => {
+ print_MAPAFunInt(i1)
+ Console.print(" =< ")
+ print_MAPAFunInt(i2)
+ }
+ case MFIntDivides(c, i) => {
+ Console.print(c + " * ")
+ print_MAPAFunInt(i)
+ }
+ }
+
+
+ def print_MAPAFunFormula(f: MAPAFunFormula):Unit = f match {
+ case MFAnd(f1, f2) => {
+ Console.print(" ( ")
+ print_MAPAFunFormula(f1)
+ print(" ) AND ( ")
+ print_MAPAFunFormula(f2)
+ print(" ) ")
+ }
+ case MFOr(f1, f2) => {
+ Console.print(" ( ")
+ print_MAPAFunFormula(f1)
+ print(" ) OR ( ")
+ print_MAPAFunFormula(f2)
+ print(" ) ")
+ }
+ case MFNot(f1) => {
+ Console.print(" NOT ( ")
+ print_MAPAFunFormula(f1)
+ print(" ) ")
+ }
+ case MFAtom(a) => print_MAPAFunAtom(a)
+ }
+
+}
\ No newline at end of file
diff --git a/src/multisets/MAPA-FunSetExpansionTranslator.scala b/src/multisets/MAPA-FunSetExpansionTranslator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7962f98ff51cbd2bac9ec90a29b99a999ee2f0c0
--- /dev/null
+++ b/src/multisets/MAPA-FunSetExpansionTranslator.scala
@@ -0,0 +1,397 @@
+package mapaFun
+
+
+import scala.collection.mutable.Map
+import scala.collection.immutable.Set
+import java.lang.Integer
+
+
+
+object SetExpansionAndCNF {
+
+
+
+
+
+
+
+
+// ---- getRidOfSetVariables
+
+
+ def simplifySetAtoms(s1: Set[String], s2: Set[String]): (Set[String], Set[String]) = {
+ val si = s1.intersect(s2)
+ val s1n = s1 -- si
+ val s2n = s2 -- si
+ (s1n, s2n)
+ }
+
+
+ def getRidOfSetVariablesinSet(s: MAPAFunSet, m: Map[String,Set[String]]): Set[String] = s match {
+ case MFSetVar(v) => m(v)
+ case MFEmptySet => Set[String]()
+ case MFUnivSet => m("ALL")
+ case MFSUnion(s1, s2) => {
+ val ss1 = getRidOfSetVariablesinSet(s1, m)
+ val ss2 = getRidOfSetVariablesinSet(s2, m)
+ ss1 ++ ss2
+ }
+ case MFSIntersec(s1, s2) => {
+ val ss1 = getRidOfSetVariablesinSet(s1, m)
+ val ss2 = getRidOfSetVariablesinSet(s2, m)
+ val ss3 = ss1.intersect(ss2)
+ ss3
+ }
+ case MFSCompl(s1) => {
+ val ss1 = getRidOfSetVariablesinSet(s1, m)
+ val ss2 = m("ALL") -- ss1
+ ss2
+ }
+ }
+
+ def createSetUnion(s: Set[String]): MAPAFunSet = {
+ val l = s.toList
+ if (l.isEmpty) MFEmptySet else {
+ var ts = MFSetVar(l.head): MAPAFunSet
+ val t = l.tail
+ t.foreach(e => {
+ val ns = MFSetVar(e)
+ ts = MFSUnion(ts, ns)
+ })
+ ts
+ }
+ }
+
+ def getRidOfSetVariablesinInt(i: MAPAFunInt, m: Map[String,Set[String]]): MAPAFunInt = i match {
+ case MFIntVar(v) => i
+ case MFIntConst(c) => i
+ case MFIPlus(i1, i2) => {
+ val i1n = getRidOfSetVariablesinInt(i1, m)
+ val i2n = getRidOfSetVariablesinInt(i2, m)
+ MFIPlus(i1n, i2n)
+ }
+ case MFITimes(c, i1) => {
+ val i1n = getRidOfSetVariablesinInt(i1, m)
+ MFITimes(c, i1n)
+ }
+ case MFSCard(s) => {
+ val sl = getRidOfSetVariablesinSet(s, m)
+ val sn = createSetUnion(sl)
+ MFSCard(sn)
+ }
+ case MFMCard(ms) => {
+ val msn = getRidOfSetVariablesinMultiset(ms, m)
+ MFMCard(msn)
+ }
+ }
+
+ def getRidOfSetVariablesinMultiset(mm: MAPAFunMultiset, m: Map[String,Set[String]]): MAPAFunMultiset = mm match {
+ case MFMSetVar(v) => mm
+ case MFEmptyMSet => mm
+ case MFMUnion(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMUnion(m1n, m2n)
+ }
+ case MFMIntersec(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMIntersec(m1n, m2n)
+ }
+ case MFMPlus(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMPlus(m1n, m2n)
+ }
+ case MFMMinus(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMMinus(m1n, m2n)
+ }
+ case MFSetMinus(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFSetMinus(m1n, m2n)
+ }
+ case MFSSetOf(m1) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ MFSSetOf(m1n)
+ }
+ case MFFunction(f, s) => {
+ val sl = getRidOfSetVariablesinSet(s, m)
+ val sn = createSetUnion(sl)
+ MFFunction(f, sn)
+ }
+ }
+
+
+ def getRidOfSetVariablesinAtom(a:MAPAFunAtom, m: Map[String,Set[String]]): MAPAFunAtom = a match {
+ case MFSetEqual(s1, s2) => {
+ val ss1l = getRidOfSetVariablesinSet(s1, m)
+ val ss2l = getRidOfSetVariablesinSet(s2, m)
+ val (ss1ln, ss2ln) = simplifySetAtoms(ss1l, ss2l)
+ val s1n = createSetUnion(ss1ln)
+ val s2n = createSetUnion(ss2ln)
+ MFSetEqual(s1n, s2n)
+ }
+ case MFSetSubset(s1, s2) => {
+ val ss1l = getRidOfSetVariablesinSet(s1, m)
+ val ss2l = getRidOfSetVariablesinSet(s2, m)
+ val (ss1ln, ss2ln) = simplifySetAtoms(ss1l, ss2l)
+ val s1n = createSetUnion(ss1ln)
+ val s2n = createSetUnion(ss2ln)
+ MFSetSubset(s1n, s2n)
+ }
+ case MFMSetEqual(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMSetEqual(m1n, m2n)
+ }
+ case MFMSetSubset(m1, m2) => {
+ val m1n = getRidOfSetVariablesinMultiset(m1, m)
+ val m2n = getRidOfSetVariablesinMultiset(m2, m)
+ MFMSetSubset(m1n, m2n)
+ }
+ case MFIntEqual(i1, i2) => {
+ val i1n = getRidOfSetVariablesinInt(i1, m)
+ val i2n = getRidOfSetVariablesinInt(i2, m)
+ MFIntEqual(i1n, i2n)
+ }
+ case MFIntLessEqual(i1, i2) => {
+ val i1n = getRidOfSetVariablesinInt(i1, m)
+ val i2n = getRidOfSetVariablesinInt(i2, m)
+ MFIntLessEqual(i1n, i2n)
+ }
+ case MFIntDivides(c, i) => {
+ val in = getRidOfSetVariablesinInt(i, m)
+ MFIntDivides(c, in)
+ }
+ }
+
+
+ def getRidOfSetVariables(f: MAPAFunFormula, m: Map[String,Set[String]]): MAPAFunFormula = f match {
+ case MFAnd(f1, f2) => {
+ val f1n = getRidOfSetVariables(f1, m)
+ val f2n = getRidOfSetVariables(f2, m)
+ MFAnd(f1n, f2n)
+ }
+ case MFOr(f1, f2) => {
+ val f1n = getRidOfSetVariables(f1, m)
+ val f2n = getRidOfSetVariables(f2, m)
+ MFOr(f1n, f2n)
+ }
+ case MFNot(f1) => {
+ val f1n = getRidOfSetVariables(f1, m)
+ MFNot(f1n)
+ }
+ case MFAtom(a) =>{
+ val an = getRidOfSetVariablesinAtom(a, m)
+ MFAtom(an)
+ }
+ }
+
+
+
+
+
+
+
+// ---- list of all sets
+
+ def setofAllSetsinInt(i: MAPAFunInt): Set[String] = i match {
+ case MFIntVar(v) => Set[String]()
+ case MFIntConst(c) => Set[String]()
+ case MFIPlus(i1, i2) => {
+ val l1 = setofAllSetsinInt(i1)
+ val l2 = setofAllSetsinInt(i2)
+ l1 ++ l2
+ }
+ case MFITimes(c, i1) => setofAllSetsinInt(i1)
+ case MFSCard(s) => setofAllSetsinSet(s)
+ case MFMCard(m) => setofAllSetsinMultiset(m)
+ }
+
+ def setofAllSetsinMultiset(m: MAPAFunMultiset): Set[String] = m match {
+ case MFMSetVar(v) => Set[String]()
+ case MFEmptyMSet => Set[String]()
+ case MFMUnion(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFMIntersec(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFMPlus(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFMMinus(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFSetMinus(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFSSetOf(m1) => setofAllSetsinMultiset(m1)
+ case MFFunction(f, s) => setofAllSetsinSet(s)
+ }
+
+ def setofAllSetsinSet(s: MAPAFunSet): Set[String] = s match {
+ case MFSetVar(v) => Set(v)
+ case MFEmptySet => Set[String]()
+ case MFUnivSet => Set[String]()
+ case MFSUnion(s1, s2) => {
+ val l1 = setofAllSetsinSet(s1)
+ val l2 = setofAllSetsinSet(s2)
+ l1 ++ l2
+ }
+ case MFSIntersec(s1, s2) => {
+ val l1 = setofAllSetsinSet(s1)
+ val l2 = setofAllSetsinSet(s2)
+ l1 ++ l2
+ }
+ case MFSCompl(s1) => setofAllSetsinSet(s1)
+ }
+
+ def setofAllSetsinAtom(a: MAPAFunAtom): Set[String] = a match {
+ case MFSetEqual(s1, s2) => {
+ val l1 = setofAllSetsinSet(s1)
+ val l2 = setofAllSetsinSet(s2)
+ l1 ++ l2
+ }
+ case MFSetSubset(s1, s2) => {
+ val l1 = setofAllSetsinSet(s1)
+ val l2 = setofAllSetsinSet(s2)
+ l1 ++ l2
+ }
+ case MFMSetEqual(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFMSetSubset(m1, m2) => {
+ val l1 = setofAllSetsinMultiset(m1)
+ val l2 = setofAllSetsinMultiset(m2)
+ l1 ++ l2
+ }
+ case MFIntEqual(i1, i2) => {
+ val l1 = setofAllSetsinInt(i1)
+ val l2 = setofAllSetsinInt(i2)
+ l1 ++ l2
+ }
+ case MFIntLessEqual(i1, i2) => {
+ val l1 = setofAllSetsinInt(i1)
+ val l2 = setofAllSetsinInt(i2)
+ l1 ++ l2
+ }
+ case MFIntDivides(c, i) => setofAllSetsinInt(i)
+ }
+
+ def setofAllSets(f: MAPAFunFormula): Set[String] = f match {
+ case MFAnd(f1, f2) => {
+ val s1 = setofAllSets(f1)
+ val s2 = setofAllSets(f2)
+ s1 ++ s2
+ }
+ case MFOr(f1, f2) => {
+ val s1 = setofAllSets(f1)
+ val s2 = setofAllSets(f2)
+ s1 ++ s2
+ }
+ case MFNot(f1) => setofAllSets(f1)
+ case MFAtom(a) => setofAllSetsinAtom(a)
+ }
+
+ def power2(n: Int): Int = {
+ var i = 1
+ for(k <- 1 to n) i = i * 2
+ i
+ }
+
+ def createListOfExponentialSize(n: Int): List[List[String]] = {
+ if (n == 0) Nil
+ else {
+ val ub = power2 (n - 1)
+ var l1: List[List[String]] = Nil
+ for (i <- 0 to (ub - 1) ) {
+ val s = (Integer.toBinaryString(i)).toList
+ var s1 = s.map (_.toString)
+ while (s1.length < (n - 1)) {
+ s1 = "0" :: s1
+ }
+ l1 = s1 :: l1
+ }
+ l1
+ }
+ }
+
+ def createStringfromList(i: Int, l: List[String]): String = {
+ val ln = l.take(i) ::: ( "1" :: l.drop(i) )
+ ln.mkString("S", "", "")
+ }
+
+
+ def createCubesForSet(i: Int, l: List[List[String]]): Set[String] = {
+ var s = Set[String]()
+ l.foreach(l1 => {
+ val st = createStringfromList(i, l1)
+ s = s ++ Set(st)
+ })
+ s
+ }
+
+
+ def createUniversalSetCubes(l: List[List[String]]): Set[String] = {
+ var s = Set[String]()
+ l.foreach(e => {
+ val l0 = "0" :: e
+ val s0 = l0.mkString("S", "", "")
+ s = s ++ Set(s0)
+ val l1 = "1" :: e
+ val s1 = l1.mkString("S", "", "")
+ s = s ++ Set(s1)
+ })
+ s
+ }
+
+ def createMapOfNewCubes(l: List[String]): Map[String,Set[String]] = {
+ val tm = Map[String, Set[String]]()
+ val n = l.length
+ var i = 0
+ val ls = createListOfExponentialSize(n)
+ l.foreach(e => {
+ val nl = createCubesForSet(i, ls)
+ i = i + 1
+ tm += (e -> nl)
+ }
+ )
+ val us = createUniversalSetCubes(ls)
+ tm += ("ALL" -> us)
+ tm
+ }
+
+ def listOfAllSets(f: MAPAFunFormula): Map[String,Set[String]] = {
+ val s1 = setofAllSets(f)
+ val l1 = s1.toList
+ val m1 = createMapOfNewCubes(l1)
+ m1
+ }
+
+
+//--------------------------------------
+
+ def noMoreSets(f: MAPAFunFormula): MAPAFunFormula = {
+ val l1 = listOfAllSets(f)
+ val f1 = getRidOfSetVariables(f, l1)
+ f1
+ }
+
+}
+
diff --git a/src/multisets/MAPA-FunTranslation2MAPA.scala b/src/multisets/MAPA-FunTranslation2MAPA.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ebb931b476fd89986e14764e609288bc61c1d05
--- /dev/null
+++ b/src/multisets/MAPA-FunTranslation2MAPA.scala
@@ -0,0 +1,214 @@
+package mapaFun
+
+import multisets._
+
+
+object MapaFunConversion {
+
+
+ def createFormulaThatTwoAreDisjoint(s1: String, s2: String): Formula = {
+ val a = AEqual(MIntersection(MVariable(s1), MVariable(s2)), MEmpty)
+ FAtom(a)
+ }
+
+ def createFormulaThatOneIsDisjoint(s: String, l: List[String]): Formula = {
+ val h = l.head
+ val t = l.tail
+ var ft = createFormulaThatTwoAreDisjoint(s, h)
+ t.foreach(e => {
+ val f1 = createFormulaThatTwoAreDisjoint(s, e)
+ ft = FAnd(f1, ft)
+ })
+ ft
+ }
+
+ def createFormulaForDisjointness(l: List[String]): Formula = {
+ var h = l.head
+ var t = l.tail
+ var ft = createFormulaThatOneIsDisjoint(h, t)
+ while (t.length > 1) {
+ h = t.head
+ t = t.tail
+ val f1 = createFormulaThatOneIsDisjoint(h, t)
+ ft = FAnd(f1, ft)
+ }
+ ft
+ }
+
+ def createFormulaInItIsSet(s: String): FormulaIn = {
+ val a0 = AIEq(TIMultiplicity(s), TIConstant(0))
+ val a1 = AIEq(TIMultiplicity(s), TIConstant(1))
+ FIOr(FIAtom(a0), FIAtom(a1))
+ }
+
+ def createFormulaInTheyAreSets(l: List[String]): FormulaIn = {
+ var f1 = createFormulaInItIsSet(l.head)
+ val t = l.tail
+ t.foreach(s => {
+ val ft = createFormulaInItIsSet(s)
+ f1 = FIAnd(ft, f1)
+ })
+ f1
+ }
+
+ def createFormulaTheyAreSets(l: List[String]): Formula = {
+ val f1 = createFormulaInTheyAreSets(l)
+ FAtom(AForAllElem(f1))
+ }
+
+ def createFormulaAboutSets(l: List[String]): Formula = {
+ val f1 = createFormulaTheyAreSets(l)
+ if (l.length == 1) f1 else {
+ val f2 = createFormulaForDisjointness(l)
+ FAnd(f1, f2)
+ }
+ }
+
+//-------------------
+
+ def convertMAPAFunSet2MapaMset(s: MAPAFunSet): (Multiset, Set[String]) = s match {
+ case MFSetVar(v) => (MVariable(v), Set(v))
+ case MFEmptySet => (MEmpty, Set[String]())
+ case MFSUnion(s1, s2) => {
+ val (m1, l1) = convertMAPAFunSet2MapaMset(s1)
+ val (m2, l2) = convertMAPAFunSet2MapaMset(s2)
+ (MPlus(m1, m2), l1 ++ l2)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def convertMAPAFunMset2MapaMset(m: MAPAFunMultiset): (Multiset, Set[String]) = m match {
+ case MFMSetVar(v) => (MVariable(v), Set[String]())
+ case MFEmptyMSet => (MEmpty, Set[String]())
+ case MFMUnion(m1, m2) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, l2) = convertMAPAFunMset2MapaMset(m2)
+ (MUnion(m1n, m2n), l1 ++ l2)
+ }
+ case MFMIntersec(m1, m2) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, l2) = convertMAPAFunMset2MapaMset(m2)
+ (MIntersection(m1n, m2n), l1 ++ l2)
+ }
+ case MFMPlus(m1, m2) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, l2) = convertMAPAFunMset2MapaMset(m2)
+ (MPlus(m1n, m2n), l1 ++ l2)
+ }
+ case MFMMinus(m1, m2) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, l2) = convertMAPAFunMset2MapaMset(m2)
+ (MMinus(m1n, m2n), l1 ++ l2)
+ }
+ case MFSetMinus(m1, m2) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, l2) = convertMAPAFunMset2MapaMset(m2)
+ (MSetMinus(m1n, m2n), l1 ++ l2)
+ }
+ case MFSSetOf(m1) => {
+ val (m1n, l1) = convertMAPAFunMset2MapaMset(m1)
+ (MSetOf(m1n), l1)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+
+ def convertMAPAFunint2MapaTO(i: MAPAFunInt): (TermOut, Set[String]) = i match {
+ case MFIntVar(v) => (TOVariable(v), Set[String]())
+ case MFIntConst(c) => (TOConstant(c), Set[String]())
+ case MFIPlus(i1, i2) => {
+ val (t1, l1) = convertMAPAFunint2MapaTO(i1)
+ val (t2, l2) = convertMAPAFunint2MapaTO(i2)
+ (TOPlus(t1, t2), l1 ++ l2)
+ }
+ case MFITimes(c, i1) => {
+ val (t1, l1) = convertMAPAFunint2MapaTO(i1)
+ (TOTimes(c, t1), l1)
+ }
+ case MFSCard(s) => {
+ val (m1, l1) = convertMAPAFunSet2MapaMset(s)
+ (TOCard(m1), l1)
+ }
+ case MFMCard(m) => {
+ val (m1, l1) = convertMAPAFunMset2MapaMset(m)
+ (TOCard(m1), l1)
+ }
+ }
+
+ def createFreshTO(n: Int): TermOut = {
+ val s = "FRESHInt" + n
+ TOVariable(s)
+ }
+
+ def convertAtomAndGetSets(a: MAPAFunAtom, i: Int): (Formula, Set[String], Int) = a match {
+ case MFSetEqual(s1, s2) => {
+ val (m1, sl1) = convertMAPAFunSet2MapaMset(s1)
+ val (m2, sl2) = convertMAPAFunSet2MapaMset(s2)
+ (FAtom(AEqual(m1, m2)), sl1 ++ sl2, i)
+ }
+ case MFSetSubset(s1, s2) => {
+ val (m1, sl1) = convertMAPAFunSet2MapaMset(s1)
+ val (m2, sl2) = convertMAPAFunSet2MapaMset(s2)
+ (FAtom(ASubset(m1, m2)), sl1 ++ sl2, i)
+ }
+ case MFMSetEqual(m1, m2) => {
+ val (m1n, sl1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, sl2) = convertMAPAFunMset2MapaMset(m2)
+ (FAtom(AEqual(m1n, m2n)), sl1 ++ sl2, i)
+ }
+ case MFMSetSubset(m1, m2) => {
+ val (m1n, sl1) = convertMAPAFunMset2MapaMset(m1)
+ val (m2n, sl2) = convertMAPAFunMset2MapaMset(m2)
+ (FAtom(ASubset(m1n, m2n)), sl1 ++ sl2, i)
+ }
+ case MFIntEqual(i1, i2) => {
+ val (i1n, sl1) = convertMAPAFunint2MapaTO(i1)
+ val (i2n, sl2) = convertMAPAFunint2MapaTO(i2)
+ (FAtom(AAtomOut(AOEq(i1n, i2n))), sl1 ++ sl2, i)
+ }
+ case MFIntLessEqual(i1, i2) => {
+ val (i1n, sl1) = convertMAPAFunint2MapaTO(i1)
+ val (i2n, sl2) = convertMAPAFunint2MapaTO(i2)
+ (FAtom(AAtomOut(AOLeq(i1n, i2n))), sl1 ++ sl2, i)
+ }
+ case MFIntDivides(c, i1) => {
+ val (i1n, sl1) = convertMAPAFunint2MapaTO(i1)
+ val ft = createFreshTO(i)
+ (FAtom(AAtomOut(AOEq(ft, TOTimes(c, i1n)))), sl1, i + 1)
+ }
+ }
+
+ def convertFormulaAndGetSets(f: MAPAFunFormula, i: Int): (Formula, Set[String], Int) = f match {
+ case MFAnd(f1, f2) => {
+ val (f1n, s1, i1) = convertFormulaAndGetSets(f1, i)
+ val (f2n, s2, i2) = convertFormulaAndGetSets(f2, i1)
+ (FAnd(f1n, f2n), s1 ++ s2, i2)
+ }
+ case MFOr(f1, f2) => {
+ val (f1n, s1, i1) = convertFormulaAndGetSets(f1, i)
+ val (f2n, s2, i2) = convertFormulaAndGetSets(f2, i1)
+ (FOr(f1n, f2n), s1 ++ s2, i2)
+ }
+ case MFNot(f1) => {
+ val (f1n, s1, i1) = convertFormulaAndGetSets(f1, i)
+ (FNot(f1n), s1, i1)
+ }
+ case MFAtom(a) => convertAtomAndGetSets(a, i)
+ }
+
+
+//--------------------------------
+
+ def mapaFun2standardMAPA(f: MAPAFunFormula): Formula = {
+ val (f1, s, _) = convertFormulaAndGetSets(f, 0)
+// i counts fresh variables introduced for divides
+ val l = s.toList
+ if (l.isEmpty) f1 else {
+ val f2 = createFormulaAboutSets(l)
+ val ff = FAnd(f1, f2)
+ ff
+ }
+ }
+
+
+}
\ No newline at end of file
diff --git a/src/multisets/MAPAParser.scala b/src/multisets/MAPAParser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0e032cd440c79a261dee669c3672ad9438a058a3
--- /dev/null
+++ b/src/multisets/MAPAParser.scala
@@ -0,0 +1,213 @@
+package multisets
+
+import scala.util.parsing.combinator.syntactical.StandardTokenParsers
+import scala.util.parsing.combinator._
+import scala.util.parsing.input._
+import scala.util.parsing.syntax._
+import scala.collection.mutable.Map
+import java.io.FileReader
+
+
+object MAPAParser extends StandardTokenParsers {
+
+ lexical.delimiters ++= List( "(", ")", ",", ".", ":", "=", "<", "_", "{", "}", "+", "|", "-", "*" );
+ lexical.reserved ++= List( "Problem", "Variables", "Formula", "And", "Or",
+ "Implies", "Equiv", "Not", "true", "false", "SUB", "ALLe", "VEC", "ite", "e",
+ "empty", "INTR", "UN", "PLUS", "SETof", "SUM" );
+
+
+ def inputFile: Parser[ List[(String, (Map[String, String], Formula))] ] = (
+ rep(oneProblemInFile)
+ | failure( "Cannot parse the input file." ))
+
+
+ def oneProblemInFile: Parser[(String, (Map[String, String], Formula))] = (
+ ("Problem" ~> "(" ~> ident <~ ",") ~ ("Variables" ~> "(" ~> myVars <~ ")" <~ ",") ~ ("Formula" ~> "(" ~> myFla <~ ")" <~ ")" <~ "." ) ^^
+ { case name ~ vars ~ fla => (name.toString, (vars, fla) ) }
+ | failure( "Cannot parse this problem." ))
+
+
+ def myVars: Parser[ Map[String, String] ] = (
+ repsep(oneVar, ",") ^^ createMap
+ | failure( "Cannot parse this Variables string." ))
+
+ def oneVar: Parser[ (String, String) ] = (
+ (ident ~ ":" ~ ident)^^ { case name ~ ":" ~ typeV => (name.toString, typeV.toString ) }
+ | failure( "Cannot parse this variable." ))
+
+ def createMap(l: List[(String, String)]): Map[String, String] = {
+ val m = Map[String, String]()
+ l.foreach(p => m += (p._1 -> p._2))
+ m
+ }
+
+
+ def myFla: Parser[ Formula ] = (
+ myAtom ^^ (FAtom(_))
+ | ("And" ~> "(" ~> myFla <~ ",") ~ (myFla <~ ")")^^ {case f1 ~ f2 => FAnd(f1, f2)}
+ | ("Or" ~> "(" ~> myFla <~ ",") ~ (myFla <~ ")")^^ {case f1 ~ f2 => FOr(f1, f2)}
+ | ("Implies" ~> "(" ~> myFla <~ ",") ~ (myFla <~ ")")^^ {case f1 ~ f2 => FOr(FNot(f1), f2)}
+ | ("Equiv" ~> "(" ~> myFla <~ ",") ~ (myFla <~ ")")^^ {case f1 ~ f2 => FOr(FAnd(f1, f2), FAnd(FNot(f1), FNot(f2)))}
+ | ("Not" ~> "(" ~> myFla <~ ")") ^^ {case f1 => FNot(f1)}
+ | "true" ^^ (f => FTrue)
+ | "false" ^^ (f => FFalse)
+ | failure( "Cannot parse this Formula string." ))
+
+
+ def myAtom: Parser[ Atom ] = (
+ myAtomOut ^^ (AAtomOut(_))
+ | ("=" ~> "(" ~> myMset <~ ",") ~ (myMset <~ ")")^^ { case m1 ~ m2 => AEqual(m1, m2) }
+ | ("SUB" ~> "(" ~> myMset <~ ",") ~ (myMset <~ ")")^^ { case m1 ~ m2 => ASubset(m1, m2) }
+ | ("ALLe" ~> "." ~> myFlaIn)^^ { case f1 => AForAllElem(f1) }
+ | failure( "Cannot parse this atom." ))
+
+
+ def myFlaOut: Parser[ FormulaOut ] = (
+ myAtomOut ^^ (FOAtom(_))
+ | ("And" ~> "(" ~> myFlaOut <~ ",") ~ (myFlaOut <~ ")")^^ {case f1 ~ f2 => FOAnd(f1, f2)}
+ | ("Or" ~> "(" ~> myFlaOut <~ ",") ~ (myFlaOut <~ ")")^^ {case f1 ~ f2 => FOOr(f1, f2)}
+ | ("Implies" ~> "(" ~> myFlaOut <~ ",") ~ (myFlaOut <~ ")")^^ {case f1 ~ f2 => FOOr(FONot(f1), f2)}
+ | ("Equiv" ~> "(" ~> myFlaOut <~ ",") ~ (myFlaOut <~ ")")^^ {case f1 ~ f2 => FOOr(FOAnd(f1, f2), FOAnd(FONot(f1), FONot(f2)))}
+ | ("Not" ~> "(" ~> myFlaOut <~ ")") ^^ {case f1 => FONot(f1)}
+ | "true" ^^ (f => FOTrue)
+ | "false" ^^ (f => FOFalse)
+ | failure( "Cannot parse this formula." ))
+
+
+ def myAtomOut: Parser[ AtomOut ] = (
+ ("=" ~> "(" ~> myTrmOut <~ ",") ~ (myTrmOut <~ ")")^^ { case i1 ~ i2 => AOEq(i1, i2) }
+ | ("<" ~> "=" ~> "(" ~> myTrmOut <~ ",") ~ (myTrmOut <~ ")")^^ { case i1 ~ i2 => AOLeq(i1, i2) }
+ | ("=" ~> "(" ~> "VEC" ~> "(" ~> myListTrmOut <~ ")" <~"," ) ~ ("SUM" ~> "_" ~> "{" ~> myFlaIn <~ "}") ~
+ ("VEC" ~> "(" ~> myListTrmIn <~ ")" <~ ")") ^^ { case l1 ~ f ~ l2 => AOSum(l1, f, l2) }
+ | failure( "Cannot parse this atom." ))
+
+
+ def myListTrmOut: Parser[ List[TermOut] ] = (
+ repsep(myTrmOut, ",")
+ | failure( "Cannot parse this vector." ))
+
+
+ def myTrmOut: Parser[ TermOut ] = (
+ myInt ^^ {case n => TOConstant(n) }
+ | ident ^^ {case s => TOVariable(s.toString) }
+ | ("*" ~> "(" ~> myInt <~ ",") ~ (myTrmOut <~ ")") ^^ {case n ~ t => TOTimes(n, t) }
+ | ("|" ~> myMset <~ "|") ^^ { case m => TOCard(m) }
+ | ("+" ~> "(" ~> myListTrmOut <~ ")") ^^ createSumOfOutterTerms
+ | ("ite" ~> "(" ~> myFlaOut <~ ",") ~ myTrmOut ~ ("," ~> myTrmOut <~ ")") ^^ { case f ~ t1 ~ t2 => TOIte(f, t1, t2) }
+ | failure( "Cannot parse this term." ))
+
+
+ def createSumOfOutterTerms(l: List[TermOut]): TermOut = {
+ if (l.isEmpty) TOConstant(0) else {
+ var t = l.head
+ val l1 = l.tail
+ l1.foreach(e => t = TOPlus(t, e))
+ t
+ }
+ }
+
+
+ def myFlaIn: Parser[ FormulaIn ] = (
+ myAtomIn ^^ (FIAtom(_))
+ | ("And" ~> "(" ~> myFlaIn <~ ",") ~ (myFlaIn <~ ")")^^ {case f1 ~ f2 => FIAnd(f1, f2)}
+ | ("Or" ~> "(" ~> myFlaIn <~ ",") ~ (myFlaIn <~ ")")^^ {case f1 ~ f2 => FIOr(f1, f2)}
+ | ("Implies" ~> "(" ~> myFlaIn <~ ",") ~ (myFlaIn <~ ")")^^ {case f1 ~ f2 => FIOr(FINot(f1), f2)}
+ | ("Equiv" ~> "(" ~> myFlaIn <~ ",") ~ (myFlaIn <~ ")")^^ {case f1 ~ f2 => FIOr(FIAnd(f1, f2), FIAnd(FINot(f1), FINot(f2)))}
+ | ("Not" ~> "(" ~> myFlaIn <~ ")") ^^ {case f1 => FINot(f1)}
+ | "true" ^^ (f => FITrue)
+ | "false" ^^ (f => FIFalse)
+ | failure( "Cannot parse this formula." ))
+
+
+ def myAtomIn: Parser[ AtomIn ] = (
+ ("=" ~> "(" ~> myTrmIn <~ ",") ~ (myTrmIn <~ ")") ^^ { case i1 ~ i2 => AIEq(i1, i2) }
+ | ("<" ~> "=" ~> "(" ~> myTrmIn <~ ",") ~ (myTrmIn <~ ")") ^^ { case i1 ~ i2 => AILeq(i1, i2) }
+ | failure( "Cannot parse this atom." ))
+
+
+ def myListTrmIn: Parser[ List[TermIn] ] = (
+ repsep(myTrmIn, ",")
+ | failure( "Cannot parse this vector." ))
+
+
+ def myTrmIn: Parser[ TermIn ] = (
+ myInt ^^ {case n => TIConstant(n) }
+ | (ident <~ "(" <~ "e" <~ ")") ^^ { case s => TIMultiplicity(s.toString) }
+ | ("*" ~> "(" ~> myInt <~ ",") ~ (myTrmIn <~ ")") ^^ {case n ~ t => TITimes(n, t) }
+ | ("+" ~> "(" ~> myListTrmIn <~ ")") ^^ createSumOfInnerTerms
+ | ("ite" ~> "(" ~> myFlaIn <~ ",") ~ myTrmIn ~ ("," ~> myTrmIn <~ ")") ^^ { case f ~ t1 ~ t2 => TIIte(f, t1, t2) }
+ | failure( "Cannot parse this term." ))
+
+ def createSumOfInnerTerms(l: List[TermIn]): TermIn = {
+ if (l.isEmpty) TIConstant(0) else {
+ var t = l.head
+ val l1 = l.tail
+ l1.foreach(e => t = TIPlus(t, e))
+ t
+ }
+ }
+
+
+ def myInt: Parser[ Int ] = (
+ "-" ~> numericLit ^^ (x => x.toInt * -1)
+ | numericLit ^^ ( x => x.toInt )
+ | failure( "Cannot parse this number." ))
+
+
+ def myMset: Parser[ Multiset ] = (
+ ident ^^ { case s => MVariable(s.toString) }
+ | "empty" ^^ { x => MEmpty}
+ | ("INTR" ~> "(" ~> myListMset <~ ")") ^^ createIntersectionOfMSets
+ | ("UN" ~> "(" ~> myListMset <~ ")") ^^ createUnionOfMSets
+ | ("PLUS" ~> "(" ~> myListMset <~ ")") ^^ createSumOfMSets
+ | ("-" ~> "(" ~> myMset <~ ",") ~ (myMset <~ ")") ^^ {case m1 ~ m2 => MMinus(m1, m2) }
+ | ("-" ~> "-" ~> "(" ~> myMset <~ ",") ~ (myMset <~ ")") ^^ {case m1 ~ m2 => MSetMinus(m1, m2) }
+ | ("SETof" ~> "(" ~> myMset <~ ")") ^^ {case m => MSetOf(m) }
+ | failure( "Cannot parse this multiset." ))
+
+ def createIntersectionOfMSets(l: List[Multiset]): Multiset = {
+ if (l.isEmpty) MEmpty else {
+ var t = l.head
+ val l1 = l.tail
+ l1.foreach(e => t = MIntersection(t, e))
+ t
+ }
+ }
+
+ def createUnionOfMSets(l: List[Multiset]): Multiset = {
+ if (l.isEmpty) MEmpty else {
+ var t = l.head
+ val l1 = l.tail
+ l1.foreach(e => t = MUnion(t, e))
+ t
+ }
+ }
+
+ def createSumOfMSets(l: List[Multiset]): Multiset = {
+ if (l.isEmpty) MEmpty else {
+ var t = l.head
+ val l1 = l.tail
+ l1.foreach(e => t = MPlus(t, e))
+ t
+ }
+ }
+
+
+ def myListMset: Parser[ List[Multiset] ] = (
+ repsep(myMset, ",")
+ | failure( "Cannot parse this vector." ))
+
+
+
+//------------------------------------------------
+
+ def main(fileName: String) : List[(String, (Map[String, String], Formula))] = {
+ val reader = StreamReader(new FileReader(fileName))
+ val tokens = new lexical.Scanner(reader)
+ phrase(inputFile)(tokens) match {
+ case Success( mapping, _ ) => mapping
+ case e => throw(new Exception("Error = " + e))
+ }
+ }
+}
+
diff --git a/src/multisets/MAPARun.scala b/src/multisets/MAPARun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7bbf5b98231e349198bfedf5aff660c86cff26bf
--- /dev/null
+++ b/src/multisets/MAPARun.scala
@@ -0,0 +1,131 @@
+package multisets
+
+
+import multisets.MultisetFormulaPrinter._
+import multisets.StarFormulaPrinter._
+
+
+
+object MAPARun {
+
+// start: describes the execution of checking satisfiability of one formula
+ def executeOneFormula (name: String, f: Formula): Boolean = {
+ println("Formula " + name + ":")
+ print_multisetFormula(f)
+ println("")
+ val (x, y, z) = multisets.NormalFormTranslator.main(f)
+ val fF = FAnd(x, FAnd(y, z))
+ println("Normalized formula " + name + ":")
+ print_multisetFormula(fF)
+ println("")
+ val (fS1, lS1, lS2, fS2) = multisets.Multiset2StarsTranslator.main(x, y, z)
+ val fS = StarFormula(fS1, lS1, lS2, fS2)
+ println("Translated formula " + name + ":")
+ print_starFormula(fS)
+ println("")
+ val (lS2N, listDNFfS2) = multisets.CreateDisjunctions.main(lS2, fS2)
+ val (ff, lpf) = multisets.RemoveDisjunctions.main(fS1, lS1, lS2N, listDNFfS2)
+ println("No more disjunctions:")
+ print_QFPAFormula(ff)
+ println(" AND " )
+ lpf.foreach(t => {
+ print_PAVector(t._1)
+ print( " IN { ")
+ print_PAVector(t._2)
+ print( " | ")
+ (t._3).foreach(c => {
+ print_QFPAFormula(c)
+ print(" AND ")
+ })
+ print( " } ^* ")
+ println(" AND " )
+ })
+ println("Semilinear set computation :")
+ val ff1 = multisets.RemoveStars.removeStarsMain(ff, lpf)
+ println("No more stars: ")
+ print_QFPAFormula(ff1)
+ val l = multisets.CheckingConsistency.checkConsistencyofOneFormula(ff1)
+ val bs = l._1
+ val b = if (bs == "sat") true else false
+ println("")
+ println("---------------------")
+ if (b) {
+ println ("This formula is " + bs)
+ println("")
+ println("---------------------")
+/* println("Here is the satisfying assignment:")
+ val m1 = guru.multisets.reconstructingModels.createSatisfyingAssignmentforQFPA(l)
+ println(m1)
+ println("")
+ println("After removing mu's and nu's : ")
+ val ff1t = guru.multisets.reconstructingModels.evaluateFormulaForVariablesStartingWith(ff1, m1, "FRESHnu")
+ val ff1s = guru.multisets.reconstructingModels.evaluateFormulaForVariablesStartingWith(ff1t, m1, "FRESHmu")
+ print_QFPAFormula(ff1s)
+ println("")
+ println("")
+ println("After removing obsolete disjuntions: ")
+ var ff2s = ff1s
+ var ltm: List[(List[TermQFPA], List[TermQFPA], List[QFPAFormula])] = Nil
+ lpf.foreach(t => {
+ if (guru.multisets.reconstructingModels.isNulVectorinGivenModel(t._1, m1)) {
+ val ff3s = guru.multisets.reconstructingModels.removeZeroVectorInFormula(ff2s, t._1)
+ ff2s = ff3s
+ } else ltm = t :: ltm
+ })
+ print_QFPAFormula(ff2s)
+ println("")
+ println("")
+ println("Star formulas and no disjunctions:")
+ print_QFPAFormula(ff)
+ println(" AND " )
+ ltm.foreach(t => {
+ print_PAVector(t._1)
+ print( " IN { ")
+ print_PAVector(t._2)
+ print( " | ")
+ (t._3).foreach(c => {
+ print_QFPAFormula(c)
+ print(" AND ")
+ })
+ print( " } ^* ")
+ println(" AND " )
+ })
+ println("")
+
+ println("Introduce the real values of vectors : ")
+ val ff4 = guru.multisets.reconstructingModels.evaluateFormulaForVariablesStartingWith(ff2s, m1, "FRESHu")
+ print_QFPAFormula(ff4) */
+ } else { println("")
+ println ("This formula is " + bs)
+ println("")
+ println("---------------------")
+ }
+ b
+ }
+// end
+
+
+
+ def run(fileName: String): Unit = {
+ val problemList = multisets.MAPAParser.main(fileName)
+ val formulasList = multisets.FormulaConstructor.main(problemList)
+ // all returned formulas are in NNF
+ formulasList.foreach(p => {
+ val flas = p._2
+ val fOrig = flas._1
+ val fOrigNeg = flas._2
+ val fCons = flas._3
+ val isValid = (executeOneFormula(p._1, FAnd(fOrigNeg, fCons)) == false)
+ if (isValid) println("This means that the original problem " + p._1 + " is valid.") else {
+ println("This was a model for the negated formula. Now we check the original formula:")
+ val isUnsat = (executeOneFormula(p._1, FAnd(fOrig, fCons)) == false)
+ if (isUnsat) println("This means, that the original problem " + p._1 + " is unsatisfiable.") else {
+ println("This means that the original problem " + p._1 + " is satisfiable, but not valid.")
+ }
+ }
+ })
+ }
+
+
+
+}
\ No newline at end of file
diff --git a/src/multisets/Main.scala b/src/multisets/Main.scala
index 3da74362d84ccc9d7bc38ba4bb24b0aee393a0e0..a44d23e4a3815adb42f77eb144a62c443ff9f59b 100644
--- a/src/multisets/Main.scala
+++ b/src/multisets/Main.scala
@@ -4,12 +4,59 @@ import purescala.Extensions.Solver
import purescala.Reporter
import purescala.Trees._
+import scala.collection.mutable.Set
+
+
+
class Main(reporter: Reporter) extends Solver(reporter) {
val description = "Multiset Solver"
- override def shortDescription = "MUNCH"
+ Global.reporter = reporter
- def solve(expr: Expr) : Option[Boolean] = {
- reporter.info("Don't know how to solve anything.")
- None
+
+
+ def createFormulaThatSomethingsIsSet(s:String):FormulaIn = {
+ val a1 = FIAtom(AIEq(TIMultiplicity(s), TIConstant(1)))
+ val a0 = FIAtom(AIEq(TIMultiplicity(s), TIConstant(0)))
+ FIOr(a1, a0)
+ }
+
+
+ def constructFormulaInAboutSets(s:Set[String]):FormulaIn = {
+ val sl = s.toList
+ val h = sl.head
+ val t = sl.tail
+ var f = createFormulaThatSomethingsIsSet(h)
+ t.foreach(e => {
+ val ft = createFormulaThatSomethingsIsSet(e)
+ f = FIAnd(f, ft)
+ })
+ f
}
+
+ def constructFormulaAboutSets(s:Set[String]):Formula = {
+ val f1 = constructFormulaInAboutSets(s)
+ FAtom(AForAllElem(f1))
+ }
+
+ def createFormula(p:(Formula,Set[String])):Formula = {
+ val f1 = p._1
+ val s = p._2
+ val f = if (s.isEmpty) f1 else {
+ val f2 = constructFormulaAboutSets(s)
+ FAnd(f1, f2)
+ }
+ f
+ }
+
+
+ def solve(expr: Expr) : Option[Boolean] = {
+ val mt = multisets.MainAST2MultisetsTranslator.translate(negate(expr))
+ val mf = mt.map(p => createFormula(p))
+ val res = mf.map(f => !MAPARun.executeOneFormula("f", f))
+ res
+ }
+}
+
+object Global {
+ var reporter: Reporter = null
}
diff --git a/src/multisets/MainAST2MultisetsTranslator.scala b/src/multisets/MainAST2MultisetsTranslator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1ee14440de20fab2d647c0eb5d4be64675660df1
--- /dev/null
+++ b/src/multisets/MainAST2MultisetsTranslator.scala
@@ -0,0 +1,226 @@
+package multisets
+
+import purescala.Trees._
+import purescala.TypeTrees._
+
+import scala.collection.mutable.Set
+
+
+
+object MainAST2MultisetsTranslator {
+
+
+ def translate(expr: Expr) : Option[(Formula, Set[String])] = {
+ case class CantTranslateExpression() extends Exception
+
+
+ def multisetTranslate(m: Expr): (Multiset, Set[String]) = m match {
+ case v @ Variable(id) if v.getType.isInstanceOf[MultisetType] => (MVariable(id.uniqueName), Set.empty[String])
+ case EmptyMultiset(_) => (MEmpty, Set.empty[String])
+ case MultisetIntersection(m1, m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (MIntersection(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case MultisetUnion(m1, m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (MUnion(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case MultisetPlus(m1, m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (MPlus(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case MultisetDifference(m1, m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (MMinus(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case MultisetToSet(m1) => {
+ val p1 = multisetTranslate(m1)
+ (MSetOf(p1._1), p1._2)
+ }
+ }
+
+ def termOutTranslate(exp: Expr): (TermOut, Set[String]) = exp match {
+ case v @ Variable(id) if v.getType == Int32Type => (TOVariable(id.uniqueName), Set.empty[String])
+ case IntLiteral(v) => (TOConstant(v), Set.empty[String])
+ case MultisetCardinality(m) => {
+ val mN = multisetTranslate(m)
+ (TOCard(mN._1), mN._2)
+ }
+ case SetCardinality(s) => {
+ val mN = setTranslate(s)
+ (TOCard(mN._1), mN._2)
+ }
+ case Plus(t1, t2) => {
+ val p1 = termOutTranslate(t1)
+ val p2 = termOutTranslate(t2)
+ (TOPlus(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case Minus(t1, t2) => {
+ val p1 = termOutTranslate(t1)
+ val p2 = termOutTranslate(t2)
+ (TOPlus(p1._1, TOTimes(-1, p2._1)), p1._2 ++ p2._2)
+ }
+ }
+
+ def setTranslate(s: Expr): (Multiset, Set[String]) = s match {
+ case v @ Variable(id) if v.getType.isInstanceOf[SetType] => (MVariable(id.uniqueName), Set(id.uniqueName))
+ case EmptySet(_) => (MEmpty, Set.empty[String])
+ case SetIntersection(s1, s2) => {
+ val p1 = setTranslate(s1)
+ val p2 = setTranslate(s2)
+ (MIntersection(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case SetUnion(s1, s2) => {
+ val p1 = setTranslate(s1)
+ val p2 = setTranslate(s2)
+ (MUnion(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case SetDifference(s1, s2) => {
+ val p1 = setTranslate(s1)
+ val p2 = setTranslate(s2)
+ (MMinus(p1._1, p2._1), p1._2 ++ p2._2)
+ }
+ case MultisetToSet(m1) => {
+ val p1 = multisetTranslate(m1)
+ (MSetOf(p1._1), p1._2)
+ }
+ }
+
+
+
+
+
+
+ def createFormulaFromAndSeq(fs: Seq[Formula]): Formula = {
+ val f = if (fs.isEmpty) FTrue else {
+ var ft = fs.head
+ val t = fs.tail
+ t.foreach(f1 => ft = FAnd(f1, ft))
+ ft
+ }
+ f
+ }
+
+ def createFormulaFromOrSeq(fs: Seq[Formula]): Formula = {
+ val f = if (fs.isEmpty) FTrue else {
+ var ft = fs.head
+ val t = fs.tail
+ t.foreach(f1 => ft = FOr(f1, ft))
+ ft
+ }
+ f
+ }
+
+
+ def createUnionOfAllSets(s: Seq[Set[String]]): Set[String] = {
+ val sr = if (s.isEmpty) Set.empty[String] else {
+ var h = s.head
+ val t = s.tail
+ t.foreach(v => h = h ++ v)
+ h
+ }
+ sr
+ }
+
+/*
+ case class UMinus(expr: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ }
+ case class Times(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ }
+ case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ } */
+
+
+ def rec(ex: Expr) : (Formula, Set[String]) = ex match {
+ case MultisetEquals(m1,m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (FAtom(AEqual(p1._1, p2._1)), p1._2 ++ p2._2)
+ }
+ case SubmultisetOf(m1,m2) => {
+ val p1 = multisetTranslate(m1)
+ val p2 = multisetTranslate(m2)
+ (FAtom(ASubset(p1._1, p2._1)), p1._2 ++ p2._2)
+ }
+ case SetEquals(s1,s2) => {
+ val p1 = setTranslate(s1)
+ val p2 = setTranslate(s2)
+ (FAtom(AEqual(p1._1, p2._1)), p1._2 ++ p2._2)
+ }
+ case SubsetOf(s1,s2) => {
+ val p1 = setTranslate(s1)
+ val p2 = setTranslate(s2)
+ (FAtom(ASubset(p1._1, p2._1)), p1._2 ++ p2._2)
+ }
+ case And(expS) => {
+ val pl = expS.map(e => rec(e))
+ val fl = pl.map(p => p._1)
+ val sl = pl.map(p => p._2)
+ val f1 = createFormulaFromAndSeq(fl)
+ val s1 = createUnionOfAllSets(sl)
+ (f1, s1)
+ }
+ case Or(expS) => {
+ val pl = expS.map(e => rec(e))
+ val fl = pl.map(p => p._1)
+ val sl = pl.map(p => p._2)
+ val f1 = createFormulaFromOrSeq(fl)
+ val s1 = createUnionOfAllSets(sl)
+ (f1, s1)
+ }
+ case Iff(f1, f2) => {
+ val p1 = rec(f1)
+ val p2 = rec(f2)
+ (FOr(FAnd(FNot(p1._1), FNot(p2._1)), FAnd(p1._1, p2._1)), p1._2 ++ p2._2)
+ }
+ case Implies(f1, f2) => {
+ val p1 = rec(f1)
+ val p2 = rec(f2)
+ (FOr(FNot(p1._1), p2._1), p1._2 ++ p2._2)
+ }
+ case Not(f1) => {
+ val p1 = rec(f1)
+ (FNot(p1._1), p1._2)
+ }
+ case LessThan(t1, t2) => {
+ val p1 = termOutTranslate(t1)
+ val p2 = termOutTranslate(t2)
+ (FAnd(FAtom(AAtomOut(AOLeq(p1._1, p2._1))), FNot(FAtom(AAtomOut(AOEq(p1._1, p2._1))))), p1._2 ++ p2._2)
+ }
+ case GreaterThan(t1, t2) => rec(LessThan(t2, t1))
+ case LessEquals(t1, t2) => {
+ val p1 = termOutTranslate(t1)
+ val p2 = termOutTranslate(t2)
+ (FAtom(AAtomOut(AOLeq(p1._1, p2._1))), p1._2 ++ p2._2)
+ }
+ case GreaterEquals(t1, t2) => rec(LessEquals(t2, t1))
+ case Equals(t1, t2) => {
+ val p1 = termOutTranslate(t1)
+ val p2 = termOutTranslate(t2)
+ (FAtom(AAtomOut(AOEq(p1._1, p2._1))), p1._2 ++ p2._2)
+ }
+ case unhandled => {
+ Global.reporter.warning("Can't translate this in Munch : " + unhandled)
+ throw CantTranslateExpression()
+ }
+ }
+
+
+ try {
+ Some(rec(expandLets(expr)))
+ } catch {
+ case CantTranslateExpression() => None
+ }
+
+ }
+
+
+}
+
diff --git a/src/multisets/Multiset.scala b/src/multisets/Multiset.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1fd8d77982fc1db010c6aed7b767e5496131abe7
--- /dev/null
+++ b/src/multisets/Multiset.scala
@@ -0,0 +1,20 @@
+// piskac@larapc01:~/guru$ pwd
+// /home/piskac/guru
+// piskac@larapc01:~/guru$ scalac -d bin/ src/guru/multisets/*.scala
+// piskac@larapc01:~/guru$ scala -cp bin/ guru.multisets.Main
+
+package multisets
+
+
+object Multisets {
+
+ def main(args: Array[String]) : Unit = {
+ if (args.length == 0) {
+ println("Usage: scala -cp bin/ guru.multisets.Main fileName ")
+ } else {
+ val fileName = args(0)
+ multisets.MAPARun.run(fileName)
+ }
+ }
+}
+
diff --git a/src/multisets/Multiset2StarsTranslator.scala b/src/multisets/Multiset2StarsTranslator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..82c372b7e159efe4bd4bc13121a153c77b75c91e
--- /dev/null
+++ b/src/multisets/Multiset2StarsTranslator.scala
@@ -0,0 +1,246 @@
+package multisets
+
+object Multiset2StarsTranslator {
+
+
+// start:
+
+ def translate2QFPAfromFormulaOut(f:FormulaOut):QFPAFormula = f match {
+ case FOAnd(f1,f2) => {
+ val f1n = translate2QFPAfromFormulaOut(f1)
+ val f2n = translate2QFPAfromFormulaOut(f2)
+ QFPAAnd(f1n, f2n)
+ }
+ case FOOr(f1,f2) => {
+ val f1n = translate2QFPAfromFormulaOut(f1)
+ val f2n = translate2QFPAfromFormulaOut(f2)
+ QFPAOr(f1n, f2n)
+ }
+ case FONot(f1) => {
+ val f1n = translate2QFPAfromFormulaOut(f1)
+ QFPANot(f1n)
+ }
+ case FOAtom(a) => {
+ val a1 = translate2QFPAAtomfromAtomOut(a)
+ QFPAAtom(a1)
+ }
+ case FOTrue => QFPATrue
+ case FOFalse => QFPAFalse
+ }
+
+
+ def translate2QFPATermfromTermOut(t:TermOut):TermQFPA = t match {
+ case TOConstant(c) => TConstant(c)
+ case TOVariable(v) => TVariable(v)
+ case TOPlus(t1, t2) => {
+ val t1n = translate2QFPATermfromTermOut(t1)
+ val t2n = translate2QFPATermfromTermOut(t2)
+ TPlus(t1n, t2n)
+ }
+ case TOTimes(c, t1)=> {
+ val t1n = translate2QFPATermfromTermOut(t1)
+ TTimes(c, t1n)
+ }
+ case TOIte(f, t1, t2)=> {
+ val f1 = translate2QFPAfromFormulaOut(f)
+ val t1n = translate2QFPATermfromTermOut(t1)
+ val t2n = translate2QFPATermfromTermOut(t2)
+ TIte(f1,t1n, t2n)
+ }
+ case _ => error("Impossible case ")
+ }
+
+ def translate2QFPAAtomfromAtomOut(a:AtomOut):AtomQFPA = a match {
+ case AOLeq(t1,t2) => {
+ val t1n = translate2QFPATermfromTermOut(t1)
+ val t2n = translate2QFPATermfromTermOut(t2)
+ ALeq(t1n, t2n)
+ }
+ case AOEq(t1,t2) => {
+ val t1n = translate2QFPATermfromTermOut(t1)
+ val t2n = translate2QFPATermfromTermOut(t2)
+ AEq(t1n, t2n)
+ }
+ case _ => error("Impossible case ")
+ }
+
+ def translate2QFPAfromFormula(f:Formula):QFPAFormula = f match {
+ case FAnd(f1,f2) => {
+ val f1n = translate2QFPAfromFormula(f1)
+ val f2n = translate2QFPAfromFormula(f2)
+ QFPAAnd(f1n, f2n)
+ }
+ case FOr(f1,f2) => {
+ val f1n = translate2QFPAfromFormula(f1)
+ val f2n = translate2QFPAfromFormula(f2)
+ QFPAOr(f1n, f2n)
+ }
+ case FNot(f1) => {
+ val f1n = translate2QFPAfromFormula(f1)
+ QFPANot(f1n)
+ }
+ case FAtom(AAtomOut(a)) => {
+ val a1 = translate2QFPAAtomfromAtomOut(a)
+ QFPAAtom(a1)
+ }
+ case FFalse => QFPAFalse
+ case FTrue => QFPATrue
+ case _ => error("Impossible case ")
+ }
+
+
+ def translate2QFPATermfromTermIn(t:TermIn):TermQFPA = t match {
+ case TIMultiplicity(v) => TVariable(v)
+ case TIConstant(c) => TConstant(c)
+ case TIPlus(t1, t2) => {
+ val t1n = translate2QFPATermfromTermIn(t1)
+ val t2n = translate2QFPATermfromTermIn(t2)
+ TPlus(t1n, t2n)
+ }
+ case TITimes(c, t1)=> {
+ val t1n = translate2QFPATermfromTermIn(t1)
+ TTimes(c, t1n)
+ }
+ case TIIte(f, t1, t2)=> {
+ val f1 = translate2QFPAfromFormulaIn(f)
+ val t1n = translate2QFPATermfromTermIn(t1)
+ val t2n = translate2QFPATermfromTermIn(t2)
+ TIte(f1,t1n, t2n)
+ }
+ }
+
+ def translate2QFPAAtomfromAtomIn(a:AtomIn):AtomQFPA = a match {
+ case AILeq(t1,t2) => {
+ val t1n = translate2QFPATermfromTermIn(t1)
+ val t2n = translate2QFPATermfromTermIn(t2)
+ ALeq(t1n, t2n)
+ }
+ case AIEq(t1,t2) => {
+ val t1n = translate2QFPATermfromTermIn(t1)
+ val t2n = translate2QFPATermfromTermIn(t2)
+ AEq(t1n, t2n)
+ }
+ }
+
+ def translate2QFPAfromFormulaIn(f:FormulaIn):QFPAFormula = f match {
+ case FIAnd(f1,f2) => {
+ val f1n = translate2QFPAfromFormulaIn(f1)
+ val f2n = translate2QFPAfromFormulaIn(f2)
+ QFPAAnd(f1n, f2n)
+ }
+ case FIOr(f1,f2) => {
+ val f1n = translate2QFPAfromFormulaIn(f1)
+ val f2n = translate2QFPAfromFormulaIn(f2)
+ QFPAOr(f1n, f2n)
+ }
+ case FINot(f1) => {
+ val f1n = translate2QFPAfromFormulaIn(f1)
+ QFPANot(f1n)
+ }
+ case FIAtom(a) => {
+ val a1 = translate2QFPAAtomfromAtomIn(a)
+ QFPAAtom(a1)
+ }
+ case FITrue => QFPATrue
+ case FIFalse => QFPAFalse
+ }
+
+ def translate2QFPAfromForAll(f:Formula):QFPAFormula = f match {
+ case FAtom(AForAllElem(f1)) => translate2QFPAfromFormulaIn(f1)
+ case FFalse => QFPAFalse
+ case FTrue => QFPATrue
+ case _ => error("Impossible case ")
+ }
+
+ def translateListofTermsOut(v1:List[TermOut]):List[TermQFPA] = {
+ var l1: List[TermQFPA] = Nil
+ v1.foreach(t => {
+ val tN = translate2QFPATermfromTermOut(t)
+ l1 = tN :: l1
+ })
+ l1.reverse
+ }
+
+ def translateListofTermsIn(v1:List[TermIn]):List[TermQFPA] = {
+ var l1: List[TermQFPA] = Nil
+ v1.foreach(t => {
+ val tN = translate2QFPATermfromTermIn(t)
+ l1 = tN :: l1
+ })
+ l1.reverse
+ }
+
+
+ def getVectorValuesFromSumFormula(f:Formula):(List[TermQFPA], List[TermQFPA]) = f match {
+ case FAtom(AAtomOut(AOSum(v1, FITrue, v2))) => {
+ val l1 = translateListofTermsOut(v1)
+ val l2 = translateListofTermsIn(v2)
+ (l1, l2)
+ }
+ case _ => error("Impossible case ")
+ }
+
+
+ def nnf(f:QFPAFormula): QFPAFormula = f match {
+ case QFPAAnd(f1, f2) => {
+ val f1N = nnf(f1)
+ val f2N = nnf(f2)
+ QFPAAnd(f1N, f2N)
+ }
+ case QFPAOr(f1, f2) => {
+ val f1N = nnf(f1)
+ val f2N = nnf(f2)
+ QFPAOr(f1N, f2N)
+ }
+ case QFPANot(QFPANot(f1)) => nnf(f1)
+ case QFPANot(QFPAAnd(f1, f2)) => QFPAOr(nnf(QFPANot(f1)), nnf(QFPANot(f2)))
+ case QFPANot(QFPAOr(f1, f2)) => QFPAAnd(nnf(QFPANot(f1)), nnf(QFPANot(f2)))
+ case QFPANot(QFPAFalse) => QFPATrue
+ case QFPANot(QFPATrue) => QFPAFalse
+ case _ => f
+ }
+
+
+
+ def removeTrueAndFalse(f:QFPAFormula): QFPAFormula = f match {
+ case QFPAAnd(QFPATrue, f2) => removeTrueAndFalse(f2)
+ case QFPAAnd(f1, QFPATrue) => removeTrueAndFalse(f1)
+ case QFPAAnd(QFPAFalse, f2) => QFPAFalse
+ case QFPAAnd(f1, QFPAFalse) => QFPAFalse
+ case QFPAAnd(f1, f2) => {
+ val f1N = removeTrueAndFalse(f1)
+ val f2N = removeTrueAndFalse(f2)
+ QFPAAnd(f1N, f2N)
+ }
+ case QFPAOr(QFPATrue, f2) => QFPATrue
+ case QFPAOr(f1, QFPATrue) => QFPATrue
+ case QFPAOr(QFPAFalse, f2) => removeTrueAndFalse(f2)
+ case QFPAOr(f1, QFPAFalse) => removeTrueAndFalse(f1)
+ case QFPAOr(f1, f2) => {
+ val f1N = removeTrueAndFalse(f1)
+ val f2N = removeTrueAndFalse(f2)
+ QFPAOr(f1N, f2N)
+ }
+ case QFPANot(f1) => {
+ val f1N = removeTrueAndFalse(f1)
+ val f1NN = if (f1N == QFPATrue) QFPAFalse else
+ if (f1N == QFPAFalse) QFPATrue else QFPANot(f1N)
+ f1NN
+ }
+ case _ => f
+ }
+
+
+// start: input fPA - presburger arithmetic formula, fForAll- for all formula, fSum-sumfourmula
+// output: $s1 AND $2 IN { $3 | $4} *
+
+
+ def main(fPA:Formula, fForAll: Formula, fSum:Formula):(QFPAFormula, List[TermQFPA], List[TermQFPA], QFPAFormula) = {
+ val f1 = removeTrueAndFalse(nnf(translate2QFPAfromFormula(fPA)))
+ val f2 = removeTrueAndFalse(nnf(translate2QFPAfromForAll(fForAll)))
+ val (l1, l2) = getVectorValuesFromSumFormula(fSum)
+ (f1, l1, l2, f2)
+ }
+
+}
+
diff --git a/src/multisets/MultisetFormulaPrinter.scala b/src/multisets/MultisetFormulaPrinter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..26e33f473f63205e8d67dd7bc913b66907f1bcf7
--- /dev/null
+++ b/src/multisets/MultisetFormulaPrinter.scala
@@ -0,0 +1,237 @@
+package multisets
+
+object MultisetFormulaPrinter {
+
+ def print_multiset(m:Multiset):Unit = m match {
+ case MVariable(v) => Console.print(v)
+ case MEmpty => Console.print("EMPTY")
+ case MUnion(m1, m2) => {
+ print_multiset(m1)
+ Console.print(" UNION ")
+ print_multiset(m2)
+ }
+ case MIntersection(m1, m2) => {
+ print_multiset(m1)
+ Console.print(" INTERSECT ")
+ print_multiset(m2)
+ }
+ case MPlus(m1, m2) => {
+ print_multiset(m1)
+ Console.print(" PLUS ")
+ print_multiset(m2)
+ }
+ case MMinus(m1, m2) => {
+ print_multiset(m1)
+ Console.print(" MINUS ")
+ print_multiset(m2)
+ }
+ case MSetMinus(m1, m2) => {
+ print_multiset(m1)
+ Console.print(" SetMINUS ")
+ print_multiset(m2)
+ }
+ case MSetOf(m1) => {
+ Console.print(" SetOf( ")
+ print_multiset(m1)
+ print(" )")
+ }
+ }
+
+ def print_termIn(t:TermIn):Unit = t match {
+ case TIMultiplicity(v) => Console.print(v + "(e)")
+ case TIConstant(c) => Console.print(c)
+ case TIPlus(t1, t2) => {
+ print_termIn(t1)
+ Console.print(" + ")
+ print_termIn(t2)
+ }
+ case TITimes(c, t1)=> {
+ Console.print(c + "*")
+ print_termIn(t1)
+ }
+ case TIIte(f, t1, t2)=> {
+ Console.print("ITE(")
+ print_formulaIn(f)
+ print("; ")
+ print_termIn(t1)
+ print(", ")
+ print_termIn(t2)
+ print(")")
+ }
+ }
+
+
+ def print_atomIn(a:AtomIn):Unit = a match {
+ case AILeq(t1,t2) => {
+ print_termIn(t1)
+ Console.print(" =< ")
+ print_termIn(t2)
+ }
+ case AIEq(t1,t2) => {
+ print_termIn(t1)
+ Console.print(" = ")
+ print_termIn(t2)
+ }
+ }
+
+ def print_formulaIn(f:FormulaIn):Unit = f match {
+ case FIAnd(f1,f2) => {
+ Console.print(" ( ")
+ print_formulaIn(f1)
+ print(" ) AND ( ")
+ print_formulaIn(f2)
+ print(" ) ")
+ }
+ case FIOr(f1,f2) => {
+ Console.print(" ( ")
+ print_formulaIn(f1)
+ print(" ) OR ( ")
+ print_formulaIn(f2)
+ print(" ) ")
+ }
+ case FINot(f1) => {
+ Console.print(" NOT ( ")
+ print_formulaIn(f1)
+ print(" ) ")
+ }
+ case FIAtom(a) => print_atomIn(a)
+ case FITrue => Console.print(" TRUE ")
+ case FIFalse => Console.print(" FALSE ")
+ }
+
+
+
+ def print_termOut(t:TermOut):Unit = t match {
+ case TOConstant(c) => Console.print(c)
+ case TOVariable(v) => Console.print(v)
+ case TOCard(m) => {
+ Console.print("| ")
+ print_multiset(m)
+ Console.print("| ")
+ }
+ case TOPlus(t1, t2) => {
+ print_termOut(t1)
+ Console.print(" + ")
+ print_termOut(t2)
+ }
+ case TOTimes(c, t1)=> {
+ Console.print(c + "*")
+ print_termOut(t1)
+ }
+ case TOIte(f, t1, t2)=> {
+ Console.print("ITE(")
+ print_formulaOut(f)
+ print("; ")
+ print_termOut(t1)
+ print(", ")
+ print_termOut(t2)
+ print(")")
+ }
+ }
+
+ def print_atomOut(a:AtomOut):Unit = a match {
+ case AOLeq(t1,t2) => {
+ print_termOut(t1)
+ Console.print(" =< ")
+ print_termOut(t2)
+ }
+ case AOEq(t1,t2) => {
+ print_termOut(t1)
+ Console.print(" = ")
+ print_termOut(t2)
+ }
+ case AOSum(l1, f, l2) => {
+ Console.print(" ( ")
+ l1.foreach(x => {
+ print_termOut(x)
+ print(", ")
+ })
+ print(") = SUM {e in E, ")
+ print_formulaIn(f)
+ print("} (")
+ l2.foreach(x => {
+ print_termIn(x)
+ print(", ")
+ })
+ print(")")
+ }
+ }
+
+
+ def print_formulaOut(f:FormulaOut):Unit = f match {
+ case FOAnd(f1,f2) => {
+ Console.print(" ( ")
+ print_formulaOut(f1)
+ print(" ) AND ( ")
+ print_formulaOut(f2)
+ print(" ) ")
+ }
+ case FOOr(f1,f2) => {
+ Console.print(" ( ")
+ print_formulaOut(f1)
+ print(" ) OR ( ")
+ print_formulaOut(f2)
+ print(" ) ")
+ }
+ case FONot(f1) => {
+ Console.print(" NOT ( ")
+ print_formulaOut(f1)
+ print(" ) ")
+ }
+ case FOAtom(a) => print_atomOut(a)
+ case FOTrue => Console.print(" TRUE ")
+ case FOFalse => Console.print(" FALSE ")
+ }
+
+ def print_atom(a:Atom):Unit = a match {
+ case AEqual(m1,m2) => {
+ print_multiset(m1)
+ Console.print(" = ")
+ print_multiset(m2)
+ }
+ case ASubset(m1,m2) => {
+ print_multiset(m1)
+ Console.print(" SUBSET ")
+ print_multiset(m2)
+ }
+ case AForAllElem(f) => {
+ Console.print(" FOR ALL e IN E. ( ")
+ print_formulaIn(f)
+ print(" ) ")
+ }
+ case AAtomOut(a1) => print_atomOut(a1)
+ }
+
+ def print_multisetFormula(f:Formula):Unit = f match {
+ case FAnd(f1,f2) => {
+ Console.print(" ( ")
+ print_multisetFormula(f1)
+ print(" ) AND ( ")
+ print_multisetFormula(f2)
+ print(" ) ")
+ }
+ case FOr(f1,f2) => {
+ Console.print(" ( ")
+ print_multisetFormula(f1)
+ print(" ) OR ( ")
+ print_multisetFormula(f2)
+ print(" ) ")
+ }
+ case FNot(FAnd(FNot(f1),FNot(f2))) => {
+ Console.print(" ( ")
+ print_multisetFormula(f1)
+ print(" ) OR ( ")
+ print_multisetFormula(f2)
+ print(" ) ")
+ }
+ case FNot(f1) => {
+ Console.print(" NOT ( ")
+ print_multisetFormula(f1)
+ print(" ) ")
+ }
+ case FAtom(a) => print_atom(a)
+ case FTrue => Console.print(" TRUE ")
+ case FFalse => Console.print(" FALSE ")
+ }
+
+}
\ No newline at end of file
diff --git a/src/multisets/NormalFormTranslator.scala b/src/multisets/NormalFormTranslator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cdc0f30fc6a0c23a99f13a685dbea823ef01917f
--- /dev/null
+++ b/src/multisets/NormalFormTranslator.scala
@@ -0,0 +1,924 @@
+package multisets
+
+
+import multisets.MultisetFormulaPrinter._
+
+
+object NormalFormTranslator {
+
+
+
+// start: this part extraxts all complex (diff. than a variable) expressions
+//input: f - Formula, mc - counter for fresh, mm - list containing (var, Multiset)
+//output : Formula - containing only variables as multisets, Int-counter List - variable, multiset
+ def extractMsetsExpr_termOut(t:TermOut, mc:Int, mm:List[(String,Multiset)]):(TermOut,Int,List[(String,Multiset)]) = t match {
+ case TOConstant(c) => (TOConstant(c), mc, mm)
+ case TOVariable(v) => (TOVariable(v), mc, mm)
+ case TOCard(MVariable(m)) => (TOCard(MVariable(m)), mc, mm)
+ case TOCard(m) => {
+ val newMulVar = "FRESHm" + mc
+ var mm1 = (newMulVar, m) :: mm
+ (TOCard(MVariable(newMulVar)), mc + 1, mm1)
+ }
+ case TOPlus(t1, t2) => {
+ val (t1n, mc1, mm1) = extractMsetsExpr_termOut(t1, mc, mm)
+ val (t2n, mc2, mm2) = extractMsetsExpr_termOut(t2, mc1, mm1)
+ (TOPlus(t1n, t2n), mc2, mm2)
+ }
+ case TOTimes(c, t1)=> {
+ val (t1n, mc1, mm1) = extractMsetsExpr_termOut(t1, mc, mm)
+ (TOTimes(c, t1n), mc1, mm1)
+ }
+ case TOIte(f, t1, t2)=> {
+ val (f1, mc1, mm1) = extractMsetsExpr_formulaOut(f, mc, mm)
+ val (t1n, mc2, mm2) = extractMsetsExpr_termOut(t1, mc1, mm1)
+ val (t2n, mc3, mm3) = extractMsetsExpr_termOut(t2, mc2, mm2)
+ (TOIte(f1,t1n, t2n), mc3, mm3)
+ }
+ }
+
+ def extractMsetsExpr_atomOut(a:AtomOut, mc:Int, mm:List[(String,Multiset)]):(AtomOut,Int,List[(String,Multiset)]) = a match {
+ case AOLeq(t1,t2) => {
+ val (t1n, mc1, mm1) = extractMsetsExpr_termOut(t1, mc, mm)
+ val (t2n, mc2, mm2) = extractMsetsExpr_termOut(t2, mc1, mm1)
+ (AOLeq(t1n, t2n), mc2, mm2)
+ }
+ case AOEq(t1,t2) => {
+ val (t1n, mc1, mm1) = extractMsetsExpr_termOut(t1, mc, mm)
+ val (t2n, mc2, mm2) = extractMsetsExpr_termOut(t2, mc1, mm1)
+ (AOEq(t1n, t2n), mc2, mm2)
+ }
+ case AOSum(l1, f, l2) => {
+ var l3: List[TermOut] = Nil
+ var mcN = mc
+ var mmN = mm
+ l1.foreach(t => {
+ val (t1, mc1, mm1) = extractMsetsExpr_termOut(t, mcN, mmN)
+ l3 = t1 :: l3
+ mcN = mc1
+ mmN = mm1
+ })
+ (AOSum(l3.reverse, f, l2), mcN, mmN)
+ }
+ }
+
+ def extractMsetsExpr_formulaOut(f:FormulaOut, mc:Int, mm:List[(String,Multiset)]):(FormulaOut,Int,List[(String,Multiset)]) = f match {
+ case FOAnd(f1,f2) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formulaOut(f1, mc, mm)
+ val (f2n, mc2, mm2) = extractMsetsExpr_formulaOut(f2, mc1, mm1)
+ (FOAnd(f1n, f2n), mc2, mm2)
+ }
+ case FOOr(f1,f2) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formulaOut(f1, mc, mm)
+ val (f2n, mc2, mm2) = extractMsetsExpr_formulaOut(f2, mc1, mm1)
+ (FOOr(f1n, f2n), mc2, mm2)
+ }
+ case FONot(f1) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formulaOut(f1, mc, mm)
+ (FONot(f1n), mc1, mm1)
+ }
+ case FOAtom(a) => {
+ val (a1, mc1, mm1) = extractMsetsExpr_atomOut(a, mc, mm)
+ (FOAtom(a1), mc1, mm1)
+ }
+ case FOTrue => (f, mc, mm)
+ case FOFalse => (f, mc, mm)
+ }
+
+ def extractMsetsExpr_atom(a:Atom, mc:Int, mm:List[(String,Multiset)]):(Atom,Int,List[(String,Multiset)]) = a match {
+ case AEqual(MVariable(v1),MVariable(v2)) => (AEqual(MVariable(v1),MVariable(v2)), mc, mm)
+ case AEqual(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc
+ var mm1 = (newMulVar, m2) :: mm
+ (AEqual(MVariable(v1),MVariable(newMulVar)), mc + 1, mm1)
+ }
+ case AEqual(m1, MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc
+ var mm1 = (newMulVar, m1) :: mm
+ (AEqual(MVariable(newMulVar),MVariable(v2)), mc + 1, mm1)
+ }
+ case AEqual(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc
+ var mm1 = (newMulVar1, m1) :: mm
+ val mcN = mc + 1
+ val newMulVar2 = "FRESHm" + mcN
+ var mm2 = (newMulVar2, m2) :: mm1
+ (AEqual(MVariable(newMulVar1),MVariable(newMulVar2)), mcN + 1, mm2)
+ }
+ case ASubset(MVariable(v1),MVariable(v2)) => (ASubset(MVariable(v1),MVariable(v2)), mc, mm)
+ case ASubset(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc
+ var mm1 = (newMulVar, m2) :: mm
+ (ASubset(MVariable(v1),MVariable(newMulVar)), mc + 1, mm1)
+ }
+ case ASubset(m1, MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc
+ var mm1 = (newMulVar, m1) :: mm
+ (ASubset(MVariable(newMulVar),MVariable(v2)), mc + 1, mm1)
+ }
+ case ASubset(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc
+ var mm1 = (newMulVar1, m1) :: mm
+ val mcN = mc + 1
+ val newMulVar2 = "FRESHm" + mcN
+ var mm2 = (newMulVar2, m2) :: mm1
+ (ASubset(MVariable(newMulVar1),MVariable(newMulVar2)), mcN + 1, mm2)
+ }
+ case AForAllElem(f) => (AForAllElem(f), mc, mm)
+ case AAtomOut(a1) => {
+ val (a2, mc1, mm1) = extractMsetsExpr_atomOut(a1, mc, mm)
+ (AAtomOut(a2), mc1, mm1)
+ }
+ }
+
+ def extractMsetsExpr_formula(f:Formula, mc:Int, mm:List[(String,Multiset)]):(Formula,Int,List[(String,Multiset)]) = f match {
+ case FAnd(f1,f2) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formula(f1, mc, mm)
+ val (f2n, mc2, mm2) = extractMsetsExpr_formula(f2, mc1, mm1)
+ (FAnd(f1n, f2n), mc2, mm2)
+ }
+ case FOr(f1,f2) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formula(f1, mc, mm)
+ val (f2n, mc2, mm2) = extractMsetsExpr_formula(f2, mc1, mm1)
+ (FOr(f1n, f2n), mc2, mm2)
+ }
+ case FNot(f1) => {
+ val (f1n, mc1, mm1) = extractMsetsExpr_formula(f1, mc, mm)
+ (FNot(f1n), mc1, mm1)
+ }
+ case FAtom(a) => {
+ val (a1, mc1, mm1) = extractMsetsExpr_atom(a, mc, mm)
+ (FAtom(a1), mc1, mm1)
+ }
+ case FTrue => (f, mc, mm)
+ case FFalse => (f, mc, mm)
+ }
+// end
+
+
+// start: list(var, multiset), can contain complex multiset expressions
+// output: list(var, multiset), simple multiset expressions
+ def flatten_multisetList(mc:Int, mm:List[(String,Multiset)], toBeChecked: Boolean):List[(String,Multiset)] = {
+ var addedFreshMultisets = false
+ var ml: List[(String,Multiset)] = Nil
+ var mc1 = mc
+ if (toBeChecked) {
+ mm.foreach(p => p._2 match {
+ case MVariable(v) => ml = p :: ml
+ case MEmpty => ml = p :: ml
+ case MUnion(MVariable(v1),MVariable(v2)) => ml = p :: ml
+ case MUnion(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MUnion(MVariable(v1),MVariable(newMulVar))) :: ((newMulVar, m2) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MUnion(m1,MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MUnion(MVariable(newMulVar),MVariable(v2))) :: ((newMulVar, m1) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MUnion(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc1
+ ml = (newMulVar1, m1) :: ml
+ mc1 = mc1 + 1
+ val newMulVar2 = "FRESHm" + mc1
+ ml = (newMulVar2, m2) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MUnion(MVariable(newMulVar1),MVariable(newMulVar2))) :: ml
+ addedFreshMultisets = true
+ }
+ case MIntersection(MVariable(v1),MVariable(v2)) => ml = p :: ml
+ case MIntersection(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MIntersection(MVariable(v1),MVariable(newMulVar))) :: ((newMulVar, m2) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MIntersection(m1,MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MIntersection(MVariable(newMulVar),MVariable(v2))) :: ((newMulVar, m1) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MIntersection(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc1
+ ml = (newMulVar1, m1) :: ml
+ mc1 = mc1 + 1
+ val newMulVar2 = "FRESHm" + mc1
+ ml = (newMulVar2, m2) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MIntersection(MVariable(newMulVar1),MVariable(newMulVar2))) :: ml
+ addedFreshMultisets = true
+ }
+ case MPlus(MVariable(v1),MVariable(v2)) => ml = p :: ml
+ case MPlus(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MPlus(MVariable(v1),MVariable(newMulVar))) :: ((newMulVar, m2) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MPlus(m1,MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MPlus(MVariable(newMulVar),MVariable(v2))) :: ((newMulVar, m1) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MPlus(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc1
+ ml = (newMulVar1, m1) :: ml
+ mc1 = mc1 + 1
+ val newMulVar2 = "FRESHm" + mc1
+ ml = (newMulVar2, m2) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MPlus(MVariable(newMulVar1),MVariable(newMulVar2))) :: ml
+ addedFreshMultisets = true
+ }
+ case MMinus(MVariable(v1),MVariable(v2)) => ml = p :: ml
+ case MMinus(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MMinus(MVariable(v1),MVariable(newMulVar))) :: ((newMulVar, m2) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MMinus(m1,MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MMinus(MVariable(newMulVar),MVariable(v2))) :: ((newMulVar, m1) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MMinus(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc1
+ ml = (newMulVar1, m1) :: ml
+ mc1 = mc1 + 1
+ val newMulVar2 = "FRESHm" + mc1
+ ml = (newMulVar2, m2) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MMinus(MVariable(newMulVar1),MVariable(newMulVar2))) :: ml
+ addedFreshMultisets = true
+ }
+ case MSetMinus(MVariable(v1),MVariable(v2)) => ml = p :: ml
+ case MSetMinus(MVariable(v1),m2) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MSetMinus(MVariable(v1),MVariable(newMulVar))) :: ((newMulVar, m2) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MSetMinus(m1,MVariable(v2)) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (p._1, MSetMinus(MVariable(newMulVar),MVariable(v2))) :: ((newMulVar, m1) :: ml)
+ mc1 = mc1 + 1
+ addedFreshMultisets = true
+ }
+ case MSetMinus(m1,m2) => {
+ val newMulVar1 = "FRESHm" + mc1
+ ml = (newMulVar1, m1) :: ml
+ mc1 = mc1 + 1
+ val newMulVar2 = "FRESHm" + mc1
+ ml = (newMulVar2, m2) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MSetMinus(MVariable(newMulVar1),MVariable(newMulVar2))) :: ml
+ addedFreshMultisets = true
+ }
+ case MSetOf(MVariable(v)) => ml = p :: ml
+ case MSetOf(m) => {
+ val newMulVar = "FRESHm" + mc1
+ ml = (newMulVar, m) :: ml
+ mc1 = mc1 + 1
+ ml = (p._1, MSetOf(MVariable(newMulVar))) :: ml
+ addedFreshMultisets = true
+ }
+ })
+ flatten_multisetList(mc1, ml, addedFreshMultisets)
+ }
+ else mm
+ }
+// end
+
+
+
+// start: input list(string, multiset) (m1, m2 un m3),...
+// output: formula: Forall e.(m1 (e) = ... AND ..)
+ def createFormulafromPair(p:(String,Multiset)):FormulaIn = p._2 match {
+ case MEmpty =>
+ FIAtom(AIEq(TIMultiplicity(p._1),TIConstant(0)))
+ case MUnion(MVariable(v1),MVariable(v2)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIIte(FIAtom(AILeq(TIMultiplicity(v1),TIMultiplicity(v2))), TIMultiplicity(v2), TIMultiplicity(v1))))
+ case MIntersection(MVariable(v1),MVariable(v2)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIIte(FIAtom(AILeq(TIMultiplicity(v1),TIMultiplicity(v2))), TIMultiplicity(v1), TIMultiplicity(v2))))
+ case MPlus(MVariable(v1),MVariable(v2)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIPlus(TIMultiplicity(v1), TIMultiplicity(v2))))
+ case MMinus(MVariable(v1),MVariable(v2)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIIte(FIAtom(AILeq(TIMultiplicity(v1),TIMultiplicity(v2))), TIConstant(0),
+ TIPlus(TIMultiplicity(v1), TITimes(-1, TIMultiplicity(v2))))))
+ case MSetMinus(MVariable(v1),MVariable(v2)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIIte(FIAtom(AIEq(TIMultiplicity(v2),TIConstant(0))), TIMultiplicity(v1), TIConstant(0))))
+ case MSetOf(MVariable(v)) =>
+ FIAtom(AIEq(TIMultiplicity(p._1),
+ TIIte(FIAtom(AILeq(TIConstant(1),TIMultiplicity(v))), TIConstant(1), TIConstant(0))))
+ case _ => error("Impossible case, canot get this here, but got " + p)
+ }
+
+ def createFormulafromMultisetList(mlist:List[(String,Multiset)]):Formula = {
+ if (mlist.isEmpty) FAtom(AForAllElem(FITrue)) else {
+ val firstPair = mlist.head
+ val theRest = mlist.tail
+ var fN = createFormulafromPair(firstPair)
+ theRest.foreach(p => {
+ val f = createFormulafromPair(p)
+ fN = FIAnd(fN, f)
+ })
+ FAtom(AForAllElem(fN))
+ }
+ }
+// end
+
+
+// start: formula with m1 SUB m2 and m1 = m2
+// output formula with forall e. m1(e) <= m2(e) and m1(e) = m2(e)
+ def redefineMultisetAtom(a:Atom):Formula = a match {
+ case AEqual(MVariable(v1),MVariable(v2)) =>
+ FAtom(AForAllElem(FIAtom(AIEq(TIMultiplicity(v1), TIMultiplicity(v2)))))
+ case ASubset(MVariable(v1),MVariable(v2)) =>
+ FAtom(AForAllElem(FIAtom(AILeq(TIMultiplicity(v1), TIMultiplicity(v2)))))
+ case AForAllElem(f) => FAtom(AForAllElem(f))
+ case AAtomOut(a1) => FAtom(AAtomOut(a1))
+ case _ => error("Impossible case ")
+ }
+
+ def redefineMultisetAtoms(f:Formula):Formula = f match {
+ case FAnd(f1,f2) => {
+ val f1n = redefineMultisetAtoms(f1)
+ val f2n = redefineMultisetAtoms(f2)
+ FAnd(f1n, f2n)
+ }
+ case FOr(f1,f2) => {
+ val f1n = redefineMultisetAtoms(f1)
+ val f2n = redefineMultisetAtoms(f2)
+ FOr(f1n, f2n)
+ }
+ case FNot(f1) => {
+ val f1n = redefineMultisetAtoms(f1)
+ FNot(f1n)
+ }
+ case FAtom(a) => {
+ val a1 = redefineMultisetAtom(a)
+ a1
+ }
+ case FTrue => f
+ case FFalse => f
+ }
+// end
+
+
+// start: input formula with cardinalities
+// output: new formula where each cardinality is replaced with a fresh int var + List(intVar, msetVar) <-both strings
+
+ def extractCardExpr_termOut(t:TermOut, ic:Int, cl:List[(String,String)]):(TermOut,Int,List[(String,String)]) = t match {
+ case TOConstant(c) => (TOConstant(c), ic, cl)
+ case TOVariable(v) => (TOVariable(v), ic, cl)
+ case TOCard(MVariable(m)) => {
+ val newIntVar = "FRESHk" + ic
+ var cl1 = (newIntVar, m) :: cl
+ (TOVariable(newIntVar), ic + 1, cl1)
+ }
+ case TOPlus(t1, t2) => {
+ val (t1n, ic1, cl1) = extractCardExpr_termOut(t1, ic, cl)
+ val (t2n, ic2, cl2) = extractCardExpr_termOut(t2, ic1, cl1)
+ (TOPlus(t1n, t2n), ic2, cl2)
+ }
+ case TOTimes(c, t1)=> {
+ val (t1n, ic1, cl1) = extractCardExpr_termOut(t1, ic, cl)
+ (TOTimes(c, t1n), ic1, cl1)
+ }
+ case TOIte(f, t1, t2)=> {
+ val (f1, ic1, cl1) = extractCardExpr_formulaOut(f, ic, cl)
+ val (t1n, ic2, cl2) = extractCardExpr_termOut(t1, ic1, cl1)
+ val (t2n, ic3, cl3) = extractCardExpr_termOut(t2, ic2, cl2)
+ (TOIte(f1,t1n, t2n), ic3, cl3)
+ }
+ case _ => error("Impossible case ")
+ }
+
+ def extractCardExpr_atomOut(a:AtomOut, ic:Int, cl:List[(String,String)]):(AtomOut,Int,List[(String,String)]) = a match {
+ case AOLeq(t1,t2) => {
+ val (t1n, ic1, cl1) = extractCardExpr_termOut(t1, ic, cl)
+ val (t2n, ic2, cl2) = extractCardExpr_termOut(t2, ic1, cl1)
+ (AOLeq(t1n, t2n), ic2, cl2)
+ }
+ case AOEq(t1,t2) => {
+ val (t1n, ic1, cl1) = extractCardExpr_termOut(t1, ic, cl)
+ val (t2n, ic2, cl2) = extractCardExpr_termOut(t2, ic1, cl1)
+ (AOEq(t1n, t2n), ic2, cl2)
+ }
+ case AOSum(l1, f, l2) => {
+ var l3: List[TermOut] = Nil
+ var icN = ic
+ var clN = cl
+ l1.foreach(t => {
+ val (t1, ic1, cl1) = extractCardExpr_termOut(t, icN, clN)
+ l3 = t1 :: l3
+ icN = ic1
+ clN = cl1
+ })
+ (AOSum(l3.reverse, f, l2), icN, clN)
+ }
+ }
+
+ def extractCardExpr_formulaOut(f:FormulaOut, ic:Int, cl:List[(String,String)]):(FormulaOut,Int,List[(String,String)]) = f match {
+ case FOAnd(f1,f2) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formulaOut(f1, ic, cl)
+ val (f2n, ic2, cl2) = extractCardExpr_formulaOut(f2, ic1, cl1)
+ (FOAnd(f1n, f2n), ic2, cl2)
+ }
+ case FOOr(f1,f2) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formulaOut(f1, ic, cl)
+ val (f2n, ic2, cl2) = extractCardExpr_formulaOut(f2, ic1, cl1)
+ (FOOr(f1n, f2n), ic2, cl2)
+ }
+ case FONot(f1) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formulaOut(f1, ic, cl)
+ (FONot(f1n), ic1, cl1)
+ }
+ case FOAtom(a) => {
+ val (a1, ic1, cl1) = extractCardExpr_atomOut(a, ic, cl)
+ (FOAtom(a1), ic1, cl1)
+ }
+ case FOTrue => (f, ic, cl)
+ case FOFalse => (f, ic, cl)
+ }
+
+
+ def extractCardExpr_atom(a:Atom, ic:Int, cl:List[(String,String)]):(Atom,Int,List[(String,String)]) = a match {
+ case AEqual(m1,m2) => (AEqual(m1,m2), ic, cl)
+ case ASubset(m1,m2) => (ASubset(m1,m2), ic, cl)
+ case AForAllElem(f) => (AForAllElem(f), ic, cl)
+ case AAtomOut(a1) => {
+ val (a2, ic1, cl1) = extractCardExpr_atomOut(a1, ic, cl)
+ (AAtomOut(a2), ic1, cl1)
+ }
+ }
+
+ def extractCardExpr_formula(f:Formula, ic:Int, cl:List[(String,String)]):(Formula,Int,List[(String,String)]) = f match {
+ case FAnd(f1,f2) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formula(f1, ic, cl)
+ val (f2n, ic2, cl2) = extractCardExpr_formula(f2, ic1, cl1)
+ (FAnd(f1n, f2n), ic2, cl2)
+ }
+ case FOr(f1,f2) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formula(f1, ic, cl)
+ val (f2n, ic2, cl2) = extractCardExpr_formula(f2, ic1, cl1)
+ (FOr(f1n, f2n), ic2, cl2)
+ }
+ case FNot(f1) => {
+ val (f1n, ic1, cl1) = extractCardExpr_formula(f1, ic, cl)
+ (FNot(f1n), ic1, cl1)
+ }
+ case FAtom(a) => {
+ val (a1, ic1, cl1) = extractCardExpr_atom(a, ic, cl)
+ (FAtom(a1), ic1, cl1)
+ }
+ case FTrue => (f, ic, cl)
+ case FFalse => (f, ic, cl)
+ }
+// end
+
+// start: input list(var, mset), output: (var) = SUM_{} mset
+ def createFormulafromCardinalityList(cl:List[(String,String)]):Formula = {
+ var l1: List[TermOut] = Nil
+ var l2: List[TermIn] = Nil
+ if (cl.isEmpty) FAtom(AAtomOut(AOSum(List(TOConstant(0)), FITrue, List(TIConstant(0))))) else {
+ cl.foreach(p => {
+ l1 = TOVariable(p._1) :: l1
+ l2 = TIMultiplicity(p._2) :: l2
+ })
+ FAtom(AAtomOut((AOSum(l1, FITrue, l2))))
+ }
+ }
+
+// end
+
+
+// start
+// input: f- formula, fFA - allready existing formula of the form forall e.f(e)
+//output: $1 - formula without top-level forall, $2-forall e. f(e)
+ def uniteForAll(fI:FormulaIn,f:Formula):Formula = f match {
+ case FAtom(AForAllElem(f1)) => {
+ val fn = if (f1 == FITrue) fI else FIAnd(fI, f1)
+ FAtom(AForAllElem(fn))
+ }
+ case _ => error("Impossible case ")
+ }
+
+
+ def topLevelForAll(f:Formula,fFA:Formula):(Formula,Formula) = f match {
+ case FAnd(FAtom(AForAllElem(fI)),f2) => {
+ val (f2N, fFAN) = topLevelForAll(f2, fFA)
+ (f2N, uniteForAll(fI, fFAN))
+ }
+ case FAnd(f1, FAtom(AForAllElem(fI))) => {
+ val (f1N, fFAN) = topLevelForAll(f1, fFA)
+ (f1N, uniteForAll(fI, fFAN))
+ }
+ case FAnd(f1,f2) => {
+ val (f1n, fFA1) = topLevelForAll(f1, fFA)
+ val (f2n, fFA2) = topLevelForAll(f2, fFA1)
+ val f3n = if (f1n == FTrue) f2n else
+ if (f2n == FTrue) f1n else FAnd(f1n, f2n)
+ (f3n, fFA2)
+ }
+ case FOr(f1,f2) => (f, fFA)
+ case FNot(f1) => (f, fFA)
+ case FAtom(AForAllElem(fI)) => (FTrue, uniteForAll(fI, fFA))
+ case FAtom(a) => (f, fFA)
+ case FTrue => (f, fFA)
+ case FFalse => (f, fFA)
+ }
+// end
+
+
+// start
+// input formula f - output f1 where every forall e. f is replaced with a sum:
+// forall e. f(e) <=> 0 = sum_{true} ite(f(e); 0, 1)
+ def replaceForAllWithSums(f:Formula):Formula = f match {
+ case FAnd(f1,f2) => {
+ val f1n = replaceForAllWithSums(f1)
+ val f2n = replaceForAllWithSums(f2)
+ FAnd(f1n, f2n)
+ }
+ case FOr(f1,f2) => {
+ val f1n = replaceForAllWithSums(f1)
+ val f2n = replaceForAllWithSums(f2)
+ FOr(f1n, f2n)
+ }
+ case FNot(f1) => {
+ val f1n = replaceForAllWithSums(f1)
+ FNot(f1n)
+ }
+ case FAtom(AForAllElem(f1)) =>
+ FAtom(AAtomOut(AOSum(List(TOConstant(0)), FITrue, List(TIIte(f1,TIConstant(0),TIConstant(1))))))
+ case FAtom(a) => f
+ case FTrue => f
+ case FFalse => f
+ }
+
+ def notTopLevelForAll(f:Formula):Formula = f match {
+ case FAnd(f1,f2) => {
+ val f1n = notTopLevelForAll(f1)
+ val f2n = notTopLevelForAll(f2)
+ FAnd(f1n, f2n)
+ }
+ case FOr(f1,f2) => {
+ val f1n = replaceForAllWithSums(f1)
+ val f2n = replaceForAllWithSums(f2)
+ FOr(f1n, f2n)
+ }
+ case FNot(f1) => FNot(replaceForAllWithSums(f1))
+ case FAtom(a) => f
+ case FTrue => f
+ case FFalse => f
+ }
+// end
+
+
+
+// start: input formula f and fS which is already a sum atom
+// output: $1 without top level sums, $2 is a sum atom
+ def eliminateConditions(f:FormulaIn, lIn: List[TermIn]):List[TermIn] = {
+ var ltemp: List[TermIn] = Nil
+ lIn.foreach(t => {
+ val t1 = TIIte(f, t, TIConstant(0))
+ ltemp = t1 :: ltemp
+ })
+ ltemp.reverse
+ }
+
+
+ def uniteSums(lTO:List[TermOut], lTI: List[TermIn], fD:FormulaIn,f:Formula):Formula = f match {
+ case FAtom(AAtomOut(AOSum(lT0o, FITrue, lTIo))) => fD match {
+ case FITrue => FAtom(AAtomOut(AOSum(lTO ::: lT0o, FITrue, lTI ::: lTIo)))
+ case _ => {
+ val ltN = eliminateConditions(fD, lTI)
+ FAtom(AAtomOut(AOSum(lTO ::: lT0o, FITrue, ltN ::: lTIo)))
+ }
+ }
+ case _ => error("Impossible case ")
+ }
+
+ def topLevelSums(f:Formula,fS:Formula):(Formula,Formula) = f match {
+ case FAnd(FAtom(AAtomOut(AOSum(lTO, ff, lTI))), f2) => {
+ val (f2N, fSN) = topLevelSums(f2, fS)
+ (f2N, uniteSums(lTO, lTI, ff, fSN))
+ }
+ case FAnd(f1, FAtom(AAtomOut(AOSum(lTO, ff, lTI)))) => {
+ val (f1N, fSN) = topLevelSums(f1, fS)
+ (f1N, uniteSums(lTO, lTI, ff, fSN))
+ }
+ case FAnd(f1,f2) => {
+ val (f1n, fS1) = topLevelForAll(f1, fS)
+ val (f2n, fS2) = topLevelForAll(f2, fS1)
+ val f3n = if (f1n == FTrue) f2n else
+ if (f2n == FTrue) f1n else FAnd(f1n, f2n)
+ (f3n, fS2)
+ }
+ case FOr(f1,f2) => (f, fS)
+ case FNot(f1) => (f, fS)
+ case FAtom(AAtomOut(AOSum(lTO, ff, lTI))) => (FTrue, uniteSums(lTO, lTI, ff, fS))
+ case FAtom(a) => (f, fS)
+ case FTrue => (f, fS)
+ case FFalse => (f, fS)
+ }
+// end
+
+
+// start: input f - formula fs- sum atom, sc -counter
+// outputs: $1 - formula without sums, $s2 - sum atom $3 -counter
+ def createEqualityAtom(to:TermOut, sc:Int):(Atom,TermOut,Int) = {
+ val newVar = "FRESHs" + sc
+ val scN = sc + 1
+ val a = AAtomOut(AOEq(to, TOVariable(newVar)))
+ (a, TOVariable(newVar), scN)
+ }
+
+ def createEqualityFormula(lTO:List[TermOut], sc:Int):(Formula,List[TermOut],Int) = {
+ var tList: List[TermOut] = Nil
+ val t1 = lTO.head
+ val theRest = lTO.tail
+ var (aN, vN, scN) = createEqualityAtom(t1, sc)
+ var fN : Formula = FAtom(aN)
+ tList = vN :: tList
+ theRest.foreach(t => {
+ val (aN1, vN1, scN1) = createEqualityAtom(t, scN)
+ scN = scN1
+ fN = FAnd(fN, FAtom(aN1))
+ tList = vN1 :: tList
+ })
+ (fN, tList.reverse, scN)
+ }
+
+ def notTopLevelSums(f:Formula,fS:Formula,sc:Int):(Formula,Formula,Int) = f match {
+ case FAnd(f1,f2) => {
+ val (f1n, fS1, sc1) = notTopLevelSums(f1, fS, sc)
+ val (f2n, fS2, sc2) = notTopLevelSums(f2, fS1, sc1)
+ (FAnd(f1n, f2n), fS2, sc2)
+ }
+ case FOr(f1,f2) => {
+ val (f1n, fS1, sc1) = notTopLevelSums(f1, fS, sc)
+ val (f2n, fS2, sc2) = notTopLevelSums(f2, fS1, sc1)
+ (FOr(f1n, f2n), fS2, sc2)
+ }
+ case FNot(f1) => {
+ val (f1n, fS1, sc1) = notTopLevelSums(f1, fS, sc)
+ (FNot(f1n), fS1, sc1)
+ }
+ case FAtom(AAtomOut(AOSum(lTO, ff, lTI))) => {
+ val (f1, l1, scN) = createEqualityFormula(lTO, sc)
+ val fN = uniteSums(l1, lTI, ff, fS)
+ (f1, fN, scN)
+ }
+ case FAtom(a) => (f, fS, sc)
+ case FTrue => (f, fS, sc)
+ case FFalse => (f, fS, sc)
+ }
+// end
+
+
+// start: input formula F, output: formula F' which does not contain True and False
+// only can contain either pure TRUE or FALSE
+ def removeTrueandFalsefromTermIn(t: TermIn): TermIn = t match {
+ case TIPlus(t1, t2) => {
+ val t1n = removeTrueandFalsefromTermIn(t1)
+ val t2n = removeTrueandFalsefromTermIn(t2)
+ TIPlus(t1n, t2n)
+ }
+ case TITimes(c, t1)=> {
+ val t1n = removeTrueandFalsefromTermIn(t1)
+ TITimes(c, t1n)
+ }
+ case TIIte(f, t1, t2) => {
+ val t1n = removeTrueandFalsefromTermIn(t1)
+ val t2n = removeTrueandFalsefromTermIn(t2)
+ val f1 = removeTrueandFalsefromFormulaIn(f)
+ TIIte(f1, t1n, t2n)
+ }
+ case _ => t
+ }
+
+ def removeTrueandFalsefromAtomIn(a: AtomIn): AtomIn = a match {
+ case AILeq(t1, t2) => {
+ val t1n = removeTrueandFalsefromTermIn(t1)
+ val t2n = removeTrueandFalsefromTermIn(t2)
+ AILeq(t1n, t2n)
+ }
+ case AIEq(t1,t2) => {
+ val t1n = removeTrueandFalsefromTermIn(t1)
+ val t2n = removeTrueandFalsefromTermIn(t2)
+ AIEq(t1n, t2n)
+ }
+ }
+
+ def removeTrueandFalsefromFormulaIn(f: FormulaIn): FormulaIn = f match {
+ case FIAnd(FIFalse, f2) => FIFalse
+ case FIAnd(f1, FIFalse) => FIFalse
+ case FIAnd(FITrue, f2) => removeTrueandFalsefromFormulaIn(f2)
+ case FIAnd(f1, FITrue) => removeTrueandFalsefromFormulaIn(f1)
+ case FIAnd(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulaIn(f1)
+ val f2n = removeTrueandFalsefromFormulaIn(f2)
+ val f3 = if (f1n == FIFalse || f2n == FIFalse) FIFalse else
+ if (f1n == FITrue) f2n else
+ if (f2n == FITrue) f1n else FIAnd(f1n, f2n)
+ f3
+ }
+ case FIOr(FITrue, f2) => FITrue
+ case FIOr(f1, FITrue) => FITrue
+ case FIOr(FIFalse, f2) => removeTrueandFalsefromFormulaIn(f2)
+ case FIOr(f1, FIFalse) => removeTrueandFalsefromFormulaIn(f1)
+ case FIOr(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulaIn(f1)
+ val f2n = removeTrueandFalsefromFormulaIn(f2)
+ val f3 = if (f1n == FITrue || f2n == FITrue) FITrue else
+ if (f1n == FIFalse) f2n else
+ if (f2n == FIFalse) f1n else FIOr(f1n, f2n)
+ f3
+ }
+ case FINot(f1) => {
+ val f1n = removeTrueandFalsefromFormulaIn(f1)
+ val f3 = if (f1n == FITrue) FIFalse else
+ if (f1n == FIFalse) FITrue else FINot(f1n)
+ f3
+ }
+ case FIAtom(a) => {
+ val a1 = removeTrueandFalsefromAtomIn(a)
+ FIAtom(a1)
+ }
+ case _ => f
+ }
+
+ def removeTrueandFalsefromTermOut(t: TermOut): TermOut = t match {
+ case TOPlus(t1, t2) => {
+ val t1n = removeTrueandFalsefromTermOut(t1)
+ val t2n = removeTrueandFalsefromTermOut(t2)
+ TOPlus(t1n, t2n)
+ }
+ case TOTimes(c, t1)=> {
+ val t1n = removeTrueandFalsefromTermOut(t1)
+ TOTimes(c, t1n)
+ }
+ case TOIte(f, t1, t2) => {
+ val t1n = removeTrueandFalsefromTermOut(t1)
+ val t2n = removeTrueandFalsefromTermOut(t2)
+ val f1 = removeTrueandFalsefromFormulaOut(f)
+ TOIte(f1, t1n, t2n)
+ }
+ case _ => t
+ }
+
+ def removeTrueandFalsefromAtomOut(a: AtomOut): AtomOut = a match {
+ case AOLeq(t1, t2) => {
+ val t1n = removeTrueandFalsefromTermOut(t1)
+ val t2n = removeTrueandFalsefromTermOut(t2)
+ AOLeq(t1n, t2n)
+ }
+ case AOEq(t1,t2) => {
+ val t1n = removeTrueandFalsefromTermOut(t1)
+ val t2n = removeTrueandFalsefromTermOut(t2)
+ AOEq(t1n, t2n)
+ }
+ case AOSum(l1, f, l2) => {
+ val l1n = l1.map(v => removeTrueandFalsefromTermOut(v))
+ val l2n = l2.map(v => removeTrueandFalsefromTermIn(v))
+ val f1 = removeTrueandFalsefromFormulaIn(f)
+ AOSum(l1n, f1, l2n)
+ }
+ }
+
+ def removeTrueandFalsefromFormulaOut(f: FormulaOut): FormulaOut = f match {
+ case FOAnd(FOFalse, f2) => FOFalse
+ case FOAnd(f1, FOFalse) => FOFalse
+ case FOAnd(FOTrue, f2) => removeTrueandFalsefromFormulaOut(f2)
+ case FOAnd(f1, FOTrue) => removeTrueandFalsefromFormulaOut(f1)
+ case FOAnd(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulaOut(f1)
+ val f2n = removeTrueandFalsefromFormulaOut(f2)
+ val f3 = if (f1n == FOFalse || f2n == FOFalse) FOFalse else
+ if (f1n == FOTrue) f2n else
+ if (f2n == FOTrue) f1n else FOAnd(f1n, f2n)
+ f3
+ }
+ case FOOr(FOTrue, f2) => FOTrue
+ case FOOr(f1, FOTrue) => FOTrue
+ case FOOr(FOFalse, f2) => removeTrueandFalsefromFormulaOut(f2)
+ case FOOr(f1, FOFalse) => removeTrueandFalsefromFormulaOut(f1)
+ case FOOr(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulaOut(f1)
+ val f2n = removeTrueandFalsefromFormulaOut(f2)
+ val f3 = if (f1n == FOTrue || f2n == FOTrue) FOTrue else
+ if (f1n == FOFalse) f2n else
+ if (f2n == FOFalse) f1n else FOOr(f1n, f2n)
+ f3
+ }
+ case FONot(f1) => {
+ val f1n = removeTrueandFalsefromFormulaOut(f1)
+ val f3 = if (f1n == FOTrue) FOFalse else
+ if (f1n == FOFalse) FOTrue else FONot(f1n)
+ f3
+ }
+ case FOAtom(a) => {
+ val a1 = removeTrueandFalsefromAtomOut(a)
+ FOAtom(a1)
+ }
+ case _ => f
+ }
+
+ def removeTrueandFalsefromAtom(a: Atom): Atom = a match {
+ case AForAllElem(f1) => {
+ val f1n = removeTrueandFalsefromFormulaIn(f1)
+ AForAllElem(f1n)
+ }
+ case AAtomOut(a1) => {
+ val a1n = removeTrueandFalsefromAtomOut(a1)
+ AAtomOut(a1n)
+ }
+ case _ => a
+ }
+
+ def removeTrueandFalsefromFormulas(f:Formula): Formula = f match {
+ case FAnd(FFalse, f2) => FFalse
+ case FAnd(f1, FFalse) => FFalse
+ case FAnd(FTrue, f2) => removeTrueandFalsefromFormulas(f2)
+ case FAnd(f1, FTrue) => removeTrueandFalsefromFormulas(f1)
+ case FAnd(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulas(f1)
+ val f2n = removeTrueandFalsefromFormulas(f2)
+ val f3 = if (f1n == FFalse || f2n == FFalse) FFalse else
+ if (f1n == FTrue) f2n else
+ if (f2n == FTrue) f1n else FAnd(f1n, f2n)
+ f3
+ }
+ case FOr(FTrue, f2) => FTrue
+ case FOr(f1, FTrue) => FTrue
+ case FOr(FFalse, f2) => removeTrueandFalsefromFormulas(f2)
+ case FOr(f1, FFalse) => removeTrueandFalsefromFormulas(f1)
+ case FOr(f1, f2) => {
+ val f1n = removeTrueandFalsefromFormulas(f1)
+ val f2n = removeTrueandFalsefromFormulas(f2)
+ val f3 = if (f1n == FTrue || f2n == FTrue) FTrue else
+ if (f1n == FFalse) f2n else
+ if (f2n == FFalse) f1n else FOr(f1n, f2n)
+ f3
+ }
+ case FNot(f1) => {
+ val f1n = removeTrueandFalsefromFormulas(f1)
+ val f3 = if (f1n == FTrue) FFalse else
+ if (f1n == FFalse) FTrue else FNot(f1n)
+ f3
+ }
+ case FAtom(a) => {
+ val a1 = removeTrueandFalsefromAtom(a)
+ FAtom(a1)
+ }
+ case _ => f
+ }
+// end
+
+
+// ------------- MAIN -------------
+
+ def main(f:Formula): (Formula,Formula,Formula) = {
+ val f0 = removeTrueandFalsefromFormulas(f)
+ // formula f0 does not contain true or false but it could be only true or false
+ val msetCounter = 0
+ var msets: List[(String,Multiset)] = Nil
+ val (f1, mc, mcm) = extractMsetsExpr_formula(f0, msetCounter, msets)
+ // formula f1 does not contain complex multisets, they are all in mcm
+ val toBeChecked = true
+ val mlist = flatten_multisetList(mc, mcm, toBeChecked)
+ val fAll = createFormulafromMultisetList(mlist)
+ // fAll is a formula All e.m1(e) = ,.. AND ... <- all complex multiset experssions as a formula
+ val f2 = redefineMultisetAtoms(f1) //replace m1 = m2 and m1 SubSET m2 with for all e....
+ val intCounter = 0
+ var cards: List[(String,String)] = Nil
+ val (f3, ic, il) = extractCardExpr_formula(f2, intCounter, cards)
+ // f3 = new formula without cardinalities, il = list of the form (intVar, msetVar)
+ val fSum = createFormulafromCardinalityList(il)
+ // fSum <- atom about all cardinalities that were pulled out of the original formula
+ val (f4, fAll1) = topLevelForAll(f3, fAll)
+ // all top level forall are united in formula fAll1 and f4 does not contain top-level forall e...
+ val f5 = notTopLevelForAll(f4)
+ // f5 does not contain any forall e. f(e) expression - they are converted using sums
+ val (f6, fSum1) = topLevelSums(f5, fSum)
+ // all top level sums are united in formula fSum1 and f6 does not contain top-level sum
+ val sumCounter = 0
+ val (f7, fSum2, _) = notTopLevelSums(f6, fSum1, sumCounter)
+ (f7, fAll1, fSum2)
+ }
+
+
+}
diff --git a/src/multisets/RemoveDisjunctions.scala b/src/multisets/RemoveDisjunctions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ab33790314a4f6062733c0ff9f5bf87aaa697bc8
--- /dev/null
+++ b/src/multisets/RemoveDisjunctions.scala
@@ -0,0 +1,83 @@
+package multisets
+
+
+object RemoveDisjunctions {
+
+//
+
+ def createListofFreshVectors(n:Int, m:Int): List[List[TermQFPA]] = {
+ var i = 0
+ var lOut: List[List[TermQFPA]] = Nil
+ while (i < n) {
+ var j = 0
+ var lIn: List[TermQFPA] = Nil
+ while (j < m) {
+ var num = i * m + j
+ var newUVar = "FRESHu" + num
+ var tmpTermVar = TVariable(newUVar)
+ lIn = tmpTermVar :: lIn
+ j += 1
+ }
+ var lInN = lIn.reverse
+ lOut = lInN :: lOut
+ i += 1
+ }
+ lOut
+ }
+
+ def createSumOfAllUVecs(i:Int, u:List[List[TermQFPA]]):TermQFPA = {
+ val n = u.length
+ var j = 0
+ var tt = (u(j))(i)
+ j += 1
+ while (j < n) {
+ var tn = (u(j))(i)
+ tt = TPlus(tt, tn)
+ j += 1
+ }
+ tt
+ }
+
+
+
+ def createFormulaWithFreshUsVariables(u:List[TermQFPA], uVec:List[List[TermQFPA]]):QFPAFormula = {
+ val m = u.length
+ var j = 0
+ var tR = createSumOfAllUVecs(j, uVec)
+ var tL = u(j)
+ var eq = AEq(tL, tR)
+ var f:QFPAFormula = QFPAAtom(eq)
+ j += 1
+ while (j < m) {
+ tR = createSumOfAllUVecs(j, uVec)
+ tL = u(j)
+ eq = AEq(tL, tR)
+ f = QFPAAnd(f, QFPAAtom(eq))
+ j += 1
+ }
+ f
+ }
+
+
+//-------------------------------------
+// main creates List of LIAStar Formulas
+// input f0 AND u IN { v | lDNF} ^*
+// output $1 AND List($2, $3, $4) where $2 IN { $3 | $4 } ^*
+
+
+ def main (f0:QFPAFormula, u:List[TermQFPA], v:List[TermQFPA], lDNF:List[List[QFPAFormula]]):
+ (QFPAFormula, List[(List[TermQFPA], List[TermQFPA], List[QFPAFormula])]) = {
+ val n = lDNF.length
+ val m = u.length
+ val listofFreshUs = createListofFreshVectors(n, m)
+ var i = 0
+ var listLIAS: List[(List[TermQFPA], List[TermQFPA], List[QFPAFormula])] = Nil
+ lDNF.foreach(c => {
+ listLIAS = (listofFreshUs(i), v, c) :: listLIAS
+ i += 1
+ })
+ val fPA = createFormulaWithFreshUsVariables(u, listofFreshUs)
+ (QFPAAnd(f0, fPA), listLIAS)
+ }
+}
+
diff --git a/src/multisets/RemoveStars.scala b/src/multisets/RemoveStars.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0a9753032c815e5caa264f224e03be29b8948747
--- /dev/null
+++ b/src/multisets/RemoveStars.scala
@@ -0,0 +1,422 @@
+package multisets
+
+import scala.collection.mutable.Set
+
+
+object RemoveStars {
+
+// start: will be needed later
+
+ def createFormulafromConjunctions(l:List[QFPAFormula]):QFPAFormula = {
+ if (l.isEmpty) QFPATrue else {
+ var ff = l.head
+ val fr = l.tail
+ fr.foreach (f => ff = QFPAAnd(ff, f))
+ ff
+ }
+ }
+
+
+ def getAllVariablesFromTerm(t:TermQFPA): Set[String] = {
+ val p = multisets.CheckingConsistency.getAllVariablesAndConstsFromTerm(t)
+ p._1
+ }
+// end
+
+
+ def updateWithNewEqualityTerm(v:String, t:TermQFPA, tt:TermQFPA):TermQFPA = tt match {
+ case TVariable(v1) => if (v == v1) t else tt
+ case TConstant(c) => tt
+ case TPlus(t1, t2) => {
+ val t1N = updateWithNewEqualityTerm(v, t, t1)
+ val t2N = updateWithNewEqualityTerm(v, t, t2)
+ TPlus(t1N, t2N)
+ }
+ case TTimes(c, t1) => {
+ val t1N = updateWithNewEqualityTerm(v, t, t1)
+ TTimes(c, t1N)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def updateWithNewEqualityOneEquality(v:String, t:TermQFPA, e:QFPAFormula):QFPAFormula = e match {
+ case QFPAAtom(AEq(t1, t2)) => {
+ val t1N = updateWithNewEqualityTerm(v, t, t1)
+ val t2N = updateWithNewEqualityTerm(v, t, t2)
+ QFPAAtom(AEq(t1N, t2N))
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+ def updateWithNewEqualityVector(va:String, t:TermQFPA, v:List[TermQFPA]):List[TermQFPA] =
+ v.map(tt => updateWithNewEqualityTerm(va, t, tt))
+
+ def updateWithNewEqualityEqualities(va:String, t:TermQFPA, c:List[QFPAFormula]):List[QFPAFormula] =
+ c.map(f => updateWithNewEqualityOneEquality(va, t, f))
+
+
+ def isGroundTerm(t:TermQFPA):Boolean = t match {
+ case TVariable(v) => false
+ case TConstant(c) => true
+ case TPlus(t1, t2) => {
+ val b1 = isGroundTerm(t1)
+ val b2 = isGroundTerm(t2)
+ b1 && b2
+ }
+ case TTimes(c, t1) => isGroundTerm(t1)
+ case TIte(f, t1, t2) => {
+ val b0 = isGroundFormula(f)
+ val b1 = isGroundTerm(t1)
+ val b2 = isGroundTerm(t2)
+ b0 && b1 && b2
+ }
+ }
+
+ def isGroundAtom(a:AtomQFPA):Boolean = a match {
+ case ALeq(t1, t2) => {
+ val b1 = isGroundTerm(t1)
+ val b2 = isGroundTerm(t2)
+ b1 && b2
+ }
+ case AEq(t1, t2) => {
+ val b1 = isGroundTerm(t1)
+ val b2 = isGroundTerm(t2)
+ b1 && b2
+ }
+ }
+
+ def isGroundFormula(f:QFPAFormula):Boolean = f match {
+ case QFPAAnd(f1, f2) => {
+ val b1 = isGroundFormula(f1)
+ val b2 = isGroundFormula(f2)
+ b1 && b2
+ }
+ case QFPAOr(f1, f2) => {
+ val b1 = isGroundFormula(f1)
+ val b2 = isGroundFormula(f2)
+ b1 && b2
+ }
+ case QFPANot(f1) => isGroundFormula(f1)
+ case QFPAAtom(a) => isGroundAtom(a)
+ case QFPAFalse => true
+ case QFPATrue => true
+ }
+
+
+ def createTermThatIsSumOfAllTermsInList(l:List[TermQFPA]):TermQFPA = {
+ val t = if (l.isEmpty) TConstant(0) else {
+ var t1 = l.head
+ val r = l.tail
+ r.foreach(tt => t1 = TPlus(tt, t1))
+ t1
+ }
+ t
+ }
+
+
+ def createTermBasedonListofValues(n:Int, l:List[(String,Int)]):TermQFPA = {
+ var lt: List[TermQFPA] = Nil
+ l.foreach(p => if (p._2 != 0) {
+ if (p._1 == "const") {
+ val m = -1 * n * p._2
+ val t = TConstant(m)
+ lt = t :: lt
+ } else {
+ val m = -1 * n * p._2
+ val t = if (m == 1) TVariable(p._1) else TTimes(m, TVariable(p._1))
+ lt = t :: lt
+ }
+ })
+ val tN = createTermThatIsSumOfAllTermsInList(lt)
+ tN
+ }
+
+ def createNewEqualityBasedOnListofValues(l:List[(String,Int)]):(String, TermQFPA) = {
+ var notFound = true
+ var lt: List[(String,Int)] = Nil
+ var n = 0
+ var v = ""
+ l.foreach(p => if (notFound && p._1 != "const" && (p._2 == 1 || p._2 == -1)) {
+ notFound = false
+ v = p._1
+ n = p._2
+ } else lt = p :: lt)
+ if (notFound) error("I am incomplete and dunno how to solve :" + lt)
+ val t = createTermBasedonListofValues(n, lt)
+ (v, t)
+ }
+
+ def reExpressEqualityandFindNewEquality(f:QFPAFormula):(String, TermQFPA) = f match {
+ case QFPAAtom(AEq(t1, t2)) => {
+ val s1 = getAllVariablesFromTerm(t1)
+ val s2 = getAllVariablesFromTerm(t2)
+ val s = s1 ++ s2
+ val vars = s.toList
+ var lt = createInitialZeroValuesList(vars)
+ val l1 = addValuesofTermToList(t1, lt)
+ val l2 = addValuesofTermToList(t2, lt)
+ val l2N = multiplyListWithConstant(-1, l2)
+ val l = sumTwoLists(l1, l2N)
+ val (v, t) = createNewEqualityBasedOnListofValues(l)
+ (v, t)
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+
+ def updateVectorVwithFormulas(v:List[TermQFPA], c:List[QFPAFormula]):List[TermQFPA] = {
+ var vTemp = v
+ var cTemp = c
+ while (! cTemp.isEmpty) {
+ val f = cTemp.head
+ val cRest = cTemp.tail
+ f match {
+ case QFPAAtom(AEq(TVariable(va), t)) => {
+ vTemp = updateWithNewEqualityVector(va, t, vTemp)
+ cTemp = updateWithNewEqualityEqualities(va, t, cRest)
+ }
+ case QFPAAtom(AEq(t, TVariable(va))) => {
+ vTemp = updateWithNewEqualityVector(va, t, vTemp)
+ cTemp = updateWithNewEqualityEqualities(va, t, cRest)
+ }
+ case _ => {
+ if (! isGroundFormula(f)) {
+ val (va, t) = reExpressEqualityandFindNewEquality(f)
+ vTemp = updateWithNewEqualityVector(va, t, vTemp)
+ cTemp = updateWithNewEqualityEqualities(va, t, cRest)
+ }
+ }
+ }
+ }
+ vTemp
+ }
+
+
+ def getAllVariablesFromVector(v:List[TermQFPA]):List[String] = {
+ var s = Set[String]()
+ v.foreach(t => {
+ val s1 = getAllVariablesFromTerm(t)
+ s = s ++ s1
+ })
+ s.toList
+ }
+
+ def createInitialZeroValuesList(v:List[String]):List[(String,Int)] = {
+ var l = List(("const", 0))
+ v.foreach(s => l = (s, 0) :: l)
+ l.reverse
+ }
+
+ def increaseConstantCount(c:Int, l:List[(String,Int)]):List[(String,Int)] = {
+ var lt: List[(String,Int)] = Nil
+ l.foreach(p => if (p._1 == "const") {
+ val k = p._2 + c
+ lt = ("const", k) :: lt
+ } else lt = p :: lt
+ )
+ lt.reverse
+ }
+
+ def increaseVariableCount(v:String, l:List[(String,Int)]):List[(String,Int)] = {
+ var lt: List[(String,Int)] = Nil
+ l.foreach(p => if (p._1 == v) {
+ val c = p._2 + 1
+ lt = (v, c) :: lt
+ } else lt = p :: lt
+ )
+ lt.reverse
+ }
+
+ def sumTwoLists(l1:List[(String,Int)], l2:List[(String,Int)]):List[(String,Int)] = {
+ var l: List[(String,Int)] = Nil
+ val n = l1.length
+ var i = 0
+ while (i < n) {
+ val p = l1(i)
+ val n = l2(i)._2
+ val s = p._2 + n
+ l = (p._1, s) :: l
+ i = i + 1
+ }
+ l.reverse
+ }
+
+ def multiplyListWithConstant(c:Int, l:List[(String,Int)]):List[(String,Int)] = {
+ var lt: List[(String,Int)] = Nil
+ val n = l.length
+ var i = 0
+ while (i < n) {
+ val p = l(i)
+ val s = c * p._2
+ lt = (p._1, s) :: lt
+ i = i + 1
+ }
+ lt.reverse
+ }
+
+ def addValuesofTermToList(t:TermQFPA, l:List[(String,Int)]):List[(String,Int)] = t match {
+ case TVariable(v) => increaseVariableCount(v, l)
+ case TConstant(c) => increaseConstantCount(c, l)
+ case TPlus(t1, t2) => {
+ val l1 = addValuesofTermToList(t1, l)
+ val l2 = addValuesofTermToList(t2, l)
+ val l3 = sumTwoLists(l1, l2)
+ l3
+ }
+ case TTimes(c, t1) => {
+ val l1 = addValuesofTermToList(t1, l)
+ val l2 = multiplyListWithConstant(c, l1)
+ l2
+ }
+ case x@_ => error("Impossible case :" + x)
+ }
+
+
+ def listContainingOccurancesOfVariables(t:TermQFPA, v:List[String]):List[(String,Int)] = {
+ var l = createInitialZeroValuesList(v)
+ val l1 = addValuesofTermToList(t, l)
+ l1
+ }
+
+ def isZeroVector(v:List[Int]):Boolean = v.forall(n => (n == 0))
+
+ def getValueinOneList(v:String, l:List[(String,Int)]):Int = {
+ var n = 0
+ l.foreach(p => if (p._1 == v) n = p._2)
+ n
+ }
+
+ def constructIntVectorforSLS(v:String, l:List[List[(String,Int)]]):List[Int] = {
+ var lt: List[Int] = Nil
+ l.foreach(s => {
+ val n = getValueinOneList(v, s)
+ lt = n :: lt
+ })
+ lt
+ }
+
+ def constructLinearSetFromList(l:List[List[(String,Int)]], v:List[String]):(List[Int], List[List[Int]]) = {
+ val baseVector = constructIntVectorforSLS("const", l)
+ var stepVectors: List[List[Int]] = Nil
+ v.foreach(s => {
+ val sV = constructIntVectorforSLS(s, l)
+ if (! isZeroVector(sV)) stepVectors = sV :: stepVectors
+ })
+ (baseVector, stepVectors)
+ }
+
+
+ def constructLinearSetFromThisNewVector(v:List[TermQFPA]):(List[Int], List[List[Int]]) = {
+ val a1 = getAllVariablesFromVector(v)
+ val n = v.length
+ var i = 0
+ var lB: List[List[(String,Int)]] = Nil
+ while (i < n) {
+ val ls = listContainingOccurancesOfVariables(v(i), a1)
+ lB = ls :: lB
+ i = i + 1
+ }
+ val sls = constructLinearSetFromList(lB, a1)
+ sls
+ }
+
+
+
+ def createSemilinearSet(v:List[TermQFPA], c:List[QFPAFormula]):(List[Int], List[List[Int]]) = {
+ val v1 = updateVectorVwithFormulas(v, c)
+ val sls = constructLinearSetFromThisNewVector(v1)
+ sls
+ }
+
+///////////////////
+
+ def createTermSumFromTermList(l:List[TermQFPA]):TermQFPA = {
+ val t1 = if (l.isEmpty) TConstant(0) else {
+ var th = l.head
+ val tt = l.tail
+ tt.foreach (t => th = TPlus(th, t))
+ th
+ }
+ t1
+ }
+
+ def createFormulaThatAllNusAreZero(s: Int, e:Int):QFPAFormula = {
+ var i = s
+ var lTemp: List[QFPAFormula] = Nil
+ while (i < e) {
+ val newNu = "FRESHnu" + i
+ val eq = QFPAAtom(AEq(TVariable(newNu), TConstant(0)))
+ lTemp = eq :: lTemp
+ i = i + 1
+ }
+ val f = createFormulafromConjunctions(lTemp)
+ f
+ }
+
+ def createFormulaFromSemilinearSet(u:List[TermQFPA], slset:(List[Int], List[List[Int]]), mc:Int, nc:Int):
+ (QFPAFormula, Int, Int) = {
+ val n = (slset._1).length
+ var i = 0
+ var lTemp: List[QFPAFormula] = Nil
+ val m = (slset._2).length
+ val newMu = "FRESHmu" + mc
+ while (i < n) {
+ val t1 = if ((slset._1)(i) == 0) TConstant(0) else
+ TTimes((slset._1)(i), TVariable(newMu))
+ var j = 0
+ var l2Temp: List[TermQFPA] = Nil
+ while (j < m) {
+ val nuN = nc + j
+ val newNu = "FRESHnu" + nuN
+ val termTemp = if (((slset._2)(j))(i) == 0) TConstant(0) else
+ TTimes(((slset._2)(j))(i), TVariable(newNu))
+ l2Temp = termTemp :: l2Temp
+ j = j + 1
+ }
+ val t2 = createTermSumFromTermList(l2Temp)
+ val eq = QFPAAtom(AEq(u(i), TPlus(t1, t2)))
+ lTemp = eq :: lTemp
+ i = i + 1
+ }
+ val fNew = createFormulafromConjunctions(lTemp)
+ val fMu = QFPANot(QFPAAtom(AEq(TVariable(newMu), TConstant(0))))
+ val fNu = createFormulaThatAllNusAreZero(nc, nc + m)
+ val constraints = QFPAOr(fMu, fNu)
+ val ff = if (slset._2 == Nil) fNew else QFPAAnd(fNew, constraints)
+ val mcN = mc + 1
+ val ncN = nc + m
+ (ff, mcN, ncN)
+ }
+
+
+ def createQFPAFormulaFromLIAStarFormula(u:List[TermQFPA], v:List[TermQFPA], c:List[QFPAFormula], mc: Int, nc: Int):
+ (QFPAFormula, Int, Int) = {
+ val slset = createSemilinearSet(v, c)
+ multisets.StarFormulaPrinter.print_PAVector(v)
+ print(" | ")
+ c.foreach(f => {
+ multisets.StarFormulaPrinter.print_QFPAFormula(f)
+ print(", ")})
+ println(" ")
+ println("semilinear set describing it is: " + slset)
+ val (fNew, m, n) = createFormulaFromSemilinearSet(u, slset, mc, nc)
+ (fNew, m, n)
+ }
+
+ def removeStarsMain(f:QFPAFormula, l:List[(List[TermQFPA], List[TermQFPA], List[QFPAFormula])]):QFPAFormula = {
+ var lTemp: List[QFPAFormula] = Nil
+ var mc = 0
+ var nc = 0
+ l.foreach(t => {
+ val (f1, m, n) = createQFPAFormulaFromLIAStarFormula(t._1, t._2, t._3, mc, nc)
+ lTemp = f1 :: lTemp
+ mc = m
+ nc = n
+ })
+ val fTemp = createFormulafromConjunctions(lTemp)
+ val g = multisets.Multiset2StarsTranslator.removeTrueAndFalse(QFPAAnd(f, fTemp))
+ g
+ }
+
+}
+
diff --git a/src/multisets/StarFormulaPrinter.scala b/src/multisets/StarFormulaPrinter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..57a0304b28c6d15ebd75b5a60a8dc6c289a6c374
--- /dev/null
+++ b/src/multisets/StarFormulaPrinter.scala
@@ -0,0 +1,90 @@
+package multisets
+
+object StarFormulaPrinter {
+
+ def print_QFPAterm(t:TermQFPA):Unit = t match {
+ case TConstant(c) => Console.print(c)
+ case TVariable(v) => Console.print(v)
+ case TPlus(t1, t2) => {
+ print_QFPAterm(t1)
+ Console.print(" + ")
+ print_QFPAterm(t2)
+ }
+ case TTimes(c, t1)=> {
+ Console.print(c + "*")
+ print_QFPAterm(t1)
+ }
+ case TIte(f, t1, t2)=> {
+ Console.print("ITE(")
+ print_QFPAFormula(f)
+ print("; ")
+ print_QFPAterm(t1)
+ print(", ")
+ print_QFPAterm(t2)
+ print(")")
+ }
+ }
+
+ def print_QFPAatom(a:AtomQFPA):Unit = a match {
+ case ALeq(t1,t2) => {
+ print_QFPAterm(t1)
+ Console.print(" =< ")
+ print_QFPAterm(t2)
+ }
+ case AEq(t1,t2) => {
+ print_QFPAterm(t1)
+ Console.print(" = ")
+ print_QFPAterm(t2)
+ }
+ }
+
+ def print_QFPAFormula(f:QFPAFormula):Unit = f match {
+ case QFPAAnd(f1,f2) => {
+ Console.print(" ( ")
+ print_QFPAFormula(f1)
+ print(" ) AND ( ")
+ print_QFPAFormula(f2)
+ print(" ) ")
+ }
+ case QFPAOr(f1,f2) => {
+ Console.print(" ( ")
+ print_QFPAFormula(f1)
+ print(" ) OR ( ")
+ print_QFPAFormula(f2)
+ print(" ) ")
+ }
+ case QFPANot(f1) => {
+ Console.print(" NOT ( ")
+ print_QFPAFormula(f1)
+ print(" ) ")
+ }
+ case QFPAAtom(a) => print_QFPAatom(a)
+ case QFPAFalse => Console.print(" FALSE ")
+ case QFPATrue => Console.print(" TRUE ")
+ }
+
+
+ def print_PAVector(l:List[TermQFPA]):Unit = {
+ Console.print(" ( ")
+ l.foreach(t => {
+ print_QFPAterm(t)
+ print(", ")
+ })
+ print(") ")
+ }
+
+ def print_starFormula(f:StarFormula):Unit = f match {
+ case StarFormula(f1, l1, l2, f2) => {
+ print_QFPAFormula(f1)
+ Console.print(" AND ")
+ print_PAVector(l1)
+ print(" IN { ")
+ print_PAVector(l2)
+ print(" | ")
+ print_QFPAFormula(f2)
+ print(" }*")
+ }
+ }
+
+}
+