From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Feb 2014 15:00:28 +0000 (-0600)
Subject: Add variable ordering for QCF to accelerate matching procedure.  Preparing for QCF_MC... 
X-Git-Tag: cvc5-1.0.0~7107
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c00db91190ce2956efee1c721e6a1f8707a57b1;p=cvc5.git

Add variable ordering for QCF to accelerate matching procedure.  Preparing for QCF_MC mode.
---

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index c36a565ea..75b9eba3e 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -86,6 +86,8 @@ typedef enum {
   QCF_CONFLICT_ONLY,
   /** use qcf for conflicts and propagations */
   QCF_PROP_EQ,
+  /** use qcf for model checking */
+  QCF_MC,
 } QcfMode;
 
 typedef enum {
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 37362982c..15d52cc96 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -122,7 +122,10 @@ conflict \n\
 + Default, apply conflict finding for finding conflicts only.\n\
 \n\
 prop-eq \n\
-+ Apply conflict finding to propagate equalities as well. \n\
++ Apply QCF to propagate equalities as well. \n\
+\n\
+mc \n\
++ Apply QCF in a complete way, so that a model is ensured when it fails. \n\
 \n\
 ";
 static const std::string userPatModeHelp = "\
@@ -247,8 +250,10 @@ inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, S
 inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg ==  "default" || optarg ==  "conflict") {
     return QCF_CONFLICT_ONLY;
-  } else if(optarg ==  "prop-eq") {
+  } else if(optarg == "prop-eq") {
     return QCF_PROP_EQ;
+  } else if(optarg == "mc" ) {
+    return QCF_MC;
   } else if(optarg ==  "help") {
     puts(qcfModeHelp.c_str());
     exit(1);
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 91c9b6653..95744a651 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -86,18 +86,24 @@ void QuantInfo::initialize( Node q, Node qn ) {
 
 
   Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
-  d_mg = new MatchGen( this, qn, true );
+  d_mg = new MatchGen( this, qn );
 
   if( d_mg->isValid() ){
     for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
       if( d_vars[j].getKind()!=BOUND_VARIABLE ){
-        d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );
+        d_var_mg[j] = new MatchGen( this, d_vars[j], true );
         if( !d_var_mg[j]->isValid() ){
           d_mg->setInvalid();
           break;
         }
       }
     }
+
+    if( d_mg->isValid() ){
+      std::vector< int > bvars;
+      d_mg->determineVariableOrder( this, bvars );
+    }
+
     //must also contain all variables?
     /*
       if( d_mg->isValid() ){
@@ -562,8 +568,8 @@ struct MatchGenSort {
 };
 */
 
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;
   if( isVar ){
@@ -674,6 +680,93 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){
   //Assert( d_children.size()==d_children_order.size() );
 }
 
+void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {
+  int v = qi->getVarNum( n );
+  if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
+    cbvars.push_back( v );
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    collectBoundVar( qi, n[i], cbvars );
+  }
+}
+
+void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
+  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;
+  bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF;
+  std::map< int, std::vector< int > > c_to_vars;
+  std::map< int, std::vector< int > > vars_to_c;
+  std::map< int, int > vb_count;
+  std::map< int, int > vu_count;
+  std::vector< bool > assigned;
+  Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );
+    assigned.push_back( false );
+    vb_count[i] = 0;
+    vu_count[i] = 0;
+    for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
+      int v = c_to_vars[i][j];
+      vars_to_c[v].push_back( i );
+      if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+        vu_count[i]++;
+        if( !isCom ){
+          bvars.push_back( v );
+        }
+      }else{
+        vb_count[i]++;
+      }
+    }
+  }
+  if( isCom ){
+    //first, do those that do not bind any new variables
+    //second, do those with common variables
+    //last, do those with no common variables
+    do {
+      int min_score = -1;
+      int min_score_index = -1;
+      for( unsigned i=0; i<d_children.size(); i++ ){
+        if( !assigned[i] ){
+          int score = vu_count[i];
+          if( min_score==-1 || score<min_score ){
+            min_score = score;
+            min_score_index = i;
+          }
+        }
+      }
+      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;
+      Assert( min_score_index!=-1 );
+      //add to children order
+      d_children_order.push_back( min_score_index );
+      assigned[min_score_index] = true;
+      //if( vb_count[min_score_index]==0 ){
+      //  d_independent.push_back( min_score_index );
+      //}
+      //determine order internal to children
+      d_children[min_score_index].determineVariableOrder( qi, bvars );
+      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
+      //now, make it a bound variable
+      for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
+        int v = c_to_vars[min_score_index][i];
+        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
+          for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
+            int vc = vars_to_c[v][j];
+            vu_count[vc]--;
+            vb_count[vc]++;
+          }
+          bvars.push_back( v );
+        }
+      }
+      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
+    }while( d_children_order.size()!=d_children.size() );
+    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
+  }else{
+    for( unsigned i=0; i<d_children.size(); i++ ){
+      d_children_order.push_back( i );
+      d_children[i].determineVariableOrder( qi, bvars );
+    }
+  }
+}
+
 
 void MatchGen::reset_round( QuantConflictFind * p ) {
   for( unsigned i=0; i<d_children.size(); i++ ){
@@ -702,7 +795,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
   d_tgt = d_type_not ? !tgt : tgt;
   Debug("qcf-match") << "     Reset for : " << d_n << ", type : ";
   debugPrintType( "qcf-match", d_type );
-  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;
+  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;
   d_qn.clear();
   d_qni.clear();
   d_qni_bound.clear();
@@ -934,7 +1027,11 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
                 success = true;
               }
             }else{
+              //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
+              //  d_child_counter--;
+              //}else{
               d_child_counter--;
+              //}
             }
           }else{
             //one child must match
@@ -1533,9 +1630,12 @@ void QuantConflictFind::check( Theory::Effort level ) {
 
           Assert( d_qinfo.find( q )!=d_qinfo.end() );
           if( qi->d_mg->isValid() ){
+            Trace("qcf-check-debug") << "Reset round..." << std::endl;
             qi->reset_round( this );
             //try to make a matches making the body false
+            Trace("qcf-check-debug") << "Reset..." << std::endl;
             qi->d_mg->reset( this, false, qi );
+            Trace("qcf-check-debug") << "Get next match..." << std::endl;
             while( qi->d_mg->getNextMatch( this, qi ) ){
 
               Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 010a8e194..2663ff0b9 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -42,14 +42,15 @@ class QuantInfo;
 
 //match generator
 class MatchGen {
+  friend class QuantInfo;
 private:
   //current children information
   int d_child_counter;
   //children of this object
-  //std::vector< int > d_children_order;
+  std::vector< int > d_children_order;
   unsigned getNumChildren() { return d_children.size(); }
-  //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
-  MatchGen * getChild( int i ) { return &d_children[i]; }
+  MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
+  //MatchGen * getChild( int i ) { return &d_children[i]; }
   //current matching information
   std::vector< QcfNodeIndex * > d_qn;
   std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;
@@ -63,9 +64,13 @@ private:
   std::map< int, TNode > d_qni_bound_cons;
   std::map< int, int > d_qni_bound_cons_var;
   std::map< int, int >::iterator d_binding_it;
+  //std::vector< int > d_independent;
   bool d_binding;
   //int getVarBindingVar();
   std::map< int, Node > d_ground_eval;
+  //determine variable order
+  void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );
+  void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );
 public:
   //type of the match generator
   enum {
@@ -80,7 +85,7 @@ public:
   void debugPrintType( const char * c, short typ, bool isTrace = false );
 public:
   MatchGen() : d_type( typ_invalid ){}
-  MatchGen( QuantInfo * qi, Node n, bool isTop = false, bool isVar = false );
+  MatchGen( QuantInfo * qi, Node n, bool isVar = false );
   bool d_tgt;
   Node d_n;
   std::vector< MatchGen > d_children;
@@ -108,7 +113,6 @@ public:
   QuantInfo() : d_mg( NULL ) {}
   std::vector< TNode > d_vars;
   std::map< TNode, int > d_var_num;
-  //std::map< EqRegistry *, bool > d_rel_eqr;
   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(); }
@@ -199,7 +203,7 @@ public:
   enum {
     effort_conflict,
     effort_prop_eq,
-    effort_prop_deq,
+    effort_mc,
   };
   short d_effort;
   //for effort_prop
@@ -210,12 +214,8 @@ public:
   bool areMatchDisequal( TNode n1, TNode n2 );
 public:
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
-
-  /** register assertions */
-  //void registerAssertions( std::vector< Node >& assertions );
   /** register quantifier */
   void registerQuantifier( Node q );
-
 public:
   /** assert quantifier */
   void assertNode( Node q );