Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c9a3a8027..101aa43cd 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -94,6 +94,7 @@ namespace quantifiers {
   class LtePartialInst;
   class AlphaEquivalence;
   class FunDefEngine;
+  class QuantEqualityEngine;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -145,6 +146,8 @@ private:
   quantifiers::LtePartialInst * d_lte_part_inst;
   /** function definitions engine */
   quantifiers::FunDefEngine * d_fun_def_engine;
+  /** quantifiers equality engine */
+  quantifiers::QuantEqualityEngine * d_uee;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -233,6 +236,8 @@ public:  //modules
   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
   /** function definition engine */
   quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
+  /** quantifiers equality engine */
+  quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;