diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
| commit | 304404e3709ff7e95156c87f65a3e2647d9f3441 (patch) | |
| tree | 10fd1c4cc42567c3fac5fd91ad76aef3d49975b5 /src/theory/quantifiers/model_builder.h | |
| parent | 697dd317af39a896865c99b922e80baac2bb4b23 (diff) | |
more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
| -rw-r--r-- | src/theory/quantifiers/model_builder.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index e2f422a0a..7c720d604 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -95,6 +95,9 @@ public: bool d_considerAxioms; // set effort void setEffort( int effort ); +protected: //helper functions + /** term has constant definition */ + bool hasConstantDefinition( Node n ); public: //options virtual bool optUseModel(); @@ -177,6 +180,8 @@ protected: private: //get selection formula for quantifier body Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption ); + //get a heuristic score for a selection formula + int getSelectionFormulaScore( Node fn ); //set selected terms in term void setSelectedTerms( Node s ); //is usable selection literal |