support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)

1 files changed, 16 insertions, 5 deletions

diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index d93070481..b1fbb3e68 100755
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -31,17 +31,28 @@ namespace quantifiers {
 class QuantifierMacros{

 private:

   void process( Node n, bool pol, std::vector< Node >& args, Node f );

-  bool containsOp( Node n, Node op );

-  bool isMacroKind( Node n, bool pol );

-  //map from operators to macro definition ( basis, definition )

-  std::map< Node, std::pair< Node, Node > > d_macro_defs;

+  bool contains( Node n, Node n_s );

+  bool containsBadOp( Node n, Node n_op );

+  bool isMacroLiteral( Node n, bool pol );

+  void getMacroCandidates( Node n, std::vector< Node >& candidates );

+  Node solveInEquality( Node n, Node lit );

+  bool isConsistentDefinition( Node op, Node cond, Node def );

+  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );

+  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

+  std::map< Node, std::vector< Node > > d_macro_basis;

+  //map from operators to map from conditions to definition cases

+  std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases;

+  //map from operators to macro definition

+  std::map< Node, Node > d_macro_defs;

 private:

   Node simplify( Node n );

 public:

   QuantifierMacros(){}

   ~QuantifierMacros(){}

 

-  void simplify( std::vector< Node >& assertions, bool doRewrite = false );

+  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );

 };

 

 }