diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2017-10-02 12:35:28 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-02 12:35:28 -0700 |
commit | fad765a539f8732461340980477ffe3f8c672fb2 (patch) | |
tree | b8c3de43c5ac7d196b85085323ea7ba43f15a030 /src/theory/quantifiers/bv_inverter.h | |
parent | f1c7be3a9b96f1a949f127344ecc775680da2c8e (diff) |
Address comments from PR #1164. (#1174)
Make eliminateSkolemFunctions(...) iterative and some more minor fixes.
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.h')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index ca6c97f83..724b3b7a7 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -42,7 +42,7 @@ class BvInverterStatus { BvInverterStatus() : d_status(0) {} ~BvInverterStatus() {} int d_status; - // TODO : may not need this (conditions are now appear explicitly in solved + // TODO : may not need this (conditions now appear explicitly in solved // forms) side conditions std::vector<Node> d_conds; }; @@ -111,11 +111,6 @@ class BvInverter { Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path, std::unordered_set<TNode, TNodeHashFunction>& visited); - /** helper function for eliminateSkolemFunctions */ - Node eliminateSkolemFunctions( - TNode n, std::vector<Node>& side_conditions, - std::unordered_map<TNode, Node, TNodeHashFunction>& visited); - // is operator k invertible? bool isInvertible(Kind k); |