Skip to content

Commit

Permalink
changes that make compilation with Scala 2.13 easier
Browse files Browse the repository at this point in the history
  • Loading branch information
pruemmer committed Jan 24, 2024
1 parent 6cff2e7 commit 814f5f3
Show file tree
Hide file tree
Showing 8 changed files with 54 additions and 42 deletions.
9 changes: 8 additions & 1 deletion src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,20 @@ import ap.util.CmdlParser

import scala.collection.mutable.ArrayBuffer

object OstrichStringTheoryBuilder {

val version = "1.3.5"

}

/**
* The entry class of the Ostrich string solver.
*/
class OstrichStringTheoryBuilder extends StringTheoryBuilder {

import OstrichStringTheoryBuilder._

val name = "OSTRICH"
val version = "1.3.5"

Console.withOut(Console.err) {
println
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/ostrich/automata/Regex2Aut.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/**
* This file is part of Ostrich, an SMT solver for strings.
* Copyright (c) 2018-2023 Matthew Hague, Philipp Ruemmer, Riccardo De Masellis. All rights reserved.
* Copyright (c) 2018-2024 Matthew Hague, Philipp Ruemmer, Riccardo De Masellis. All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
Expand Down Expand Up @@ -285,7 +285,7 @@ class ECMAToSymbAFA2(theory : OstrichStringTheory, parser: ECMARegexParser) {
builder.emptyAtomic2AFA(dir)

case IFunApp(`re_charrange`, Seq(Const(l), Const(u))) =>
builder.charrangeAtomic2AFA(dir, new Range(l.intValue, u.intValue+1, 1))
builder.charrangeAtomic2AFA(dir, Range(l.intValue, u.intValue+1, 1))

case IFunApp(`re_allchar`, _) => builder.allcharAtomic2AFA(dir)

Expand Down
16 changes: 10 additions & 6 deletions src/main/scala/ostrich/automata/afa2/AFA2PrintingUtils.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/**
* This file is part of Ostrich, an SMT solver for strings.
* Copyright (c) 2022-2023 Riccado De Masellis. All rights reserved.
* Copyright (c) 2022-2024 Riccado De Masellis. All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
Expand Down Expand Up @@ -36,7 +36,7 @@ import ostrich.automata.afa2.concrete.{AFA2}
import ostrich.automata.afa2.symbolic.{EpsAFA2, SymbAFA2, SymbExtAFA2}

import java.io.{BufferedWriter, File, FileWriter}
import scala.collection.{breakOut, mutable}
import scala.collection.mutable

/*
Classes for printing to dot file the several different versions of 2AFA
Expand Down Expand Up @@ -137,7 +137,8 @@ object AFA2PrintingUtils {
if (t.targets.length > 1) res.append(",color=" + color)
res.append("]\n")
}
res.append("}\n") toString()
res.append("}\n")
res.toString()
}

def toDot(aut: EpsAFA2): String = {
Expand Down Expand Up @@ -175,7 +176,8 @@ object AFA2PrintingUtils {
if (t.targets.length > 1) res.append(",color=" + color)
res.append("]\n")
}
res.append("}\n") toString()
res.append("}\n")
res.toString()
}


Expand Down Expand Up @@ -213,7 +215,8 @@ object AFA2PrintingUtils {
if (t.targets.length > 1) res.append(",color=" + color)
res.append("]\n")
}
res.append("}\n") toString()
res.append("}\n")
res.toString()
}


Expand Down Expand Up @@ -249,7 +252,8 @@ object AFA2PrintingUtils {
if (t.targets.length > 1) res.append(",color=" + color)
res.append("]\n")
}
res.append("}\n") toString()
res.append("}\n")
res.toString()
}


Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/ostrich/automata/afa2/concrete/AFA2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ case class AFA2(initialStates : Seq[Int],
//println("Reduced trans:\n" + reducedTrans)
val newTrans = reducedTrans.mapValues(_.map(x => StepTransition(x.label, x.step, x.targets.map(stateMap))))

val newAut = AFA2(aut.initialStates, aut.finalStates, newTrans)
val newAut = AFA2(aut.initialStates, aut.finalStates, newTrans.toMap)

newAut.restrictToReachableStates
}
Expand Down Expand Up @@ -317,7 +317,7 @@ case class AFA2(initialStates : Seq[Int],
(st, newTS)
}

val newAut = AFA2(aut.initialStates, aut.finalStates, newTrans)
val newAut = AFA2(aut.initialStates, aut.finalStates, newTrans.toMap)

newAut.restrictToReachableStates
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,6 @@ class AFA2StateDuplicator(afa : AFA2) {
}

val result =
new AFA2(newInitial, newFinal, newTransitions).restrictToReachableStates
new AFA2(newInitial, newFinal, newTransitions.toMap).restrictToReachableStates

}
36 changes: 18 additions & 18 deletions src/main/scala/ostrich/automata/afa2/symbolic/SymbEpsReducer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -141,8 +141,8 @@ class SymbEpsReducer(theory: OstrichStringTheory, extafa: SymbExtAFA2) {
val newTargets = for (_ <- targets) yield newState
epsBackwardsSteps ++= newTargets zip targets
Seq(
SymbTransition(new Range(0, theory.alphabetSize, 1), Right, newTargets),
SymbTransition(new Range(endMarker, endMarker + 1, 1), Right, newTargets)
SymbTransition(Range(0, theory.alphabetSize, 1), Right, newTargets),
SymbTransition(Range(endMarker, endMarker + 1, 1), Right, newTargets)
)
}

Expand All @@ -153,18 +153,18 @@ class SymbEpsReducer(theory: OstrichStringTheory, extafa: SymbExtAFA2) {
yield (source -> trans2)

val extraTransitions: Seq[(Int, SymbTransition)] =
(for ((source, target) <- epsBackwardsSteps) yield
(for ((source, target) <- epsBackwardsSteps.toSeq) yield
Seq(
(source, SymbTransition(new Range(0, theory.alphabetSize, 1), Left, Seq(target))),
(source, SymbTransition(new Range(endMarker, endMarker + 1, 1), Left, Seq(target)))
(source, SymbTransition(Range(0, theory.alphabetSize, 1), Left, Seq(target))),
(source, SymbTransition(Range(endMarker, endMarker + 1, 1), Left, Seq(target)))
)).flatten

val newFlatTransitions = newFlatPreTransitions ++ extraTransitions

val newTransitions =
newFlatTransitions groupBy (_._1) mapValues { l => l map (_._2) }

SymbAFA2(Seq(epsafa.initialState), epsafa.finalStates, newTransitions)
SymbAFA2(Seq(epsafa.initialState), epsafa.finalStates, newTransitions.toMap)
}


Expand All @@ -185,22 +185,22 @@ class SymbEpsReducer(theory: OstrichStringTheory, extafa: SymbExtAFA2) {

newFlatTransWEps ++= (
for (s <- extafa.initialStates)
yield (newInitialState -> SymbTransition(new Range(beginMarker, beginMarker + 1, 1), Right, Seq(s)))
yield (newInitialState -> SymbTransition(Range(beginMarker, beginMarker + 1, 1), Right, Seq(s)))
) ++ (
for (s <- extafa.finalRightStates)
yield (s -> SymbTransition(new Range(endMarker, endMarker + 1, 1), Right, Seq(newFinalEndState)))
yield (s -> SymbTransition(Range(endMarker, endMarker + 1, 1), Right, Seq(newFinalEndState)))
) ++ Seq(
(newFinalBeginState -> SymbTransition(new Range(0, theory.alphabetSize, 1), Right, Seq(newFinalBeginState))),
(newFinalBeginState -> SymbTransition(new Range(beginMarker, beginMarker + 1, 1), Right, Seq(newFinalBeginState))),
(newFinalBeginState -> SymbTransition(new Range(endMarker, endMarker + 1, 1), Right, Seq(newFinalBeginState)))
(newFinalBeginState -> SymbTransition(Range(0, theory.alphabetSize, 1), Right, Seq(newFinalBeginState))),
(newFinalBeginState -> SymbTransition(Range(beginMarker, beginMarker + 1, 1), Right, Seq(newFinalBeginState))),
(newFinalBeginState -> SymbTransition(Range(endMarker, endMarker + 1, 1), Right, Seq(newFinalBeginState)))
) ++ (
for (s <- extafa.finalLeftStates)
yield (s -> SymbTransition(new Range(beginMarker, beginMarker + 1, 1), Left, Seq(newFinalBeginState)))
yield (s -> SymbTransition(Range(beginMarker, beginMarker + 1, 1), Left, Seq(newFinalBeginState)))
)

val transWEps = newFlatTransWEps.toList.groupBy (_._1) mapValues { l => l map (_._2) }

EpsAFA2(newInitialState, Seq(newFinalEndState, newFinalBeginState), transWEps)
EpsAFA2(newInitialState, Seq(newFinalEndState, newFinalBeginState), transWEps.toMap)
}


Expand Down Expand Up @@ -251,7 +251,7 @@ symbolic MacrostateAFA2, which has still universal epsilon transitions.
case concStep: StepTransition =>
throw new RuntimeException(
"Unexpected transition in epsilon elimination: " + concStep)
}))
})).toMap

// We do not need the starting states of those transitions anymore (as they are all in mst)
val outTrans = outms.values.flatten
Expand Down Expand Up @@ -284,9 +284,9 @@ symbolic MacrostateAFA2, which has still universal epsilon transitions.

val finMStates = analysed.filter(x => x.states.intersect(epsafa.finalStates.toSet) != Set.empty)

val mtransMap = macroTrans.groupBy(_._1).mapValues(l => l map (_._2))
val mtransMap = macroTrans.groupBy(_._1).mapValues(l => l.map(_._2).toSeq)

SymbMAFA2(initMState, analysed.toSet, finMStates.toSet, mtransMap)
SymbMAFA2(initMState, analysed.toSet, finMStates.toSet, mtransMap.toMap)
}


Expand All @@ -304,9 +304,9 @@ It transforms a MAFA2 with universal eps transitions back into an epsAFA2 which
case et: SymbMEpsTransition => (stMap.get(st).get, EpsTransition(et._targets.map(stMap).toList))
case str: SymbMStepTransition => (stMap.get(st).get, SymbTransition(str.label, str.step, str.targets.map(stMap).toList))
}
val trans = flatTrans.toList.groupBy(_._1).mapValues(l => l map (_._2))
val trans = flatTrans.toList.groupBy(_._1).mapValues(l => l.map(_._2).toSeq)

EpsAFA2(initState, finalStates.toSeq, trans)
EpsAFA2(initState, finalStates.toSeq, trans.toMap)
}


Expand Down
23 changes: 12 additions & 11 deletions src/main/scala/ostrich/automata/afa2/symbolic/SymbMutableAFA2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -58,12 +58,12 @@ object SymbMutableAFA2 {
if (newSeq.nonEmpty) {
while (currInd < newSeq.length) {
if (currInd + 1 < newSeq.length && newSeq(currInd + 1) != newSeq(currInd) + 1) {
newRanges += (new Range(newSeq(lastInd), newSeq(currInd) + 1, 1))
newRanges += Range(newSeq(lastInd), newSeq(currInd) + 1, 1)
lastInd = currInd + 1
}
currInd += 1
}
newRanges += (new Range(newSeq(lastInd), newSeq(currInd - 1) + 1, 1))
newRanges += Range(newSeq(lastInd), newSeq(currInd - 1) + 1, 1)
}
newRanges.toSet
}
Expand Down Expand Up @@ -137,7 +137,7 @@ the ECMAregex cases.
def allcharAtomic2AFA(dir: Step): SymbMutableAFA2 = {
val iniState = new BState(dir)
val finState = new BState(dir)
val allCharrange = new Range(min_char, alphabet_size, 1)
val allCharrange = Range(min_char, alphabet_size, 1)

val trans: ArrayBuffer[(BState, SymbBTransition)] =
ArrayBuffer[(BState, SymbBTransition)]() += ((iniState, SymbBStepTransition(allCharrange, dir, Seq(finState))))
Expand Down Expand Up @@ -526,7 +526,7 @@ the ECMAregex cases.
direction should the loop be? It does not really matter, because it is a final sink state. For consistency,
I have chosen to be the same direction of the state direction.
*/
aut.transitions += ((aut.mainFinState, SymbBStepTransition(new Range(min_char, alphabet_size, 1), aut.mainFinState.dir, Seq(aut.mainFinState))))
aut.transitions += ((aut.mainFinState, SymbBStepTransition(Range(min_char, alphabet_size, 1), aut.mainFinState.dir, Seq(aut.mainFinState))))

// The mainFinal state becomes secondary final state.
aut.finStates += aut.mainFinState
Expand Down Expand Up @@ -557,7 +557,7 @@ the ECMAregex cases.
I have chosen to be the same direction of the state direction.
*/
aut.transitions +=
((aut.mainFinState, SymbBStepTransition(new Range(min_char, alphabet_size, 1), aut.mainFinState.dir, Seq(aut.mainFinState))))
((aut.mainFinState, SymbBStepTransition(Range(min_char, alphabet_size, 1), aut.mainFinState.dir, Seq(aut.mainFinState))))

// The mainFinal state becomes secondary final state.
aut.finStates += aut.mainFinState
Expand Down Expand Up @@ -627,7 +627,7 @@ case class SymbMutableAFA2(builder: SymbAFA2Builder,
Set.empty ++ allStates
}

private def transToMap(): Map[BState, Seq[SymbBTransition]] = transitions.groupBy(_._1).mapValues(l => l map (_._2))
private def transToMap(): Map[BState, Seq[SymbBTransition]] = transitions.groupBy(_._1).mapValues(l => l.map(_._2).toSeq).toMap


def builderToSymbExtAFA(): SymbExtAFA2 = {
Expand All @@ -643,9 +643,9 @@ case class SymbMutableAFA2(builder: SymbAFA2Builder,
case et: SymbBEpsTransition => EpsTransition(et._targets.map(stMap))
})

val transMap = trans.groupBy(_._1).mapValues(l => l map (_._2))
val transMap = trans.groupBy(_._1).mapValues(l => l.map(_._2).toSeq)

SymbExtAFA2(Seq(initialState), finalLeftStates.toSeq, finalRightStates.toSeq, transMap)
SymbExtAFA2(Seq(initialState), finalLeftStates.toSeq, finalRightStates.toSeq, transMap.toMap)
}


Expand All @@ -657,7 +657,7 @@ case class SymbMutableAFA2(builder: SymbAFA2Builder,
ts <- transMap.get(s).iterator;
t <- ts;
if (t.isInstanceOf[SymbBStepTransition] &&
t.asInstanceOf[SymbBStepTransition].label==new Range(builder.min_char, builder.alphabet_size, 1) &&
t.asInstanceOf[SymbBStepTransition].label== Range(builder.min_char, builder.alphabet_size, 1) &&
t.targets==Seq(s)))
yield s
}
Expand Down Expand Up @@ -697,7 +697,8 @@ case class SymbMutableAFA2(builder: SymbAFA2Builder,

for (state <- allStepStates) {
// Compute the set of ranges NOT appearing in outgoing transitions
var outRanges = Set(new Range(builder.min_char, builder.alphabet_size, 1))
var outRanges : Set[Range] =
Set(Range(builder.min_char, builder.alphabet_size))
for (ts <- transMap.get(state);
t <- ts) t match {
case SymbBStepTransition(label, _, _) => {
Expand Down Expand Up @@ -813,7 +814,7 @@ case class SymbMutableAFA2(builder: SymbAFA2Builder,
transitions.filter(x => x._2.isInstanceOf[SymbBStepTransition]).asInstanceOf[ArrayBuffer[(BState, SymbBStepTransition)]]

var transMapStep: Map[(BState, Range), Seq[Seq[BState]]] =
transBufNotEps.groupBy(x => (x._1, x._2.label)).mapValues(x => x map (y => y._2.targets))
transBufNotEps.groupBy(x => (x._1, x._2.label)).mapValues(x => x.map(y => y._2.targets).toSeq).toMap


// check (1)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ object SymbToConcTranslator {

//println("New flat trans:\n"+ newTransFlat.map{t=>t._2})

newTransFlat.groupBy(_._1).mapValues(l => l map (_._2))
newTransFlat.groupBy(_._1).mapValues(l => l.map(_._2).toSeq).toMap
}


Expand Down

0 comments on commit 814f5f3

Please sign in to comment.