From b5f4f1285128eaae135a7326dd6f3aebba0ca5cb Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 May 2015 16:09:05 +0200
Subject: [PATCH] simpler encoding of division
---
.../leon/solvers/smtlib/SMTLIBSolver.scala | 25 +++----------------
1 file changed, 4 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 560141602..6866cc1b5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -639,27 +639,10 @@ abstract class SMTLIBSolver(val context: LeonContext,
val ar = toSMT(a)
val br = toSMT(b)
- val case1 = (
- Core.And(Ints.LessThan(ar, Ints.NumeralLit(0)), Ints.LessThan(br, Ints.NumeralLit(0))),
- Ints.Div(Ints.Neg(ar), Ints.Neg(br))
- )
- val case2 = (
- Core.And(Ints.LessThan(ar, Ints.NumeralLit(0)), Ints.GreaterEquals(br, Ints.NumeralLit(0))),
- Ints.Neg(Ints.Div(Ints.Neg(ar), br))
- )
- val case3 = (
- Core.And(Ints.GreaterEquals(ar, Ints.NumeralLit(0)), Ints.LessThan(br, Ints.NumeralLit(0))),
- Ints.Div(ar, br)
- )
- val case4 = (
- Core.And(Ints.GreaterEquals(ar, Ints.NumeralLit(0)), Ints.GreaterEquals(br, Ints.NumeralLit(0))),
- Ints.Div(ar, br)
- )
-
- Core.ITE(case1._1, case1._2,
- Core.ITE(case2._1, case2._2,
- Core.ITE(case3._1, case3._2,
- Core.ITE(case4._1, case4._2, Ints.NumeralLit(0)))))
+ Core.ITE(
+ Ints.GreaterEquals(ar, Ints.NumeralLit(0)),
+ Ints.Div(ar, br),
+ Ints.Neg(Ints.Div(Ints.Neg(ar), br)))
}
case Modulo(a,b) => {
val q = toSMT(Division(a, b))
--
GitLab