diff options
32 files changed, 162 insertions, 75 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index c70fed889..f88914fd2 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -114,9 +114,9 @@ namespace expr { static Node exportConstant(TNode n, NodeManager* to); Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { - if(n.getMetaKind() == kind::metakind::CONSTANT) { + if(n.isConst()) { return exportConstant(n, NodeManager::fromExprManager(to)); - } else if(n.getMetaKind() == kind::metakind::VARIABLE) { + } else if(n.isVar()) { Expr from_e(from, new Node(n)); Expr& to_e = vmap.d_typeMap[from_e]; if(! to_e.isNull()) { @@ -522,7 +522,7 @@ ${getConst_implementations} namespace expr { static Node exportConstant(TNode n, NodeManager* to) { - Assert(n.getMetaKind() == kind::metakind::CONSTANT); + Assert(n.isConst()); switch(n.getKind()) { ${exportConstant_cases} diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 8b21814dc..28a47d84d 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -62,6 +62,9 @@ mkConst_instantiations= mkConst_implementations= exportConstant_cases= +typerules= +construles= + seen_theory=false seen_theory_builtin=false @@ -139,6 +142,16 @@ function typerule { " } +function construle { + # isconst OPERATOR isconst-checking-class + lineno=${BASH_LINENO[0]} + check_theory_seen + construles="${construles} + case kind::$1: + return $2::computeIsConst(nodeManager, n); +" +} + function sort { # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} @@ -262,6 +275,7 @@ for var in \ exportConstant_cases \ typechecker_includes \ typerules \ + construles \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done diff --git a/src/expr/mkkind b/src/expr/mkkind index 89e77754f..88c28d4b9 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -142,6 +142,12 @@ function typerule { check_theory_seen } +function construle { + # construle OPERATOR isconst-checking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 654a1f94f..5608d2972 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -117,6 +117,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/expr/node.h b/src/expr/node.h index b0fda3354..cada443a1 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -442,10 +442,7 @@ public: * Returns true if this node represents a constant * @return true if const */ - inline bool isConst() const { - assertTNodeNotExpired(); - return getMetaKind() == kind::metakind::CONSTANT; - } + inline bool isConst() const; /** * Returns true if this node represents a constant @@ -917,6 +914,7 @@ inline std::ostream& operator<<(std::ostream& out, #include "expr/attribute.h" #include "expr/node_manager.h" +#include "expr/type_checker.h" namespace CVC4 { @@ -1263,6 +1261,36 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const return NodeManager::currentNM()->getType(*this, check); } +/** Is this node constant? (and has that been computed yet?) */ +struct IsConstTag { }; +struct IsConstComputedTag { }; +typedef expr::Attribute<IsConstTag, bool> IsConstAttr; +typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr; + +template <bool ref_count> +inline bool +NodeTemplate<ref_count>::isConst() const { + assertTNodeNotExpired(); + if(isNull()) { + return false; + } + switch(getMetaKind()) { + case kind::metakind::CONSTANT: + return true; + case kind::metakind::VARIABLE: + return false; + default: + if(getAttribute(IsConstComputedAttr())) { + return getAttribute(IsConstAttr()); + } else { + bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this); + const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval); + const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true); + return bval; + } + } +} + template <bool ref_count> inline Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 501a0f4fd..ce6a91483 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -54,8 +54,8 @@ class TypeChecker; // Definition of an attribute for the variable name. // TODO: hide this attribute behind a NodeManager interface. namespace attr { - struct VarNameTag {}; - struct SortArityTag {}; + struct VarNameTag { }; + struct SortArityTag { }; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; @@ -230,8 +230,8 @@ class NodeManager { };/* struct NodeManager::NVStorage<N> */ // attribute tags - struct TypeTag {}; - struct TypeCheckedTag; + struct TypeTag { }; + struct TypeCheckedTag { }; // NodeManager's attributes. These aren't exposed outside of this // class; use the getters. diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 0c8093469..f198e33ca 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -18,11 +18,12 @@ #include "cvc4_private.h" +// ordering dependence +#include "expr/node.h" + #ifndef __CVC4__EXPR__TYPE_CHECKER_H #define __CVC4__EXPR__TYPE_CHECKER_H -#include "expr/node.h" - namespace CVC4 { namespace expr { @@ -32,6 +33,9 @@ public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check = false) throw (TypeCheckingExceptionPrivate, AssertionException); + static bool computeIsConst(NodeManager* nodeManager, TNode n) + throw (AssertionException); + };/* class TypeChecker */ }/* CVC4::expr namespace */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 2791376b5..9359a6ab8 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -62,5 +62,22 @@ ${typerules} }/* TypeChecker::computeType */ +bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) + throw (AssertionException) { + + Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED); + + switch(n.getKind()) { +${construles} + +#line 74 "${template}" + + default:; + } + + return false; + +}/* TypeChecker::computeIsConst */ + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 664ea58fc..564769207 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -81,7 +81,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } // variables - if(n.getMetaKind() == kind::metakind::VARIABLE) { + if(n.isVar()) { string s; if(n.getAttribute(expr::VarNameAttr(), s)) { out << s; @@ -102,7 +102,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo } // constants - if(n.getMetaKind() == kind::metakind::CONSTANT) { + if(n.isConst()) { switch(n.getKind()) { case kind::BITVECTOR_TYPE: out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")"; diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 81183182d..580bec63c 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -53,12 +53,12 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { // the count beyond the threshold already, we've done the same // for all subexpressions, so it isn't useful to traverse and // increment again (they'll be dagified anyway). - return current.getMetaKind() == kind::metakind::VARIABLE || - current.getMetaKind() == kind::metakind::CONSTANT || + return current.isVar() || + current.isConst() || ( ( current.getKind() == kind::NOT || current.getKind() == kind::UMINUS ) && - ( current[0].getMetaKind() == kind::metakind::VARIABLE || - current[0].getMetaKind() == kind::metakind::CONSTANT ) ) || + ( current[0].isVar() || + current[0].isConst() ) ) || current.getKind() == kind::SORT_TYPE || d_nodeCount[current] > d_threshold; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 892de551c..dcb37d3d9 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -80,7 +80,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } // variable - if(n.getMetaKind() == kind::metakind::VARIABLE) { + if(n.isVar()) { string s; if(n.getAttribute(expr::VarNameAttr(), s)) { out << s; @@ -102,7 +102,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } // constant - if(n.getMetaKind() == kind::metakind::CONSTANT) { + if(n.isConst()) { switch(n.getKind()) { case kind::TYPE_CONSTANT: switch(n.getConst<TypeConstant>()) { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b498f1e40..c5345c5a7 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -150,7 +150,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { } if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL && - n.getMetaKind() != kind::metakind::VARIABLE ) { + !n.isVar() ) { // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 272bfe04e..6b7ca8d2f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1743,7 +1743,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { ( d_definedFunctions->find(n.getOperator()) != d_definedFunctions->end() ) && n.getNumChildren() == 0 ) || - n.getMetaKind() == kind::metakind::VARIABLE ), e, + n.isVar() ), e, "expected variable or defined-function application " "in addToAssignment(),\ngot %s", e.toString().c_str() ); if(!options::produceAssignments()) { @@ -1809,7 +1809,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) Assert((*i).getNumChildren() == 0); v.push_back((*i).getOperator().toString()); } else { - Assert((*i).getMetaKind() == kind::metakind::VARIABLE); + Assert((*i).isVar()); v.push_back((*i).toString()); } v.push_back(resultNode.toString()); 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; diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp index 862f1e5fc..e21aadf05 100644 --- a/src/util/boolean_simplification.cpp +++ b/src/util/boolean_simplification.cpp @@ -37,7 +37,7 @@ BooleanSimplification::push_back_associative_commute_recursive } }else{ if(negateNode){ - if(child.getMetaKind() == kind::metakind::CONSTANT) { + if(child.isConst()) { if((k == kind::AND && child.getConst<bool>()) || (k == kind::OR && !child.getConst<bool>())) { buffer.clear(); @@ -48,7 +48,7 @@ BooleanSimplification::push_back_associative_commute_recursive buffer.push_back(negate(child)); } }else{ - if(child.getMetaKind() == kind::metakind::CONSTANT) { + if(child.isConst()) { if((k == kind::OR && child.getConst<bool>()) || (k == kind::AND && !child.getConst<bool>())) { buffer.clear(); diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index b3dffa475..a5a646231 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -187,7 +187,7 @@ public: base = base[0]; polarity = !polarity; } - if(n.getMetaKind() == kind::metakind::CONSTANT) { + if(n.isConst()) { return NodeManager::currentNM()->mkConst(!n.getConst<bool>()); } if(polarity){ |