diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-28 15:46:13 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-28 15:46:20 -0500 |
| commit | a23c5715ce7cd279d83e75b232fd24b5c53032ba (patch) | |
| tree | d61ea9030f7d50995942d77e912a07c656d6807a /src/theory/quantifiers/full_model_check.h | |
| parent | 3355cd887a424ace6bc7b51e63f8adc90d24e3a9 (diff) | |
More bug fixes for interval models.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 2cb2198ef..8ebef640c 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -130,6 +130,8 @@ public: FullModelChecker( context::Context* c, QuantifiersEngine* qe );
~FullModelChecker(){}
+ bool optBuildAtFullModel();
+
int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
|