Skip to content
Snippets Groups Projects
Commit 454b6dc4 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Fix functionsAvailable, add enum solver

parent c5ba0f22
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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
}
......@@ -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) {
......
......@@ -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)
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment