Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 98cc7813dd18745fb8ffc3ca529fe4af33107105..cd3a7943ef619a91895abf3589a58f0e3bb22cc5 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1300,6 +1300,7 @@ void SmtEngine::setDefaults() {
     }
   }
   if( options::dtStcInduction() ){
+    //leads to unfairness FIXME
     if( !options::dtForceAssignment.wasSetByUser() ){
       options::dtForceAssignment.set( true );
     }

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f74384d59b70f10be39037752ca2724381f3c9da..8e90f5056d5029b91e6e1b998a671b660e2a0d13 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -62,6 +62,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 
   d_true = NodeManager::currentNM()->mkConst( true );
+  d_dtfCounter = 0;
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -190,8 +191,8 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
             }
-
-            if( !needSplit && options::dtForceAssignment() ){
+            //d_dtfCounter++;
+            if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
               //for the sake of termination, we must choose the constructor of a ground term
               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
               // TODO: this is probably not good enough, actually need fair enumeration strategy

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 132077e293cb491a9fec70f3ef212b7c42016397..3592dbe3065f82c3a2c96ead8e0f471f5d609cea 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -174,6 +174,8 @@ private:
   context::CDList<TNode> d_consTerms;
   /** All the selector terms that the theory has seen */
   context::CDList<TNode> d_selTerms;
+  /** counter for forcing assignments (ensures fairness) */
+  unsigned d_dtfCounter;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 17489b6bab601cbec83f3d3e6dc12fbafc57ab54..c775bb55802bbb9e55581c2de9e9c3167ffc45da 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -710,12 +710,12 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               Trace("sg-rel-term") << std::endl;\r
 \r
               for( unsigned r=0; r<2; r++ ){\r
-                Trace("sg-gen-tg-eqc") << "...from equivalence classes (" << r << ") : ";\r
+                Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";\r
                 int index = d_ccand_eqc[r].size()-1;\r
                 for( unsigned j=0; j<d_ccand_eqc[r][index].size(); j++ ){\r
-                  Trace("sg-gen-tg-eqc") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";\r
+                  Trace("sg-rel-term-debug") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";\r
                 }\r
-                Trace("sg-gen-tg-eqc") << std::endl;\r
+                Trace("sg-rel-term-debug") << std::endl;\r
               }\r
               TypeNode tnn = nn.getType();\r
               Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;\r
@@ -766,7 +766,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               int index = d_ccand_eqc[1].size()-1;\r
               for( unsigned j=0; j<d_ccand_eqc[1][index].size(); j++ ){\r
                 TNode r = d_ccand_eqc[1][index][j];\r
-                Trace("sg-gen-tg-eqc") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;\r
+                Trace("sg-rel-term-debug") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;\r
                 std::map< TypeNode, std::map< unsigned, TNode > > subs;\r
                 std::map< TNode, bool > rev_subs;\r
                 //only get ground terms\r
@@ -779,17 +779,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
                     unsigned tindex = typ_to_subs_index[it->first];\r
                     for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
                       if( !firstTime ){\r
-                        Trace("sg-gen-tg-eqc") << ", ";\r
+                        Trace("sg-rel-term-debug") << ", ";\r
                       }else{\r
                         firstTime = false;\r
-                        Trace("sg-gen-tg-eqc") << "    ";\r
+                        Trace("sg-rel-term-debug") << "    ";\r
                       }\r
-                      Trace("sg-gen-tg-eqc") << it->first << ":x" << it2->first << " -> " << it2->second;\r
+                      Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;\r
                       Assert( tindex+it2->first<gsubs_terms.size() );\r
                       gsubs_terms[tindex+it2->first] = it2->second;\r
                     }\r
                   }\r
-                  Trace("sg-gen-tg-eqc") << std::endl;\r
+                  Trace("sg-rel-term-debug") << std::endl;\r
                   d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );\r
                 }\r
               }\r
