normalization.assumptions.push_back(assumptions);
BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl;
- BVDebug("bitvector") << " assumptions " << setToString(assumptions) << std::endl;
+ BVDebug("bitvector") << " assumptions " << utils::setToString(assumptions) << std::endl;
BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl;
std::set<TNode> assumptions;
for (unsigned i = 0; i < vec.size(); ++ i) {
BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl;
- BVDebug("bitvector") << " assumptions " << setToString(d_normalization[equality]->assumptions[i]) << std::endl;
+ BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl;
assumptions.insert(vec[i].begin(), vec[i].end());
}
d_out->explanation(utils::mkConjunction(assumptions));
virtual ~OutputChannel() {
}
- /**
- * Notify the OutputChannel that a new fact has been received by
- * the theory.
- */
- virtual void newFact(TNode n) { }
-
/**
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
d_factsHead = d_factsHead + 1;
Trace("theory") << "Theory::get() => " << fact
<< " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
- d_out->newFact(fact);
return fact;
}
*/
virtual void preRegisterTerm(TNode) { }
- /**
- * Register a term.
- *
- * When get() is called to get the next thing off the theory queue,
- * setup() is called on its subterms (in TheoryEngine). Then setup()
- * is called on this node.
- *
- * This is done in a "context escape" -- that is, at context level 0.
- * setup() MUST NOT MODIFY context-dependent objects that it hasn't
- * itself just created.
- */
- virtual void registerTerm(TNode) { }
-
/**
* Assert a fact in the current context.
*/
*/
virtual std::string identify() const = 0;
+ /** A set of theories */
+ typedef uint32_t Set;
+
+ /** Add the theory to the set. If no set specified, just returns a singleton set */
+ static inline Set setInsert(TheoryId theory, Set set = 0) {
+ return set | (1 << theory);
+ }
+
+ /** Check if the set containt the theory */
+ static inline bool setContains(TheoryId theory, Set set) {
+ return set & (1 << theory);
+ }
+
+ static inline Set setUnion(Set a, Set b) {
+ return a | b;
+ }
+
+ static inline std::string setToString(theory::Theory::Set theorySet) {
+ std::stringstream ss;
+ ss << "[";
+ for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
+ if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
+ ss << (theory::TheoryId) theoryId << " ";
+ }
+ }
+ ss << "]";
+ return ss.str();
+ }
+
};/* class Theory */
std::ostream& operator<<(std::ostream& os, Theory::Effort level);
using namespace CVC4;
using namespace CVC4::theory;
-/** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-struct RegisteredAttrTag {};
-/** The "registerTerm()-has-been-called" flag on Nodes */
-typedef expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr;
-
/** Tag for the "preregisterTerm()-has-benn-called" flag on nodes */
struct PreRegisteredAttrTag {};
/** The "preregisterTerm()-has-been-called" flag on Nodes */
-typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegisteredAttr;
-
-void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
- TimerStat::CodeTimer codeTimer(d_newFactTimer);
-
- if (fact.getKind() == kind::NOT) {
- // No need to register negations - only atoms
- fact = fact[0];
- }
-
- if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) && d_engine->d_needRegistration) {
- RegisterVisitor visitor(*d_engine);
- NodeVisitor<RegisterVisitor, RegisteredAttr>::run(visitor, fact);
- }
-}
+typedef expr::Attribute<PreRegisteredAttrTag, Theory::Set> PreRegisteredAttr;
TheoryEngine::TheoryEngine(context::Context* ctxt) :
d_propEngine(NULL),
d_context(ctxt),
d_activeTheories(0),
- d_needRegistration(false),
d_theoryOut(this, ctxt),
d_hasShutDown(false),
d_incomplete(ctxt, false),
- d_statistics() {
+ d_statistics(),
+ d_preRegistrationVisitor(*this) {
for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
d_theoryTable[theoryId] = NULL;
- d_theoryIsActive[theoryId] = false;
}
Rewriter::init();
};/* struct preprocess_stack_element */
void TheoryEngine::preRegister(TNode preprocessed) {
- PreRegisterVisitor visitor(*this);
- NodeVisitor<PreRegisterVisitor, PreRegisteredAttr>::run(visitor, preprocessed);
+ NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
}
/**
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
+ if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
if (d_theoryOut.d_inConflict) { \
return; \
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \
+ if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
}
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \
+ if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \
}
CVC4_FOR_EACH_THEORY;
}
-bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
- switch(th) {
- // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- case THEORY: \
- return theory::TheoryTraits<THEORY>::hasRegisterTerm;
-
- CVC4_FOR_EACH_THEORY
- default:
- Unhandled(th);
- }
-}
-
theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) {
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl;
* runs (no sharing), can reduce the cost of walking the DAG on
* registration, etc.
*/
- bool d_theoryIsActive[theory::THEORY_LAST];
-
- /**
- * The count of active theories in the d_theoryIsActive bitmap.
- */
- size_t d_activeTheories;
-
- /**
- * Need the registration infrastructure when theory sharing is on
- * (>=2 active theories) or when the sole active theory has
- * requested it.
- */
- bool d_needRegistration;
+ theory::Theory::Set d_activeTheories;
/**
* Cache from proprocessing of atoms.
*/
std::vector<TNode> d_propagatedLiterals;
- /** Time spent in newFact() (largely spent doing term registration) */
- KEEP_STATISTIC(TimerStat,
- d_newFactTimer,
- "theory::newFactTimer");
-
/**
* Check if the node is in conflict for debug purposes
*/
// Construct the lemma (note that no CNF caching should happen as all the literals already exists)
Assert(isProperConflict(conflictNode));
- d_engine->newLemma(conflictNode, true, true);
+ d_engine->newLemma(conflictNode, true, false);
if(safe) {
throw theory::Interrupted();
/**
* Mark a theory active if it's not already.
*/
- void markActive(theory::TheoryId th) {
- if(!d_theoryIsActive[th]) {
- d_theoryIsActive[th] = true;
- if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) {
- if(++d_activeTheories == 1) {
- // theory requests registration
- d_needRegistration = hasRegisterTerm(th);
- } else {
- // need it for sharing
- d_needRegistration = true;
- }
- }
- Notice() << "Theory " << th << " has been activated (registration is "
- << (d_needRegistration ? "on" : "off") << ")." << std::endl;
- }
+ void markActive(theory::Theory::Set theories) {
+ d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories);
}
- bool hasRegisterTerm(theory::TheoryId th) const;
+ /**
+ * Is the theory active.
+ */
+ bool isActive(theory::TheoryId theory) {
+ return theory::Theory::setContains(theory, d_activeTheories);
+ }
/** The logic of the problem */
std::string d_logic;
return d_theoryTable[theory::Theory::theoryOf(node)];
}
+ /**
+ * Get the theory associated to a the given theory id.
+ *
+ * @returns the theory, or NULL if the TNode is
+ * of built-in type.
+ */
+ inline theory::Theory* theoryOf(theory::TheoryId theoryId) {
+ return d_theoryTable[theoryId];
+ }
+
/**
* Solve the given literal with a theory that owns it.
*/
/** The engine */
TheoryEngine& d_engine;
+ /**
+ * Cache from proprocessing of atoms.
+ */
+ typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ TNodeVisitedMap d_visited;
+
+ /**
+ * All the theories of the visitation.
+ */
+ theory::Theory::Set d_theories;
+
+ std::string toString() const {
+ std::stringstream ss;
+ TNodeVisitedMap::const_iterator it = d_visited.begin();
+ for (; it != d_visited.end(); ++ it) {
+ ss << it->first << ": " << theory::Theory::setToString(it->second) << std::endl;
+ }
+ return ss.str();
+ }
+
public:
- PreRegisterVisitor(TheoryEngine& engine): d_engine(engine) {}
+ PreRegisterVisitor(TheoryEngine& engine): d_engine(engine), d_theories(0) {}
- void operator () (TNode current) {
- // Get the theory of the term and pre-register it with the owning theory
- theory::TheoryId currentTheoryId = theory::Theory::theoryOf(current);
- Debug("register") << "preregistering " << current << " with " << currentTheoryId << std::endl;
- d_engine.markActive(currentTheoryId);
- theory::Theory* currentTheory = d_engine.theoryOf(current);
- currentTheory->preRegisterTerm(current);
+ bool alreadyVisited(TNode current, TNode parent) {
+
+ Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => ";
+
+ using namespace theory;
+
+ TNodeVisitedMap::iterator find = d_visited.find(current);
+
+ // If node is not visited at all, just return false
+ if (find == d_visited.end()) {
+ Debug("register::internal") << "1:false" << std::endl;
+ return false;
+ }
+
+ TheoryId currentTheoryId = Theory::theoryOf(current);
+ if (Theory::setContains(currentTheoryId, find->second)) {
+ // The current theory has already visited it, so now it depends on the parent
+ TheoryId parentTheoryId = Theory::theoryOf(parent);
+ if (parentTheoryId == currentTheoryId) {
+ // If it's the same theory, we've visited it already
+ Debug("register::internal") << "2:true" << std::endl;
+ return true;
+ }
+ // If not the same theory, we might have visited it, just check
+ Debug("register::internal") << (Theory::setContains(parentTheoryId, find->second) ? "3:true" : "3:false") << std::endl;
+ return Theory::setContains(parentTheoryId, find->second);
+ } else {
+ // If the current theory is not registered, it still needs to be visited
+ Debug("register::internal") << "4:false" << std::endl;
+ return false;
+ }
}
- };
- /**
- * Visitor that calls the apropriate theory to preregister the term.
- */
- class RegisterVisitor {
+ void visit(TNode current, TNode parent) {
- /** The engine */
- TheoryEngine& d_engine;
+ Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
+ Debug("register::internal") << toString() << std::endl;
- public:
+ using namespace theory;
+
+ // Get the theories of the terms
+ TheoryId currentTheoryId = Theory::theoryOf(current);
+ TheoryId parentTheoryId = Theory::theoryOf(parent);
+
+ if (currentTheoryId == parentTheoryId) {
+ // If it's the same theory we just add it
+ TNodeVisitedMap::iterator find = d_visited.find(current);
+ if (find == d_visited.end()) {
+ d_visited[current] = Theory::setInsert(currentTheoryId);
+ } else {
+ find->second = Theory::setInsert(currentTheoryId, find->second);
+ }
+ // Visit it
+ d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+ // Mark the theory as active
+ d_theories = Theory::setInsert(currentTheoryId, d_theories);
+ } else {
+ // If two theories, one might have visited it already
+ // If it's the same theory we just add it
+ TNodeVisitedMap::iterator find = d_visited.find(current);
+ if (find == d_visited.end()) {
+ // If not in the map at all, we just add both
+ d_visited[current] = Theory::setInsert(parentTheoryId, Theory::setInsert(currentTheoryId));
+ // And visit both
+ d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+ d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current);
+ // Mark both theories as active
+ d_theories = Theory::setInsert(currentTheoryId, d_theories);
+ d_theories = Theory::setInsert(parentTheoryId, d_theories);
+ } else {
+ if (!Theory::setContains(currentTheoryId, find->second)) {
+ find->second = Theory::setInsert(currentTheoryId, find->second);
+ d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current);
+ d_theories = Theory::setInsert(currentTheoryId, d_theories);
+ }
+ if (!Theory::setContains(parentTheoryId, find->second)) {
+ find->second = Theory::setInsert(parentTheoryId, find->second);
+ d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current);
+ d_theories = Theory::setInsert(parentTheoryId, d_theories);
+ }
+ }
+ }
- RegisterVisitor(TheoryEngine& engine): d_engine(engine) {}
+ Assert(d_visited.find(current) != d_visited.end());
+ Assert(alreadyVisited(current, parent));
+ }
- void operator () (TNode current) {
- // Register this node to it's theory
- theory::Theory* currentTheory = d_engine.theoryOf(current);
- Debug("register") << "registering " << current << " with " << currentTheory->getId() << std::endl;
- currentTheory->registerTerm(current);
+ void start(TNode node) {
+ d_theories = 0;
}
+
+ void done(TNode node) {
+ d_engine.markActive(d_theories);
+ }
+
};
+ /** Default visitor for pre-registration */
+ PreRegisterVisitor d_preRegistrationVisitor;
+
};/* class TheoryEngine */
}/* CVC4 namespace */
/**
* Traverses the nodes topologically and call the visitor when all the children have been visited.
*/
-template<typename Visitor, typename VisitedAttribute>
+template<typename Visitor>
class NodeVisitor {
public:
struct stack_element {
/** The node to be visited */
TNode node;
+ /** The parent of the node */
+ TNode parent;
+ /** Have the children been queued up for visitation */
bool children_added;
- stack_element(TNode node)
- : node(node), children_added(false) {}
+ stack_element(TNode node, TNode parent)
+ : node(node), parent(parent), children_added(false) {}
};/* struct preprocess_stack_element */
/**
* Performs the traversal.
*/
- static void run(Visitor visitor, TNode node) {
- // If the node has been visited already, we're done
- if (node.getAttribute(VisitedAttribute())) {
- return;
- }
+ static void run(Visitor& visitor, TNode node) {
+
+ // Notify of a start
+ visitor.start(node);
+
// Do a topological sort of the subexpressions and preregister them
std::vector<stack_element> toVisit;
- toVisit.push_back((TNode) node);
+ toVisit.push_back(stack_element(node, node));
while (!toVisit.empty()) {
stack_element& stackHead = toVisit.back();
// The current node we are processing
TNode current = stackHead.node;
+ TNode parent = stackHead.parent;
- if (current.getAttribute(VisitedAttribute())) {
+ if (visitor.alreadyVisited(current, parent)) {
// If already visited, we're done
toVisit.pop_back();
} else if (stackHead.children_added) {
- // If children have been processed, we can visit the current
- current.setAttribute(VisitedAttribute(), true);
// Call the visitor
- visitor(current);
+ visitor.visit(current, parent);
// Done with this node, remove from the stack
toVisit.pop_back();
} else {
// We need to add the children
for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
TNode childNode = *child_it;
- if (!childNode.getAttribute(VisitedAttribute())) {
- toVisit.push_back(childNode);
+ if (!visitor.alreadyVisited(childNode, current)) {
+ toVisit.push_back(stack_element(childNode, current));
}
}
}
}
+ // Notify that we're done
+ visitor.done(node);
}
};
projects / cvc5.git / commitdiff