diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
commit | 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 (patch) | |
tree | c30f7f17ae963e3f51cef111b2d549eacff1a852 /src/expr | |
parent | e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 (diff) |
Add nullary operator metakind.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 5 | ||||
-rwxr-xr-x | src/expr/mkexpr | 6 | ||||
-rwxr-xr-x | src/expr/mkkind | 9 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 9 | ||||
-rw-r--r-- | src/expr/node.h | 9 | ||||
-rw-r--r-- | src/expr/node_builder.h | 5 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 9 | ||||
-rw-r--r-- | src/expr/node_manager.h | 3 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/type_checker_template.cpp | 4 |
12 files changed, 46 insertions, 21 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 470a6eeca..82cabbd3e 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -946,9 +946,9 @@ Expr ExprManager::mkBoundVar(Type type) { return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); } -Expr ExprManager::mkUniqueVar(Type type, Kind k){ +Expr ExprManager::mkNullaryOperator(Type type, Kind k){ NodeManagerScope nms(d_nodeManager); - Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); + Node n = d_nodeManager->mkNullaryOperator(*type.d_typeNode, k); return n.toExpr(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index ed9247e5e..9e962d970 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -549,7 +549,7 @@ public: /** * Create unique variable of type */ - Expr mkUniqueVar( Type type, Kind k); + Expr mkNullaryOperator( Type type, Kind k); /** Get a reference to the statistics registry for this ExprManager */ Statistics getStatistics() const throw(); diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 1c03cf407..2dcf24b09 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -98,7 +98,8 @@ enum MetaKind_t { VARIABLE, /**< special node kinds: no operator */ OPERATOR, /**< operators that get "inlined" */ PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */ - CONSTANT /**< constants */ + CONSTANT, /**< constants */ + NULLARY_OPERATOR /**< nullary operator */ };/* enum MetaKind_t */ }/* CVC4::kind::metakind namespace */ @@ -338,7 +339,7 @@ ${metakind_operatorKinds} }/* CVC4::kind namespace */ -#line 342 "${template}" +#line 343 "${template}" namespace theory { diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 963e297b4..60ee758d8 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -248,6 +248,12 @@ template <> $2 const & Expr::getConst() const { case $1: return to->mkConst(n.getConst< $2 >());" } +function nullaryoperator { + # nullaryoperator K ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function check_theory_seen { if $seen_endtheory; then echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 diff --git a/src/expr/mkkind b/src/expr/mkkind index 271c8bc7a..2b1901f5d 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -239,6 +239,15 @@ function constant { register_kind "$1" 0 "$5" } +function nullaryoperator { + # nullaryoperator K ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_kind "$1" 0 "$2" +} + function register_sort { id=$1 cardinality=$2 diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 3e06a88a5..19e6e2244 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -302,6 +302,15 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { " } +function nullaryoperator { + # nullaryoperator K ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_metakind NULLARY_OPERATOR "$1" 0 +} + function registerOperatorToKind { operatorKind=$1 applyKind=$2 diff --git a/src/expr/node.h b/src/expr/node.h index 31721b2ef..6d98b940b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -464,12 +464,6 @@ public: assertTNodeNotExpired(); return getMetaKind() == kind::metakind::VARIABLE; } - inline bool isUninterpretedVar() const { - assertTNodeNotExpired(); - return getMetaKind() == kind::metakind::VARIABLE && - getKind() != kind::UNIVERSE_SET && - getKind() != kind::SEP_NIL; - } inline bool isClosure() const { assertTNodeNotExpired(); @@ -1259,6 +1253,9 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { case kind::metakind::CONSTANT: IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind"); + case kind::metakind::NULLARY_OPERATOR: + IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind"); + default: Unhandled(mk); } diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index d92524a19..7cb14ed5a 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -933,7 +933,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { // file comments at the top of this file. // Case 0: If a VARIABLE - if(getMetaKind() == kind::metakind::VARIABLE) { + if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) { /* 0. If a VARIABLE, treat similarly to 1(b), except that we know * there are no children (no reference counts to reason about), * and we don't keep VARIABLE-kinded Nodes in the NodeManager @@ -1123,7 +1123,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { // file comments at the top of this file. // Case 0: If a VARIABLE - if(getMetaKind() == kind::metakind::VARIABLE) { + if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) { /* 0. If a VARIABLE, treat similarly to 1(b), except that we know * there are no children (no reference counts to reason about), * and we don't keep VARIABLE-kinded Nodes in the NodeManager @@ -1336,6 +1336,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const if( d_nm->getOptions()[options::earlyTypeChecking] ) { kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE + && mk != kind::metakind::NULLARY_OPERATOR && mk != kind::metakind::CONSTANT ) { d_nm->getType(n, true); } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index ebf78f541..2a819935d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -315,7 +315,7 @@ void NodeManager::reclaimZombies() { // remove from the pool kind::MetaKind mk = nv->getMetaKind(); - if(mk != kind::metakind::VARIABLE) { + if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) { poolRemove(nv); } @@ -787,14 +787,15 @@ Node NodeManager::mkBooleanTermVariable() { return n; } -Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { +Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ Node n = NodeBuilder<0>(this, k); n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + //should type check it + //n.setAttribute(TypeCheckedAttr(), true); d_unique_vars[k][type] = n; - Assert( n.getMetaKind() == kind::metakind::VARIABLE ); + Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR ); return n; }else{ return it->second; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d2b45a636..3aa826b49 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -536,7 +536,7 @@ public: Node mkAbstractValue(const TypeNode& type); /** make unique (per Type,Kind) variable. */ - Node mkUniqueVar(const TypeNode& type, Kind k); + Node mkNullaryOperator(const TypeNode& type, Kind k); /** * Create a constant of type T. It will have the appropriate @@ -1240,6 +1240,7 @@ inline bool NodeManager::hasOperator(Kind k) { case kind::metakind::INVALID: case kind::metakind::VARIABLE: + case kind::metakind::NULLARY_OPERATOR: return false; case kind::metakind::OPERATOR: diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 40649ef2c..f8de8c0c8 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -60,7 +60,7 @@ void NodeValue::printAst(std::ostream& out, int ind) const { indent(out, ind); out << '('; out << getKind(); - if (getMetaKind() == kind::metakind::VARIABLE) { + if (getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR ) { out << ' ' << getId(); } else if (getMetaKind() == kind::metakind::CONSTANT) { out << ' '; diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 8ed894a22..757a32529 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -61,7 +61,7 @@ ${typerules} bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) throw (AssertionException) { - Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED); + Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); switch(n.getKind()) { ${construles} @@ -78,7 +78,7 @@ ${construles} bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n) throw (AssertionException) { - Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED); + Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); switch(n.getKind()) { ${neverconstrules} |