From 9b97c9144875e072da4098f102f8989be26e5cdf Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 28 Apr 2014 17:34:00 +0200 Subject: Optimizations for datatypes: check for clashes modulo equality. Avoid building model at fullModel=false when possible. Minor cleanup. --- src/theory/quantifiers/quant_conflict_find.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.h') 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"; } }; } -- cgit v1.2.3