diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-22 08:59:03 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-22 08:59:09 +0100 |
| commit | 48bc3c425947542ca1a337e08044c8f745600690 (patch) | |
| tree | cc08928a21cb4d8c81d2d8ab338a65fe7cca5128 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b (diff) | |
New trigger options. --inst-no-entail on by default. Misc cleanup.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 7c57c6d60..838eff57b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -79,8 +79,6 @@ public: static Node rewriteRewriteRule( Node r ); static bool containsQuantifiers(Node n); static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); -private: - static bool isDtStrInductionQuantifier( Node q ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ |