Permalink
Browse files

BUGFIX: Fixed type-checking of Equals, LT and LE.

LT and LE are only allowed over (INT, INT) and (REAL, REAL), while
equals is allowed for ('a, 'a) except if `a is BOOL.
  • Loading branch information...
mikand authored and marcogario committed Oct 26, 2017
1 parent 9e6eec7 commit 770195c2cf60444006eee479f230394434da5e1f
Showing with 50 additions and 7 deletions.
  1. +2 −2 pysmt/test/test_formula.py
  2. +9 −1 pysmt/test/test_regressions.py
  3. +25 −1 pysmt/test/test_typechecker.py
  4. +14 −3 pysmt/type_checker.py
@@ -727,7 +727,7 @@ def test_infix(self):
x[1]
def test_infix_extended(self):
p, r, x, y = self.p, self.r, self.x, self.y
p, r, s, x, y = self.p, self.r, self.s, self.x, self.y
get_env().enable_infix_notation = True
self.assertEqual(Plus(p, Int(1)), p + 1)
@@ -772,7 +772,7 @@ def test_infix_extended(self):
x.Ite(1,2)
self.assertEqual(6 - r, Plus(Times(r, Real(-1)), Real(6)))
self.assertEqual(Not(Equals(x,y)), x.NotEquals(y))
self.assertEqual(Not(Equals(r,s)), r.NotEquals(s))
# BVs
# BV_CONSTANT: We use directly python numbers
@@ -29,7 +29,7 @@
from pysmt.test import (TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic,
skipIfNoQEForLogic)
from pysmt.test import main
from pysmt.exceptions import ConvertExpressionError, PysmtValueError
from pysmt.exceptions import ConvertExpressionError, PysmtValueError, PysmtTypeError
from pysmt.test.examples import get_example_formulae
from pysmt.environment import Environment
from pysmt.rewritings import cnf_as_set
@@ -470,6 +470,14 @@ def test_parse_bvconst_width(self):
const = expr.args()[0]
self.assertEqual(const.bv_width(), 8, const.bv_width())
def test_equality_typing(self):
x = Symbol('x', BOOL)
y = Symbol('y', BOOL)
with self.assertRaises(PysmtTypeError):
Equals(x, y)
with self.assertRaises(PysmtTypeError):
LE(x, y)
if __name__ == "__main__":
main()
@@ -15,7 +15,7 @@
# See the License for the specific language governing permissions and
# limitations under the License.
#
from pysmt.typing import REAL, BOOL, INT, FunctionType
from pysmt.typing import REAL, BOOL, INT, FunctionType, BV8
from pysmt.type_checker import (assert_no_boolean_in_args,
assert_boolean_args,
assert_same_type_args,
@@ -60,6 +60,30 @@ def test_boolean(self):
self.assertEqual(res, BOOL)
def test_arith_relations(self):
self.assertEqual(self.tc.walk(LE(self.p, self.q)), BOOL)
self.assertEqual(self.tc.walk(LT(self.p, self.q)), BOOL)
self.assertEqual(self.tc.walk(LE(self.r, self.s)), BOOL)
self.assertEqual(self.tc.walk(LT(self.r, self.s)), BOOL)
with self.assertRaises(PysmtTypeError):
LE(self.p, self.r)
with self.assertRaises(PysmtTypeError):
LT(self.p, self.r)
with self.assertRaises(PysmtTypeError):
LE(self.x, self.y)
with self.assertRaises(PysmtTypeError):
LT(self.x, self.y)
bv_a = Symbol("BV_A", BV8)
bv_b = Symbol("BV_B", BV8)
with self.assertRaises(PysmtTypeError):
LE(bv_a, bv_b)
with self.assertRaises(PysmtTypeError):
LT(bv_a, bv_b)
def test_functions(self):
vi = Symbol("At", INT)
vr = Symbol("Bt", REAL)
View
@@ -155,13 +155,24 @@ def walk_bv_extend(self, formula, args, **kwargs):
return None
return BVType(target_width)
@walkers.handles(op.EQUALS, op.LE, op.LT)
def walk_math_relation(self, formula, args, **kwargs):
def walk_equals(self, formula, args, **kwargs):
#pylint: disable=unused-argument
if args[0].is_bv_type():
if args[0].is_bool_type():
raise PysmtTypeError("The formula '%s' is not well-formed."
"Equality operator is not supported for Boolean"
" terms. Use Iff instead." \
% str(formula))
elif args[0].is_bv_type():
return self.walk_bv_to_bool(formula, args)
return self.walk_type_to_type(formula, args, args[0], BOOL)
@walkers.handles(op.LE, op.LT)
def walk_math_relation(self, formula, args, **kwargs):
#pylint: disable=unused-argument
if args[0].is_real_type():
return self.walk_type_to_type(formula, args, REAL, BOOL)
return self.walk_type_to_type(formula, args, INT, BOOL)
def walk_ite(self, formula, args, **kwargs):
assert formula is not None
if None in args: return None

0 comments on commit 770195c

Please sign in to comment.