Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
	src/printer/smt2/smt2_printer.cpp

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 409c9b4dd491c21fc5818f60ae379bca85be2c9c..09de0d378d7a15d9e6a37fc7540582e1e0294895 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -277,9 +277,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_CONCAT: out << "str.++ "; break;
   case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
   case kind::STRING_LENGTH: out << "str.len "; break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
+  case kind::STRING_SUBSTR:
+  case kind::STRING_SUBSTR_TOTAL:
+         out << "str.substr "; break;
+  case kind::STRING_CHARAT:
+  case kind::STRING_CHARAT_TOTAL:
+         out << "str.at "; break;
   case kind::STRING_STRCTN: out << "str.contain "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
   case kind::STRING_STRIDOF: out << "str.indexof "; break;
   case kind::STRING_STRREPL: out << "str.replace "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3c3bbe97124ad0a808cc37a03ba5591996da72e4..761348890fed0e2b84c6b97acbac926a63ce14be 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -305,6 +305,13 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   hash_map<Node, Node, NodeHashFunction> d_abstractValues;
 
+  /**
+   * Function symbol used to implement uninterpreted undefined string
+   * semantics.  Needed to deal with partial charat/substr function.
+   */
+  Node d_charAtUndef;
+  Node d_substrUndef;
+
   /**
    * Function symbol used to implement uninterpreted division-by-zero
    * semantics.  Needed to deal with partial division function ("/").
@@ -433,6 +440,8 @@ public:
     d_fakeContext(),
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
+       d_charAtUndef(),
+       d_substrUndef(),
     d_divByZero(),
     d_intDivByZero(),
     d_modZero(),
@@ -1525,6 +1534,59 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         node = expandBVDivByZero(node);
         break;
 
+         case kind::STRING_CHARAT: {
+               if(d_charAtUndef.isNull()) {
+                       std::vector< TypeNode > argTypes;
+                       argTypes.push_back(NodeManager::currentNM()->stringType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes,
+                                                                       NodeManager::currentNM()->stringType()),
+                                                               "partial charat undef",
+                                                               NodeManager::SKOLEM_EXACT_NAME);
+                       if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+                               d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+                               d_smt.d_logic.enableTheory(THEORY_UF);
+                               d_smt.d_logic.lock();
+                       }
+           }
+               TNode str = n[0], num = n[1];
+               Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
+               Node cond = nm->mkNode(kind::GT, lenx, num);
+               Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num);
+               Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num);
+               node = nm->mkNode(kind::ITE, cond, total, undef);
+         }
+               break;
+         case kind::STRING_SUBSTR: {
+               if(d_substrUndef.isNull()) {
+                       std::vector< TypeNode > argTypes;
+                       argTypes.push_back(NodeManager::currentNM()->stringType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       argTypes.push_back(NodeManager::currentNM()->integerType());
+                       d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef", 
+                                                               NodeManager::currentNM()->mkFunctionType(
+                                                                       argTypes,
+                                                                       NodeManager::currentNM()->stringType()),
+                                                               "partial substring undef",
+                                                               NodeManager::SKOLEM_EXACT_NAME);
+                       if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
+                               d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+                               d_smt.d_logic.enableTheory(THEORY_UF);
+                               d_smt.d_logic.lock();
+                       }
+           }
+               TNode str = n[0];
+               Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
+               Node num = nm->mkNode(kind::PLUS, n[1], n[2]);
+               Node cond = nm->mkNode(kind::GEQ, lenx, num);
+               Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]);
+               Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]);
+               node = nm->mkNode(kind::ITE, cond, total, undef);
+         }
+               break;
+
       case kind::DIVISION: {
         // partial function: division
         if(d_divByZero.isNull()) {

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1bf53db9149ce65ac32598b0008c199e78a13762..d7111ea39485ce53dd8b139c851cf6e1e211a0f3 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -27,21 +27,36 @@ using namespace std;
 \r
 namespace CVC4 {\r
 \r
-Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) {\r
+/*\r
+Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) {\r
   if( index==(int)n.getNumChildren() ){\r
     if( d_children.empty() ){\r
-      if( doAdd ){\r
-        d_children[ n ].clear();\r
-        return n;\r
-      }else{\r
-        return Node::null();\r
-      }\r
+      return Node::null();\r
     }else{\r
       return d_children.begin()->first;\r
     }\r
   }else{\r
     Node r = qcf->getRepresentative( n[index] );\r
-    return d_children[r].addTerm( qcf, n, doAdd, index+1 );\r
+    if( d_children.find( r )==d_children.end() ){\r
+      return n;\r
+    }else{\r
+      return d_children[r].existsTerm( qcf, n, index+1 );\r
+    }\r
+  }\r
+}\r
+\r
+\r
+Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) {\r
+  if( index==(int)n.getNumChildren() ){\r
+    if( d_children.empty() ){\r
+      d_children[ n ].clear();\r
+      return n;\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    Node r = qcf->getRepresentative( n[index] );\r
+    return d_children[r].addTerm( qcf, n, index+1 );\r
   }\r
 }\r
 \r
@@ -54,6 +69,49 @@ bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int ind
     return d_children[r].addTermEq( qcf, n1, n2, index+1 );\r
   }\r
 }\r
+*/\r
+\r
+\r
+\r
+Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) {\r
+  if( index==(int)reps.size() ){\r
+    if( d_children.empty() ){\r
+      return Node::null();\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    if( d_children.find( reps[index] )==d_children.end() ){\r
+      return Node::null();\r
+    }else{\r
+      return d_children[reps[index]].existsTerm( n, reps, index+1 );\r
+    }\r
+  }\r
+}\r
+\r
+Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) {\r
+  if( index==(int)reps.size() ){\r
+    if( d_children.empty() ){\r
+      d_children[ n ].clear();\r
+      return n;\r
+    }else{\r
+      return d_children.begin()->first;\r
+    }\r
+  }else{\r
+    return d_children[reps[index]].addTerm( n, reps, index+1 );\r
+  }\r
+}\r
+\r
+bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) {\r
+  if( index==(int)reps1.size() ){\r
+    Node n = addTerm( n2, reps2 );\r
+    return n==n2;\r
+  }else{\r
+    return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 );\r
+  }\r
+}\r
+\r
+\r
 \r
 void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
   for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
