More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.

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