@@ -1000,9 +1000,10 @@ bool ConjectureGenerator::considerCurrentTerm() {
         std::map< TNode, bool > rev_subs;\r
         unsigned mode;\r
         if( r==0 ){\r
-          mode = optReqDistinctVarPatterns() ? 1 : 0;\r
+          mode = optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;\r
+          mode = mode | (1 << 2 );\r
         }else{\r
-          mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? 2 : 0;\r
+          mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;\r
         }\r
         d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );\r
         if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){\r
@@ -1539,9 +1540,9 @@ void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned
   d_match_children_end.clear();\r
   d_match_mode = mode;\r
   //if this term generalizes, it must generalize a non-ground term\r
-  if( mode<2 && s->isGroundEqc( eqc ) && d_status==5 ){\r
-    d_match_status = -1;\r
-  }\r
+  //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){\r
+  //  d_match_status = -1;\r
+  //}\r
 }\r
 \r
 bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {\r
@@ -1572,13 +1573,19 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
     //a variable\r
     if( d_match_status==0 ){\r
       d_match_status++;\r
-      if( d_match_mode>=2 ){\r
+      if( (d_match_mode & ( 1 << 1 ))!=0 ){\r
         //only ground terms\r
         if( !s->isGroundEqc( eqc ) ){\r
           return false;\r
         }\r
+      }else if( (d_match_mode & ( 1 << 2 ))!=0 ){\r
+        //only non-ground terms\r
+        //if( s->isGroundEqc( eqc ) ){\r
+        //  return false;\r
+        //}\r
       }\r
-      if( d_match_mode%2==1 ){\r
+      //store the match : restricted if match_mode.0 = 1\r
+      if( (d_match_mode & ( 1 << 0 ))!=0 ){\r
         std::map< TNode, bool >::iterator it = rev_subs.find( eqc );\r
         if( it==rev_subs.end() ){\r
           rev_subs[eqc] = true;\r
@@ -1592,7 +1599,7 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
     }else{\r
       //clean up\r
       subs[d_typ].erase( d_status_num );\r
-      if( d_match_mode%2==1 ){\r
+      if( (d_match_mode & ( 1 << 0 ))!=0 ){\r
         rev_subs.erase( eqc );\r
       }\r
       return false;\r

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 94a13829caa8a0167c968771401f9a0a862e5589..93cda731153d2b4251ef3ca4b22603b395b3543f 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -85,10 +85,10 @@ public:
   //match status\r
   int d_match_status;\r
   int d_match_status_child_num;\r
-  //match mode\r
-  //1 : different variables must have different matches\r
-  //2 : variables must map to ground terms\r
-  //3 : both 1 and 2\r
+  //match mode bits\r
+  //0 : different variables must have different matches\r
+  //1 : variables must map to ground terms\r
+  //2 : variables must map to non-ground terms\r
   unsigned d_match_mode;\r
   //children\r
   std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;\r
@@ -312,7 +312,6 @@ public:  //for generalization
     return isGeneralization( patg, pat, subs );\r
   }\r
   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );\r
-\r
 public:  //for property enumeration\r
   //process this candidate conjecture\r
   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );\r

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index aa68aefcc0657312a752b0db9e03e0c636be6620..d30e5de4a326cb0c21ffcc2ec1bf085402baf006 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -26,7 +26,7 @@ option prenexQuant /--disable-prenex-quant bool :default true
 #   forall y. P( c, y )
 option varElimQuant /--disable-var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
-option dtVarExpandQuant --dt-var-exp-quant bool :default false
+option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
 
 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 504c3dcffaf1898bcc94e7a92e4535d8dc04f281..ee4464f877b48f62f67e02b65df9327585993e99 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2010,9 +2010,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
             //try to make a matches making the body false\r
             Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
             while( qi->d_mg->getNextMatch( this, qi ) ){\r
-              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
-              qi->debugPrintMatch("qcf-check");\r
-              Trace("qcf-check") << std::endl;\r
+              Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;\r
+              qi->debugPrintMatch("qcf-inst");\r
+              Trace("qcf-inst") << std::endl;\r
               std::vector< int > assigned;\r
               if( !qi->isMatchSpurious( this ) ){\r
                 if( qi->completeMatch( this, assigned ) ){\r
@@ -2042,7 +2042,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                         ++(d_statistics.d_prop_inst);\r
                       }\r
                     }else{\r
-                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
+                      Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;\r
                       //Assert( false );\r
                     }\r
                   }\r
@@ -2050,10 +2050,10 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                   qi->revertMatch( assigned );\r
                   d_tempCache.clear();\r
                 }else{\r
-                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+                  Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
                 }\r
               }else{\r
-                Trace("qcf-check") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;\r
+                Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;\r
               }\r
             }\r
             if( d_conflict ){\r

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 624856671e4d8987cd6a3ec7a6a2fa421e319e76..754bfacb12970f74316d5a8ad38911b8b0161e21 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -368,7 +368,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
     //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
     if( it->first.getKind()==EQUAL ){
-      if( it->second ){
+      if( it->second && options::varElimQuant() ){
         for( int i=0; i<2; i++ ){
           int j = i==0 ? 1 : 0;
           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
@@ -388,14 +388,33 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
         }
       }
     }
-    /*
-    else if( options::dtVarExpandQuant() && it->first.getKind()==APPLY_TESTER && it->first[0].getKind()==BOUND_VARIABLE ){
-      if( it->second ){
+    else if( it->first.getKind()==APPLY_TESTER ){
+      if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
         Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
         std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
+        if( ita!=args.end() ){
+          vars.push_back( it->first[0] );
+          Expr testerExpr = it->first.getOperator().toExpr();
+          int index = Datatype::indexOf( testerExpr );
+          const Datatype& dt = Datatype::datatypeOf(testerExpr);
+          const DatatypeConstructor& c = dt[index];
+          std::vector< Node > newChildren;
+          newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
+          std::vector< Node > newVars;
+          for( unsigned j=0; j<c.getNumArgs(); j++ ){
+            TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
+            tn = tn[1];
+            Node v = NodeManager::currentNM()->mkBoundVar( tn );
+            newChildren.push_back( v );
+            newVars.push_back( v );
+          }
+          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
+          Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+          args.erase( ita );
+          args.insert( args.end(), newVars.begin(), newVars.end() );
+        }
       }
     }
-    */
   }
   if( !vars.empty() ){
     Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
@@ -933,7 +952,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return options::varElimQuant();
+    return options::varElimQuant() || options::dtVarExpandQuant();
   }else if( computeOption==COMPUTE_CNF ){
     return false;//return options::cnfQuant() ; FIXME
   }else if( computeOption==COMPUTE_SPLIT ){

diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2
index 109940090e3e0c386b14cfd881e995275e7c359f..37403d8a30dc718f4a3b4884ff9ce188293f6a2d 100644 (file)
--- a/test/regress/regress0/bug567.smt2
+++ b/test/regress/regress0/bug567.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL_SUPPORTED)
 ; COMMAND-LINE: --incremental
 ; EXPECT: unknown
-; EXPECT: unknown
+; EXPECT: unsat
 ; EXPECT: unknown
 (declare-datatypes () ((OptInt0 (Some (value0 Int)) (None))))
 (declare-datatypes () ((List0 (Cons (head0 Int) (tail0 List0)) (Nil))))