From 06ca7e3709fefbbec5d20f9c99e4a630a391dc28 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 2 Jan 2018 18:17:06 -0800 Subject: [PATCH] Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463) --- src/theory/quantifiers/bv_inverter.cpp | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 8068b563e..67ce8d217 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -517,20 +517,16 @@ static Node getScBvUrem(bool pol, /* s % x < t * with side condition: * (and - * (=> (= s z) (bvsle t z)) - * (=> (bvsgt s z) (bvsge s t)) + * (=> (bvsge s z) (bvsge s t)) * (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t))) * where z = 0 with getSize(z) = w */ Node i1 = nm->mkNode(IMPLIES, - s.eqNode(z), nm->mkNode(BITVECTOR_SLE, t, z)); + nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGE, s, t)); Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, s, t)); - Node i3 = nm->mkNode(IMPLIES, nm->mkNode(AND, nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, t, z)), nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t)); - scl = nm->mkNode(AND, i1, i2, i3); - return Node::null(); + scl = nm->mkNode(AND, i1, i2); } } } -- 2.30.2