From 4dec9ec917d8dea194ad48d4d3b23d19f1c6d3b8 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 6 Jan 2015 16:08:20 +0100
Subject: [PATCH] Add (in)equalities in ExpressionGrammars
---
.../leon/synthesis/utils/ExpressionGrammar.scala | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 46bffd958..55550d59f 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -73,7 +73,11 @@ object ExpressionGrammars {
Generator(Nil, { _ => BooleanLiteral(false) }),
Generator(List(BooleanType), { case Seq(a) => Not(a) }),
Generator(List(BooleanType, BooleanType), { case Seq(a, b) => And(a, b) }),
- Generator(List(BooleanType, BooleanType), { case Seq(a, b) => LeonOr(a, b) })
+ Generator(List(BooleanType, BooleanType), { case Seq(a, b) => LeonOr(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessThan(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessEquals(a, b) }),
+ Generator(List(Int32Type, Int32Type ), { case Seq(a, b) => Equals(a, b) }),
+ Generator(List(BooleanType, BooleanType), { case Seq(a, b) => Equals(a, b) })
)
case Int32Type =>
List(
@@ -109,6 +113,9 @@ object ExpressionGrammars {
Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
)
+ case UnitType =>
+ List( Generator(Nil, { case _ => UnitLiteral() }) )
+
case _ =>
Nil
}
@@ -150,6 +157,9 @@ object ExpressionGrammars {
Generator(List(base), { case elems => FiniteSet(elems.toSet).setType(st) }),
Generator(List(base, base), { case elems => FiniteSet(elems.toSet).setType(st) })
)
+
+ case UnitType =>
+ List( Generator(Nil, { case _ => UnitLiteral() }) )
case _ =>
Nil
--
GitLab