diff --git a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala index d8657e9d422db1762a19a6ec38d69bb9e8a73192..602873aba9df1859650ee94486c59d9487ec7fbd 100644 --- a/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala +++ b/src/main/scala/leon/solvers/combinators/Z3StringCapableSolver.scala @@ -24,7 +24,7 @@ import leon.utils.Bijection import leon.solvers.z3.StringEcoSystem object Z3StringCapableSolver { - def convert(p: Program): (Program, Option[Z3StringConversion]) = { + def convert(p: Program, force: Boolean = false): (Program, Option[Z3StringConversion]) = { val converter = new Z3StringConversion(p) import converter.Forward._ var globalFdMap = Map[FunDef, (Map[Identifier, Identifier], FunDef)]() @@ -46,7 +46,7 @@ object Z3StringCapableSolver { } else None ) }) - if(!hasStrings) { + if(!hasStrings && !force) { (p, None) } else { converter.globalFdMap ++= globalFdMap.view.map(kv => (kv._1, kv._2._2)) @@ -58,11 +58,17 @@ object Z3StringCapableSolver { } } } +trait ForcedProgramConversion { self: Z3StringCapableSolver[_] => + override def convertProgram(p: Program): (Program, Option[Z3StringConversion]) = { + Z3StringCapableSolver.convert(p, true) + } +} abstract class Z3StringCapableSolver[+TUnderlying <: Solver](val context: LeonContext, val program: Program, val underlyingConstructor: (Program, Option[Z3StringConversion]) => TUnderlying) extends Solver { - protected val (new_program, someConverter) = Z3StringCapableSolver.convert(program) + def convertProgram(p: Program): (Program, Option[Z3StringConversion]) = Z3StringCapableSolver.convert(p) + protected val (new_program, someConverter) = convertProgram(program) val underlying = underlyingConstructor(new_program, someConverter) @@ -71,6 +77,7 @@ extends Solver { someConverter match { case None => model case Some(converter) => + println("Conversion") val ids = model.ids.toSeq val exprs = ids.map(model.apply) import converter.Backward._ @@ -86,21 +93,17 @@ extends Solver { // Members declared in leon.solvers.Solver def assertCnstr(expression: Expr): Unit = { - someConverter match { - case None => underlying.assertCnstr(expression) - case Some(converter) => - import converter.Forward._ - val newExpression = convertExpr(expression)(Map()) - underlying.assertCnstr(newExpression) - } + someConverter.map{converter => + import converter.Forward._ + val newExpression = convertExpr(expression)(Map()) + underlying.assertCnstr(newExpression) + }.getOrElse(underlying.assertCnstr(expression)) } def getUnsatCore: Set[Expr] = { - someConverter match { - case None => underlying.getUnsatCore - case Some(converter) => - import converter.Backward._ - underlying.getUnsatCore map (e => convertExpr(e)(Map())) - } + someConverter.map{converter => + import converter.Backward._ + underlying.getUnsatCore map (e => convertExpr(e)(Map())) + }.getOrElse(underlying.getUnsatCore) } def check: Option[Boolean] = underlying.check def free(): Unit = underlying.free() @@ -127,26 +130,24 @@ trait Z3StringQuantificationSolver[TUnderlying <: QuantificationSolver] extends // Members declared in leon.solvers.QuantificationSolver override def getModel: leon.solvers.HenkinModel = { val model = underlying.getModel - someConverter match { - case None => model - case Some(converter) => - val ids = model.ids.toSeq - val exprs = ids.map(model.apply) - import converter.Backward._ - val original_ids = ids.map(convertId) - val original_exprs = exprs.map{ case e => convertExpr(e)(Map()) } - - val new_domain = new HenkinDomains( - model.doms.lambdas.map(kv => - (convertExpr(kv._1)(Map()).asInstanceOf[Lambda], - kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap, - model.doms.tpes.map(kv => - (convertType(kv._1), - kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap - ) - - new HenkinModel(original_ids.zip(original_exprs).toMap, new_domain) - } + someConverter map { converter => + val ids = model.ids.toSeq + val exprs = ids.map(model.apply) + import converter.Backward._ + val original_ids = ids.map(convertId) + val original_exprs = exprs.map{ case e => convertExpr(e)(Map()) } + + val new_domain = new HenkinDomains( + model.doms.lambdas.map(kv => + (convertExpr(kv._1)(Map()).asInstanceOf[Lambda], + kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap, + model.doms.tpes.map(kv => + (convertType(kv._1), + kv._2.map(e => e.map(e => convertExpr(e)(Map()))))).toMap + ) + + new HenkinModel(original_ids.zip(original_exprs).toMap, new_domain) + } getOrElse model } } diff --git a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala index 2a2b6e596937c53444860cd014dbcb8dc9b80541..21df018db70935ad63b6c22e7d6bc77894005b23 100644 --- a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala +++ b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala @@ -191,16 +191,18 @@ trait Z3StringConverters { self: Z3StringConversion => convertExpr(kv._2))), default.map(d => convertExpr(d)), convertType(tpe).asInstanceOf[FunctionType]) case Lambda(args, body) => + println("Converting Lambda :" + e) val new_bindings = scala.collection.mutable.ListBuffer[(Identifier, Identifier)]() - for(arg <- args) { + val new_args = for(arg <- args) yield { val in = arg.getType - if(convertType(in) ne in) { - new_bindings += (arg.id -> convertId(arg.id)) - } + val new_id = convertId(arg.id) + if(new_id ne arg.id) { + new_bindings += (arg.id -> new_id) + ValDef(new_id) + } else arg } - val new_args = new_bindings.map(x => ValDef(x._2)) - Lambda(new_args, - convertExpr(body)(bindings ++ new_bindings.map(t => (t._1, Variable(t._2))))).copiedFrom(e) + val res = Lambda(new_args, convertExpr(body)(bindings ++ new_bindings.map(t => (t._1, Variable(t._2))))).copiedFrom(e) + res case Let(a, expr, body) if isTypeToConvert(a.getType) => val new_a = convertId(a) val new_bindings = bindings + (a -> Variable(new_a)) diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala index 77169aa2b585b9453558bcf085800d28776d80c1..c5571fa4f9b2def4f33a586247aa7eb213483a10 100644 --- a/src/test/scala/leon/integration/solvers/SolversSuite.scala +++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala @@ -22,13 +22,13 @@ class SolversSuite extends LeonTestSuiteWithProgram { val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = { (if (SolverFactory.hasNativeZ3) Seq( - ("fairz3", (ctx: LeonContext, pgm: Program) => new Z3StringFairZ3Solver(ctx, pgm)) + ("fairz3", (ctx: LeonContext, pgm: Program) => new Z3StringFairZ3Solver(ctx, pgm) with ForcedProgramConversion ) ) else Nil) ++ (if (SolverFactory.hasZ3) Seq( - ("smt-z3", (ctx: LeonContext, pgm: Program) => new Z3StringUnrollingSolver(ctx, pgm, pgm => new SMTLIBZ3Solver(ctx, pgm))) + ("smt-z3", (ctx: LeonContext, pgm: Program) => new Z3StringUnrollingSolver(ctx, pgm, pgm => new SMTLIBZ3Solver(ctx, pgm)) with ForcedProgramConversion ) ) else Nil) ++ (if (SolverFactory.hasCVC4) Seq( - ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new Z3StringUnrollingSolver(ctx, pgm, pgm => new SMTLIBCVC4Solver(ctx, pgm))) + ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new Z3StringUnrollingSolver(ctx, pgm, pgm => new SMTLIBCVC4Solver(ctx, pgm)) with ForcedProgramConversion ) ) else Nil) } @@ -78,7 +78,7 @@ class SolversSuite extends LeonTestSuiteWithProgram { } } case _ => - fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!?") + fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!? Solver was "+solver.getClass) } } finally { solver.free()