Minor cleanup and fixes for conflict-based instantiation (#2123)

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8f179531b994b0e2678442a98f65d243096b925d..6f9d3102425b4c57d6a622480831728b062818f0 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -331,12 +331,6 @@ prop-eq \n\
 conflict \n\
 + Apply QCF algorithm to find conflicts only.\n\
 \n\
-partial \n\
-+ Apply QCF algorithm 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\
 ";
 
 const std::string OptionsHandler::s_userPatModeHelp = "\
@@ -716,8 +710,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
     return theory::quantifiers::QCF_CONFLICT_ONLY;
   } else if(optarg ==  "default" || optarg == "prop-eq") {
     return theory::quantifiers::QCF_PROP_EQ;
-  } else if(optarg == "partial") {
-    return theory::quantifiers::QCF_PARTIAL;
   } else if(optarg ==  "help") {
     puts(s_qcfModeHelp.c_str());
     exit(1);

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f7521ff4a4b2cc9f49a3e3eaa7dd6580bccb5dfb..3b2a650abc077ae2de742227562de71394118ced 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -253,28 +253,6 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) {
   d_curr_var_deq.clear();
   d_tconstraints.clear();
   
-  //add built-in variable constraints
-  for( unsigned r=0; r<2; r++ ){
-    for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
-         it != d_var_constraint[r].end(); ++it ){
-      for( unsigned j=0; j<it->second.size(); j++ ){
-        Node rr = it->second[j];
-        if( !isVar( rr ) ){
-          rr = p->getRepresentative( rr );
-        }
-        if( addConstraint( p, it->first, rr, r==0 )==-1 ){
-          d_var_constraint[0].clear();
-          d_var_constraint[1].clear();
-          //quantified formula is actually equivalent to true
-          Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;
-          d_mg->d_children.clear();
-          d_mg->d_n = NodeManager::currentNM()->mkConst( true );
-          d_mg->d_type = MatchGen::typ_ground;
-          return false;
-        }
-      }
-    }
-  }
   d_mg->reset_round( p );
   for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
     it->second->reset_round( p );
@@ -664,24 +642,6 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
     }else{
       return chEnt;
     }
