From e0bb8a4606968c34ddf62dafcc922db5572e047a Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Tue, 22 Sep 2015 18:26:03 +0200 Subject: [PATCH] Fix quantifiedTerm to respect bindings --- .../leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 2 +- .../solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala | 2 +- .../scala/leon/solvers/smtlib/SMTLIBSolver.scala | 12 ++++++++---- .../solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala | 4 ++-- 4 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala index 1f0b760d7..281310a81 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala @@ -30,7 +30,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free override def assertCnstr(e: Expr) = try { - sendCommand(SMTAssert(quantifiedTerm(SMTExists, e))) + sendCommand(SMTAssert(quantifiedTerm(SMTExists, e)(Map()))) } catch { case _ : SolverUnsupportedError => addError() diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala index 232867dcc..382122cba 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala @@ -100,7 +100,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program application(post, Seq(tfd.applied)) ) try { - sendCommand(SMTAssert(quantifiedTerm(SMTForall, term))) + sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)(Map()))) } catch { case _ : SolverUnsupportedError => addError() diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala index aa18becd2..f82df1a3b 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala @@ -141,8 +141,10 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program) quantifier: (SortedVar, Seq[SortedVar], Term) => Term, vars: Seq[Identifier], body: Expr - ) : Term = { - if (vars.isEmpty) toSMT(body)(Map()) + )( + implicit bindings: Map[Identifier, Term] + ): Term = { + if (vars.isEmpty) toSMT(body) else { val sortedVars = vars map { id => SortedVar(id2sym(id), declareSort(id.getType)) @@ -150,13 +152,15 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program) quantifier( sortedVars.head, sortedVars.tail, - toSMT(body)(vars.map{ id => id -> (id2sym(id): Term)}.toMap) + toSMT(body)(bindings ++ vars.map{ id => id -> (id2sym(id): Term)}) ) } } // Returns a quantified term where all free variables in the body have been quantified - protected def quantifiedTerm(quantifier: (SortedVar, Seq[SortedVar], Term) => Term, body: Expr): Term = + protected def quantifiedTerm(quantifier: (SortedVar, Seq[SortedVar], Term) => Term, body: Expr)( + implicit bindings: Map[Identifier, Term] + ): Term = quantifiedTerm(quantifier, variablesOf(body).toSeq, body) protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match { diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala index 2ec571f1e..9a8e60e6b 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala @@ -47,7 +47,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) FunctionInvocation(tfd, tfd.params.map {_.toVariable}), tfd.body.get ) - ) + )(Map()) sendCommand(SMTAssert(term)) } @@ -62,7 +62,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) application(post, Seq(tfd.applied)) ) try { - sendCommand(SMTAssert(quantifiedTerm(SMTForall, term))) + sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)(Map()))) } catch { case _ : SolverUnsupportedError => addError() -- GitLab