diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-27 18:17:27 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-27 18:17:27 +0100 |
| commit | 3d82de01011931ee352715ac4f45c7bbc66f2201 (patch) | |
| tree | 27009ced9e0af2cc1706053ffed6913ac7344447 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | b2334221c88ba8ae6adbd27b0802aa2b02641378 (diff) | |
Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simplify option names.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index badf97c46..7c57c6d60 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -26,10 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// attribute for "contains instantiation constants from" -struct NestedQuantAttributeId {}; -typedef expr::Attribute<NestedQuantAttributeId, Node> NestedQuantAttribute; - class QuantifiersRewriter { public: static bool isClause( Node n ); @@ -43,14 +39,11 @@ private: static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static bool hasArg( std::vector< Node >& args, Node n ); static bool hasArg1( Node a, Node n ); - static void setNestedQuantifiers( Node n, Node q ); - static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); - static void setAttributes( Node in, Node n ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); - static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); + static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); + static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); static Node computeProcessIte( Node body, bool hasPol, bool pol ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); |