diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 99d5abc48d07397fe35162d766e0d6d4a5094a35..f59087beed61b5cf9ca9c9b1eac46ce3a7cdcbb6 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -134,14 +134,30 @@ object SolverFactory {
// Fast solver used by simplifications, to discharge simple tautologies
def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
- if (hasNativeZ3) {
- SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
- } else {
- if (!reported) {
- ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
- reported = true
+ val names = ctx.findOptionOrDefault(SharedOptions.optSelectedSolvers)
+
+ if ((names contains "fairz3") && !hasNativeZ3) {
+ if (hasZ3) {
+ if (!reported) {
+ ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-z3.")
+ reported = true
+ }
+ SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ } else if (hasCVC4) {
+ if (!reported) {
+ ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-cvc4.")
+ reported = true
+ }
+ SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ } else {
+ ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
+ } else if(names contains "smt-cvc4") {
+ SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ } else if(names contains "smt-z3") {
SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ } else {
+ ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
}
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index b1b93568a1977fb43c14eb740295e44be114e916..55ad7cf6c705735946b0744af1973192955a840f 100644
--- a/src/main/scala/leon/solvers/string/StringSolver.scala
+++ b/src/main/scala/leon/solvers/string/StringSolver.scala
@@ -459,7 +459,7 @@ object StringSolver {
/** Solves the problem and returns all possible satisfying assignment */
def solve(p: Problem): Stream[Assignment] = {
val realProblem = forwardStrategy(p, Map())
- /*if(realProblem.nonEmpty) {
+ /*if(realProblem.nonEmpty && realProblem.get._1.nonEmpty) {
println("Problem:\n"+renderProblem(p))
println("Solutions:\n"+realProblem.get._2)
println("Real problem:\n"+renderProblem(realProblem.get._1))
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 3c02166e853535689b138fc7c17a789dc72d8de8..1aebc53d791e1a8d69ffbedf89293c6e6c8e980d 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -145,8 +145,10 @@ case object StringRender extends Rule("StringRender") {
}
gatherEquations(examples.valids.collect{ case io:InOutExample => io }.toList) match {
case Some(problem) =>
- hctx.reporter.ifDebug(printer => printer("Problem: ["+StringSolver.renderProblem(problem)+"]"))
- StringSolver.solve(problem)
+ hctx.reporter.debug("Problem: ["+StringSolver.renderProblem(problem)+"]")
+ val res = StringSolver.solve(problem)
+ hctx.reporter.debug("Solution found:"+res.nonEmpty)
+ res
case None =>
hctx.reporter.ifDebug(printer => printer("No problem found"))
Stream.empty
@@ -188,16 +190,22 @@ case object StringRender extends Rule("StringRender") {
object StringTemplateGenerator extends TypedTemplateGenerator(StringType)
- case class DependentType(caseClassParent: Option[TypeTree], typeToConvert: TypeTree)
+ case class DependentType(caseClassParent: Option[TypeTree], inputName: String, typeToConvert: TypeTree)
/** Creates an empty function definition for the dependent type */
def createEmptyFunDef(tpe: DependentType)(implicit hctx: SearchContext): FunDef = {
+ def defaultFunName(t: TypeTree) = t match {
+ case AbstractClassType(c, d) => c.id.asString(hctx.context)
+ case CaseClassType(c, d) => c.id.asString(hctx.context)
+ case t => t.asString(hctx.context)
+ }
+
val funName2 = tpe.caseClassParent match {
- case None => tpe.typeToConvert.asString(hctx.context) + "ToString"
- case Some(t) => tpe.typeToConvert.asString(hctx.context)+"In"+t.asString(hctx.context) + "ToString"
+ case None => defaultFunName(tpe.typeToConvert) + "_" + tpe.inputName + "_s"
+ case Some(t) => defaultFunName(tpe.typeToConvert) + "In"+defaultFunName(t) + "_" + tpe.inputName + "_s"
}
- val funName3 = funName2.replace("]","").replace("[","")
+ val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
val funName = funName3(0).toLower + funName3.substring(1)
val funId = FreshIdentifier(funName, alwaysShowUniqueID = true)
val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
@@ -226,12 +234,12 @@ case object StringRender extends Rule("StringRender") {
adtToString: Map[DependentType, (FunDef, Stream[Expr])],
inputs: Seq[Identifier])(implicit hctx: SearchContext): (Stream[Expr], Map[DependentType, (FunDef, Stream[Expr])]) = {
- def extractCaseVariants(caseClassParent: TypeTree, cct: CaseClassType, assignments2: Map[DependentType, (FunDef, Stream[Expr])]) = cct match {
+ def extractCaseVariants(cct: CaseClassType, assignments2: Map[DependentType, (FunDef, Stream[Expr])]) = cct match {
case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
val typeMap = tparams.zip(tparams2).toMap
val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd, typeMap).id )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
- val (rhs, assignments2tmp2) = createFunDefsTemplates(Some(caseClassParent), assignments2, fields) // Invoke functions for each of the fields.
+ val (rhs, assignments2tmp2) = createFunDefsTemplates(Some(cct), assignments2, fields) // Invoke functions for each of the fields.
val newCases = rhs.map(MatchCase(pattern, None, _))
(assignments2tmp2, newCases)
}
@@ -275,7 +283,7 @@ case object StringRender extends Rule("StringRender") {
result: ListBuffer[Stream[Expr]] = ListBuffer()): (List[Stream[Expr]], Map[DependentType, (FunDef, Stream[Expr])]) = inputs match {
case Nil => (result.toList, assignments1)
case input::q =>
- val dependentType = DependentType(currentCaseClassParent, input.getType)
+ val dependentType = DependentType(currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
assignments1.get(dependentType) match {
case Some(fd) =>
gatherInputs(currentCaseClassParent, assignments1, q, result += Stream(functionInvocation(fd._1, Seq(Variable(input)))))
@@ -307,7 +315,7 @@ case object StringRender extends Rule("StringRender") {
//TODO: Test other templates not only with Wilcard patterns, but more cases options for non-recursive classes (e.g. Option, Boolean, Finite parameterless case classes.)
val (assignments3, cases) = ((assignments2, ListBuffer[Stream[MatchCase]]()) /: act.knownCCDescendants) {
case ((assignments2, acc), cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2)) =>
- val (assignments2tmp2, newCases) = extractCaseVariants(t, cct, assignments2)
+ val (assignments2tmp2, newCases) = extractCaseVariants(cct, assignments2)
(assignments2tmp2, acc += newCases)
case ((adtToString, acc), e) => hctx.reporter.fatalError("Could not handle this class definition for string rendering " + e)
}
@@ -319,7 +327,7 @@ case object StringRender extends Rule("StringRender") {
val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
gatherInputs(currentCaseClassParent, assignments4, q, result += Stream(functionInvocation(fd, Seq(Variable(input)))))
case cct@CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) =>
- val (assignments3, newCases) = extractCaseVariants(t, cct, assignments2)
+ val (assignments3, newCases) = extractCaseVariants(cct, assignments2)
val allMatchExprs = newCases.map(acase => mergeMatchCases(fd)(Seq(acase)))
val assignments4 = assignments3 + (dependentType -> (fd, allMatchExprs))
gatherInputs(currentCaseClassParent, assignments4, q, result += Stream(functionInvocation(fd, Seq(Variable(input)))))
@@ -350,7 +358,7 @@ case object StringRender extends Rule("StringRender") {
}
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- hctx.reporter.debug("StringRender:Output variables="+p.xs+", their types="+p.xs.map(_.getType))
+ //hctx.reporter.debug("StringRender:Output variables="+p.xs+", their types="+p.xs.map(_.getType))
p.xs match {
case List(IsTyped(v, StringType)) =>
val description = "Creates a standard string conversion function"
@@ -365,9 +373,9 @@ case object StringRender extends Rule("StringRender") {
val (expr, funDefs) = createFunDefsTemplates(None, Map(), p.as)
val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
- t + "\n" + s.toString
+ t + "\n" + s._2._1.toString
))
- hctx.reporter.ifDebug(printer => printer("Inferred expression:\n" + expr + toDebug))
+ hctx.reporter.debug("Inferred expression:\n" + expr + toDebug)
findSolutions(examples, expr, funDefs.values.toSeq)
}
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 09a09ce4061045d9cd5fd17276206ffdff4b1188..521e98aa6eb35e28e820c4e0aea8ff11709643e1 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -17,7 +17,7 @@ object StreamUtils {
if(streams.isEmpty) Stream() else {
val (take, leave) = streams.splitAt(diag)
val (nonEmpty, empty) = take partition (_.nonEmpty)
- nonEmpty.map(_.head) ++ rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
+ nonEmpty.map(_.head) #::: rec(nonEmpty.map(_.tail) ++ leave, diag + 1 - empty.size)
}
}
rec(streams, 1)
@@ -27,7 +27,7 @@ object StreamUtils {
def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
if (streams.isEmpty) Stream() else {
val nonEmpty = streams filter (_.nonEmpty)
- nonEmpty.toStream.map(_.head) ++ interleave(nonEmpty.map(_.tail))
+ nonEmpty.toStream.map(_.head) #::: interleave(nonEmpty.map(_.tail))
}
}
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index 8d5530578d488ec2214367ac3f8817b7b4eb74e8..3045ea0dc4f407e78553ade6fd5a289b9780cbc3 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -184,8 +184,8 @@ class StringSolverSuite extends FunSuite with Matchers {
firstSolution(idMap("const8")) should equal("List(")
}
- /*test("solveJadProblem") {
- val lhs = """const26+const22+const7+const+const8+const3+const9+const5+"5"+const6+const10+const23+const18+const11+const+const12+const19+const18+const7+const1+const8+const2+const9+const4+const10+const19+const18+const13+const+const14+const3+const15+const5+"5"+const6+const16+const4+const17+const19+const18+const11+const1+const12+const19+const18+const13+const1+const14+const2+const15+const4+const16+const5+"5"+const6+const17+const19+const21+const20+const20+const20+const20+const20+const24+const27"""
+ test("solveJadProblem") {
+ val lhs = """const38+const34+const7+"T1"+const8+const3+const9+const5+"5"+const6+const10+const35+const30+const13+"T1"+const14+const31+const30+const7+"T2"+const8+const2+const9+const4+const10+const31+const30+const25+"T1"+const26+"Push"+const27+const20+"5"+const21+const28+const22+const29+const31+const30+const13+"T2"+const14+const31+const30+const25+"T2"+const26+"Pop"+const27+const19+const28+const23+"5"+const24+const29+const31+const33+const32+const32+const32+const32+const32+const36+const39=="T1: call Push(5)"""
implicit val idMap = MMap[String, Identifier]()
val lhsSf = makeSf(lhs)
@@ -200,5 +200,5 @@ T2: ret Pop() -> 5"""
println("Problem to solve:" + StringSolver.renderProblem(problem))
solve(problem) should not be 'empty
- }*/
+ }
}
\ No newline at end of file
diff --git a/testcases/stringrender/Example-Stack.scala b/testcases/stringrender/Example-Stack.scala
index bb9f64d1f83bf2f91a03a0c6fbf581f03083971b..b01dd6f268f70d167560e7a49bfc3b7cb56ea7fa 100644
--- a/testcases/stringrender/Example-Stack.scala
+++ b/testcases/stringrender/Example-Stack.scala
@@ -357,6 +357,18 @@ object AtomicStack {
}
}
+ def threadToStringSimple2(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
+ ???[String]
+ } ensuring {
+ res => (p, res) passes {
+ case Cons(RetEvent(T1(), Push(), Some(BigInt(5)), None()),
+ Cons(InternalEvent(T2()),
+ Cons(RetEvent(T2(), Pop(), None(), Some(BigInt(5))), Nil())))
+ =>
+ "T1: ret Push(5)\nT2: internal\nT2: ret Pop() -> 5"
+ }
+ }
+
/** This is THE method we want to render */
def threadToString(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {