diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
commit | 2bf0735176e0ff5fb9720bfb255ca22443584dcc (patch) | |
tree | 16926686e86f182e383efd8153b7d0e11bbc694a /src/theory/quantifiers/full_model_check.h | |
parent | b48a369333f077fa7cce117976f760cd6332691a (diff) |
Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
-rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 92c866ffd..00a910567 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -65,8 +65,8 @@ public: d_has_simplified = false;
}
bool addEntry( FullModelChecker * m, Node c, Node v);
- Node evaluate( FullModelChecker * m, std::vector<Node> inst );
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+ Node evaluate( FullModelChecker * m, std::vector<Node>& inst );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );
void simplify( FullModelChecker * m );
void debugPrint(const char * tr, Node op, FullModelChecker * m);
};
@@ -141,6 +141,8 @@ public: /** process build model */
void processBuildModel(TheoryModel* m, bool fullModel);
+ /** get current model value */
+ Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
};
}
|