Rework inst-closure.

8 files changed, 46 insertions, 7 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 81e93ebe6..e536ed7cc 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2002,6 +2002,8 @@ builtinOp[CVC4::Kind& kind]
   
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
   
+  | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
+  
   | FP_TOK        { $kind = CVC4::kind::FLOATINGPOINT_FP; }
   | FP_EQ_TOK     { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
   | FP_ABS_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
@@ -2470,6 +2472,8 @@ DTSIZE_TOK : 'dt.size';
 
 FMFCARD_TOK : 'fmf.card';
 
+INST_CLOSURE_TOK : 'inst-closure';
+
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
 // Other set theory operators are not
 // tokenized and handled directly when
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index a8774440e..793e4a611 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -44,6 +44,8 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
+operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
+
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
@@ -51,6 +53,7 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
 typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
 typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
+typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
 
 # for rewrite rules
 # types...
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bb0b3248d..69271e021 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -111,7 +111,7 @@ Node TermDb::getOperator( Node n ) {
   }
 }
 
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
+void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
   //don't add terms in quantifier bodies
   if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
@@ -152,9 +152,13 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     }
     rec = true;
   }
+  if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
+    d_iclosure_processed.insert( n );
+    rec = true;
+  }
   if( rec ){
     for( size_t i=0; i<n.getNumChildren(); i++ ){
-      addTerm( n[i], added, withinQuant );
+      addTerm( n[i], added, withinQuant, withinInstClosure );
     }
   }
 }
@@ -432,7 +436,8 @@ void TermDb::reset( Theory::Effort effort ){
     Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
     for( unsigned i=0; i<it->second.size(); i++ ){
       Node n = it->second[i];
-      if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+      //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term
+      if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){
         if( !n.getAttribute(NoMatchAttribute()) ){
           if( options::finiteModelFind() ){
             computeModelBasisArgAttribute( n );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index fca2e1261..f841bb2d8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -127,6 +127,8 @@ private:
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
   std::hash_set< Node, NodeHashFunction > d_processed;
+  /** terms processed */
+  std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
 private:
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
@@ -158,7 +160,7 @@ public:
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
   /** add a term to the database */
-  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
+  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
   /** reset (calculate which terms are active) */
   void reset( Theory::Effort effort );
   /** get operator*/
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 89549a71b..12edaa31c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -129,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
+    case kind::INST_CLOSURE:
+      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+      break;
+    case kind::EQUAL:
+      //do nothing
+      break;
     case kind::NOT:
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
           assertExistential( assertion );
           break;
+        case kind::EQUAL:
+          //do nothing
+          break;
+        case kind::INST_CLOSURE:
         default:
           Unhandled(assertion[0].getKind());
           break;
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 2d5cce6ed..3ce0250fe 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -125,6 +125,21 @@ struct QuantifierInstPatternListTypeRule {
   }
 };/* struct QuantifierInstPatternListTypeRule */
 
+struct QuantifierInstClosureTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::INST_CLOSURE );
+    if( check ){
+      TypeNode tn = n[0].getType(check);
+      if( tn.isBoolean() ){
+        throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct QuantifierInstClosureTypeRule */
+
+
 class RewriteRuleTypeRule {
 public:
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3ef5b4a65..52b4fd17d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -497,9 +497,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){
   return Node::null();
 }
 
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
+void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
   std::set< Node > added;
-  getTermDatabase()->addTerm( n, added, withinQuant );
+  getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
   //maybe have triggered instantiations if we are doing eager instantiation
   if( options::eagerInstQuant() ){
     flushLemmas();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2fc479f4c..14e26f2b6 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -297,7 +297,7 @@ public:
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
-  void addTermToDatabase( Node n, bool withinQuant = false );
+  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
   /** debug print equality engine */