From 8816abc7357ac5a086c5b7ed8e11c94b6d4a1520 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 19 Aug 2015 13:50:22 +0200
Subject: [PATCH] Improvements
---
.../scala/leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
.../leon/synthesis/rules/IntegerInequalities.scala | 2 +-
src/main/scala/leon/utils/ModelEnumerator.scala | 13 +++++++------
3 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index cd49ece38..5f23fade2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -354,7 +354,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case more =>
val es = freshSym("e")
SMTLet(VarBinding(es, toSMT(e)), Seq(),
- Core.Or((oneOf map (FunctionApplication(_, Seq(es:Term)))): _*)
+ Core.Or(oneOf.map(FunctionApplication(_, Seq(es:Term))): _*)
)
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 9bd49fceb..0c7c8a961 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -33,7 +33,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
- val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains)
+ val candidateVars = ineqVars.intersect(problem.xs.toSet).diff(nonIneqVars)
val processedVars: Set[(Identifier, Int)] = candidateVars.flatMap(v => {
try {
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index e813d8b50..2467a9021 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -51,11 +51,11 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
s.check == Some(true)
}
- def next = {
+ def next() = {
val sm = s.getModel
- val model = (ids.map { id =>
+ val model = ids.map { id =>
id -> sm.getOrElse(id, simplestValue(id.getType))
- }).toMap
+ }.toMap
// Vary the model
@@ -131,7 +131,8 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
Stream.empty
} else {
// Assert a new pivot point
- val thisTry = getPivot().map { t =>
+ val thisTry = getPivot()
+ thisTry.foreach { t =>
s.push()
dir match {
case Up =>
@@ -145,9 +146,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
s.check match {
case Some(true) =>
val sm = s.getModel
- val m = (ids.map { id =>
+ val m = ids.map { id =>
id -> sm.getOrElse(id, simplestValue(id.getType))
- }).toMap
+ }.toMap
evaluator.eval(measure, m).result match {
case Some(InfiniteIntegerLiteral(measureVal)) =>
--
GitLab