diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:35:58 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 20:07:39 -0400 |
commit | 0a3422299da7e882bae22c5fa3e5ec3c80b42046 (patch) | |
tree | d00f31a33f03f11608ee046b851f4c63e194fe87 /src/theory | |
parent | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (diff) |
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 95 | ||||
-rw-r--r-- | src/theory/arith/kinds | 26 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 5 | ||||
-rw-r--r-- | src/theory/arith/options | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 160 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 59 |
9 files changed, 325 insertions, 27 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index aa5049ed4..247c09294 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -29,7 +29,8 @@ namespace theory { namespace arith { bool ArithRewriter::isAtom(TNode n) { - return arith::isRelationOperator(n.getKind()); + Kind k = n.getKind(); + return arith::isRelationOperator(k) || k == kind::IS_INTEGER || k == kind::DIVISIBLE; } RewriteResponse ArithRewriter::rewriteConstant(TNode t){ @@ -98,11 +99,28 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return preRewritePlus(t); case kind::MULT: return preRewriteMult(t); - //case kind::INTS_DIVISION: - //case kind::INTS_MODULUS: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + return RewriteResponse(REWRITE_DONE, t); case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t,true); + case kind::ABS: + if(t[0].isConst()) { + const Rational& rat = t[0].getConst<Rational>(); + if(rat >= 0) { + return RewriteResponse(REWRITE_DONE, t[0]); + } else { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(-rat)); + } + } + return RewriteResponse(REWRITE_DONE, t); + case kind::IS_INTEGER: + case kind::TO_INTEGER: + return RewriteResponse(REWRITE_DONE, t); + case kind::TO_REAL: + return RewriteResponse(REWRITE_DONE, t[0]); default: Unhandled(k); } @@ -126,11 +144,44 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return postRewritePlus(t); case kind::MULT: return postRewriteMult(t); - //case kind::INTS_DIVISION: - //case kind::INTS_MODULUS: + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + return RewriteResponse(REWRITE_DONE, t); case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false); + case kind::ABS: + if(t[0].isConst()) { + const Rational& rat = t[0].getConst<Rational>(); + if(rat >= 0) { + return RewriteResponse(REWRITE_DONE, t[0]); + } else { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(-rat)); + } + } + case kind::TO_REAL: + return RewriteResponse(REWRITE_DONE, t[0]); + case kind::TO_INTEGER: + if(t[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor()))); + } + if(t[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, t[0]); + } + //Unimplemented("TO_INTEGER, nonconstant"); + //return rewriteToInteger(t); + return RewriteResponse(REWRITE_DONE, t); + case kind::IS_INTEGER: + if(t[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst<Rational>().getDenominator() == 1)); + } + if(t[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + //Unimplemented("IS_INTEGER, nonconstant"); + //return rewriteIsInteger(t); + return RewriteResponse(REWRITE_DONE, t); default: Unreachable(); } @@ -190,6 +241,25 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ } RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ + if(atom.getKind() == kind::IS_INTEGER) { + if(atom[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst<Rational>().isIntegral())); + } + if(atom[0].getType().isInteger()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + // not supported, but this isn't the right place to complain + return RewriteResponse(REWRITE_DONE, atom); + } else if(atom.getKind() == kind::DIVISIBLE) { + if(atom[0].isConst()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst<Rational>() / atom.getOperator().getConst<Divisible>().k).isIntegral()))); + } + if(atom.getOperator().getConst<Divisible>().k.isOne()) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], NodeManager::currentNM()->mkConst(Rational(atom.getOperator().getConst<Divisible>().k))), NodeManager::currentNM()->mkConst(Rational(0)))); + } + // left |><| right TNode left = atom[0]; TNode right = atom[1]; @@ -217,6 +287,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ }else if(atom.getKind() == kind::LT){ Node geq = currNM->mkNode(kind::GEQ, atom[0], atom[1]); return RewriteResponse(REWRITE_DONE, currNM->mkNode(kind::NOT, geq)); + }else if(atom.getKind() == kind::IS_INTEGER){ + if(atom[0].getType().isInteger()){ + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); + } + }else if(atom.getKind() == kind::DIVISIBLE){ + if(atom.getOperator().getConst<Divisible>().k.isOne()){ + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); + } } return RewriteResponse(REWRITE_DONE, atom); @@ -329,6 +407,13 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); return RewriteResponse(REWRITE_AGAIN, n); } + }else if(dIsConstant && d.getConst<Rational>().isNegativeOne()){ + if(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + }else{ + Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::UMINUS, n)); + } }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){ Assert(d.getConst<Rational>().isIntegral()); Assert(n.getConst<Rational>().isIntegral()); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 07cfcc9e5..a8a4047ca 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -23,8 +23,16 @@ operator INTS_DIVISION 2 "ints division (user symbol)" operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)" operator INTS_MODULUS 2 "ints modulus (user symbol)" operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)" +operator ABS 1 "absolute value" +parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate" operator POW 2 "arithmetic power" +constant DIVISIBLE_OP \ + ::CVC4::Divisible \ + ::CVC4::DivisibleHashFunction \ + "util/divisible.h" \ + "operator for the divisibility-by-k predicate" + sort REAL_TYPE \ Cardinality::REALS \ well-founded \ @@ -72,6 +80,10 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" +operator IS_INTEGER 1 "term is integer" +operator TO_INTEGER 1 "cast term to integer" +operator TO_REAL 1 "cast term to real" + typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule @@ -86,11 +98,17 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule -typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule -typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule +typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule +typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule + +typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule +typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule +typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule +typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule +typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule +typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule endtheory diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index c6af7010f..1dddb5a5b 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -241,6 +241,11 @@ public: case kind::INTS_MODULUS_TOTAL: case kind::DIVISION_TOTAL: return isDivMember(n); + case kind::ABS: + case kind::TO_INTEGER: + // Treat to_int as a variable; it is replaced in early preprocessing + // by a variable. + return true; default: return (!isRelationOperator(k)) && (Theory::isLeafOf(n, theory::THEORY_ARITH)); diff --git a/src/theory/arith/options b/src/theory/arith/options index 7d92f5351..57ef3d1b9 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -100,5 +100,7 @@ option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-wri option soiQuickExplain --soi-qe bool :default false :read-write Use quick explain to minimize the sum of infeasibility conflicts. +option rewriteDivk rewrite-divk --rewrite-divk bool :default false + rewrite division and mod when by a constant into linear terms endmodule diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c0442da90..120ac0154 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -47,6 +47,7 @@ void TheoryArith::addSharedTerm(TNode n){ } Node TheoryArith::ppRewrite(TNode atom) { + CodeTimer timer(d_ppRewriteTimer); return d_internal->ppRewrite(atom); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 10c79b293..6b9fd5515 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -42,6 +42,7 @@ private: TheoryArithPrivate* d_internal; + KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index dd5e404c6..a01397973 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -737,19 +737,142 @@ void TheoryArithPrivate::addSharedTerm(TNode n){ } } +namespace attr { + struct ToIntegerTag { }; + struct LinearIntDivTag { }; +}/* CVC4::theory::arith::attr namespace */ + +/** + * This attribute maps the child of a to_int / is_int to the + * corresponding integer skolem. + */ +typedef expr::Attribute<attr::ToIntegerTag, Node> ToIntegerAttr; + +/** + * This attribute maps division-by-constant-k terms to a variable + * used to eliminate them. + */ +typedef expr::Attribute<attr::LinearIntDivTag, Node> LinearIntDivAttr; + +Node TheoryArithPrivate::ppRewriteTerms(TNode n) { + if(Theory::theoryOf(n) != THEORY_ARITH) { + return n; + } + + NodeManager* nm = NodeManager::currentNM(); + + switch(Kind k = n.getKind()) { + + case kind::TO_INTEGER: + case kind::IS_INTEGER: { + Node intVar; + if(!n[0].getAttribute(ToIntegerAttr(), intVar)) { + intVar = nm->mkSkolem("toInt", nm->integerType(), "a conversion of a Real term to its Integer part"); + n[0].setAttribute(ToIntegerAttr(), intVar); + d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LT, nm->mkNode(kind::MINUS, n[0], nm->mkConst(Rational(1))), intVar), nm->mkNode(kind::LEQ, intVar, n[0]))); + } + if(n.getKind() == kind::TO_INTEGER) { + Node node = intVar; + return node; + } else { + Node node = nm->mkNode(kind::EQUAL, node[0], intVar); + return node; + } + Unreachable(); + } + + case kind::INTS_DIVISION: + case kind::INTS_DIVISION_TOTAL: { + if(!options::rewriteDivk()) { + return n; + } + Node num = Rewriter::rewrite(n[0]); + Node den = Rewriter::rewrite(n[1]); + if(den.isConst()) { + const Rational& rat = den.getConst<Rational>(); + Assert(!num.isConst()); + if(rat != 0) { + Node intVar; + Node rw = nm->mkNode(k, num, den); + if(!rw.getAttribute(LinearIntDivAttr(), intVar)) { + intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); + rw.setAttribute(LinearIntDivAttr(), intVar); + if(rat > 0) { + d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))); + } else { + d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1))))))); + } + } + return intVar; + } + } + break; + } + + case kind::INTS_MODULUS: + case kind::INTS_MODULUS_TOTAL: { + if(!options::rewriteDivk()) { + return n; + } + Node num = Rewriter::rewrite(n[0]); + Node den = Rewriter::rewrite(n[1]); + if(den.isConst()) { + const Rational& rat = den.getConst<Rational>(); + Assert(!num.isConst()); + if(rat != 0) { + Node intVar; + Node rw = nm->mkNode(k, num, den); + if(!rw.getAttribute(LinearIntDivAttr(), intVar)) { + intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term"); + rw.setAttribute(LinearIntDivAttr(), intVar); + if(rat > 0) { + d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1))))))); + } else { + d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1))))))); + } + } + Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar)); + return node; + } + } + break; + } + + default: + ; + } + + for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) { + Node rewritten = ppRewriteTerms(*i); + if(rewritten != *i) { + NodeBuilder<> b(n.getKind()); + b.append(n.begin(), i); + b << rewritten; + for(++i; i != n.end(); ++i) { + b << ppRewriteTerms(*i); + } + rewritten = b; + return rewritten; + } + } + + return n; +} + Node TheoryArithPrivate::ppRewrite(TNode atom) { Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; - if (atom.getKind() == kind::EQUAL && options::arithRewriteEq()) { Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; + leq = ppRewriteTerms(leq); + geq = ppRewriteTerms(geq); Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; return rewritten; } else { - return atom; + return ppRewriteTerms(atom); } } @@ -902,7 +1025,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ // vl is the product of at least 2 variables // vl : (* v1 v2 ...) if(getLogicInfo().isLinear()){ - throw LogicException("Non-linear term was asserted to arithmetic in a linear logic."); + throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic."); } setIncomplete(); @@ -939,7 +1062,7 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ Assert(v.isDivLike()); if(getLogicInfo().isLinear()){ - throw LogicException("Non-linear term was asserted to arithmetic in a linear logic."); + throw LogicException("A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic;\nif you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option."); } Node vnode = v.getNode(); @@ -1161,16 +1284,22 @@ void TheoryArithPrivate::setupAtom(TNode atom) { void TheoryArithPrivate::preRegisterTerm(TNode n) { Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; - if(isRelationOperator(n.getKind())){ - if(!isSetup(n)){ - setupAtom(n); + try { + if(isRelationOperator(n.getKind())){ + if(!isSetup(n)){ + setupAtom(n); + } + Constraint c = d_constraintDatabase.lookup(n); + Assert(c != NullConstraint); + + Debug("arith::preregister") << "setup constraint" << c << endl; + Assert(!c->canBePropagated()); + c->setPreregistered(); } - Constraint c = d_constraintDatabase.lookup(n); - Assert(c != NullConstraint); - - Debug("arith::preregister") << "setup constraint" << c << endl; - Assert(!c->canBePropagated()); - c->setPreregistered(); + } catch(LogicException& le) { + std::stringstream ss; + ss << le.getMessage() << endl << "The fact in question: " << n << endl; + throw LogicException(ss.str()); } Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl; @@ -1187,7 +1316,10 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){ //TODO : The VarList trick is good enough? Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS); if(getLogicInfo().isLinear() && Variable::isDivMember(x)){ - throw LogicException("Non-linear term was asserted to arithmetic in a linear logic."); + stringstream ss; + ss << "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: " << x << endl + << "if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option."; + throw LogicException(ss.str()); } Assert(!d_partialModel.hasArithVar(x)); Assert(x.getType().isReal()); // real or integer diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 86c8e213e..7370cfc15 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -346,7 +346,8 @@ private: Node axiomIteForTotalDivision(Node div_tot); Node axiomIteForTotalIntDivision(Node int_div_like); - + // handle linear /, div, mod, and also is_int, to_int + Node ppRewriteTerms(TNode atom); public: TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index cc8451f8b..45e18fe0d 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -62,12 +62,37 @@ public: } } } - Kind k = n.getKind(); - bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL; - return (isInteger && !isDivision ? integerType : realType); + switch(Kind k = n.getKind()) { + case kind::TO_REAL: + return realType; + case kind::TO_INTEGER: + return integerType; + default: { + bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL; + return (isInteger && !isDivision ? integerType : realType); + } + } } };/* class ArithOperatorTypeRule */ +class IntOperatorTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + if(check) { + for(; child_it != child_it_end; ++child_it) { + TypeNode childType = (*child_it).getType(check); + if (!childType.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm"); + } + } + } + return nodeManager->integerType(); + } +};/* class IntOperatorTypeRule */ + class ArithPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -87,6 +112,34 @@ public: } };/* class ArithPredicateTypeRule */ +class ArithUnaryPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isReal()) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term"); + } + } + return nodeManager->booleanType(); + } +};/* class ArithUnaryPredicateTypeRule */ + +class IntUnaryPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting an integer term"); + } + } + return nodeManager->booleanType(); + } +};/* class IntUnaryPredicateTypeRule */ + class SubrangeProperties { public: inline static Cardinality computeCardinality(TypeNode type) { |