diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-22 14:29:28 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-22 14:29:38 -0500 |
| commit | bdb5789713c03cf16f0ce6178b2fdc66f96ddc9e (patch) | |
| tree | d898e2b126b425641342626a625bb8d470985f1b /src/theory/quantifiers/full_model_check.h | |
| parent | 41c6b7593504671873b25040d806ad1e50c37093 (diff) | |
Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 8ebef640c..fb810c355 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -90,6 +90,7 @@ protected: std::map< Node, Node > d_array_term_cond;
std::map<Node, std::map< Node, int > > d_quant_var_id;
std::map<Node, std::vector< int > > d_star_insts;
+ void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
protected:
|