diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 16 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 10 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 4 | ||||
-rwxr-xr-x | src/theory/mkinstantiator | 6 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 6 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 6 | ||||
-rw-r--r-- | src/theory/model.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory.cpp | 6 | ||||
-rw-r--r-- | src/theory/theory.h | 6 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 16 |
17 files changed, 60 insertions, 48 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index d7a6c0443..6b38dacce 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -30,23 +30,19 @@ namespace CVC4 { namespace theory { namespace arith { -bool isVariable(TNode t){ - return t.getMetaKind() == kind::metakind::VARIABLE; -} - bool ArithRewriter::isAtom(TNode n) { return arith::isRelationOperator(n.getKind()); } RewriteResponse ArithRewriter::rewriteConstant(TNode t){ - Assert(t.getMetaKind() == kind::metakind::CONSTANT); + Assert(t.isConst()); Assert(t.getKind() == kind::CONST_RATIONAL); return RewriteResponse(REWRITE_DONE, t); } RewriteResponse ArithRewriter::rewriteVariable(TNode t){ - Assert(isVariable(t)); + Assert(t.isVar()); return RewriteResponse(REWRITE_DONE, t); } @@ -82,9 +78,9 @@ RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ } RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ - if(t.getMetaKind() == kind::metakind::CONSTANT){ + if(t.isConst()){ return rewriteConstant(t); - }else if(isVariable(t)){ + }else if(t.isVar()){ return rewriteVariable(t); }else if(t.getKind() == kind::MINUS){ return rewriteMinus(t, true); @@ -116,9 +112,9 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ } } RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ - if(t.getMetaKind() == kind::metakind::CONSTANT){ + if(t.isConst()){ return rewriteConstant(t); - }else if(isVariable(t)){ + }else if(t.isVar()){ return rewriteVariable(t); }else if(t.getKind() == kind::MINUS){ return rewriteMinus(t, false); diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index a478f3cfb..46b0264ea 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -135,7 +135,7 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet case IMPLIES: // == 3-FINITE VALUE SET : Collect information == if(n[1].getKind() == EQUAL && - n[1][0].getMetaKind() == metakind::VARIABLE && + n[1][0].isVar() && defTrue.find(n) != defTrue.end()){ Node eqTo = n[1][1]; Node rewriteEqTo = Rewriter::rewrite(eqTo); @@ -166,12 +166,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet break; } Node var, c1, c2; - if(n[0][0].getMetaKind() == metakind::VARIABLE && - n[0][1].getMetaKind() == metakind::CONSTANT) { + if(n[0][0].isVar() && + n[0][1].isConst()) { var = n[0][0]; c1 = n[0][1]; - } else if(n[0][1].getMetaKind() == metakind::VARIABLE && - n[0][0].getMetaKind() == metakind::CONSTANT) { + } else if(n[0][1].isVar() && + n[0][0].isConst()) { var = n[0][1]; c1 = n[0][0]; } else { diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index b054f9804..33fc42cea 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -49,7 +49,7 @@ namespace arith { * * variable := n * where - * n.getMetaKind() == metakind::VARIABLE or is foreign + * n.isVar() or is foreign * n.getType() \in {Integer, Real} * * constant := n @@ -244,7 +244,7 @@ public: } bool isMetaKindVariable() const { - return getNode().getMetaKind() == kind::metakind::VARIABLE; + return getNode().isVar(); } bool operator<(const Variable& v) const { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d55860c41..6b7efa1ee 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -741,7 +741,7 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst case kind::LT: case kind::GEQ: case kind::GT: - if (in[0].getMetaKind() == kind::metakind::VARIABLE) { + if (in[0].isVar()) { d_learner.addBound(in); } break; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 5add52d1f..47f3e31db 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -280,11 +280,11 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs { d_ppFacts.push_back(in); d_ppEqualityEngine.assertEquality(in, true, in); - if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + if (in[0].isVar() && !in[1].hasSubterm(in[0])) { outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + if (in[1].isVar() && !in[0].hasSubterm(in[1])) { outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 63b44f7ca..1018289ab 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -366,7 +366,7 @@ bool CircuitPropagator::propagate() { Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl; // Is this an atom - bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE; + bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar(); // If an atom, add to the list for simplification if (atom) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b6dcc6662..2bb4857a3 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -154,12 +154,12 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu switch(in.getKind()) { case kind::EQUAL: - if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + if (in[0].isVar() && !in[1].hasSubterm(in[0])) { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + if (in[1].isVar() && !in[0].hasSubterm(in[1])) { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 896133e46..39e5bc599 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -425,8 +425,8 @@ Node RewriteRule<MultDistribConst>::apply(TNode node) { template<> inline bool RewriteRule<SolveEq>::applies(TNode node) { if (node.getKind() != kind::EQUAL || - (node[0].getMetaKind() == kind::metakind::VARIABLE && !node[1].hasSubterm(node[0])) || - (node[1].getMetaKind() == kind::metakind::VARIABLE && !node[0].hasSubterm(node[1]))) { + (node[0].isVar() && !node[1].hasSubterm(node[0])) || + (node[1].isVar() && !node[0].hasSubterm(node[1]))) { return false; } return true; diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator index 73b88986b..73fc6706d 100755 --- a/src/theory/mkinstantiator +++ b/src/theory/mkinstantiator @@ -143,6 +143,12 @@ function typerule { check_theory_seen } +function construle { + # construle OPERATOR isconst-checking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # rewriter class header lineno=${BASH_LINENO[0]} diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index ffdc1d4c6..0d00b616c 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -118,6 +118,12 @@ function typerule { check_theory_seen } +function construle { + # construle OPERATOR isconst-checking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # rewriter class header class="$1" diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 3607d5232..60ff05d35 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -232,6 +232,12 @@ function typerule { check_theory_seen } +function construle { + # construle OPERATOR isconst-checking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function instantiator { # instantiator class header lineno=${BASH_LINENO[0]} diff --git a/src/theory/model.cpp b/src/theory/model.cpp index feedc0c31..882a3034a 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -157,16 +157,14 @@ void TheoryModel::toStream( std::ostream& out ){ Node TheoryModel::getValue( TNode n ){ Debug("model") << "TheoryModel::getValue " << n << std::endl; - kind::MetaKind metakind = n.getMetaKind(); - //// special case: prop engine handles boolean vars - //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) { + //if(n.isVar() && n.getType().isBoolean()) { // Debug("model") << "-> Propositional variable." << std::endl; // return d_te->getPropEngine()->getValue( n ); //} // special case: value of a constant == itself - if(metakind == kind::metakind::CONSTANT) { + if(n.isConst()) { Debug("model") << "-> Constant." << std::endl; return n; } @@ -174,7 +172,7 @@ Node TheoryModel::getValue( TNode n ){ Node nn; if( n.getNumChildren()>0 ){ std::vector< Node > children; - if( metakind == kind::metakind::PARAMETERIZED ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ Debug("model-debug") << "get operator: " << n.getOperator() << std::endl; children.push_back( n.getOperator() ); } @@ -194,7 +192,7 @@ Node TheoryModel::getValue( TNode n ){ nn = Rewriter::rewrite( nn ); // special case: value of a constant == itself - if(metakind == kind::metakind::CONSTANT) { + if(n.isConst()) { Debug("model") << "-> Theory-interpreted term." << std::endl; return nn; }else{ @@ -444,7 +442,7 @@ void TheoryEngineModelBuilder::buildModel( Model* m ){ while( !eqc_i.isFinished() ){ Node n = *eqc_i; //check if this is constant, if so, we will use it as representative - if( n.getMetaKind()==kind::metakind::CONSTANT ){ + if( n.isConst() ){ const_rep = n; } //theory-specific information needed diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5d7317cbc..fd616948c 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -168,7 +168,7 @@ void FirstOrderModel::toStream(std::ostream& out){ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ //do not print things that have interpretations in model - if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){ + if( !(*eqc_i).isConst() && !hasInterpretedValue( *eqc_i ) ){ out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; } ++eqc_i; diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 9c1c4c89e..7461f3477 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -380,7 +380,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ //if not set already, rewrite and consult model for interpretation if( !setVal ){ val = Rewriter::rewrite( val ); - if( val.getMetaKind()!=kind::metakind::CONSTANT ){ + if( !val.isConst() ){ //FIXME: we cannot do this until we trust all theories collectModelInfo! //val = d_model->getInterpretedValue( val ); //val = d_model->getRepresentative( val ); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 77daa5f53..79e4f6a36 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -66,7 +66,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { switch(mode) { case THEORY_OF_TYPE_BASED: // Constants, variables, 0-ary constructors - if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { + if (node.isVar() || node.isConst()) { return theoryOf(node.getType()); } // Equality is owned by the theory that owns the domain @@ -78,7 +78,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { break; case THEORY_OF_TERM_BASED: // Variables - if (node.getMetaKind() == kind::metakind::VARIABLE) { + if (node.isVar()) { if (theoryOf(node.getType()) != theory::THEORY_BOOL) { // We treat the varibables as uninterpreted return s_uninterpretedSortOwner; @@ -88,7 +88,7 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { } } // Constants - if (node.getMetaKind() == kind::metakind::CONSTANT) { + if (node.isConst()) { // Constants go to the theory of the type return theoryOf(node.getType()); } diff --git a/src/theory/theory.h b/src/theory/theory.h index f3a9db394..397f7cff7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -583,15 +583,15 @@ public: */ virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) { if (in.getKind() == kind::EQUAL) { - if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + if (in[0].isVar() && !in[1].hasSubterm(in[0])) { outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + if (in[1].isVar() && !in[0].hasSubterm(in[1])) { outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } - if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) { + if (in[0].isConst() && in[1].isConst()) { if (in[0] != in[1]) { return PP_ASSERT_STATUS_CONFLICT; } diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 26678f21d..6298ff1ca 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -81,13 +81,13 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) { } if(t.getNumChildren() == 0) { - if(t.getMetaKind() == kind::metakind::CONSTANT) { - Assert(n.getMetaKind() == kind::metakind::CONSTANT); + if(t.isConst()) { + Assert(n.isConst()); Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl; return false; } - Assert(t.getMetaKind() == kind::metakind::VARIABLE && - n.getMetaKind() == kind::metakind::VARIABLE); + Assert(t.isVar() && + n.isVar()); t = find(t); n = find(n); Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl; @@ -218,8 +218,8 @@ Node SymmetryBreaker::normInternal(TNode n) { } else if((*i).getKind() == kind::IFF || (*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i)); - if((*i)[0].getMetaKind() == kind::metakind::VARIABLE || - (*i)[1].getMetaKind() == kind::metakind::VARIABLE) { + if((*i)[0].isVar() || + (*i)[1].isVar()) { d_termEqs[(*i)[0]].insert((*i)[1]); d_termEqs[(*i)[1]].insert((*i)[0]); Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl; @@ -237,8 +237,8 @@ Node SymmetryBreaker::normInternal(TNode n) { case kind::IFF: case kind::EQUAL: - if(n[0].getMetaKind() == kind::metakind::VARIABLE || - n[1].getMetaKind() == kind::metakind::VARIABLE) { + if(n[0].isVar() || + n[1].isVar()) { d_termEqs[n[0]].insert(n[1]); d_termEqs[n[1]].insert(n[0]); Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; |