From 1b9c0d0c93402d08ba5a7f70cb25498b451a1669 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 11 May 2012 14:18:22 +0200
Subject: [PATCH] use reflection to load test generation and support nodefaults
option
---
src/main/scala/leon/Extensions.scala | 2 +-
src/main/scala/leon/TestGeneration.scala | 4 +++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 89cfe4492..e9fdde89c 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -99,7 +99,7 @@ object Extensions {
allLoaded = defaultExtensions ++ loaded
analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
- analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
+ //analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala
index 10ab5ef7b..0ca94eb2d 100644
--- a/src/main/scala/leon/TestGeneration.scala
+++ b/src/main/scala/leon/TestGeneration.scala
@@ -13,8 +13,10 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
def description: String = "Generate random testcases"
override def shortDescription: String = "test"
+ private val z3Solver = new FairZ3Solver(reporter)
def analyse(program: Program) {
+ z3Solver.setProgram(program)
reporter.info("Running test generation")
val allFuns = program.definedFunctions
allFuns.foreach(fd => {
@@ -37,7 +39,7 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
reporter.info("Now considering path condition: " + pathCond)
var testcase: Option[Map[Identifier, Expr]] = None
- val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
+ //val z3Solver: FairZ3Solver = loadedSolverExtensions.find(se => se.isInstanceOf[FairZ3Solver]).get.asInstanceOf[FairZ3Solver]
z3Solver.init()
z3Solver.restartZ3
--
GitLab