diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/theory/uf | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 78 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 4 | ||||
-rw-r--r-- | src/theory/uf/kinds | 3 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 51 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 51 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 52 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 8 |
8 files changed, 174 insertions, 83 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 828d53144..8df323992 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -314,10 +314,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // How many children are not constants yet d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { - if (isConstant(getNodeId(t[i]))) { - Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; - subtermEvaluates(result); - } + if (isConstant(getNodeId(t[i]))) { + Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; + subtermEvaluates(result); + } } } } else { @@ -335,7 +335,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); - // Setup the new set + // Setup the new set Theory::Set newSetTags = 0; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = THEORY_LAST; @@ -629,12 +629,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // If it's interpreted and we can interpret - if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id - TNode term = d_nodes[funId]; - subtermEvaluates(getNodeId(term)); - } - // Check if there is an application with find arguments + if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { + // Get the actual term id + TNode term = d_nodes[funId]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); @@ -972,7 +972,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // If the nodes are the same, we're done if (t1Id == t2Id){ if( eqp ) { - eqp->d_node = d_nodes[t1Id]; + eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); } return; } @@ -1029,6 +1029,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; EqProof * eqpc = NULL; //make child proof if a proof is being constructed @@ -1051,6 +1052,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); + Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl; + if( d_nodes[currentNode].getKind()==kind::EQUAL ){ + //leave node null for now + eqpc->d_node = Node::null(); + }else{ + Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; + if(d_nodes[f1.a].getKind() == kind::APPLY_UF || + d_nodes[f1.a].getKind() == kind::SELECT || + d_nodes[f1.a].getKind() == kind::STORE) { + eqpc->d_node = d_nodes[f1.a]; + } else { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]); + } + } } Debug("equality") << pop; break; @@ -1103,13 +1118,14 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Construct the equality Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; if( eqpc ){ - if( reasonType==MERGED_THROUGH_EQUALITY ){ + if(reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = d_equalityEdges[currentEdge].getReason(); - }else{ - //theory-specific proof rule : TODO - eqpc->d_id = reasonType; - //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId(); + } else { + // theory-specific proof rule + eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]); + Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl; } + eqpc->d_id = reasonType; } equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; @@ -1120,13 +1136,32 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; + //---from Morgan--- + if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { + if(eqpc->d_node.isNull()) { + Assert(eqpc->d_children.size() == 1); + EqProof *p = eqpc; + eqpc = p->d_children[0]; + delete p; + } else { + Assert(eqpc->d_children.empty()); + } + } + //---end from Morgan--- + eqp_trans.push_back( eqpc ); } while (currentEdge != null_id); - if( eqp ){ - eqp->d_id = MERGED_THROUGH_TRANS; - eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + if(eqp) { + if(eqp_trans.size() == 1) { + *eqp = *eqp_trans[0]; + delete eqp_trans[0]; + } else { + eqp->d_id = MERGED_THROUGH_TRANS; + eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); + } } // Done @@ -2057,8 +2092,7 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } - -void EqProof::debug_print( const char * c, unsigned tb ){ +void EqProof::debug_print( const char * c, unsigned tb ) const{ for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; } Debug( c ) << d_id << "("; if( !d_children.empty() || !d_node.isNull() ){ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 87074aebc..9cfa16adf 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -879,8 +879,8 @@ public: MergeReasonType d_id; Node d_node; std::vector< EqProof * > d_children; - void debug_print( const char * c, unsigned tb = 0 ); -}; + void debug_print( const char * c, unsigned tb = 0 ) const; +};/* class EqProof */ } // Namespace eq } // Namespace theory diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index f0b50b778..888fa140f 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -21,6 +21,9 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature" typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule +parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application" +typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule + operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S" typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index d5e18ed14..4f7a2667c 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -167,7 +167,8 @@ void SymmetryBreaker::Template::reset() { d_reps.clear(); } -SymmetryBreaker::SymmetryBreaker(context::Context* context) : +SymmetryBreaker::SymmetryBreaker(context::Context* context, + std::string name) : ContextNotifyObj(context), d_assertionsToRerun(context), d_rerunningAssertions(false), @@ -178,7 +179,10 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) : d_template(), d_normalizationCache(), d_termEqs(), - d_termEqsOnly() { + d_termEqsOnly(), + d_name(name), + d_stats(d_name) +{ } class SBGuard { @@ -461,7 +465,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Debug("ufsymm") << "UFSYMM =====================================================" << endl << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl; if(!d_permutations.empty()) { - { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer); + { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer); // normalize d_phi for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { @@ -476,12 +480,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { for(Permutations::iterator i = d_permutations.begin(); i != d_permutations.end(); ++i) { - ++d_permutationSetsConsidered; + ++(d_stats.d_permutationSetsConsidered); const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { - ++d_permutationSetsInvariant; + ++(d_stats.d_permutationSetsInvariant); selectTerms(p); set<Node> cts; while(!d_terms.empty() && cts.size() <= n) { @@ -539,11 +543,11 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Node d; if(disj.getNumChildren() > 1) { d = disj; - ++d_clauses; + ++(d_stats.d_clauses); } else { d = disj[0]; disj.clear(); - ++d_units; + ++(d_stats.d_units); } if(Debug.isOn("ufsymm")) { Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl; @@ -569,7 +573,7 @@ void SymmetryBreaker::guessPermutations() { } bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer); // use d_phi Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl; @@ -681,7 +685,7 @@ static bool isSubset(const T1& s, const T2& t) { } void SymmetryBreaker::selectTerms(const Permutation& p) { - TimerStat::CodeTimer codeTimer(d_selectTermsTimer); + TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer); // use d_phi, put into d_terms Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl; @@ -733,6 +737,35 @@ void SymmetryBreaker::selectTerms(const Permutation& p) { } } +SymmetryBreaker::Statistics::Statistics(std::string name) + : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0) + , d_units(name + "theory::uf::symmetry_breaker::units", 0) + , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0) + , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0) + , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations") + , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms") + , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization") +{ + smtStatisticsRegistry()->registerStat(&d_clauses); + smtStatisticsRegistry()->registerStat(&d_units); + smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered); + smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant); + smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer); + smtStatisticsRegistry()->registerStat(&d_selectTermsTimer); + smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer); +} + +SymmetryBreaker::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_clauses); + smtStatisticsRegistry()->unregisterStat(&d_units); + smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered); + smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant); + smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer); + smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer); + smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer); +} + SymmetryBreaker::Terms::iterator SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { // use d_phi diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 763ced650..5523c1c0d 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -128,35 +128,30 @@ private: Node normInternal(TNode phi, size_t level); Node norm(TNode n); + std::string d_name; + // === STATISTICS === /** number of new clauses that come from the SymmetryBreaker */ - KEEP_STATISTIC(IntStat, - d_clauses, - "theory::uf::symmetry_breaker::clauses", 0); - /** number of new clauses that come from the SymmetryBreaker */ - KEEP_STATISTIC(IntStat, - d_units, - "theory::uf::symmetry_breaker::units", 0); - /** number of potential permutation sets we found */ - KEEP_STATISTIC(IntStat, - d_permutationSetsConsidered, - "theory::uf::symmetry_breaker::permutationSetsConsidered", 0); - /** number of invariant permutation sets we found */ - KEEP_STATISTIC(IntStat, - d_permutationSetsInvariant, - "theory::uf::symmetry_breaker::permutationSetsInvariant", 0); - /** time spent in invariantByPermutations() */ - KEEP_STATISTIC(TimerStat, - d_invariantByPermutationsTimer, - "theory::uf::symmetry_breaker::timers::invariantByPermutations"); - /** time spent in selectTerms() */ - KEEP_STATISTIC(TimerStat, - d_selectTermsTimer, - "theory::uf::symmetry_breaker::timers::selectTerms"); - /** time spent in initial round of normalization */ - KEEP_STATISTIC(TimerStat, - d_initNormalizationTimer, - "theory::uf::symmetry_breaker::timers::initNormalization"); + struct Statistics { + /** number of new clauses that come from the SymmetryBreaker */ + IntStat d_clauses; + IntStat d_units; + /** number of potential permutation sets we found */ + IntStat d_permutationSetsConsidered; + /** number of invariant permutation sets we found */ + IntStat d_permutationSetsInvariant; + /** time spent in invariantByPermutations() */ + TimerStat d_invariantByPermutationsTimer; + /** time spent in selectTerms() */ + TimerStat d_selectTermsTimer; + /** time spent in initial round of normalization */ + TimerStat d_initNormalizationTimer; + + Statistics(std::string name); + ~Statistics(); + }; + + Statistics d_stats; protected: @@ -167,7 +162,7 @@ protected: public: - SymmetryBreaker(context::Context* context); + SymmetryBreaker(context::Context* context, std::string name = ""); ~SymmetryBreaker() throw() {} void assertFormula(TNode phi); void apply(std::vector<Node>& newClauses); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e21b7ef7d..93a920f82 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -20,30 +20,34 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/theory_uf_strong_solver.h" using namespace std; -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; + +namespace CVC4 { +namespace theory { +namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo, SmtGlobals* globals, std::string name) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ d_thss(NULL), - d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true), + d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_functionsTerms(c), - d_symb(u) + d_symb(u, name) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){ } } -void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { +void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp); + d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); } - //for now, just print debug - //TODO : send the proof outwards : d_out->conflict( lem, eqp ); - if( eqp ){ - eqp->debug_print("uf-pf"); + if( pf ){ + Debug("uf-pf") << std::endl; + pf->debug_print("uf-pf"); } } Node TheoryUF::explain(TNode literal) { + return explain(literal, NULL); +} + +Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; - explain(literal, assumptions); + explain(literal, assumptions, pf); return mkAnd(assumptions); } @@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - //TODO: create EqProof at this level if d_proofEnabled = true + eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b)); + d_conflictNode = explain(a.iffNode(b),pf); } else { - d_conflictNode = explain(a.eqNode(b)); + d_conflictNode = explain(a.eqNode(b),pf); } - d_out->conflict(d_conflictNode); + ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; + d_out->conflict(d_conflictNode, puf); d_conflict = true; } @@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_thss->assertDisequal(t1, t2, reason); } } + + +} /* namespace CVC4::theory::uf */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index aff78f53d..bd0016be7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -128,9 +128,15 @@ private: /** * Explain why this literal is true by adding assumptions + * with proof (if "pf" is non-NULL). */ - void explain(TNode literal, std::vector<TNode>& assumptions); + void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf); + /** + * Explain a literal, with proof (if "pf" is non-NULL). + */ + Node explain(TNode literal, eq::EqProof* pf); + /** Literals to propagate */ context::CDList<Node> d_literalsToPropagate; @@ -163,7 +169,7 @@ public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + SmtGlobals* globals, std::string name = ""); ~TheoryUF(); diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 6faab8517..05b95e9e1 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -107,6 +107,14 @@ public: } };/* class CardinalityConstraintTypeRule */ +class PartialTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + return n.getOperator().getType().getRangeType(); + } +};/* class PartialTypeRule */ + class CardinalityValueTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) |