diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
| -rw-r--r-- | src/theory/quantifiers/model_builder.h | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 2dc561074..73e2937ab 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -60,13 +60,11 @@ public: class TermArgBasisTrie { -private: - bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); public: /** the data */ std::map< Node, TermArgBasisTrie > d_data; -public: - bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); } + /** add term to the trie */ + bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0); };/* class TermArgBasisTrie */ /** model builder class @@ -93,7 +91,7 @@ protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; //initialize quantifiers, return number of lemmas produced - virtual int initializeQuantifier( Node f, Node fp ); + virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm); //analyze model virtual void analyzeModel( FirstOrderModel* fm ); //analyze quantifiers |