diff options
Diffstat (limited to 'src/theory/arith/arith_rewriter.h')
| -rw-r--r-- | src/theory/arith/arith_rewriter.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 844663ce8..a2a8b1b4b 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -67,7 +67,11 @@ class ArithRewriter{ private: ArithConstants* d_constants; + //This is where the core of the work is done for rewriteAtom + //With a few additional checks done by rewriteAtom + Node rewriteAtomCore(TNode atom); Node rewriteAtom(TNode atom); + Node rewriteTerm(TNode t); Node rewriteMult(TNode t); Node rewritePlus(TNode t); @@ -76,6 +80,8 @@ private: Node var2pnf(TNode variable); + Node multPnfByNonZero(TNode pnf, Rational& q); + public: ArithRewriter(ArithConstants* ac) : d_constants(ac) |