@@ -172,7 +230,7 @@ void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {
 \r
 void QuantConflictFind::registerAssertion( Node n ) {\r
   if( n.getKind()==FORALL ){\r
-    registerQuant( Node::null(), n[1], NULL, true, true );\r
+    registerNode( Node::null(), n[1], NULL, true, true );\r
   }else{\r
     if( n.getType().isBoolean() ){\r
       for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
@@ -182,7 +240,7 @@ void QuantConflictFind::registerAssertion( Node n ) {
   }\r
 }\r
 */\r
-void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {\r
+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {\r
   //qcf->d_node = n;\r
   bool recurse = true;\r
   if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
@@ -217,7 +275,7 @@ void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {
       //QcfNode * qcfc = new QcfNode( d_c );\r
       //qcfc->d_parent = qcf;\r
       //qcf->d_child[i] = qcfc;\r
-      registerQuant( q, n[i], newHasPol, newPol );\r
+      registerNode( q, n[i], newHasPol, newPol );\r
     }\r
   }\r
 }\r
@@ -251,7 +309,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   //make QcfNode structure\r
   Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
   //d_qinfo[q].d_cf = new QcfNode( d_c );\r
-  registerQuant( q, q[1], true, true );\r
+  registerNode( q, q[1], true, true );\r
 \r
   //debug print\r
   Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
@@ -270,6 +328,14 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
   d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );\r
 \r
+  for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+    d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );\r
+    if( !d_qinfo[q].d_var_mg[j]->isValid() ){\r
+      d_qinfo[q].d_mg->setInvalid();\r
+      break;\r
+    }\r
+  }\r
+\r
   Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
 }\r
 \r
