Add nullary operator metakind.

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<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}
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;