From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 26 Aug 2016 21:27:57 +0000 (-0500)
Subject: Basic support for EPR+CBQI. Minor cleanup.
X-Git-Tag: cvc5-1.0.0~6028^2~75
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ac5255577a07e3bef123908d55003f89dea7619;p=cvc5.git

Basic support for EPR+CBQI. Minor cleanup.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cb4f292c1..9f8f088de 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -306,6 +306,9 @@ option cbqiLitDepend --cbqi-lit-dep bool :default false
 option cbqiInnermost --cbqi-innermost bool :default false
  only process innermost quantified formulas in counterexample-based quantifier instantiation
  
+option quantEpr --quant-epr bool :default false
+ infer whether in effectively propositional fragment, use for cbqi
+ 
 ### local theory extensions options 
 
 option localTheoryExt --local-t-ext bool :default false
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 21df4c712..b9a415e46 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -82,6 +82,35 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
           registerCounterexampleLemma( q, lem );
           
+          //totality lemmas for EPR
+          QuantEPR * qepr = d_quantEngine->getQuantEPR();
+          if( qepr!=NULL ){   
+            for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+              TypeNode tn = q[0][i].getType();
+              if( tn.isSort() ){
+                if( qepr->isEPR( tn ) ){
+                  //add totality lemma
+                  std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
+                  if( itc!=qepr->d_consts.end() ){
+                    Assert( !itc->second.empty() );
+                    Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
+                    std::vector< Node > disj;
+                    for( unsigned j=0; j<itc->second.size(); j++ ){
+                      disj.push_back( ic.eqNode( itc->second[j] ) );
+                    }
+                    Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
+                    Trace("cbqi") << "EPR totality lemma : " << tlem << std::endl;
+                    d_quantEngine->getOutputChannel().lemma( tlem );
+                  }else{
+                    Assert( false );
+                  }                  
+                }else{
+                  Assert( !options::cbqiAll() );
+                }
+              }
+            }
+          }      
+          
           //compute dependencies between quantified formulas
           if( options::cbqiLitDepend() || options::cbqiInnermost() ){
             std::vector< Node > ics;
@@ -243,21 +272,28 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
   }
   return false;
 }
-bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+  int hmin = 1;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){
-      if( options::cbqiSplx() ){
-        return true;
-      }else{
-        //datatypes supported in new implementation
-        if( !tn.isDatatype() ){
-          return true;
-        }
+    int handled = -1;
+    if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
+      handled = 0;
+    }else if( tn.isDatatype() ){
+      handled = !options::cbqiSplx() ? 0 : -1;
+    }else if( tn.isSort() ){
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){
+        handled = qepr->isEPR( tn ) ? 1 : -1;
       }
     }
+    if( handled==-1 ){
+      return -1;
+    }else if( handled<hmin ){
+      hmin = handled;
+    }
   }
-  return false;
+  return hmin;
 }
 
 bool InstStrategyCbqi::doCbqi( Node q ){
@@ -274,11 +310,17 @@ bool InstStrategyCbqi::doCbqi( Node q ){
         if( options::cbqiAll() ){
           ret = true;
         }else{
-          //if quantifier has a non-arithmetic variable, then do not use cbqi
+          //if quantifier has a non-handled variable, then do not use cbqi
           //if quantifier has an APPLY_UF term, then do not use cbqi
           //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
-          std::map< Node, bool > visited;
-          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
+          int ncbqiv = hasNonCbqiVariable( q );
+          if( ncbqiv==1 ){
+            //all variables imply this will be handled regardless of body (e.g. for EPR)
+            ret = true;
+          }else if( ncbqiv==0 ){
+            std::map< Node, bool > visited;
+            ret = !hasNonCbqiOperator( q[1], visited );
+          }
         }
       }
     }
@@ -727,6 +769,16 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
     if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
       return true;
     }else{
+      TypeNode tn = n.getType();
+      if( tn.isSort() ){
+        QuantEPR * qepr = d_quantEngine->getQuantEPR();
+        if( qepr!=NULL ){
+          //legal if in the finite set of constants of type tn
+          if( qepr->isEPRConstant( tn, n ) ){
+            return true;
+          }
+        }
+      }
       //only legal if current quantified formula contains n
       return TermDb::containsTerm( d_curr_quant, n );
     }
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 20d872c36..18931f8f6 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -52,7 +52,7 @@ protected:
   /** has added cbqi lemma */
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
   /** helper functions */
-  bool hasNonCbqiVariable( Node q );
+  int hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
   /** process functions */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b9aab0236..8ba6aa611 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -419,3 +419,71 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol,
   }
 }
 
