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

7 files changed, 63 insertions, 23 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8dce0b639..d2409ba15 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2214,6 +2214,7 @@ builtinOp[CVC4::Kind& kind]
 
   | DTSIZE_TOK     { $kind = CVC4::kind::DT_SIZE; }
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
+  | FMFCARDVAL_TOK    { $kind = CVC4::kind::CARDINALITY_VALUE; }
   | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
   
   // NOTE: Theory operators no longer go here, add to smt2.cpp. Only
@@ -2613,6 +2614,7 @@ REALLCHAR_TOK : 're.allchar';
 DTSIZE_TOK : 'dt.size';
 
 FMFCARD_TOK : 'fmf.card';
+FMFCARDVAL_TOK : 'fmf.card.val';
 
 INST_CLOSURE_TOK : 'inst-closure';
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b9b309d4a..56ad9c35a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -446,6 +446,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::REGEXP_EMPTY: out << "re.nostr "; break;
   case kind::REGEXP_SIGMA: out << "re.allchar "; break;
 
+  case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
+  case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
+  
     // bv theory
   case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break;
   case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 914c0614f..822baaaaf 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -865,32 +865,42 @@ struct sortSiInstanceIndices {
   }
 };
 
-/*
-Node removeBooleanIte( Node n ){
+
+Node CegConjectureSingleInv::postProcessSolution( Node n ){
+  /*
+  ////remove boolean ITE (not allowed for sygus comp 2015)
   if( n.getKind()==ITE && n.getType().isBoolean() ){
-    Node n1 = removeBooleanIte( n[1] );
-    Node n2 = removeBooleanIte( n[2] );
+    Node n1 = postProcessSolution( n[1] );
+    Node n2 = postProcessSolution( n[2] );
     return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
                                                  NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
   }else{
-    bool childChanged = false;
-    std::vector< Node > children;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node nn = removeBooleanIte( n[i] );
-      children.push_back( nn );
-      childChanged = childChanged || nn!=n[i];
-    }
-    if( childChanged ){
-      if( n.hasOperator() ){
-        children.insert( children.begin(), n.getOperator() );
-      }
-      return NodeManager::currentNM()->mkNode( n.getKind(), children );
-    }else{
-      return n;
+    */
+  bool childChanged = false;
+  Kind k = n.getKind();
+  if( n.getKind()==INTS_DIVISION_TOTAL ){
+    k = INTS_DIVISION;
+    childChanged = true;
+  }else if( n.getKind()==INTS_MODULUS_TOTAL ){
+    k = INTS_MODULUS;
+    childChanged = true;
+  }
+  std::vector< Node > children;
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    Node nn = postProcessSolution( n[i] );
+    children.push_back( nn );
+    childChanged = childChanged || nn!=n[i];
+  }
+  if( childChanged ){
+    if( n.hasOperator() && k==n.getKind() ){
+      children.insert( children.begin(), n.getOperator() );
     }
+    return NodeManager::currentNM()->mkNode( k, children );
+  }else{
+    return n;
   }
 }
-*/
+
 
 Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
   Assert( d_sol!=NULL );
@@ -994,9 +1004,12 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
   }else{
-    ////remove boolean ITE (not allowed for sygus comp 2015)
-    //d_solution = removeBooleanIte( d_solution );
-    //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl;
+    Trace("csi-sol") << "Post-process solution..." << std::endl;
+    Node prev = d_solution;
+    d_solution = postProcessSolution( d_solution );
+    if( prev!=d_solution ){ 
+      Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
+    }
   }
 
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 0bdf246f0..99dcaabb9 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -72,6 +72,7 @@ private:
   void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
   //constructing solution
   Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
+  Node postProcessSolution( Node n );
 private:
   //map from programs to variables in single invocation property
   std::map< Node, Node > d_single_inv_map;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c62a0dd4a..44e4193eb 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -88,11 +88,14 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
   //for now, we only handle cardinalities for uninterpreted sorts
   if( tn.isSort() ){
     if( d_rep_set.hasType( tn ) ){
+      Debug("model-getvalue-debug") << "Get cardinality sort, #rep : " << d_rep_set.getNumRepresentatives( tn ) << std::endl;
       return Cardinality( d_rep_set.getNumRepresentatives( tn ) );
     }else{
-      return Cardinality( CardinalityUnknown() );
+      Debug("model-getvalue-debug") << "Get cardinality sort, unconstrained, return 1." << std::endl;
+      return Cardinality( 1 );
     }
   }else{
+      Debug("model-getvalue-debug") << "Get cardinality other sort, unknown." << std::endl;
     return Cardinality( CardinalityUnknown() );
   }
 }
@@ -191,7 +194,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       ret = Rewriter::rewrite(ret);
       Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
       if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) {
+        Debug("model-getvalue-debug") << "get cardinality constraint " << ret[0].getType() << std::endl;
         ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
+      }else if(ret.getKind() == kind::CARDINALITY_VALUE) {
+        Debug("model-getvalue-debug") << "get cardinality value " << ret[0].getType() << std::endl;
+        ret = NodeManager::currentNM()->mkConst(Rational(getCardinality(ret[0].getType().toType()).getFiniteCardinality()));
       }
       d_modelCache[n] = ret;
       return ret;
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 */