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

4 files changed, 124 insertions, 17 deletions

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 );