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

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index c36a565ea80fb1a1ead5f29e27d740e0ef9fffd0..75b9eba3e4ff55419145cb6e0a85f66e64386bab 100644 (file)
--- 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 37362982c92f7dbe6f98f06454677c791b2ac0b3..15d52cc9655bd7e3589b7aef7918f04be0267e26 100644 (file)
--- 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 91c9b665309f19d4a140ca1424e31c591c20375a..95744a651929dd873b9dda4ca3b53cec2a85b953 100755 (executable)
--- 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 ) {
 \r
 \r
   Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
-  d_mg = new MatchGen( this, qn, true );\r
+  d_mg = new MatchGen( this, qn );\r
 \r
   if( d_mg->isValid() ){\r
     for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
       if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
-        d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );\r
+        d_var_mg[j] = new MatchGen( this, d_vars[j], true );\r
         if( !d_var_mg[j]->isValid() ){\r
           d_mg->setInvalid();\r
           break;\r
         }\r
       }\r
     }\r
+\r
+    if( d_mg->isValid() ){\r
+      std::vector< int > bvars;\r
+      d_mg->determineVariableOrder( this, bvars );\r
+    }\r
+\r
     //must also contain all variables?\r
     /*\r
       if( d_mg->isValid() ){\r
@@ -562,8 +568,8 @@ struct MatchGenSort {
 };\r
 */\r
 \r
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){\r
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){\r
+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;\r
   std::vector< Node > qni_apps;\r
   d_qni_size = 0;\r
   if( isVar ){\r
@@ -674,6 +680,93 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){
   //Assert( d_children.size()==d_children_order.size() );\r
 }\r
 \r
+void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {\r
+  int v = qi->getVarNum( n );\r
+  if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){\r
+    cbvars.push_back( v );\r
+  }\r
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+    collectBoundVar( qi, n[i], cbvars );\r
+  }\r
+}\r
+\r
+void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {\r
+  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;\r
+  bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF;\r
+  std::map< int, std::vector< int > > c_to_vars;\r
+  std::map< int, std::vector< int > > vars_to_c;\r
+  std::map< int, int > vb_count;\r
+  std::map< int, int > vu_count;\r
+  std::vector< bool > assigned;\r
+  Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;\r
+  for( unsigned i=0; i<d_children.size(); i++ ){\r
+    collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );\r
+    assigned.push_back( false );\r
+    vb_count[i] = 0;\r
+    vu_count[i] = 0;\r
+    for( unsigned j=0; j<c_to_vars[i].size(); j++ ){\r
+      int v = c_to_vars[i][j];\r
+      vars_to_c[v].push_back( i );\r
+      if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){\r
+        vu_count[i]++;\r
+        if( !isCom ){\r
+          bvars.push_back( v );\r
+        }\r
+      }else{\r
+        vb_count[i]++;\r
+      }\r
+    }\r
+  }\r
+  if( isCom ){\r
+    //first, do those that do not bind any new variables\r
+    //second, do those with common variables\r
+    //last, do those with no common variables\r
+    do {\r
+      int min_score = -1;\r
+      int min_score_index = -1;\r
+      for( unsigned i=0; i<d_children.size(); i++ ){\r
+        if( !assigned[i] ){\r
+          int score = vu_count[i];\r
+          if( min_score==-1 || score<min_score ){\r
+            min_score = score;\r
+            min_score_index = i;\r
+          }\r
+        }\r
+      }\r
+      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;\r
+      Assert( min_score_index!=-1 );\r
+      //add to children order\r
+      d_children_order.push_back( min_score_index );\r
+      assigned[min_score_index] = true;\r
+      //if( vb_count[min_score_index]==0 ){\r
+      //  d_independent.push_back( min_score_index );\r
+      //}\r
+      //determine order internal to children\r
+      d_children[min_score_index].determineVariableOrder( qi, bvars );\r
+      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;\r
+      //now, make it a bound variable\r
+      for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){\r
+        int v = c_to_vars[min_score_index][i];\r
+        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){\r
+          for( unsigned j=0; j<vars_to_c[v].size(); j++ ){\r
+            int vc = vars_to_c[v][j];\r
+            vu_count[vc]--;\r
+            vb_count[vc]++;\r
+          }\r
+          bvars.push_back( v );\r
+        }\r
+      }\r
+      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;\r
+    }while( d_children_order.size()!=d_children.size() );\r
+    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;\r
+  }else{\r
+    for( unsigned i=0; i<d_children.size(); i++ ){\r
+      d_children_order.push_back( i );\r
+      d_children[i].determineVariableOrder( qi, bvars );\r
+    }\r
+  }\r
+}\r
+\r
 \r
 void MatchGen::reset_round( QuantConflictFind * p ) {\r
   for( unsigned i=0; i<d_children.size(); i++ ){\r
@@ -702,7 +795,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
   d_tgt = d_type_not ? !tgt : tgt;\r
   Debug("qcf-match") << "     Reset for : " << d_n << ", type : ";\r
   debugPrintType( "qcf-match", d_type );\r
-  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;\r
+  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;\r
   d_qn.clear();\r
   d_qni.clear();\r
   d_qni_bound.clear();\r
@@ -934,7 +1027,11 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
                 success = true;\r
               }\r
             }else{\r
+              //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){\r
+              //  d_child_counter--;\r
+              //}else{\r
               d_child_counter--;\r
+              //}\r
             }\r
           }else{\r
             //one child must match\r
@@ -1533,9 +1630,12 @@ void QuantConflictFind::check( Theory::Effort level ) {
 \r
           Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
           if( qi->d_mg->isValid() ){\r
+            Trace("qcf-check-debug") << "Reset round..." << std::endl;\r
             qi->reset_round( this );\r
             //try to make a matches making the body false\r
+            Trace("qcf-check-debug") << "Reset..." << std::endl;\r
             qi->d_mg->reset( this, false, qi );\r
+            Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
             while( qi->d_mg->getNextMatch( this, qi ) ){\r
 \r
               Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 010a8e1944b6f8ce51ea479c9123ae1b00b724ed..2663ff0b927f1800617e89feb894c58e68611083 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -42,14 +42,15 @@ class QuantInfo;
 \r
 //match generator\r
 class MatchGen {\r
+  friend class QuantInfo;\r
 private:\r
   //current children information\r
   int d_child_counter;\r
   //children of this object\r
-  //std::vector< int > d_children_order;\r
+  std::vector< int > d_children_order;\r
   unsigned getNumChildren() { return d_children.size(); }\r
-  //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
-  MatchGen * getChild( int i ) { return &d_children[i]; }\r
+  MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
+  //MatchGen * getChild( int i ) { return &d_children[i]; }\r
   //current matching information\r
   std::vector< QcfNodeIndex * > d_qn;\r
   std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;\r
@@ -63,9 +64,13 @@ private:
   std::map< int, TNode > d_qni_bound_cons;\r
   std::map< int, int > d_qni_bound_cons_var;\r
   std::map< int, int >::iterator d_binding_it;\r
+  //std::vector< int > d_independent;\r
   bool d_binding;\r
   //int getVarBindingVar();\r
   std::map< int, Node > d_ground_eval;\r
+  //determine variable order\r
+  void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );\r
+  void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );\r
 public:\r
   //type of the match generator\r
   enum {\r
@@ -80,7 +85,7 @@ public:
   void debugPrintType( const char * c, short typ, bool isTrace = false );\r
 public:\r
   MatchGen() : d_type( typ_invalid ){}\r
-  MatchGen( QuantInfo * qi, Node n, bool isTop = false, bool isVar = false );\r
+  MatchGen( QuantInfo * qi, Node n, bool isVar = false );\r
   bool d_tgt;\r
   Node d_n;\r
   std::vector< MatchGen > d_children;\r
@@ -108,7 +113,6 @@ public:
   QuantInfo() : d_mg( NULL ) {}\r
   std::vector< TNode > d_vars;\r
   std::map< TNode, int > d_var_num;\r
-  //std::map< EqRegistry *, bool > d_rel_eqr;\r
   std::map< int, std::vector< Node > > d_var_constraint[2];\r
   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }\r
   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }\r
@@ -199,7 +203,7 @@ public:
   enum {\r
     effort_conflict,\r
     effort_prop_eq,\r
-    effort_prop_deq,\r
+    effort_mc,\r
   };\r
   short d_effort;\r
   //for effort_prop\r
@@ -210,12 +214,8 @@ public:
   bool areMatchDisequal( TNode n1, TNode n2 );\r
 public:\r
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
-\r
-  /** register assertions */\r
-  //void registerAssertions( std::vector< Node >& assertions );\r
   /** register quantifier */\r
   void registerQuantifier( Node q );\r
-\r
 public:\r
   /** assert quantifier */\r
   void assertNode( Node q );\r