@@ -433,7 +499,8 @@ Node QuantConflictFind::getRepresentative( Node n ) {
 }\r
 Node QuantConflictFind::getTerm( Node n ) {\r
   if( n.getKind()==APPLY_UF ){\r
-    Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false );\r
+    computeArgReps( n );\r
+    Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
     if( !nn.isNull() ){\r
       return nn;\r
     }\r
@@ -544,6 +611,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
   Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
   if( d_conflict ){\r
     Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+    if( level>=Theory::EFFORT_FULL ){\r
+      Assert( false );\r
+    }\r
   }else{\r
     bool addedLemma = false;\r
     if( d_performCheck ){\r
@@ -580,61 +650,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
             Trace("qcf-check") << std::endl;\r
 \r
             if( !d_qinfo[q].isMatchSpurious( this ) ){\r
-              //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
-              Trace("qcf-check") << std::endl;\r
-              std::vector< int > unassigned;\r
-              std::vector< TypeNode > unassigned_tn;\r
-              for( int i=0; i<d_qinfo[q].getNumVars(); i++ ){\r
-                if( d_qinfo[q].d_match.find( i )==d_qinfo[q].d_match.end() ){\r
-                  Assert( i<(int)q[0].getNumChildren() );\r
-                  unassigned.push_back( i );\r
-                  unassigned_tn.push_back( d_qinfo[q].getVar( i ).getType() );\r
-                }\r
-              }\r
-              bool success = true;\r
-              if( !unassigned.empty() ){\r
-                Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
-                int index = 0;\r
-                std::vector< int > eqc_count;\r
-                do {\r
-                  bool invalidMatch;\r
-                  while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){\r
-                    invalidMatch = false;\r
-                    if( index==(int)eqc_count.size() ){\r
-                      eqc_count.push_back( 0 );\r
-                    }else{\r
-                      Assert( index==(int)eqc_count.size()-1 );\r
-                      if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){\r
-                        int currIndex = eqc_count[index];\r
-                        eqc_count[index]++;\r
-                        Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl;\r
-                        if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){\r
-                          Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
-                          index++;\r
-                        }else{\r
-                          Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
-                          invalidMatch = true;\r
-                        }\r
-                      }else{\r
-                        Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
-                        eqc_count.pop_back();\r
-                        index--;\r
-                      }\r
-                    }\r
-                  }\r
-                  success = index>=0;\r
-                  if( success ){\r
-                    index = (int)unassigned.size()-1;\r
-                    Trace("qcf-check-unassign") << "  Try: " << std::endl;\r
-                    for( unsigned i=0; i<unassigned.size(); i++ ){\r
-                      int ui = unassigned[i];\r
-                      Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_qinfo[q].d_vars[ui] << " -> " << d_qinfo[q].d_match[ui] << std::endl;\r
-                    }\r
-                  }\r
-                }while( success && d_qinfo[q].isMatchSpurious( this ) );\r
-              }\r
-\r
-              if( success ){\r
+              std::vector< int > assigned;\r
+              if( d_qinfo[q].completeMatch( this, q, assigned ) ){\r
                 InstMatch m;\r
                 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
                   Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );\r
@@ -657,12 +674,13 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;\r
                   Assert( false );\r
                 }\r
+                //clean up assigned\r
+                for( unsigned i=0; i<assigned.size(); i++ ){\r
+                  d_qinfo[q].d_match.erase( assigned[i] );\r
+                }\r
               }else{\r
                 Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
               }\r
-              for( unsigned i=0; i<unassigned.size(); i++ ){\r
-                d_qinfo[q].d_match.erase( unassigned[i] );\r
-              }\r
             }else{\r
               Trace("qcf-check") << "   ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
             }\r
@@ -683,8 +701,12 @@ void QuantConflictFind::check( Theory::Effort level ) {
 \r
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
   d_performCheck = false;\r
-  if( !d_conflict && level==Theory::EFFORT_FULL ){\r
-    d_performCheck = true;\r
+  if( !d_conflict ){\r
+    if( level==Theory::EFFORT_FULL ){\r
+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+    }else if( level==Theory::EFFORT_STANDARD ){\r
+      d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+    }\r
   }\r
   return d_performCheck;\r
 }\r
@@ -701,6 +723,7 @@ void QuantConflictFind::computeRelevantEqr() {
   d_uf_terms.clear();\r
   d_eqc_uf_terms.clear();\r
   d_eqcs.clear();\r
+  d_arg_reps.clear();\r
 \r
   //which nodes are irrelevant for disequality matches\r
   std::map< Node, bool > irrelevant_dnode;\r
@@ -740,9 +763,10 @@ void QuantConflictFind::computeRelevantEqr() {
       Node n = (*eqc_i);\r
       bool isRedundant;\r
       if( n.getKind()==APPLY_UF ){\r
-        Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n );\r
+        computeArgReps( n );\r
+        Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] );\r
         isRedundant = (nadd!=n);\r
-        d_uf_terms[n.getOperator()].addTerm( this, n );\r
+        d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
       }else{\r
         isRedundant = false;\r
       }\r
