#include "context/cdlist.h"
#include "context/cdmap.h"
#include "context/cdo.h"
-
+#include "theory/rewriter.h"
#include "util/stats.h"
namespace CVC4 {
public:
struct PropUnit {
// consequent <= antecedent
+ // i.e. the antecedent is the explanation of the consequent.
Node consequent;
Node antecedent;
bool flag;
private:
context::CDList<PropUnit> d_propagated;
-
context::CDO<uint32_t> d_propagatedPos;
- typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
+ /* This maps the node a theory engine will request on an explain call to
+ * to its corresponding PropUnit.
+ * This is node is potentially both the consequent or Rewriter::rewrite(consequent).
+ */
+ typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
ExplainMap d_explanationMap;
size_t getIndex(TNode n) const {
void propagate(TNode n, Node reason, bool flag) {
Assert(!isPropagated(n));
+ if(flag){
+ Node rewritten = Rewriter::rewrite(n);
+ d_explanationMap.insert(rewritten, d_propagated.size());
+ }else{
+ //If !flag, then the rewriter is idempotent on n.
+ Assert(Rewriter::rewrite(n) == n);
+ }
d_explanationMap.insert(n, d_propagated.size());
d_propagated.push_back(PropUnit(n, reason, flag));
void DifferenceManager::propagate(TNode x){
Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
- d_queue.propagate(x, Node::null(), true);
+ d_queue.propagate(x, explain(x), true);
}
void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
ArithVar x_i = determineLeftVariable(assertion, simpKind);
DeltaRational c_i = determineRightConstant(assertion, simpKind);
- Debug("arith::assertions") << "arith assertion(" << assertion
+ Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel()
+ <<"(" << assertion
<< " \\-> "
<< x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
switch(simpKind){
}
Node TheoryArith::explain(TNode n) {
- Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+ Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
Assert(d_propManager.isPropagated(n));
- if(d_propManager.isFlagged(n)){
- return d_differenceManager.explain(n);
- }else{
- return d_propManager.explain(n);
- }
+ return d_propManager.explain(n);
}
void flattenAnd(Node n, std::vector<TNode>& out){
TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
- Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl;
+ Debug("arith::propagate") << "propagate @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
if(flag) {
//Currently if the flag is set this came from an equality detected by the
}else{
Node exp = d_differenceManager.explain(toProp);
Node lp = flattenAnd(exp.andNode(notNormalized));
- Debug("arith::propagate") << "propagate conflict" << lp << endl;
+ Debug("arith::propagate") << "propagate conflict" << lp << endl;
d_out->conflict(lp);
propagated = true;