diff options
author | Tim King <taking@cs.nyu.edu> | 2011-12-15 22:23:25 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-12-15 22:23:25 +0000 |
commit | 9f5e56a0460c2668e8c5547d616fb34a58ff6d88 (patch) | |
tree | 9f033c30d44c1df2ad01b5c14248b28d75a8c267 /src/theory/arith/arith_prop_manager.h | |
parent | f2d98d87361fc1a44e64677586f5c8d4625a4756 (diff) |
Partial fix to bug 295.
Diffstat (limited to 'src/theory/arith/arith_prop_manager.h')
-rw-r--r-- | src/theory/arith/arith_prop_manager.h | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 912c4fdf8..bf7564593 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -31,7 +31,7 @@ #include "context/cdlist.h" #include "context/cdmap.h" #include "context/cdo.h" - +#include "theory/rewriter.h" #include "util/stats.h" namespace CVC4 { @@ -42,6 +42,7 @@ class PropManager { public: struct PropUnit { // consequent <= antecedent + // i.e. the antecedent is the explanation of the consequent. Node consequent; Node antecedent; bool flag; @@ -52,10 +53,13 @@ public: 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 { @@ -86,6 +90,13 @@ public: 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)); |