@@ -773,7 +797,7 @@ void QuantConflictFind::computeRelevantEqr() {
                 //fn with m\r
                 std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );\r
                 if( itm!=itn[j]->second.end() ){\r
-                  if( itm->second->d_qni.addTerm( this, n )==n ){\r
+                  if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){\r
                     Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
                     Trace("qcf-reqr") << fn << " " << m << std::endl;\r
                   }\r
@@ -782,9 +806,10 @@ void QuantConflictFind::computeRelevantEqr() {
               if( !fm.isNull() ){\r
                 std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );\r
                 if( itm!=itn[j]->second.end() ){\r
+                  Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
                   if( j==0 ){\r
                     //n with fm\r
-                    if( itm->second->d_qni.addTerm( this, m )==m ){\r
+                    if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){\r
                       Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
                       Trace("qcf-reqr") << n << " " << fm << std::endl;\r
                     }\r
@@ -795,7 +820,7 @@ void QuantConflictFind::computeRelevantEqr() {
                       if( i==0 || m.getOperator()==n.getOperator() ){\r
                         Node am = ((i==0)==mltn) ? n : m;\r
                         Node an = ((i==0)==mltn) ? m : n;\r
-                        if( itm->second->d_qni.addTermEq( this, an, am ) ){\r
+                        if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){\r
                           Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
                           Trace("qcf-reqr") << fn << " " << fm << std::endl;\r
                         }\r
@@ -826,6 +851,14 @@ void QuantConflictFind::computeRelevantEqr() {
   }\r
 }\r
 \r
+void QuantConflictFind::computeArgReps( Node n ) {\r
+  if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
+    for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
+      d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
+    }\r
+  }\r
+}\r
+\r
 \r
 void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {\r
   d_match.clear();\r
@@ -853,6 +886,9 @@ void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {
     }\r
   }\r
   d_mg->reset_round( p );\r
+  for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){\r
+    it->second->reset_round( p );\r
+  }\r
 }\r
 \r
 int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {\r
@@ -913,7 +949,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N
   //for handling equalities between variables, and disequalities involving variables\r
   Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";\r
   Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;\r
-  Assert( n==getCurrentValue( n ) );\r
+  Assert( doRemove || n==getCurrentValue( n ) );\r
   Assert( doRemove || v==getCurrentRepVar( v ) );\r
   Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
   if( polarity ){\r
@@ -1060,6 +1096,90 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;\r
 }\r
 \r
+bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) {\r
+  //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
+  Trace("qcf-check") << std::endl;\r
+  std::vector< int > unassigned[2];\r
+  std::vector< TypeNode > unassigned_tn[2];\r
+  for( int i=0; i<getNumVars(); i++ ){\r
+    if( d_match.find( i )==d_match.end() ){\r
+      Assert( i<(int)q[0].getNumChildren() );\r
+      int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
+      unassigned[rindex].push_back( i );\r
+      unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
+      assigned.push_back( i );\r
+    }\r
+  }\r
+  bool success = true;\r
+  for( unsigned r=0; r<2; r++ ){\r
+    if( success && !unassigned[r].empty() ){\r
+      Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;\r
+      int index = 0;\r
+      std::vector< int > eqc_count;\r
+      do {\r
+        bool invalidMatch;\r
+        while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){\r
+          invalidMatch = false;\r
+          if( index==(int)eqc_count.size() ){\r
+            //check if it has now been assigned\r
+            if( r==0 ){\r
+              d_var_mg[ unassigned[r][index] ]->reset( p, true, q );\r
+            }\r
+            eqc_count.push_back( 0 );\r
+          }else{\r
+            if( r==0 ){\r
+              if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){\r
+                Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl;\r
+                index++;\r
+              }else{\r
+                Trace("qcf-check-unassign") << "Failed match with mg" << std::endl;\r
+                eqc_count.pop_back();\r
+                index--;\r
+              }\r
+            }else{\r
+              Assert( index==(int)eqc_count.size()-1 );\r
+              if( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\r
+                int currIndex = eqc_count[index];\r
+                eqc_count[index]++;\r
+                Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;\r
+                if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){\r
+                  Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
+                  index++;\r
+                }else{\r
+                  Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
+                  invalidMatch = true;\r
+                }\r
+              }else{\r
+                Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
+                eqc_count.pop_back();\r
+                index--;\r
+              }\r
+            }\r
+          }\r
+        }\r
+        success = index>=0;\r
+        if( success ){\r
+          index = (int)unassigned[r].size()-1;\r
+          Trace("qcf-check-unassign") << "  Try: " << std::endl;\r
+          for( unsigned i=0; i<unassigned[r].size(); i++ ){\r
+            int ui = unassigned[r][i];\r
+            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
+          }\r
+        }\r
+      }while( success && isMatchSpurious( p ) );\r
+    }\r
+  }\r
+  if( success ){\r
+    return true;\r
+  }else{\r
+    for( unsigned i=0; i<assigned.size(); i++ ){\r
+      d_match.erase( assigned[i] );\r
+    }\r
+    assigned.clear();\r
+    return false;\r
+  }\r
+}\r
+\r
 void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {\r
   for( int i=0; i<getNumVars(); i++ ){\r
     Trace(c) << "  " << d_vars[i] << " -> ";\r
@@ -1095,7 +1215,8 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
     Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
     if( n.getKind()==APPLY_UF ){\r
       d_type = typ_var;\r
-      d_type_not = true;  //implicit disequality, in disjunction at top level\r
+      //d_type_not = true;  //implicit disequality, in disjunction at top level\r
+      d_type_not = false;\r
       d_n = n;\r
       qni_apps.push_back( n );\r
     }else{\r
@@ -1103,6 +1224,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
       d_type = typ_invalid;\r
     }\r
   }else{\r
+    /*\r
     if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
       //conjoin extra constraints based on flattening with quantifier body\r
       d_children.push_back( MatchGen( p, q, n ) );\r
@@ -1113,7 +1235,9 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         d_type = typ_top;\r
       }\r
       d_type_not = false;\r
-    }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+    }else\r
+    */\r
+    if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
       //we handle not immediately\r
       d_n = n.getKind()==NOT ? n[0] : n;\r
       d_type_not = n.getKind()==NOT;\r
@@ -1123,8 +1247,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
           d_children.push_back( MatchGen( p, q, d_n[i] ) );\r
           if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
-            d_type = typ_invalid;\r
-            d_children.clear();\r
+            setInvalid();\r
             break;\r
           }else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\r
             Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;\r
@@ -1197,6 +1320,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
           //std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
         //}\r
       }\r
