diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-02 18:17:06 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-02 18:17:06 -0800 |
commit | 06ca7e3709fefbbec5d20f9c99e4a630a391dc28 (patch) | |
tree | 5a3f4891b4d55654892601ce9c6e3ed4cf84ce95 /src | |
parent | f8f8103229a9b84e944148985ebb05abed814619 (diff) |
Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 10 |
1 files 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); } } } |