diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
| commit | 1c779966545190efa59b019572237562eea66dbf (patch) | |
| tree | f827fe0e4bcbbca8c84174f815948b3212391423 /src/theory/quantifiers/inst_match.h | |
| parent | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (diff) | |
more minor updates to inst gen and representative selection, clean up of equality query
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 43c0d26c7..41ebb63d2 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -55,13 +55,13 @@ public: /** is complete? */ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } /** make complete */ - //void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal: ensure that no term in d_map contains instantiation constants */ - //void makeInternal( QuantifiersEngine* qe ); + void makeComplete( Node f, QuantifiersEngine* qe ); + /** make internal representative */ + void makeInternalRepresentative( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** get value */ - Node getValue( Node var ); + Node getValue( Node var ) const; /** clear */ void clear(){ d_map.clear(); } /** is_empty */ |