+      /*\r
       if( isTop ){\r
         int base = d_children.size();\r
         //add additional constraints based on flattening\r
@@ -1231,6 +1355,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo
           }\r
         }\r
       }\r
+      */\r
     }\r
   }\r
   if( d_type!=typ_invalid ){\r
@@ -1355,6 +1480,41 @@ bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q )
   Debug("qcf-match") << ", children = " << d_children.size() << std::endl;\r
   if( d_children.empty() ){\r
     bool success = doMatching( p, q );\r
+    if( success ){\r
+      Debug("qcf-match") << "     Produce matches for bound variables..." << std::endl;\r
+      //also need to create match for each variable we bound\r
+      std::map< int, int >::iterator it = d_qni_bound.begin();\r
+      bool doReset = true;\r
+      while( success && it!=d_qni_bound.end() ){\r
+        std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second );\r
+        if( itm!=p->d_qinfo[q].d_var_mg.end() ){\r
+          Debug("qcf-match-debug") << "       process variable " << it->second << ", reset = " << doReset << std::endl;\r
+          if( doReset ){\r
+            itm->second->reset( p, true, q );\r
+          }\r
+          if( !itm->second->getNextMatch( p, q ) ){\r
+            do {\r
+              if( it==d_qni_bound.begin() ){\r
+                Debug("qcf-match-debug") << "       failed." << std::endl;\r
+                success = false;\r
+              }else{\r
+                Debug("qcf-match-debug") << "       decrement..." << std::endl;\r
+                --it;\r
+              }\r
+            }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() );\r
+            doReset = false;\r
+          }else{\r
+            Debug("qcf-match-debug") << "       increment..." << std::endl;\r
+            ++it;\r
+            doReset = true;\r
+          }\r
+        }else{\r
+          Debug("qcf-match-debug") << "       skip..." << std::endl;\r
+          ++it;\r
+          doReset = true;\r
+        }\r
+      }\r
+    }\r
     if( !success ){\r
       for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
         if( !it->second.isNull() ){\r
@@ -1621,6 +1781,11 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo
   }\r
 }\r
 \r
