diff --git a/.gitignore b/.gitignore index a0e5ebc..a1bfd48 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,10 @@ target .*.swp *~ + +.metals +.bloop +.vscode +project/.bloop +project/metals.sbt +project/project diff --git a/.larabot.conf b/.larabot.conf index 33eebde..379454e 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,12 +1,5 @@ commands = [ - "sbt -batch ++2.10.7 test" - "sbt -batch ++2.11.12 test" - "sbt -batch ++2.12.8 test" - "sbt -batch ++2.13.0 test" - "sbt -batch ++2.10.7 it:test" - "sbt -batch ++2.11.12 it:test" - "sbt -batch ++2.12.8 it:test" - "sbt -batch ++2.13.0 it:test" + "sbt -batch ++2.12.13 it:test" ] trusted = [ diff --git a/build.sbt b/build.sbt index e7aae83..7e6c72d 100644 --- a/build.sbt +++ b/build.sbt @@ -8,7 +8,9 @@ javaOptions in IntegrationTest ++= Seq("-Xss128M") fork in IntegrationTest := true -libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.8" % "test,it" +libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" +libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test" + logBuffered in IntegrationTest := false @@ -17,19 +19,13 @@ parallelExecution in Test := true lazy val commonSettings = Seq( organization := "com.regblanc", name := "scala-smtlib", - scalaVersion := "2.12.8", - crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.13.0") -) - -lazy val publishSettings = Seq( - bintrayOrganization := Some("epfl-lara"), - bintrayRepository := "maven", + scalaVersion := "2.12.13", + crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.0", "2.13.5") ) lazy val root = (project in file(".")). configs(IntegrationTest). settings(commonSettings: _*). - settings(publishSettings: _*). settings(Defaults.itSettings: _*) publishMavenStyle := true diff --git a/project/build.properties b/project/build.properties index c0bab04..080a737 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1 +1 @@ -sbt.version=1.2.8 +sbt.version=1.3.0 diff --git a/project/plugins.sbt b/project/plugins.sbt index 01bed96..23d5057 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -1,6 +1 @@ addSbtPlugin("com.typesafe.sbt" % "sbt-git" % "1.0.0") - -// avoids warning from sbt-git, see https://github.com/sbt/sbt-git#known-issues -libraryDependencies += "org.slf4j" % "slf4j-nop" % "1.7.21" - -addSbtPlugin("org.foundweekends" % "sbt-bintray" % "0.5.4") diff --git a/src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2 b/src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2 index 38d983d..8a4ea20 100644 --- a/src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2 +++ b/src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2 @@ -1,5 +1,5 @@ (set-option :print-success true) -(set-logic QF_UF) +(set-logic UF) (declare-sort U 0) (declare-fun x0 () U) (declare-fun y0 () U) diff --git a/src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2 b/src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2 index 96609c5..057a732 100644 --- a/src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2 +++ b/src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2 @@ -1,5 +1,5 @@ (set-option :print-success true) -(set-logic QF_UF) +(set-logic UF) (declare-sort U 0) (declare-fun x0 () U) (declare-fun y0 () U) diff --git a/src/it/scala/smtlib/it/ProcessInterpreterTests.scala b/src/it/scala/smtlib/it/ProcessInterpreterTests.scala index 9e6c35b..9e07597 100644 --- a/src/it/scala/smtlib/it/ProcessInterpreterTests.scala +++ b/src/it/scala/smtlib/it/ProcessInterpreterTests.scala @@ -3,7 +3,7 @@ package it import scala.sys.process._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import java.io.File import java.io.FileReader @@ -14,7 +14,7 @@ import printer.RecursivePrinter import interpreters._ -class ProcessInterpreterTests extends FunSuite with TestHelpers { +class ProcessInterpreterTests extends AnyFunSuite with TestHelpers { //TODO: properly get all interpreters def interpreters: Seq[Interpreter] = Seq(getZ3Interpreter) diff --git a/src/it/scala/smtlib/it/SmtLibRunnerTests.scala b/src/it/scala/smtlib/it/SmtLibRunnerTests.scala index 90d8c1f..4db70f0 100644 --- a/src/it/scala/smtlib/it/SmtLibRunnerTests.scala +++ b/src/it/scala/smtlib/it/SmtLibRunnerTests.scala @@ -3,7 +3,7 @@ package it import scala.sys.process._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import java.io.File import java.io.FileReader @@ -21,7 +21,7 @@ import interpreters._ * * TODO: proper way to display warning when not all tests are run because of not found executables. */ -class SmtLibRunnerTests extends FunSuite with TestHelpers { +class SmtLibRunnerTests extends AnyFunSuite with TestHelpers { filesInResourceDir("regression/smtlib/solving/all", _.endsWith(".smt2")).foreach(file => { if(isZ3Available) { @@ -72,7 +72,7 @@ class SmtLibRunnerTests extends FunSuite with TestHelpers { val lexer = new Lexer(new FileReader(file)) val parser = new Parser(lexer) - for(expected <- scala.io.Source.fromFile(want).getLines) { + for(expected <- scala.io.Source.fromFile(want).getLines()) { val cmd = parser.parseCommand assert(cmd !== null) val res: String = interpreter.eval(cmd).toString diff --git a/src/it/scala/smtlib/it/TestHelpers.scala b/src/it/scala/smtlib/it/TestHelpers.scala index fe6da85..72eb089 100644 --- a/src/it/scala/smtlib/it/TestHelpers.scala +++ b/src/it/scala/smtlib/it/TestHelpers.scala @@ -3,7 +3,7 @@ package it import scala.sys.process._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import java.io.File import java.io.FileReader diff --git a/src/it/scala/smtlib/it/TheoriesBuilderTests.scala b/src/it/scala/smtlib/it/TheoriesBuilderTests.scala index e058d36..90af020 100644 --- a/src/it/scala/smtlib/it/TheoriesBuilderTests.scala +++ b/src/it/scala/smtlib/it/TheoriesBuilderTests.scala @@ -3,7 +3,7 @@ package it import scala.sys.process._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import java.io.File import java.io.FileReader @@ -16,7 +16,7 @@ import trees.CommandsResponses._ /** Checks that formula build with theories module are correctly handled by solvers */ -class TheoriesBuilderTests extends FunSuite with TestHelpers { +class TheoriesBuilderTests extends AnyFunSuite with TestHelpers { def mkTest(formula: Term, expectedStatus: Status, prefix: String) = { diff --git a/src/main/scala/smtlib/extensions/tip/Parser.scala b/src/main/scala/smtlib/extensions/tip/Parser.scala index 1ffa2cf..c68c36e 100644 --- a/src/main/scala/smtlib/extensions/tip/Parser.scala +++ b/src/main/scala/smtlib/extensions/tip/Parser.scala @@ -38,13 +38,13 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { override protected def parseTermWithoutParens(startPos: Position): Term = getPeekToken.kind match { case Tokens.Lambda => eat(Tokens.Lambda) - val args = parseMany(parseSortedVar _) + val args = parseMany(() => parseSortedVar) val body = parseTerm Lambda(args, body) case Tokens.At => eat(Tokens.At) - val (caller +: args) = parseUntil(LT.CParen, eatEnd = false)(parseTerm _) + val (caller +: args) = parseUntil(LT.CParen, eatEnd = false)(() => parseTerm) Application(caller, args) case Tokens.Match => @@ -59,7 +59,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { Default case LT.OParen => - val (sym, binders) = parseOneOrMore(parseSymbol _) + val (sym, binders) = parseOneOrMore(() => parseSymbol) CaseClass(sym, binders) case _ => @@ -82,7 +82,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { getPeekToken.kind match { case LT.Par => eat(LT.Par) - val tps = parseMany(parseSymbol _) + val tps = parseMany(() => parseSymbol) val res = parseTerm eat(LT.CParen) (Some(tps), res) @@ -123,8 +123,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { case LT.OParen => eat(LT.OParen) eat(LT.Par) - val tps = parseMany(parseSymbol _) - val (sym, sort) = parseWithin(LT.OParen, LT.CParen)(parseDecl _) + val tps = parseMany(() => parseSymbol) + val (sym, sort) = parseWithin(LT.OParen, LT.CParen)(() => parseDecl) eat(LT.CParen) DeclareConstPar(tps, sym, sort) case _ => @@ -136,7 +136,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { eat(LT.DeclareFun) def parseDecl: (SSymbol, Seq[Sort], Sort) = { val sym = parseSymbol - val sorts = parseMany(parseSort _) + val sorts = parseMany(() => parseSort) val resultSort = parseSort (sym, sorts, resultSort) } @@ -144,8 +144,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { case LT.OParen => eat(LT.OParen) eat(LT.Par) - val tps = parseMany(parseSymbol _) - val (sym, args, resultSort) = parseWithin(LT.OParen, LT.CParen)(parseDecl _) + val tps = parseMany(() => parseSymbol) + val (sym, args, resultSort) = parseWithin(LT.OParen, LT.CParen)(() => parseDecl) eat(LT.CParen) DeclareFunPar(tps, sym, args, resultSort) case _ => @@ -159,8 +159,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { case LT.OParen => eat(LT.OParen) eat(LT.Par) - val tps = parseMany(parseSymbol _) - val funDef = parseWithin(LT.OParen, LT.CParen)(parseFunDef _) + val tps = parseMany(() => parseSymbol) + val funDef = parseWithin(LT.OParen, LT.CParen)(() => parseFunDef) eat(LT.CParen) DefineFunPar(tps, funDef) @@ -175,8 +175,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { case LT.OParen => eat(LT.OParen) eat(LT.Par) - val tps = parseMany(parseSymbol _) - val funDef = parseWithin(LT.OParen, LT.CParen)(parseFunDef _) + val tps = parseMany(() => parseSymbol) + val funDef = parseWithin(LT.OParen, LT.CParen)(() => parseFunDef) eat(LT.CParen) DefineFunRecPar(tps, funDef) @@ -192,8 +192,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { val funDec = getPeekToken.kind match { case LT.Par => eat(LT.Par) - val tps = parseMany(parseSymbol _) - val funDec = parseWithin(LT.OParen, LT.CParen)(parseFunDec _) + val tps = parseMany(() => parseSymbol) + val funDec = parseWithin(LT.OParen, LT.CParen)(() => parseFunDec) Left(FunDecPar(tps, funDec.name, funDec.params, funDec.returnSort)) case _ => Right(parseFunDec) @@ -201,7 +201,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { eat(LT.CParen) funDec }) - val (body, bodies) = parseOneOrMore(parseTerm _) + val (body, bodies) = parseOneOrMore(() => parseTerm) assert(funDecs.size == bodies.size) if ((funDec +: funDecs).exists(_.isLeft)) { @@ -213,8 +213,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) { case LT.DeclareDatatypes => eat(LT.DeclareDatatypes) - val tps = parseMany(parseSymbol _) - val datatypes = parseMany(parseDatatypes _) + val tps = parseMany(() => parseSymbol) + val datatypes = parseMany(() => parseDatatypes) DeclareDatatypesPar(tps, datatypes) case _ => super.parseCommandWithoutParens diff --git a/src/main/scala/smtlib/parser/ParserCommands.scala b/src/main/scala/smtlib/parser/ParserCommands.scala index 7b048d4..4f775b4 100644 --- a/src/main/scala/smtlib/parser/ParserCommands.scala +++ b/src/main/scala/smtlib/parser/ParserCommands.scala @@ -22,13 +22,13 @@ trait ParserCommands { this: ParserCommon with ParserTerms => Script(cmds.toList) } - protected def parseCommandWithoutParens: Command = nextToken.kind match { + protected def parseCommandWithoutParens: Command = nextToken().kind match { case Tokens.Assert => { Assert(parseTerm) } case Tokens.CheckSat => CheckSat() case Tokens.CheckSatAssuming => { - val props = parseMany(parsePropLit _) + val props = parseMany(() => parsePropLit) CheckSatAssuming(props) } @@ -64,8 +64,8 @@ trait ParserCommands { this: ParserCommon with ParserTerms => DefineFunRec(funDef) } case Tokens.DefineFunsRec => { - val (funDef, funDefs) = parseOneOrMore(() => parseWithin(Tokens.OParen, Tokens.CParen)(parseFunDec _)) - val (body, bodies) = parseOneOrMore(parseTerm _) + val (funDef, funDefs) = parseOneOrMore(() => parseWithin(Tokens.OParen, Tokens.CParen)(() => parseFunDec)) + val (body, bodies) = parseOneOrMore(() => parseTerm) assert(funDefs.size == bodies.size) DefineFunsRec(funDef +: funDefs, body +: bodies) } @@ -151,7 +151,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => eat(Tokens.OParen) eat(Tokens.CParen) - val datatypes = parseMany(parseDatatypes _) + val datatypes = parseMany(() => parseDatatypes) DeclareDatatypes(datatypes) } @@ -162,7 +162,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => } def parseCommand: Command = if(peekToken == null) null else { - val head = nextToken + val head = nextToken() check(head, Tokens.OParen) val cmd = parseCommandWithoutParens eat(Tokens.CParen) @@ -192,7 +192,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => def parseFunDec: FunDec = { val name = parseSymbol - val sortedVars = parseMany(parseSortedVar _) + val sortedVars = parseMany(() => parseSortedVar) val sort = parseSort @@ -202,7 +202,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => def parseFunDef: FunDef = { val name = parseSymbol - val sortedVars = parseMany(parseSortedVar _) + val sortedVars = parseMany(() => parseSortedVar) val sort = parseSort @@ -241,7 +241,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => def parseInfoFlag: InfoFlag = { - val t = nextToken + val t = nextToken() val flag = t match { case Tokens.Keyword("all-statistics") => AllStatisticsInfoFlag() case Tokens.Keyword("assertion-stack-levels") => AssertionStackLevelsInfoFlag() @@ -261,52 +261,52 @@ trait ParserCommands { this: ParserCommon with ParserTerms => val peekPosition = peekToken.getPos val opt = peekToken match { case Tokens.Keyword("diagnostic-output-channel") => - nextToken + nextToken() DiagnosticOutputChannel(parseString.value) case Tokens.Keyword("global-declarations") => - nextToken + nextToken() GlobalDeclarations(parseBool) case Tokens.Keyword("interactive-mode") => - nextToken + nextToken() InteractiveMode(parseBool) case Tokens.Keyword("print-success") => - nextToken + nextToken() PrintSuccess(parseBool) case Tokens.Keyword("produce-assertions") => - nextToken + nextToken() ProduceAssertions(parseBool) case Tokens.Keyword("produce-assignments") => - nextToken + nextToken() ProduceAssignments(parseBool) case Tokens.Keyword("produce-models") => - nextToken + nextToken() ProduceModels(parseBool) case Tokens.Keyword("produce-proofs") => - nextToken + nextToken() ProduceProofs(parseBool) case Tokens.Keyword("produce-unsat-assumptions") => - nextToken + nextToken() ProduceUnsatAssumptions(parseBool) case Tokens.Keyword("produce-unsat-cores") => - nextToken + nextToken() ProduceUnsatCores(parseBool) case Tokens.Keyword("random-seed") => - nextToken + nextToken() RandomSeed(parseNumeral.value.toInt) case Tokens.Keyword("regular-output-channel") => - nextToken + nextToken() RegularOutputChannel(parseString.value) case Tokens.Keyword("reproducible-resource-limit") => - nextToken + nextToken() ReproducibleResourceLimit(parseNumeral.value.toInt) case Tokens.Keyword("verbosity") => - nextToken + nextToken() Verbosity(parseNumeral.value.toInt) case _ => @@ -316,7 +316,7 @@ trait ParserCommands { this: ParserCommon with ParserTerms => } def parseBool: Boolean = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("true") => true case Tokens.SymbolLit("false") => false case t => expected(t) //TODO: not sure how to tell we were expecting one of two specific symbols diff --git a/src/main/scala/smtlib/parser/ParserCommandsResponses.scala b/src/main/scala/smtlib/parser/ParserCommandsResponses.scala index f0f4e7b..3542190 100644 --- a/src/main/scala/smtlib/parser/ParserCommandsResponses.scala +++ b/src/main/scala/smtlib/parser/ParserCommandsResponses.scala @@ -15,7 +15,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC * Parsing error response, assuming "(" has been parsed */ private def parseErrorResponse: Error = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("error") => val msg = parseString.value eat(Tokens.CParen) @@ -24,7 +24,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } } - def parseGenResponse: GenResponse = nextToken match { + def parseGenResponse: GenResponse = nextToken() match { case Tokens.SymbolLit("success") => Success case Tokens.SymbolLit("unsupported") => Unsupported case t => @@ -41,14 +41,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC (sym, bool) } - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val pairs = parseUntil(Tokens.CParen)(parsePair _) + val pairs = parseUntil(Tokens.CParen)(() => parsePair) GetAssignmentResponseSuccess(pairs) } } @@ -65,14 +65,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC (t1, t2) } - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val pairs = parseUntil(Tokens.CParen)(parsePair _) + val pairs = parseUntil(Tokens.CParen)(() => parsePair) GetValueResponseSuccess(pairs) } } @@ -84,14 +84,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC tryParseConstant match { case Some(cst) => GetOptionResponseSuccess(cst) case None => { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case Tokens.SymbolLit(sym) => GetOptionResponseSuccess(SSymbol(sym)) case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse - case _ => GetOptionResponseSuccess(SList(parseUntil(Tokens.CParen)(parseSExpr _).toList)) + case _ => GetOptionResponseSuccess(SList(parseUntil(Tokens.CParen)(() => parseSExpr).toList)) } } } @@ -103,7 +103,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC tryParseConstant match { case Some(cst) => GetProofResponseSuccess(cst) case None => { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case Tokens.SymbolLit(sym) => GetProofResponseSuccess(SSymbol(sym)) case Tokens.Keyword(key) => GetProofResponseSuccess(SKeyword(key)) @@ -111,7 +111,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse - case _ => GetProofResponseSuccess(SList(parseUntil(Tokens.CParen)(parseSExpr _).toList)) + case _ => GetProofResponseSuccess(SList(parseUntil(Tokens.CParen)(() => parseSExpr).toList)) } } } @@ -120,17 +120,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseGetModelResponse: GetModelResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - nextToken match { - case Tokens.SymbolLit("model") => () - case t => expected(t, Tokens.SymbolLitKind) //TODO: expected symbol of value "model" - } + if (peekToken == Tokens.SymbolLit("model")) nextToken() val exprs: ListBuffer[SExpr] = new ListBuffer while(peekToken.kind != Tokens.CParen) { try { @@ -139,7 +136,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC case ex: UnknownCommandException => { ex.commandName match { //recover for exceptions case in get-model case Tokens.Forall => - val vars = parseMany(parseSortedVar _) + val vars = parseMany(() => parseSortedVar) val term = parseTerm eat(Tokens.CParen) exprs.append(Forall(vars.head, vars.tail, term)) @@ -160,25 +157,25 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC def parseInfoResponse: InfoResponse = { peekToken match { case Tokens.Keyword("assertion-stack-levels") => - nextToken + nextToken() AssertionStackLevelsInfoResponse(parseNumeral.value.toInt) case Tokens.Keyword("authors") => - nextToken + nextToken() AuthorsInfoResponse(parseString.value) case Tokens.Keyword("error-behavior") => - nextToken - val behaviour = nextToken match { + nextToken() + val behaviour = nextToken() match { case Tokens.SymbolLit("immediate-exit") => ImmediateExitErrorBehavior case Tokens.SymbolLit("continued-execution") => ContinuedExecutionErrorBehavior case t => expected(t) //TODO: precise error } ErrorBehaviorInfoResponse(behaviour) case Tokens.Keyword("name") => - nextToken + nextToken() NameInfoResponse(parseString.value) case Tokens.Keyword("reason-unknown") => - nextToken - val reason = nextToken match { + nextToken() + val reason = nextToken() match { case Tokens.SymbolLit("timeout") => TimeoutReasonUnknown case Tokens.SymbolLit("memout") => MemoutReasonUnknown case Tokens.SymbolLit("incomplete") => IncompleteReasonUnknown @@ -186,7 +183,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } ReasonUnknownInfoResponse(reason) case Tokens.Keyword("version") => - nextToken + nextToken() VersionInfoResponse(parseString.value) case _ => AttributeInfoResponse(parseAttribute) @@ -194,14 +191,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseGetInfoResponse: GetInfoResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val responses = parseUntil(Tokens.CParen)(parseInfoResponse _) + val responses = parseUntil(Tokens.CParen)(() => parseInfoResponse) GetInfoResponseSuccess(responses.head, responses.tail) } } @@ -210,7 +207,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseCheckSatResponse: CheckSatResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("sat") => CheckSatStatus(SatStatus) case Tokens.SymbolLit("unsat") => CheckSatStatus(UnsatStatus) case Tokens.SymbolLit("unknown") => CheckSatStatus(UnknownStatus) @@ -223,7 +220,7 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseEchoResponse: EchoResponse = { - nextToken match { + nextToken() match { case Tokens.StringLit(value) => EchoResponseSuccess(value) case Tokens.SymbolLit("unsupported") => Unsupported case t => { @@ -234,14 +231,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseGetAssertionsResponse: GetAssertionsResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val terms = parseUntil(Tokens.CParen)(parseTerm _) + val terms = parseUntil(Tokens.CParen)(() => parseTerm) GetAssertionsResponseSuccess(terms) } } @@ -250,14 +247,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseGetUnsatAssumptionsResponse: GetUnsatAssumptionsResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val props = parseUntil(Tokens.CParen)(parsePropLit _) + val props = parseUntil(Tokens.CParen)(() => parsePropLit) GetUnsatAssumptionsResponseSuccess(props) } } @@ -266,14 +263,14 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC } def parseGetUnsatCoreResponse: GetUnsatCoreResponse = { - nextToken match { + nextToken() match { case Tokens.SymbolLit("unsupported") => Unsupported case t => { check(t, Tokens.OParen) peekToken match { case Tokens.SymbolLit("error") => parseErrorResponse case t => { - val syms = parseUntil(Tokens.CParen)(parseSymbol _) + val syms = parseUntil(Tokens.CParen)(() => parseSymbol) GetUnsatCoreResponseSuccess(syms) } } diff --git a/src/main/scala/smtlib/parser/ParserCommon.scala b/src/main/scala/smtlib/parser/ParserCommon.scala index 06f15e9..097fdff 100644 --- a/src/main/scala/smtlib/parser/ParserCommon.scala +++ b/src/main/scala/smtlib/parser/ParserCommon.scala @@ -70,7 +70,7 @@ trait ParserCommon { * Make sure the next token has the expected kind and read it */ protected def eat(expected: TokenKind): Token = { - val token = nextToken + val token = nextToken() check(token, expected) token } @@ -78,7 +78,7 @@ trait ParserCommon { * Make sure the next token is exactly ``expected`` (usually a symbol lit) */ protected def eat(expected: Token): Token = { - val token = nextToken + val token = nextToken() if(token != expected) throw new UnexpectedTokenException(token, Seq(expected.kind)) token @@ -181,7 +181,7 @@ trait ParserCommon { def parseKeyword: SKeyword = { - nextToken match { + nextToken() match { case t@Tokens.Keyword(k) => { val keyword = SKeyword(k) keyword.setPos(t) @@ -201,7 +201,7 @@ trait ParserCommon { } else { val name = parseIdentifier - val subSorts = parseUntil(Tokens.CParen, eatEnd = false)(parseSort _) + val subSorts = parseUntil(Tokens.CParen, eatEnd = false)(() => parseSort) Sort(name, subSorts.toList).setPos(startPos) } @@ -230,7 +230,7 @@ trait ParserCommon { val sym = parseSymbol val head = parseSExpr - val indices = parseUntil(Tokens.CParen, eatEnd = false)(parseSExpr _) + val indices = parseUntil(Tokens.CParen, eatEnd = false)(() => parseSExpr) Identifier(sym, head +: indices) } @@ -245,7 +245,7 @@ trait ParserCommon { def parseIdentifier: Identifier = { if(getPeekToken.kind == Tokens.OParen) { val pos = getPeekToken.getPos - parseWithin(Tokens.OParen, Tokens.CParen)(parseUnderscoreIdentifier _).setPos(pos) + parseWithin(Tokens.OParen, Tokens.CParen)(() => parseUnderscoreIdentifier).setPos(pos) } else { val sym = parseSymbol Identifier(sym).setPos(sym) @@ -253,7 +253,7 @@ trait ParserCommon { } def parseSymbol: SSymbol = { - nextToken match { + nextToken() match { case t@Tokens.SymbolLit(s) => { val symbol = SSymbol(s) symbol.setPos(t) @@ -270,7 +270,7 @@ trait ParserCommon { */ def parseString: SString = { - nextToken match { + nextToken() match { case t@Tokens.StringLit(s) => { val str = SString(s) str.setPos(t) @@ -280,7 +280,7 @@ trait ParserCommon { } def parseNumeral: SNumeral = { - nextToken match { + nextToken() match { case t@Tokens.NumeralLit(n) => { val num = SNumeral(n) num.setPos(t) @@ -290,7 +290,7 @@ trait ParserCommon { } def parseDecimal: SDecimal = { - nextToken match { + nextToken() match { case t@Tokens.DecimalLit(n) => { val dec = SDecimal(n) dec.setPos(t) @@ -300,7 +300,7 @@ trait ParserCommon { } def parseHexadecimal: SHexadecimal = { - nextToken match { + nextToken() match { case t@Tokens.HexadecimalLit(h) => { val hexa = SHexadecimal(h) hexa.setPos(t) @@ -310,7 +310,7 @@ trait ParserCommon { } def parseBinary: SBinary = { - nextToken match { + nextToken() match { case t@Tokens.BinaryLit(b) => { val bin = SBinary(b.toList) bin.setPos(t) @@ -319,7 +319,7 @@ trait ParserCommon { } } - def parseSList: SList = SList(parseMany(parseSExpr _).toList) + def parseSList: SList = SList(parseMany(() => parseSExpr).toList) /** * diff --git a/src/main/scala/smtlib/parser/ParserTerms.scala b/src/main/scala/smtlib/parser/ParserTerms.scala index cb336dc..2d26199 100644 --- a/src/main/scala/smtlib/parser/ParserTerms.scala +++ b/src/main/scala/smtlib/parser/ParserTerms.scala @@ -37,19 +37,19 @@ trait ParserTerms { this: ParserCommon => protected def parseTermWithoutParens(startPos: Position): Term = getPeekToken.kind match { case Tokens.Let => eat(Tokens.Let) - val (head, bindings) = parseOneOrMore(parseVarBinding _) + val (head, bindings) = parseOneOrMore(() => parseVarBinding) val term = parseTerm Let(head, bindings, term) case Tokens.Forall => eat(Tokens.Forall) - val (head, vars) = parseOneOrMore(parseSortedVar _) + val (head, vars) = parseOneOrMore(() => parseSortedVar) val term = parseTerm Forall(head, vars, term) case Tokens.Exists => eat(Tokens.Exists) - val (head, vars) = parseOneOrMore(parseSortedVar _) + val (head, vars) = parseOneOrMore(() => parseSortedVar) val term = parseTerm Exists(head, vars, term) @@ -57,7 +57,7 @@ trait ParserTerms { this: ParserCommon => eat(Tokens.ExclamationMark) val term = parseTerm val head = parseAttribute - val attrs = parseUntil(Tokens.CParen, eatEnd = false)(parseAttribute _) + val attrs = parseUntil(Tokens.CParen, eatEnd = false)(() => parseAttribute) AnnotatedTerm(term, head, attrs) case Tokens.As => @@ -69,7 +69,7 @@ trait ParserTerms { this: ParserCommon => case _ => //should be function application val id = parseQualifiedIdentifier val head = parseTerm - val terms = parseUntil(Tokens.CParen, eatEnd = false)(parseTerm _) + val terms = parseUntil(Tokens.CParen, eatEnd = false)(() => parseTerm) FunctionApplication(id, head::terms.toList) } diff --git a/src/main/scala/smtlib/theories/Constructors.scala b/src/main/scala/smtlib/theories/Constructors.scala index 1bacb9a..7fd41bb 100644 --- a/src/main/scala/smtlib/theories/Constructors.scala +++ b/src/main/scala/smtlib/theories/Constructors.scala @@ -75,7 +75,7 @@ object Constructors { } } - def or(t1: Term, t2: Term, ts: Term*): Term = and(t1 +: t2 +: ts) + def or(t1: Term, t2: Term, ts: Term*): Term = or(t1 +: t2 +: ts) def or(ts: Seq[Term]): Term = { val flat = ts.flatMap{ case Or(es@_*) => es diff --git a/src/main/scala/smtlib/trees/TreeTransformer.scala b/src/main/scala/smtlib/trees/TreeTransformer.scala index 184db17..2580455 100644 --- a/src/main/scala/smtlib/trees/TreeTransformer.scala +++ b/src/main/scala/smtlib/trees/TreeTransformer.scala @@ -328,13 +328,13 @@ abstract class SimpleTreeTransformer extends PrePostTreeTransformer { final def transform(term: Term): Term = transform(term, ())._1 final def transform(sort: Sort): Sort = transform(sort, ())._1 - override final def transform(id: Identifier, c: C): (Identifier, R) = transform(id, c) + override final def transform(id: Identifier, c: C): (Identifier, R) = super.transform(id, c) final def transform(id: Identifier): Identifier = transform(id, ())._1 - override final def transform(varBinding: VarBinding, c: C): (VarBinding, R) = transform(varBinding, c) + override final def transform(varBinding: VarBinding, c: C): (VarBinding, R) = super.transform(varBinding, c) final def transform(varBinding: VarBinding): VarBinding = transform(varBinding, ())._1 - override final def transform(sortedVar: SortedVar, c: C): (SortedVar, R) = transform(sortedVar, c) + override final def transform(sortedVar: SortedVar, c: C): (SortedVar, R) = super.transform(sortedVar, c) final def transform(sortedVar: SortedVar): SortedVar = transform(sortedVar, ())._1 } diff --git a/src/main/scala/smtlib/trees/Trees.scala b/src/main/scala/smtlib/trees/Trees.scala index 71b81da..bf7c547 100644 --- a/src/main/scala/smtlib/trees/Trees.scala +++ b/src/main/scala/smtlib/trees/Trees.scala @@ -113,7 +113,7 @@ object Terms { sealed trait Constant extends Term with AttributeValue /* - * Literal do not necessarly have an associated expected meaning (SNumeral as an + * Literal do not necessarily have an associated expected meaning (SNumeral as an * integer or SBinary as a 2-complement integer). They are just syntactic units, * and each local theory gives them a semantics. * diff --git a/src/test/scala/smtlib/common/BinaryTests.scala b/src/test/scala/smtlib/common/BinaryTests.scala index 78f1e29..8bc11f4 100644 --- a/src/test/scala/smtlib/common/BinaryTests.scala +++ b/src/test/scala/smtlib/common/BinaryTests.scala @@ -1,9 +1,9 @@ package smtlib package common -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class BinaryTests extends FunSuite { +class BinaryTests extends AnyFunSuite { test("toIntBits works with one bit") { assert(Binary(List(true)).toIntBits === 1) diff --git a/src/test/scala/smtlib/common/HexadecimalTests.scala b/src/test/scala/smtlib/common/HexadecimalTests.scala index 133e738..987716f 100644 --- a/src/test/scala/smtlib/common/HexadecimalTests.scala +++ b/src/test/scala/smtlib/common/HexadecimalTests.scala @@ -1,9 +1,9 @@ package smtlib package common -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class HexadecimalTests extends FunSuite { +class HexadecimalTests extends AnyFunSuite { test("Build hexadecimal with one digit string") { val zero = Hexadecimal.fromString("0") diff --git a/src/test/scala/smtlib/common/LinkedListTests.scala b/src/test/scala/smtlib/common/LinkedListTests.scala index 926434a..49476a7 100644 --- a/src/test/scala/smtlib/common/LinkedListTests.scala +++ b/src/test/scala/smtlib/common/LinkedListTests.scala @@ -1,8 +1,8 @@ package smtlib.common -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class LinkedListTests extends FunSuite { +class LinkedListTests extends AnyFunSuite { test("append one element on empty list pop the same element") { diff --git a/src/test/scala/smtlib/lexer/LexerTests.scala b/src/test/scala/smtlib/lexer/LexerTests.scala index af726eb..1b65bd7 100644 --- a/src/test/scala/smtlib/lexer/LexerTests.scala +++ b/src/test/scala/smtlib/lexer/LexerTests.scala @@ -8,12 +8,12 @@ import Lexer.IllegalTokenException import java.io.StringReader -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import org.scalatest.concurrent.TimeLimits import org.scalatest.time.SpanSugar._ -class LexerTests extends FunSuite with TimeLimits { +class LexerTests extends AnyFunSuite with TimeLimits { override def suiteName = "Lexer Test Suite" diff --git a/src/test/scala/smtlib/parser/CommandsParserTests.scala b/src/test/scala/smtlib/parser/CommandsParserTests.scala index e6ddd7a..aebafab 100644 --- a/src/test/scala/smtlib/parser/CommandsParserTests.scala +++ b/src/test/scala/smtlib/parser/CommandsParserTests.scala @@ -11,12 +11,12 @@ import trees.TreesOps import java.io.StringReader -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import org.scalatest.concurrent.TimeLimits import scala.language.implicitConversions -class CommandsParserTests extends FunSuite with TimeLimits { +class CommandsParserTests extends AnyFunSuite with TimeLimits { override def suiteName = "SMT-LIB commands Parser suite" diff --git a/src/test/scala/smtlib/parser/CommandsResponsesParserTests.scala b/src/test/scala/smtlib/parser/CommandsResponsesParserTests.scala index 0aef14d..c88f4cf 100644 --- a/src/test/scala/smtlib/parser/CommandsResponsesParserTests.scala +++ b/src/test/scala/smtlib/parser/CommandsResponsesParserTests.scala @@ -7,11 +7,11 @@ import trees.Commands._ import trees.CommandsResponses._ import trees.Terms._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import scala.language.implicitConversions -class CommandsResponsesParserTests extends FunSuite { +class CommandsResponsesParserTests extends AnyFunSuite { private implicit def strToSym(str: String): SSymbol = SSymbol(str) private implicit def strToId(str: String): Identifier = Identifier(SSymbol(str)) @@ -343,7 +343,7 @@ class CommandsResponsesParserTests extends FunSuite { /* * TODO: the standard requires at least one value, currently we return empty list */ - ignore("get-value response must contains at least one valuation pair") { + ignore("get-value response must contain at least one valuation pair") { intercept[UnexpectedTokenException] { Parser.fromString("()").parseGetValueResponse } diff --git a/src/test/scala/smtlib/parser/ParserTests.scala b/src/test/scala/smtlib/parser/ParserTests.scala index 7f543e2..b8cf1ed 100644 --- a/src/test/scala/smtlib/parser/ParserTests.scala +++ b/src/test/scala/smtlib/parser/ParserTests.scala @@ -11,13 +11,13 @@ import trees.TreesOps import java.io.StringReader -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import org.scalatest.concurrent.TimeLimits import org.scalatest.time.SpanSugar._ import scala.language.implicitConversions -class ParserTests extends FunSuite with TimeLimits { +class ParserTests extends AnyFunSuite with TimeLimits { override def suiteName = "SMT-LIB Parser suite" diff --git a/src/test/scala/smtlib/parser/TermsOpsTests.scala b/src/test/scala/smtlib/parser/TermsOpsTests.scala index 63b305b..d39b8b1 100644 --- a/src/test/scala/smtlib/parser/TermsOpsTests.scala +++ b/src/test/scala/smtlib/parser/TermsOpsTests.scala @@ -1,12 +1,12 @@ package smtlib package trees -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import Terms._ import TermsOps._ -class TermsOpsTests extends FunSuite { +class TermsOpsTests extends AnyFunSuite { val s1 = Sort(Identifier(SSymbol("S1"))) val s2 = Sort(Identifier(SSymbol("S2"))) diff --git a/src/test/scala/smtlib/parser/TreesOpsTests.scala b/src/test/scala/smtlib/parser/TreesOpsTests.scala index 7b699f1..5677cc9 100644 --- a/src/test/scala/smtlib/parser/TreesOpsTests.scala +++ b/src/test/scala/smtlib/parser/TreesOpsTests.scala @@ -1,13 +1,13 @@ package smtlib package trees -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import Terms._ import Commands._ import TreesOps._ -class TreesOpsTests extends FunSuite { +class TreesOpsTests extends AnyFunSuite { val s1 = Sort(Identifier(SSymbol("S1"))) val s2 = Sort(Identifier(SSymbol("S2"))) diff --git a/src/test/scala/smtlib/printer/PrinterTests.scala b/src/test/scala/smtlib/printer/PrinterTests.scala index ffd031a..24813de 100644 --- a/src/test/scala/smtlib/printer/PrinterTests.scala +++ b/src/test/scala/smtlib/printer/PrinterTests.scala @@ -8,12 +8,12 @@ import parser.Parser import common._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite import scala.language.implicitConversions import scala.annotation.tailrec -class PrinterTests extends FunSuite { +class PrinterTests extends AnyFunSuite { /* * TODO: test the requirement from the standard: diff --git a/src/test/scala/smtlib/theories/ArraysExTests.scala b/src/test/scala/smtlib/theories/ArraysExTests.scala index 14b9fdd..5795b23 100644 --- a/src/test/scala/smtlib/theories/ArraysExTests.scala +++ b/src/test/scala/smtlib/theories/ArraysExTests.scala @@ -5,9 +5,9 @@ import trees.Terms._ import ArraysEx._ import Ints.{IntSort, NumeralLit} -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class ArraysExTests extends FunSuite { +class ArraysExTests extends AnyFunSuite { override def suiteName = "ArraysEx Theory test suite" diff --git a/src/test/scala/smtlib/theories/CoreTests.scala b/src/test/scala/smtlib/theories/CoreTests.scala index ca57e44..8de25a3 100644 --- a/src/test/scala/smtlib/theories/CoreTests.scala +++ b/src/test/scala/smtlib/theories/CoreTests.scala @@ -4,9 +4,9 @@ package theories import trees.Terms._ import Core._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class CoreTests extends FunSuite { +class CoreTests extends AnyFunSuite { override def suiteName = "Core Theory test suite" diff --git a/src/test/scala/smtlib/theories/FixedSizeBitVectorsTests.scala b/src/test/scala/smtlib/theories/FixedSizeBitVectorsTests.scala index a147575..296649c 100644 --- a/src/test/scala/smtlib/theories/FixedSizeBitVectorsTests.scala +++ b/src/test/scala/smtlib/theories/FixedSizeBitVectorsTests.scala @@ -4,9 +4,9 @@ package theories import FixedSizeBitVectors._ import parser.Parser -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class FixedSizeBitVectorsTests extends FunSuite { +class FixedSizeBitVectorsTests extends AnyFunSuite { override def suiteName = "Bit Vector theory test suite" diff --git a/src/test/scala/smtlib/theories/IntsTests.scala b/src/test/scala/smtlib/theories/IntsTests.scala index 912a34f..66427af 100644 --- a/src/test/scala/smtlib/theories/IntsTests.scala +++ b/src/test/scala/smtlib/theories/IntsTests.scala @@ -3,9 +3,9 @@ package theories import Ints._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class IntsTests extends FunSuite { +class IntsTests extends AnyFunSuite { override def suiteName = "Ints theory test suite" diff --git a/src/test/scala/smtlib/theories/RealsTests.scala b/src/test/scala/smtlib/theories/RealsTests.scala index 2a33ac8..3ef4a07 100644 --- a/src/test/scala/smtlib/theories/RealsTests.scala +++ b/src/test/scala/smtlib/theories/RealsTests.scala @@ -3,9 +3,9 @@ package theories import Reals._ -import org.scalatest.FunSuite +import org.scalatest.funsuite.AnyFunSuite -class RealsTests extends FunSuite { +class RealsTests extends AnyFunSuite { override def suiteName = "Reals theory test suite" diff --git a/src/test/scala/smtlib/theories/experimental/SetsTests.scala b/src/test/scala/smtlib/theories/experimental/SetsTests.scala index d02dd28..ccf1d5a 100644 --- a/src/test/scala/smtlib/theories/experimental/SetsTests.scala +++ b/src/test/scala/smtlib/theories/experimental/SetsTests.scala @@ -7,9 +7,9 @@ import trees.Terms._ import Sets._ import Ints.{IntSort, NumeralLit} -import org.scalatest.{FunSuite, Matchers} +import org.scalatest.funsuite.AnyFunSuite -class SetsTests extends FunSuite with Matchers { +class SetsTests extends AnyFunSuite { override def suiteName = "Set theory test suite" diff --git a/src/test/scala/smtlib/theories/experimental/StringsTests.scala b/src/test/scala/smtlib/theories/experimental/StringsTests.scala index 0694d46..aedc850 100644 --- a/src/test/scala/smtlib/theories/experimental/StringsTests.scala +++ b/src/test/scala/smtlib/theories/experimental/StringsTests.scala @@ -7,9 +7,10 @@ import trees.Terms._ import Strings._ import Ints.NumeralLit -import org.scalatest.{FunSuite, Matchers} +import org.scalatest.funsuite.AnyFunSuite +import org.scalatest.matchers.should.Matchers -class StringsTests extends FunSuite with Matchers { +class StringsTests extends AnyFunSuite with Matchers { override def suiteName = "Strings theory test suite"