diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 12:13:13 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 12:13:23 -0600 |
| commit | 93f084750d8a76d63fc74d242944bce0635c2194 (patch) | |
| tree | 8b781cf252fb78e16158e307de973e61f6f331eb /src/theory/quantifiers/full_model_check.h | |
| parent | 9846e1db91243c3b507300dad318e81e28f9d4f4 (diff) | |
Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.h')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 606392831..db5abb01e 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,7 +92,6 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; 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); @@ -138,7 +137,6 @@ public: 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); void debugPrint(const char * tr, Node n, bool dispStar = false); |