From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 25 Nov 2014 15:15:10 +0000 (+0100)
Subject: Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure... 
X-Git-Tag: cvc5-1.0.0~6478^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=29bdfca306a7cd35801c7d9cb3023d78a8b82a1f;p=cvc5.git

Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bdad45606..511b67997 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1620,6 +1620,8 @@ builtinOp[CVC4::Kind& kind]
   | DTSIZE_TOK     { $kind = CVC4::kind::DT_SIZE; }
   
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
+  
+  | INST_CLOSURE_TOK  { $kind = CVC4::kind::INST_CLOSURE; }
 
   // NOTE: Theory operators go here
   ;
@@ -2026,6 +2028,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/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index cfaa6d1ad..9e3fed20a 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -197,16 +197,17 @@ void CandidateGeneratorQEAll::reset( Node eqc ) {
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
-    Node n = (*d_eq);
+    TNode n = (*d_eq);
     ++d_eq;
     if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
-      if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+      TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n );
+      if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 ){
-          n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
+          nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
         }
         d_firstTime = false;
         //an equivalence class with the same type as the pattern, return it
-        return n;
+        return nh;
       }
     }
   }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ffe64beba..bf9409f06 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -248,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
         Node t = getModelTerm( conj->d_candidates[i] );
         model_terms.push_back( t );
-        Trace("cegqi-engine") << t << " ";
+        Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " ";
       }
       Trace("cegqi-engine") << std::endl;
       d_quantEngine->addInstantiation( q, model_terms, false );
@@ -279,7 +279,7 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node
   for( unsigned i=0; i<n.size(); i++ ){
     Node nv = getModelValue( n[i] );
     v.push_back( nv );
-    Trace("cegqi-engine") << nv << " ";
+    Trace("cegqi-engine") << n[i] << " -> " << nv << " ";
     if( nv.isNull() ){
       success = false;
     }
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/options b/src/theory/quantifiers/options
index a428633cc..cac78af46 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions
+option termDbInstClosure --term-db-inst-closure bool :default false
+  only consider inst closure terms for E-matching
  
 endmodule
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a95de086a..34c40c8c4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -111,13 +111,17 @@ 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;
   }
+  bool rec = false;
   if( d_processed.find( n )==d_processed.end() ){
     d_processed.insert(n);
+    if( withinInstClosure ){
+      d_iclosure_processed.insert( n );
+    }
     d_type_map[ n.getType() ].push_back( n );
     //if this is an atomic trigger, consider adding it
     //Call the children?
@@ -137,9 +141,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         d_op_map[op].push_back( n );
         added.insert( n );
 
-        for( size_t i=0; i<n.getNumChildren(); i++ ){
-          addTerm( n[i], added, withinQuant );
-          if( options::eagerInstQuant() ){
+        if( options::eagerInstQuant() ){
+          for( size_t i=0; i<n.getNumChildren(); i++ ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
               for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
@@ -149,10 +152,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
           }
         }
       }
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        addTerm( n[i], added, withinQuant );
-      }
+    }
+    rec = true;
+  }else 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, withinInstClosure );
     }
   }
 }
@@ -317,30 +325,65 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
 }
 
 bool TermDb::hasTermCurrent( Node n ) {
-  //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n );
-  if( options::termDbMode()==TERM_DB_ALL ){
-    return true;
-  }else if( options::termDbMode()==TERM_DB_RELEVANT ){
-    return d_has_map.find( n )!=d_has_map.end();
-  }else{
-    Assert( false );
+  if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
     return false;
+  }else{
+    //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+    if( options::termDbMode()==TERM_DB_ALL ){
+      return true;
+    }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+      return d_has_map.find( n )!=d_has_map.end();
+    }else{
+      Assert( false );
+      return false;
+    }
   }
 }
 
-void TermDb::setHasTerm( Node n ) {
-  if( inst::Trigger::isAtomicTrigger( n ) ){
-    if( d_has_map.find( n )==d_has_map.end() ){
-      d_has_map[n] = true;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        setHasTerm( n[i] );
+Node TermDb::getHasTermEqc( Node r ) {
+  if( hasTermCurrent( r ) ){
+    return r;
+  }else{
+    if( options::termDbInstClosure()  ){
+      std::map< Node, Node >::iterator it = d_has_eqc.find( r );
+      if( it==d_has_eqc.end() ){
+        Node h;
+        eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( h.isNull() && !eqc_i.isFinished() ){
+          TNode n = (*eqc_i);
+          ++eqc_i;
+          if( hasTermCurrent( n ) ){
+            h = n;
+          }
+        }
+        d_has_eqc[r] = h;
+        return h;
+      }else{
+        return it->second;
       }
+    }else{
+      //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
+      return Node::null();
+    }
+  }
+}
+
+void TermDb::setHasTerm( Node n ) {
+  //if( inst::Trigger::isAtomicTrigger( n ) ){
+  if( d_has_map.find( n )==d_has_map.end() ){
+    d_has_map[n] = true;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      setHasTerm( n[i] );
     }
+  }
+    /*
   }else{
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       setHasTerm( n[i] );
     }
   }
+  */
 }
 
 void TermDb::reset( Theory::Effort effort ){
@@ -356,6 +399,7 @@ void TermDb::reset( Theory::Effort effort ){
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT ){
     d_has_map.clear();
+    d_has_eqc.clear();
     eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2b151bb04..cb9f5eeef 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -123,6 +123,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;
@@ -144,6 +146,8 @@ public:
   std::map< Node, std::vector< Node > > d_op_map;
   /** has map */
   std::map< Node, bool > d_has_map;
+  /** map from reps to a term in eqc in d_has_map */
+  std::map< Node, Node > d_has_eqc;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
@@ -152,7 +156,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*/
@@ -176,6 +180,8 @@ public:
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
   /** has term */
   bool hasTermCurrent( Node n );
+  /** get has term eqc */
+  Node getHasTermEqc( Node r );
   
 //for model basis
 private:
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5c68e52a7..de0f98af6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
-  d_numRestarts(0),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
@@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
+void TheoryQuantifiers::computeCareGraph() {
+  //do nothing
+}
+
 void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
   if(fullModel) {
     for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
@@ -126,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: //cannot negate inst closure
         default:
           Unhandled(assertion[0].getKind());
           break;
@@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){
   //}else{
   //  return false;
   //}
-
-  if( !d_out->flipDecision() ){
-    return restart();
-  }
-  return true;
-}
-
-bool TheoryQuantifiers::restart(){
-  static const int restartLimit = 0;
-  if( d_numRestarts==restartLimit ){
-    Debug("quantifiers-flip") << "No more restarts." << std::endl;
-    return false;
-  }else{
-    d_numRestarts++;
-    Debug("quantifiers-flip") << "Do restart." << std::endl;
-    return true;
-  }
+  return false;
 }
 
 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index aace13b24..6d3fa4d46 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -44,17 +44,15 @@ private:
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
-  /** number of restarts */
-  int d_numRestarts;
 
   eq::EqualityEngine* d_masterEqualityEngine;
-
+private:
+  void computeCareGraph();  
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void preRegisterTerm(TNode n);
@@ -73,7 +71,6 @@ public:
 private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
-  bool restart();
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index e44712412..341e656c7 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -126,6 +126,20 @@ 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 04b6c5d16..4dc8df09d 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -472,9 +472,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 199fe79b9..2b466b96b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -290,7 +290,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 */