Optimizations for datatypes: check for clashes modulo equality. Avoid building model at fullModel=false when possible. Minor cleanup.

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 62bd347c7..8a0d956ac 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -116,7 +116,7 @@ public:
 class QuantInfo {

 private:

   void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );

-  void flatten( Node n, bool beneathQuant );
+  void flatten( Node n, bool beneathQuant );

 private: //for completing match

   std::vector< int > d_unassigned;

   std::vector< TypeNode > d_unassigned_tn;

@@ -156,8 +156,8 @@ public:
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );

   void revertMatch( std::vector< int >& assigned );

   void debugPrintMatch( const char * c );

-  bool isConstrainedVar( int v );
-public:
+  bool isConstrainedVar( int v );

+public:

   void getMatch( std::vector< Node >& terms );

 };

 

@@ -274,6 +274,8 @@ public:
     ~Statistics();

   };

   Statistics d_statistics;

+  /** Identify this module */

+  std::string identify() const { return "QcfEngine"; }

 };

 

 }