+void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) {
+  int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
+  if( visited[vindex].find( n )==visited[vindex].end() ){
+    visited[vindex][n] = true;
+    if( n.getKind()==FORALL ){
+      if( beneathQuant || !hasPol || !pol ){
+        for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+          d_non_epr[n[0][i].getType()] = true;
+        }
+      }else{
+        beneathQuant = true;
+      }
+    }
+    TypeNode tn = n.getType();
+    
+    if( n.getNumChildren()>0 ){
+      if( tn.isSort() ){
+        if( d_non_epr.find( tn )==d_non_epr.end() ){
+          Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl;
+          d_non_epr[tn] = true;
+        }
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+        registerNode( n[i], visited, beneathQuant, newHasPol, newPol );
+      }
+    }else if( tn.isSort() ){
+      if( n.getKind()==BOUND_VARIABLE ){
+        if( d_consts.find( tn )==d_consts.end() ){
+          //mark that at least one constant must occur
+          d_consts[tn].clear();
+        }
+      }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){
+        d_consts[tn].push_back( n );
+      }
+    }
+  }
+}
+
+void QuantEPR::registerAssertion( Node assertion ) {
+  std::map< int, std::map< Node, bool > > visited;
+  registerNode( assertion, visited, false, true, true );
+}
+
+void QuantEPR::finishInit() {
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){
+    if( d_non_epr.find( it->first )!=d_non_epr.end() ){
+      it->second.clear();
+    }else{
+      if( it->second.empty() ){
+        it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) );
+      }
+      if( Trace.isOn("quant-epr") ){
+        Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Trace("quant-epr") << "  " << it->second[i] << std::endl;
+        }
+      }
+    }
+  }
+}
+
+bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) {
+  return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end();
+}
+
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 79cdae437..049644ffb 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -149,7 +149,7 @@ public:
 };
 
 
-class EqualityQuery : public QuantifiersUtil{
+class EqualityQuery : public QuantifiersUtil {
 public:
   EqualityQuery(){}
   virtual ~EqualityQuery(){};
@@ -171,6 +171,30 @@ public:
   virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
 };/* class EqualityQuery */
 
+class QuantEPR
+{
+private:
+  void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol );
+  /** non-epr */
+  std::map< TypeNode, bool > d_non_epr;
+public:
+  QuantEPR(){}
+  virtual ~QuantEPR(){}
+  /** constants per type */
+  std::map< TypeNode, std::vector< Node > > d_consts;
+  /* reset */
+  //bool reset( Theory::Effort e ) {}
+  /** identify */
+  //std::string identify() const { return "QuantEPR"; }
+  /** register assertion */
+  void registerAssertion( Node assertion );
+  /** finish init */
+  void finishInit();
+  /** is EPR */
+  bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; }
+  /** is EPR constant */
+  bool isEPRConstant( TypeNode tn, Node k ); 
+};
 
 }
 }
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 2b90520fd..8bc8e1f04 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -72,6 +72,7 @@ public:
   RDomain * getRDomain( Node n, int i, bool getParent = true );
 };/* class RelevantDomain */
 
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d3a5e178f..5d8564adf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -3125,7 +3125,6 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           std::string name = std::string( str.begin() + found +1, str.end() );
           out << name;
         }else{
-          Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl;
           out << op;
         }
         if( n.getNumChildren()>0 ){
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index f6ee639b6..e97a76ce6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -89,7 +89,10 @@ void TheoryQuantifiers::presolve() {
 }
 
 void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) {
-  getQuantifiersEngine()->ppNotifyAssertions( assertions );
+  Trace("quantifiers-presolve") << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
+  if( getQuantifiersEngine() ){
+    getQuantifiersEngine()->ppNotifyAssertions( assertions );
+  }
 }
 
 Node TheoryQuantifiers::getValue(TNode n) {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0c7deb85d..603f6f5fd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -112,6 +112,17 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
     d_quant_rel = NULL;
   }
 
+  if( options::quantEpr() ){
+    if( !options::incrementalSolving() ){
+      d_qepr = new QuantEPR;
+    }else{
+      d_qepr = NULL;
+    }
+  }else{
+    d_qepr = NULL;
+  }
+
+
   d_qcf = NULL;
   d_sg_gen = NULL;
   d_inst_engine = NULL;
@@ -152,6 +163,7 @@ QuantifiersEngine::~QuantifiersEngine(){
 
   delete d_alpha_equiv;
   delete d_builder;
+  delete d_qepr;
   delete d_rr_engine;
   delete d_bint;
   delete d_model_engine;
@@ -275,7 +287,7 @@ void QuantifiersEngine::finishInit(){
     d_modules.push_back( d_fs );
     needsRelDom = true;
   }
-
+ 
   if( needsRelDom ){
     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
     d_util.push_back( d_rel_dom );
@@ -344,9 +356,18 @@ void QuantifiersEngine::presolve() {
 }
 
 void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) {
-  if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
+  Trace("quant-engine-proc") << "ppNotifyAssertions in QE" << std::endl;
+  if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){
     for( unsigned i=0; i<assertions.size(); i++ ) {
-      setInstantiationLevelAttr( assertions[i], 0 );
+      if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
+        setInstantiationLevelAttr( assertions[i], 0 );
+      }
+      if( d_qepr!=NULL ){
+        d_qepr->registerAssertion( assertions[i] );
+      }
+    }
+    if( d_qepr!=NULL ){
+      d_qepr->finishInit(); 
     }
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7b4453330..7f0785340 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -113,6 +113,9 @@ private:
   quantifiers::AlphaEquivalence * d_alpha_equiv;
   /** model builder */
   quantifiers::QModelBuilder* d_builder;
+  /** utility for effectively propositional logic */
+  QuantEPR * d_qepr;
+private:
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -228,6 +231,8 @@ public:
   QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
   /** get the model builder */
   quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
+  /** get utility for EPR */
+  QuantEPR* getQuantEPR() { return d_qepr; }
 public:  //modules
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7caa1cbb1..4526300f8 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -905,7 +905,6 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
         }
         for (unsigned c = 0; c < currentPairs.size(); ++ c) {
           Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
-          Trace("ajr-temp") << currentPairs[c].first << ", " << currentPairs[c].second << std::endl;
           addCarePair(currentPairs[c].first, currentPairs[c].second);
         }
       }