-/*
-    if( chEnt ){
-      //check if it is entailed
-      Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
-      std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
-      ++(p->d_statistics.d_entailment_checks);
-      Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
-      if( !et.first ){
-        Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
-        return false;
-      }else{
-        return true;
-      }
-    }else{
-      Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
-      return true;
-    }
-*/
   }else{
     Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
     return true;
@@ -1287,12 +1247,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     TNode f = getMatchOperator( p, d_n );
     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
     TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
-    if( qni!=NULL ){
-      d_qn.push_back( qni );
-    }else{
+    if (qni == nullptr || qni->empty())
+    {
       //inform irrelevant quantifiers
       p->setIrrelevantFunction( f );
     }
+    else
+    {
+      d_qn.push_back(qni);
+    }
     d_matched_basis = false;
   }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
     for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
@@ -1526,7 +1489,9 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     d_wasSet = success;
     return success;
-  }else if( d_type==typ_formula || d_type==typ_ite_var ){
+  }
+  else if (d_type == typ_formula)
+  {
     bool success = false;
     if( d_child_counter<0 ){
       if( d_child_counter<-1 ){
@@ -1597,7 +1562,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
               d_child_counter++;
               getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
             }else{
-              if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){
+              if (d_child_counter == 4)
+              {
                 d_child_counter = -1;
               }else{
                 d_child_counter +=2;
@@ -1630,84 +1596,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
   return false;
 }
 
-bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {
-  if( d_type==typ_eq ){
-    Node n[2];
-    for( unsigned i=0; i<2; i++ ){
-      Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;
-      n[i] = getExplanationTerm( p, qi, d_n[i], exp );
-    }
-    Node eq = n[0].eqNode( n[1] );
-    if( !d_tgt_orig ){
-      eq = eq.negate();
-    }
-    exp.push_back( eq );
-    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;
-    return true;
-  }else if( d_type==typ_pred ){
-    Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;
-    Node n = getExplanationTerm( p, qi, d_n, exp );
-    if( !d_tgt_orig ){
-      n = n.negate();
-    }
-    exp.push_back( n );
-    Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;
-    return true;
-  }else if( d_type==typ_formula ){
-    Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;
-    if( d_n.getKind()==OR || d_n.getKind()==AND ){
-      if( (d_n.getKind()==AND)==d_tgt ){
-        for( unsigned i=0; i<getNumChildren(); i++ ){
-          if( !getChild( i )->getExplanation( p, qi, exp ) ){
-            return false;
-          }
-        }
-      }else{
-        return getChild( d_child_counter )->getExplanation( p, qi, exp );
-      }
-    }else if( d_n.getKind()==EQUAL ){
-      for( unsigned i=0; i<2; i++ ){
-        if( !getChild( i )->getExplanation( p, qi, exp ) ){
-          return false;
-        }
-      }
-    }else if( d_n.getKind()==ITE ){
-      for( unsigned i=0; i<3; i++ ){
-        bool isActive = ( ( i==0 && d_child_counter!=5 ) ||
-                          ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||
-                          ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );
-        if( isActive ){
-          if( !getChild( i )->getExplanation( p, qi, exp ) ){
-            return false;
-          }
-        }
-      }
-    }else{
-      return false;
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {
-  Node v = qi->getCurrentExpValue( t );
-  if( isHandledUfTerm( t ) ){
-    for( unsigned i=0; i<t.getNumChildren(); i++ ){
-      Node vi = getExplanationTerm( p, qi, t[i], exp );
-      if( vi!=v[i] ){
-        Node eq = vi.eqNode( v[i] );
-        if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
-          Trace("qcf-explain") << "  add : " << eq << "." << std::endl;
-          exp.push_back( eq );
-        }
-      }
-    }
-  }
-  return v;
-}
-
 bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
   if( !d_qn.empty() ){
     if( d_qn[0]==NULL ){
@@ -1843,7 +1731,6 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_pred: Trace(c) << "pred";break;
     case typ_formula: Trace(c) << "formula";break;
     case typ_var: Trace(c) << "var";break;
-    case typ_ite_var: Trace(c) << "ite_var";break;
     case typ_bool_var: Trace(c) << "bool_var";break;
     }
   }else{
@@ -1854,7 +1741,6 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
     case typ_pred: Debug(c) << "pred";break;
     case typ_formula: Debug(c) << "formula";break;
     case typ_var: Debug(c) << "var";break;
-    case typ_ite_var: Debug(c) << "ite_var";break;
     case typ_bool_var: Debug(c) << "bool_var";break;
     }
   }
@@ -1907,10 +1793,6 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
       d_effort(EFFORT_INVALID),
       d_needs_computeRelEqr() {}
 
-Node QuantConflictFind::mkEqNode( Node a, Node b ) {
-  return a.eqNode( b );
-}
-
 //-------------------------------------------------- registration
 
 void QuantConflictFind::registerQuantifier( Node q ) {
@@ -2031,14 +1913,8 @@ inline QuantConflictFind::Effort QcfEffortStart() {
 // Returns the beginning of a range of efforts. The value returned is included
 // in the range.
 inline QuantConflictFind::Effort QcfEffortEnd() {
-  switch (options::qcfMode()) {
-    case QCF_PROP_EQ:
-    case QCF_PARTIAL:
-      return QuantConflictFind::EFFORT_PROP_EQ;
-    case QCF_CONFLICT_ONLY:
-    default:
-      return QuantConflictFind::EFFORT_PROP_EQ;
-  }
+  return options::qcfMode() == QCF_PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ
+                                           : QuantConflictFind::EFFORT_CONFLICT;
 }
 
 }  // namespace

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 507d929a7de95d9e3818865195e92d3ebf10ba9c..e4eefe9ad984e4ef3688452054c141b08535d141 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -75,7 +75,6 @@ public:
     typ_eq,
     typ_formula,
     typ_var,
-    typ_ite_var,
     typ_bool_var,
     typ_tconstraint,
     typ_tsym,
@@ -94,8 +93,6 @@ public:
   void reset_round( QuantConflictFind * p );
   void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
-  bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );
-  Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );
   bool isValid() { return d_type!=typ_invalid; }
   void setInvalid();
 
@@ -138,7 +135,6 @@ public:
   std::map< TNode, int > d_var_num;
   std::vector< int > d_tsym_vars;
   std::map< TNode, bool > d_inMatchConstraint;
-  std::map< int, std::vector< Node > > d_var_constraint[2];
   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
   int getNumVars() { return (int)d_vars.size(); }
@@ -205,7 +201,6 @@ private:
 private:
   std::map< Node, Node > d_op_node;
   std::map< Node, int > d_fid;
-  Node mkEqNode( Node a, Node b );
 public:  //for ground terms
   Node d_true;
   Node d_false;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e9dd371df29d09be024a7bdcfc9fb5db2f106cda..7e3806e8c05a3bfb014d88f4f481ed68f13a4c9b 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -96,6 +96,8 @@ public:
  void debugPrint(const char* c, Node n, unsigned depth = 0);
  /** clear all data from this trie */
  void clear() { d_data.clear(); }
+ /** is empty */
+ bool empty() { return d_data.empty(); }
 };/* class TermArgTrie */
 
 namespace fmcheck {