Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b9ce2063a..92296ebac 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -101,6 +101,7 @@ namespace quantifiers {
   class InstStrategyCbqi;
   class InstStrategyCegqi;
   class QuantDSplit;
+  class QuantAntiSkolem;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -162,6 +163,8 @@ private:
   quantifiers::InstStrategyCbqi * d_i_cbqi;
   /** quantifiers splitting */
   quantifiers::QuantDSplit * d_qsplit;
+  /** quantifiers anti-skolemization */
+  quantifiers::QuantAntiSkolem * d_anti_skolem;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -260,6 +263,8 @@ public:  //modules
   quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
   /** get quantifiers splitting */
   quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
+  /** get quantifiers anti-skolemization */
+  quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;