diff options
Diffstat (limited to 'src/theory/quantifiers/macros.h')
-rw-r--r-- | src/theory/quantifiers/macros.h | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 74fb0f47b..06e2d652a 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -23,6 +23,7 @@ #include <map> #include "expr/node.h" #include "expr/type_node.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -30,16 +31,18 @@ namespace quantifiers { class QuantifierMacros{ private: + QuantifiersEngine * d_qe; +private: bool d_ground_macros; bool processAssertion( Node n ); bool isBoundVarApplyUf( Node n ); bool process( Node n, bool pol, std::vector< Node >& args, Node f ); - bool contains( Node n, Node n_s ); - bool containsBadOp( Node n, Node op, std::vector< Node >& opc ); + bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ); bool isMacroLiteral( Node n, bool pol ); - void getMacroCandidates( Node n, std::vector< Node >& candidates ); + bool isGroundUfTerm( Node f, Node n ); + void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ); Node solveInEquality( Node n, Node lit ); - bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ); + bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ); bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); //map from operators to macro basis terms @@ -49,14 +52,15 @@ private: std::map< Node, Node > d_macro_defs_new; //operators to macro ops that contain them std::map< Node, std::vector< Node > > d_macro_def_contains; - //simplify cache + //simplify caches std::map< Node, Node > d_simplify_cache; + std::map< Node, bool > d_quant_macros; private: Node simplify( Node n ); void addMacro( Node op, Node n, std::vector< Node >& opc ); void debugMacroDefinition( Node oo, Node n ); public: - QuantifierMacros(){} + QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){} ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); |