diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-04-26 12:55:13 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-05-02 14:47:20 -0400 |
commit | fb05d8411fdf905550d0bfdef56f4a4c3ed6a8ef (patch) | |
tree | ecdcda2fc6c9a2e11e8029333e7ca7998cd69d82 /src/theory/atom_requests.cpp | |
parent | a5d1513db484457ac64a96711088aca1460af62e (diff) |
* splitLemma to request atoms
* normalizing in bv before bitblasting
Diffstat (limited to 'src/theory/atom_requests.cpp')
-rw-r--r-- | src/theory/atom_requests.cpp | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp new file mode 100644 index 000000000..3d111f9f8 --- /dev/null +++ b/src/theory/atom_requests.cpp @@ -0,0 +1,62 @@ +#include "theory/atom_requests.h" + +using namespace CVC4; + +AtomRequests::AtomRequests(context::Context* context) +: d_allRequests(context) +, d_requests(context) +, d_triggerToRequestMap(context) +{} + +AtomRequests::element_index AtomRequests::getList(TNode trigger) const { + trigger_to_list_map::const_iterator find = d_triggerToRequestMap.find(trigger); + if (find == d_triggerToRequestMap.end()) { + return null_index; + } else { + return (*find).second; + } +} + +bool AtomRequests::isTrigger(TNode atom) const { + return getList(atom) != null_index; +} + +AtomRequests::atom_iterator AtomRequests::getAtomIterator(TNode trigger) const { + return atom_iterator(*this, getList(trigger)); +} + +void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory) { + + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << ")" << std::endl; + + Request request(atomToSend, toTheory); + + if (d_allRequests.find(request) != d_allRequests.end()) { + // Have it already + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): already there" << std::endl; + return; + } + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): adding" << std::endl; + + /// Mark the new request + d_allRequests.insert(request); + + // Index of the new request in the list of trigger + element_index index = d_requests.size(); + element_index previous = getList(triggerAtom); + d_requests.push_back(Element(request, previous)); + d_triggerToRequestMap[triggerAtom] = index; +} + +bool AtomRequests::atom_iterator::done() const { + return index == null_index; +} + +void AtomRequests::atom_iterator::next() { + index = requests.d_requests[index].previous; +} + +const AtomRequests::Request& AtomRequests::atom_iterator::get() const { + return requests.d_requests[index].request; +} + |