diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-08 21:25:27 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-08 21:25:27 +0000 |
commit | b3470b5e0b7a664443b9f835db5dd86fb1487866 (patch) | |
tree | cbfe76629fc1de740b552e574a058906eb4f2321 /src/theory/arith/theory_arith.h | |
parent | 2d422bab11e46f056bfafa85b0d49282fec289d8 (diff) |
Improved support for division by zero. This adds the *_TOTAL kinds and uninterpreted functions for division by 0.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index fd664e04a..da4a80208 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -107,13 +107,15 @@ private: d_setupNodes.insert(n); } - void interpretDivLike(const Variable& x); + void setupDivLike(const Variable& x); void setupVariable(const Variable& x); void setupVariableList(const VarList& vl); void setupPolynomial(const Polynomial& poly); void setupAtom(TNode atom); + void cautiousSetupPolynomial(const Polynomial& p); + class SetupLiteralCallBack : public TNodeCallBack { private: TheoryArith* d_arith; @@ -305,6 +307,21 @@ private: /** TODO : get rid of this. */ DeltaRational getDeltaValueWithNonlinear(TNode n, bool& failed); + /** Uninterpretted function symbol for use when interpreting + * division by zero. + */ + Node d_realDivideBy0Func; + Node d_intDivideBy0Func; + Node d_intModulusBy0Func; + Node getRealDivideBy0Func(); + Node getIntDivideBy0Func(); + Node getIntModulusBy0Func(); + + Node definingIteForDivLike(Node divLike); + Node axiomIteForTotalDivision(Node div_tot); + Node axiomIteForTotalIntDivision(Node int_div_like); + + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); virtual ~TheoryArith(); |