diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-12-06 04:45:06 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-06 06:45:06 -0600 |
| commit | 6a37fd136eea6ad95aae4e598faee0d47c110343 (patch) | |
| tree | fb6d016a14cded96e6b05d988f3c7856100dc71b /src/theory/quantifiers/conjecture_generator.h | |
| parent | 108b5ed9d1f66884af7ede96155670bb1dc2fb43 (diff) | |
Remove CDChunkList (#1414)
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index a67530556..fa74795c3 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -18,7 +18,6 @@ #define CONJECTURE_GENERATOR_H #include "context/cdhashmap.h" -#include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" #include "theory/type_enumerator.h" @@ -229,7 +228,6 @@ class ConjectureGenerator : public QuantifiersModule friend class SubsEqcIndex; friend class TermGenerator; friend class TermGenEnv; - typedef context::CDChunkList<Node> NodeList; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; //this class maintains a congruence closure for *universal* facts |