+void QuantConflictFind::MatchGen::setInvalid() {\r
+  d_type = typ_invalid;\r
+  d_children.clear();\r
+}\r
+\r
 \r
 //-------------------------------------------------- debugging\r
 \r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 930b6ea52dc1809665df79a0be404c3cf904c5e6..0b503d49b22eb943698c5168b6e555b375cbcc65 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -33,9 +33,14 @@ class QcfNodeIndex {
 public:\r
   std::map< Node, QcfNodeIndex > d_children;\r
   void clear() { d_children.clear(); }\r
-  Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 );\r
-  bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );\r
+  //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 );\r
+  //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 );\r
+  //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );\r
   void debugPrint( const char * c, int t );\r
+  //optimized versions\r
+  Node existsTerm( Node n, std::vector< Node >& reps, int index = 0 );\r
+  Node addTerm( Node n, std::vector< Node >& reps, int index = 0 );\r
+  bool addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index = 0 );\r
 };\r
 \r
 class EqRegistry {\r
@@ -78,7 +83,7 @@ private:
   context::CDO< bool > d_conflict;\r
   bool d_performCheck;\r
   //void registerAssertion( Node n );\r
-  void registerQuant( Node q, Node n, bool hasPol, bool pol );\r
+  void registerNode( Node q, Node n, bool hasPol, bool pol );\r
   void flatten( Node q, Node n );\r
 private:\r
   std::map< TypeNode, Node > d_fv;\r
@@ -142,6 +147,7 @@ public:  //for quantifiers
     void reset( QuantConflictFind * p, bool tgt, Node q );\r
     bool getNextMatch( QuantConflictFind * p, Node q );\r
     bool isValid() { return d_type!=typ_invalid; }\r
+    void setInvalid();\r
   };\r
 private:\r
   //currently asserted quantifiers\r
@@ -159,6 +165,7 @@ private:
     int getNumVars() { return (int)d_vars.size(); }\r
     Node getVar( int i ) { return d_vars[i]; }\r
     MatchGen * d_mg;\r
+    std::map< int, MatchGen * > d_var_mg;\r
     void reset_round( QuantConflictFind * p );\r
   public:\r
     //current constraints\r
@@ -171,6 +178,7 @@ private:
     int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );\r
     bool setMatch( QuantConflictFind * p, int v, Node n );\r
     bool isMatchSpurious( QuantConflictFind * p );\r
+    bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned );\r
     void debugPrintMatch( const char * c );\r
   };\r
   std::map< Node, QuantInfo > d_qinfo;\r
@@ -197,6 +205,10 @@ private:  //for equivalence classes
   std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms;\r
   // type -> list(eqc)\r
   std::map< TypeNode, std::vector< Node > > d_eqcs;\r
+  //mapping from UF terms to representatives of their arguments\r
+  std::map< Node, std::vector< Node > > d_arg_reps;\r
+  //compute arg reps\r
+  void computeArgReps( Node n );\r
 public:\r
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
 \r

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 9e0897c00eea8956be960c9ca37ff665d590d5e7..b30bf8f36d699aed6e887d250e526edf2ca3fd35 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -13,9 +13,11 @@ typechecker "theory/strings/theory_strings_type_rules.h"
 operator STRING_CONCAT 2: "string concat"
 operator STRING_IN_REGEXP 2 "membership"
 operator STRING_LENGTH 1 "string length"
-operator STRING_SUBSTR 3 "string substr"
+operator STRING_SUBSTR 3 "string substr (user symbol)"
+operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
+operator STRING_CHARAT 2 "string charat (user symbol)"
+operator STRING_CHARAT_TOTAL 2 "string charat (internal symbol)"
 operator STRING_STRCTN 2 "string contains"
-operator STRING_CHARAT 2 "string charat"
 operator STRING_STRIDOF 3 "string indexof"
 operator STRING_STRREPL 3 "string replace"
 
@@ -105,8 +107,10 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
+typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
+typerule STRING_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule
+typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
 

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 543238d310a9e977bff5661ce23009f55187c674..11e206eebaf1a5b2b998b1bac7313b347e267d94 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -23,6 +23,9 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+StringsPreprocess::StringsPreprocess() {
+}
+
 void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
        int k = r.getKind();
        switch( k ) {
@@ -115,48 +118,47 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        // TODO
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
-       } else if( t.getKind() == kind::STRING_SUBSTR ){
-               if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" );
-                       Node x = simplify( t[0], new_nodes );
-                       Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
-                       new_nodes.push_back( x_eq_123 );
-                       Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
-                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-                       new_nodes.push_back( len_sk1_eq_i );
-                       Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
-                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-                       new_nodes.push_back( len_sk2_eq_j );
+       } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" );
+               Node x = simplify( t[0], new_nodes );
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
+                                                       NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
+               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
 
