Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.

13 files changed, 75 insertions, 29 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 64b321613..e9e6ba857 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
     Parser::addOperator(kind::APPLY_TESTER);
     Parser::addOperator(kind::APPLY_SELECTOR);
+    Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
     break;
 
   case THEORY_STRINGS:
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 4d784c383..63529c2a5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::APPLY_CONSTRUCTOR:
     case kind::APPLY_SELECTOR:
+    case kind::APPLY_SELECTOR_TOTAL:
     case kind::APPLY_TESTER:
       toStream(op, n.getOperator(), depth, types, false);
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ea335f2e5..1250bc659 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_TESTER:
   case kind::APPLY_CONSTRUCTOR:
   case kind::APPLY_SELECTOR:
+  case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
 
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 111324dfa..e46a76ed7 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
       appctorb << (*dt2)[i].getConstructor();
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
       }
       Node appctor = appctorb;
       if(i == 0) {
@@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
         TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
         asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType);
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType);
       }
       Node appctor = appctorb;
       if(i == 0) {
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 37a656555..8cb3fb4a2 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -88,7 +88,7 @@ public:
       const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
       return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
       // These strange (half-tuple-converted) terms can be created by
       // the system if you have something like "foo.1" for a tuple
@@ -118,7 +118,7 @@ public:
       Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
       return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
       // where the selector doesn't match the constructor,
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index bb6fd4373..b222738ae 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -39,6 +39,7 @@ cardinality TESTER_TYPE \
 parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application"
 
 parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
+parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)"
 
 parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
 
@@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \
 
 typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
+typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
 typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule
 typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b00b4148d..0b0f5807c 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -54,7 +54,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
 }
 
@@ -318,6 +318,47 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
   flushPendingFacts();
 }
 
+Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
+  switch( n.getKind() ){
+  case kind::APPLY_SELECTOR: {
+      Node selector = n.getOperator();
+      Expr selectorExpr = selector.toExpr();
+      size_t selectorIndex = Datatype::cindexOf(selectorExpr);
+      const Datatype& dt = Datatype::datatypeOf(selectorExpr);
+      const DatatypeConstructor& c = dt[selectorIndex];
+      Expr tester = c.getTester();
+      Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
+      tst = Rewriter::rewrite( tst );
+      Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
+      Node n_ret;
+      if( tst==NodeManager::currentNM()->mkConst( true ) ){
+        n_ret = sel;
+      }else{
+        if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
+          std::stringstream ss;
+          ss << selector << "_uf";
+          d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+                                            NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
+        }
+        Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
+        if( tst==NodeManager::currentNM()->mkConst( false ) ){
+          n_ret = sk;
+        }else{
+          n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk );
+        }
+      }
+      //n_ret = Rewriter::rewrite( n_ret );
+      Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
+      return n_ret;
+    }
+    break;
+  default:
+    return n;
+    break;
+  }
+  Unreachable();
+}
+
 void TheoryDatatypes::presolve() {
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 }
@@ -332,7 +373,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
   } else if(in.getKind() == kind::RECORD_SELECT) {
     TypeNode t = in[0].getType();
     if(t.hasAttribute(expr::DatatypeRecordAttr())) {
@@ -340,7 +381,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
   }
 
   TypeNode t = in.getType();
@@ -404,7 +445,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
         b << in[1];
         Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
       } else {
-        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]);
         Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
       }
     }
@@ -848,7 +889,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
-  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c );
+  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   Node rr = Rewriter::rewrite( r );
   //if( r!=rr ){
     //Node eq_exp = NodeManager::currentNM()->mkConst(true);
@@ -1075,7 +1116,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
         //eqc->d_selectors = true;
       }
       */
-    }else if( n.getKind() == APPLY_SELECTOR ){
+    }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){
       //we must also record which selectors exist
       Debug("datatypes") << "  Found selector " << n << endl;
       if (n.getType().isBoolean()) {
@@ -1117,7 +1158,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index,
     std::vector< Node > children;
     children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
     for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
-      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n );
+      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
       if( mkVar ){
         TypeNode tn = nc.getType();
         if( dt.isParametric() ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 3a29433f8..2a93878d0 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -166,6 +166,8 @@ private:
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
   std::vector< Node > d_pending_merge;
+  /** expand definition skolem functions */
+  std::map< Node, Node > d_exp_def_skolem;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -208,6 +210,7 @@ public:
 
   void check(Effort e);
   void preRegisterTerm(TNode n);
+  Node expandDefinition(LogicRequest &logicRequest, Node n);
   Node ppRewrite(TNode n);
   void presolve();
   void addSharedTerm(TNode t);
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 527d110e0..d08b511dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule {
 struct DatatypeSelectorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::APPLY_SELECTOR);
+    Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL );
     TypeNode selType = n.getOperator().getType(check);
     Type t = selType[0].toType();
     Assert( t.isDatatype() );
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 164e9e643..b7e624a66 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -92,8 +92,8 @@ instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
 gen-ev \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper.\n\
++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper based on generalizing evaluations.\n\
 \n\
 fmc-interval \n\
 + Same as default, but with intervals for models of integer functions.\n\
@@ -131,9 +131,6 @@ conflict \n\
 partial \n\
 + Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
-partial \n\
-+ Apply QCF to instantiate heuristically as well. \n\
-\n\
 mc \n\
 + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
@@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
 }
 
 inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "gen-ev") {
+  if(optarg == "gen-ev") {
     return MBQI_GEN_EVAL;
-  } else if(optarg ==  "none") {
+  } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg ==  "instgen") {
+  } else if(optarg == "instgen") {
     return MBQI_INST_GEN;
-  } else if(optarg ==  "default" || optarg ==  "fmc") {
+  } else if(optarg == "default" || optarg ==  "fmc") {
     return MBQI_FMC;
-  } else if(optarg ==  "fmc-interval") {
+  } else if(optarg == "fmc-interval") {
     return MBQI_FMC_INTERVAL;
-  } else if(optarg ==  "interval") {
+  } else if(optarg == "interval") {
     return MBQI_INTERVAL;
-  } else if(optarg ==  "trust") {
+  } else if(optarg == "trust") {
     return MBQI_TRUST;
-  } else if(optarg ==  "help") {
+  } else if(optarg == "help") {
     puts(mbqiModeHelp.c_str());
     exit(1);
   } else {
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c0b318f23..e27d438be 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 

 bool MatchGen::isHandledUfTerm( TNode n ) {

   return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||

-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;

+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;

 }

 

 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 6912c9e89..3de12b9c9 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 
 bool Trigger::isAtomicTrigger( Node n ){
   return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;
+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
 }
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 405fceb6f..f207bdb8e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_eeContext->push();
 }
@@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t
 
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
-  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR);
+  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
 }