diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-13 22:12:27 -0800 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-01-13 22:12:27 -0800 |
| commit | a7dc71b4344cc0573997fcb4134ebf242f59bd7e (patch) | |
| tree | 0e03bb9f56d9c6d24ec81422e303ef4e061da510 | |
| parent | 17820d7e0606b19e22dc082b2f438b323ac49ff8 (diff) | |
Remove BITVECTOR_SUB from isInvertible(). (#1513)
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index a96f05a35..ec88f229e 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -78,8 +78,7 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) } } } - // TODO : compute the value if the condition is deterministic, e.g. calc - // multiplicative inverse of 2 constants + if (c.isNull()) { NodeManager* nm = NodeManager::currentNM(); @@ -117,7 +116,6 @@ static bool isInvertible(Kind k, unsigned index) || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND || k == BITVECTOR_PLUS - || k == BITVECTOR_SUB || k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL |