summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/full_model_check.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
-rwxr-xr-xsrc/theory/quantifiers/full_model_check.h1
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback