From 454b6dc4208c604620798af5f18a3d54b337b234 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Aug 2016 12:01:28 +0200
Subject: [PATCH] Fix functionsAvailable, add enum solver
---
src/main/scala/inox/ast/Definitions.scala | 4 ++--
src/main/scala/inox/grammars/utils/Helpers.scala | 6 +-----
.../scala/inox/solvers/EnumerationSolver.scala | 1 -
src/main/scala/inox/solvers/SolverFactory.scala | 15 ++++++++++++++-
4 files changed, 17 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index 69f9b2269..fda6fb737 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -93,8 +93,8 @@ trait Definitions { self: Trees =>
with Constructors
with Paths { self0: Symbols =>
- protected[ast] val classes: Map[Identifier, ClassDef]
- protected[ast] val functions: Map[Identifier, FunDef]
+ val classes: Map[Identifier, ClassDef]
+ val functions: Map[Identifier, FunDef]
private[ast] val trees: self.type = self
protected val symbols: this.type = this
diff --git a/src/main/scala/inox/grammars/utils/Helpers.scala b/src/main/scala/inox/grammars/utils/Helpers.scala
index 2cc098131..24a689970 100644
--- a/src/main/scala/inox/grammars/utils/Helpers.scala
+++ b/src/main/scala/inox/grammars/utils/Helpers.scala
@@ -103,9 +103,5 @@ trait Helpers { self: GrammarsUniverse =>
* - all functions in main units
* - all functions imported, or methods of classes imported
*/
- def functionsAvailable(p: Program): Set[FunDef]// = {
- // visibleFunDefsFromMain(p)
- //}
-
-
+ def functionsAvailable(p: Program): Set[p.trees.FunDef] = p.symbols.functions.values.toSet
}
diff --git a/src/main/scala/inox/solvers/EnumerationSolver.scala b/src/main/scala/inox/solvers/EnumerationSolver.scala
index 1863547a8..51a7b7db0 100644
--- a/src/main/scala/inox/solvers/EnumerationSolver.scala
+++ b/src/main/scala/inox/solvers/EnumerationSolver.scala
@@ -59,7 +59,6 @@ trait EnumerationSolver extends Solver { self =>
val evaluator: DeterministicEvaluator { val program: self.program.type } = self.evaluator
val grammar: grammars.ExpressionGrammar = grammars.ValueGrammar
val program: self.program.type = self.program
- def functionsAvailable(p: Program): Set[FunDef] = Set()
})
if (interrupted) {
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 392898a05..1d6b48f41 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -3,6 +3,8 @@
package inox
package solvers
+import inox.grammars.GrammarsUniverse
+
trait SolverFactory {
val program: Program
@@ -38,7 +40,8 @@ object SolverFactory {
"nativez3" -> "Native Z3 with z3-templates for unrolling (default)",
"unrollz3" -> "Native Z3 with leon-templates for unrolling",
"smt-cvc4" -> "CVC4 through SMT-LIB",
- "smt-z3" -> "Z3 through SMT-LIB"
+ "smt-z3" -> "Z3 through SMT-LIB",
+ "enum" -> "Enumeration-based counter-example finder"
)
def getFromName(name: String)
@@ -88,6 +91,16 @@ object SolverFactory {
} with smtlib.Z3Solver
})
+ case "enum" => create(p)(name, () => new {
+ val program: p.type = p
+ val options = opts
+ } with EnumerationSolver with TimeoutSolver {
+ val evaluator = ev
+ val grammars: GrammarsUniverse {val program: p.type} = new GrammarsUniverse {
+ val program: p.type = p
+ }
+ })
+
case _ => throw FatalError("Unknown solver: " + name)
}
--
GitLab