diff options
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); |