-                       d_cache[t] = sk2;
-                       retNode = sk2;
-               } else {
-                       throw LogicException("substring not supported in this release");
-               }
-       } else if( t.getKind() == kind::STRING_CHARAT ){
-               if(options::stringExp()) {
-                       Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
-                       Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
-                       Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
-                       Node x = simplify( t[0], new_nodes );
-                       Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
-                       new_nodes.push_back( x_eq_123 );
-                       Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
-                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-                       new_nodes.push_back( len_sk1_eq_i );
-                       Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-                                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-                       new_nodes.push_back( len_sk2_eq_1 );
+               Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_j );
+               tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
+               new_nodes.push_back( tp );
 
-                       d_cache[t] = sk2;
-                       retNode = sk2;
-               } else {
-                       throw LogicException("string char at not supported in this release");
-               }
+               d_cache[t] = sk2;
+               retNode = sk2;
+       } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
+               Node x = simplify( t[0], new_nodes );
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] );
+               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+
+               Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 );
+               tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
+               new_nodes.push_back( tp );
+
+               d_cache[t] = sk2;
+               retNode = sk2;
        } else if( t.getKind() == kind::STRING_STRIDOF ){
                if(options::stringExp()) {
                        Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
@@ -224,7 +226,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("string replace not supported in this release");
                }
-       } else if( t.getNumChildren()>0 ){
+       } else if(t.getKind() == kind::STRING_CHARAT || t.getKind() == kind::STRING_SUBSTR) {
+               InternalError("CharAt and Substr should not be reached here.");
+       } else if( t.getNumChildren()>0 ) {
                std::vector< Node > cc;
                if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
                        cc.push_back(t.getOperator());

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 698ef6ba158ce72c0c8668a5fc250ea5b476da35..6d278cc7a606830f760603054f194ba9415682d5 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -36,6 +36,7 @@ private:
        Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
     void simplify(std::vector< Node > &vec_node);
+       StringsPreprocess();
 };
 
 }/* CVC4::theory::strings namespace */

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index d217548208cd56124d25fa2e30422abeffce111f..9f278aac2c276cab5db6d97fae2f1a199db0bd5a 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -340,15 +340,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    } else if(node.getKind() == kind::STRING_SUBSTR) {
+    } else if(node.getKind() == kind::STRING_SUBSTR_TOTAL) {
                if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
                        if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
                                retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
-                       } else {
-                               // TODO: some issues, must be guarded by users
-                               retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
        } else if(node.getKind() == kind::STRING_STRCTN) {
@@ -363,14 +360,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
-       } else if(node.getKind() == kind::STRING_CHARAT) {
+       } else if(node.getKind() == kind::STRING_CHARAT_TOTAL) {
                if( node[0].isConst() && node[1].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        if( node[0].getConst<String>().size() > (unsigned) i ) {
                                retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, 1) );
-                       } else {
-                               // TODO: some issues, must be guarded by users
-                               retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
        } else if(node.getKind() == kind::STRING_STRIDOF) {

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index a5c6ae2f4e583fe7d2d4a007c6b1c6547d63e294..a2142eeb38e253331c47118b8c0e3cdce4f635ae 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -19,6 +19,7 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =        \
+  at001.smt2 \
   cardinality.smt2 \
   str001.smt2 \
   str002.smt2 \

diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2
new file mode 100644 (file)
index 0000000..8559574
--- /dev/null
+++ b/test/regress/regress0/strings/at001.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun i () Int)\r
+\r
+(assert (= (str.at x i) "b"))\r
+(assert (> i 5))\r
+(assert (< (str.len x) 4))\r
+(assert (> (str.len x) 2))\r
+\r
+(check-sat)\r

diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2
index c0554c48141276ec692a071c9b032d3c2c27ec51..476b8269940a0d2ed3a2ebc4d0f62e3f2bdb0a60 100644 (file)
--- a/test/regress/regress0/strings/substr001.smt2
+++ b/test/regress/regress0/strings/substr001.smt2
@@ -1,5 +1,4 @@
 (set-logic QF_S)\r
-(set-option :strings-exp true)\r
 (set-info :status sat)\r
 \r
 (declare-fun x () String)\r