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 /src/theory/quantifiers/bv_inverter.cpp | |
parent | 17820d7e0606b19e22dc082b2f438b323ac49ff8 (diff) |
Remove BITVECTOR_SUB from isInvertible(). (#1513)
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-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 |