diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-10 15:53:51 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-10 15:53:51 +0100 |
| commit | be316870ef337a435d65f46a26f40ef0eab97934 (patch) | |
| tree | 24db24b777180ea71d0e9078b7bcf4eff05ae9dc /src/theory/quantifiers/term_database.h | |
| parent | 8a43f6c6aa01f9b27434caf1c5dd9ef6b2dcd963 (diff) | |
Do not eliminate variables only occurring in patterns. Minor improvements to sort inference. Remove unused code.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e40635d4e..1d3757d65 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -170,16 +170,6 @@ public: TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); -public: - /** parent structure (for efficient E-matching): - n -> op -> index -> L - map from node "n" to a list of nodes "L", where each node n' in L - has operator "op", and n'["index"] = n. - for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... } - */ - /* Todo replace int by size_t */ - std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; - const std::vector<Node> & getParents(TNode n, TNode f, int arg); //for model basis private: |