diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-17 21:29:57 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-17 21:29:57 +0000 |
commit | 21e0c5dd0de5edef8ec12f48b76887109b67db52 (patch) | |
tree | 61925a690688577e8cf96072a1afb75ede17f35d /src/theory/uf/theory_uf.h | |
parent | 2dadba52dd55084bbec52b3b338add5f8be77c13 (diff) |
Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r-- | src/theory/uf/theory_uf.h | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h new file mode 100644 index 000000000..06b0ee4f8 --- /dev/null +++ b/src/theory/uf/theory_uf.h @@ -0,0 +1,47 @@ + +#ifndef __CVC4__THEORY__THEORY_UF_H +#define __CVC4__THEORY__THEORY_UF_H + +#include "expr/node.h" +#include "theory/theory.h" +#include "theory/output_channel.h" +#include "context/context.h" +#include "theory/uf/ecdata.h" + +namespace CVC4 { +namespace theory { + +class TheoryUF : public Theory { +private: + context::Context* d_context; + context::CDList<Node> d_pending; + context::CDList<Node> d_disequality; + context::CDO<unsigned> d_currentPendingIdx; + +public: + void setup(const Node& n); + + void check(OutputChannel& out, Effort level= FULL_EFFORT); + + void propagate(OutputChannel& out, Effort level= FULL_EFFORT){} + + void explain(OutputChannel& out, + const Node& n, + Effort level = FULL_EFFORT){} + +private: + bool equiv(Node x, Node y); + void ccUnion(ECData* ecX, ECData* ecY); + ECData* ccFind(ECData* x); + + void merge(); + //TODO put back in theory + + +}; + +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__THEORY_UF_H */ |