diff options
author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-04-28 17:34:00 +0200 |
---|---|---|
committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-04-28 17:34:00 +0200 |
commit | 9b97c9144875e072da4098f102f8989be26e5cdf (patch) | |
tree | 2f95fbd431085345784a7b4e0c7c569d3a428db3 /src/theory/quantifiers/quant_conflict_find.h | |
parent | 698f5a09b1c0177abfd2eaa2b110de100fd108ef (diff) |
Optimizations for datatypes: check for clashes modulo equality. Avoid building model at fullModel=false when possible. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 8 |
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"; }
};
}
|