From 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 12 Apr 2017 16:47:12 -0500 Subject: [PATCH] Add nullary operator metakind. --- src/expr/expr_manager_template.cpp | 4 ++-- src/expr/expr_manager_template.h | 2 +- src/expr/metakind_template.h | 5 +++-- src/expr/mkexpr | 6 ++++++ src/expr/mkkind | 9 +++++++++ src/expr/mkmetakind | 9 +++++++++ src/expr/node.h | 9 +++------ src/expr/node_builder.h | 5 +++-- src/expr/node_manager.cpp | 9 +++++---- src/expr/node_manager.h | 3 ++- src/expr/node_value.cpp | 2 +- src/expr/type_checker_template.cpp | 4 ++-- src/parser/cvc/Cvc.g | 4 ++-- src/parser/smt2/Smt2.g | 8 ++++---- src/smt/smt_engine.cpp | 3 ++- src/theory/sep/kinds | 3 ++- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sep/theory_sep_type_rules.h | 11 +++++++++++ src/theory/sets/kinds | 4 ++-- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 2 +- src/theory/sets/theory_sets_type_rules.h | 14 +++++++++++++- src/theory/theory.cpp | 4 ++-- 23 files changed, 87 insertions(+), 37 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 NodeTemplate::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::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::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::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} diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a5d5febe9..2dc74afdb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1839,7 +1839,7 @@ postfixTerm[CVC4::Expr& f] } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) { f = MK_CONST(CVC4::EmptySet(t)); } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) { - f = EXPR_MANAGER->mkUniqueVar(t, kind::UNIVERSE_SET); + f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET); } else { if(f.getType() != t) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2075,7 +2075,7 @@ simpleTerm[CVC4::Expr& f] { f = MK_CONST(EmptySet(Type())); } | UNIVSET_TOK { //booleanType is placeholder - f = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); + f = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } /* finite set literal */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 33674770d..740e35ba4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1868,12 +1868,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { - expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET); + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET); } else if(f.getKind() == CVC4::kind::SEP_NIL) { //We don't want the nil reference to be a constant: for instance, it //could be of type Int but is not a const rational. However, the //expression has 0 children. So we convert to a SEP_NIL variable. - expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2304,11 +2304,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | UNIVSET_TOK { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } | NILREF_TOK { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here ; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8ae432162..94ff5d9b3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -893,7 +893,8 @@ public: Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl; if(n.getMetaKind() == kind::metakind::CONSTANT || - n.getMetaKind() == kind::metakind::VARIABLE) + n.getMetaKind() == kind::metakind::VARIABLE || + n.getMetaKind() == kind::metakind::NULLARY_OPERATOR) { return n; } diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 358c63f55..b83515d38 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -12,7 +12,7 @@ properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" -variable SEP_NIL "separation nil" +nullaryoperator SEP_NIL "separation nil" operator SEP_EMP 2 "separation empty heap" operator SEP_PTO 2 "points to relation" @@ -25,5 +25,6 @@ typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule typerule SEP_LABEL ::CVC4::theory::sep::SepLabelTypeRule +typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule endtheory diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index ce5c02179..9d064d74d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1226,7 +1226,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node TheorySep::getNilRef( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); if( it==d_nil_ref.end() ){ - Node nil = NodeManager::currentNM()->mkUniqueVar( tn, kind::SEP_NIL ); + Node nil = NodeManager::currentNM()->mkNullaryOperator( tn, kind::SEP_NIL ); setNilRef( tn, nil ); return nil; }else{ diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 23e725a25..25166ca8e 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -99,6 +99,17 @@ struct SepLabelTypeRule { } };/* struct SepLabelTypeRule */ +struct SepNilTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::SEP_NIL); + Assert(check); + TypeNode type = n.getType(false); + return type; + } +};/* struct SepLabelTypeRule */ + + }/* CVC4::theory::sep namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index ab0ca3428..cfe7eb632 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -44,6 +44,7 @@ operator SINGLETON 1 "the set of the single element given as a parameter" operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" operator CARD 1 "set cardinality operator" operator COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)" +nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" @@ -60,14 +61,13 @@ typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule CARD ::CVC4::theory::sets::CardTypeRule typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule +typerule UNIVERSE_SET ::CVC4::theory::sets::UniverseSetTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule -variable UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." - construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5b9f4bf03..57ab8c0cf 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1531,7 +1531,7 @@ Node TheorySetsPrivate::getEmptySet( TypeNode tn ) { Node TheorySetsPrivate::getUnivSet( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_univset.find( tn ); if( it==d_univset.end() ){ - Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET); + Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET); d_univset[tn] = n; return n; }else{ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 9669561a6..8facf1f48 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -306,7 +306,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; }//kind::UNION case kind::COMPLEMENT: { - Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET ); + Node univ = NodeManager::currentNM()->mkNullaryOperator( node[0].getType(), kind::UNIVERSE_SET ); return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) ); } break; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 11f375d5b..541835980 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -174,7 +174,19 @@ struct ComplementTypeRule { } };/* struct ComplementTypeRule */ - +struct UniverseSetTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::UNIVERSE_SET); + // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation + Assert(check); + TypeNode setType = n.getType(false); + if(!setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found"); + } + return setType; + } +};/* struct ComplementTypeRule */ struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2b2ebbf5e..37d65972e 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -271,12 +271,12 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, // 1) x is a variable // 2) x is not in the term t // 3) x : T and t : S, then S <: T - if (in[0].isUninterpretedVar() && !in[1].hasSubterm(in[0]) && + if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){ outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isUninterpretedVar() && !in[0].hasSubterm(in[1]) && + if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){ outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; -- 2.30.2