Front-end support for get-value of sort cardinality, minor fixes for sygus solution reconstruction.

2 files changed, 14 insertions, 0 deletions

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index ccdac32ab..f0b50b778 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -21,4 +21,7 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul
 operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
 typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
 
+operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
+typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
+
 endtheory
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 93fd1dc6f..0040a38c3 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -99,6 +99,17 @@ public:
   }
 };/* class CardinalityConstraintTypeRule */
 
+class CardinalityValueTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw(TypeCheckingExceptionPrivate) {
+    if( check ) {
+      n[0].getType(check);
+    }
+    return nodeManager->integerType();
+  }
+};/* class CardinalityValueTypeRule */
+
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */