Add entailment checks between length terms to reduce splitting in strings solver. Minor additions to datatypes and qcf.

6 files changed, 93 insertions, 6 deletions

diff --git a/src/options/strings_options b/src/options/strings_options
index 65c293dbc..1b64af83f 100644
--- a/src/options/strings_options
+++ b/src/options/strings_options
@@ -53,6 +53,8 @@ option stringInferSym strings-infer-sym --strings-infer-sym bool :default true
  strings split on empty string
 option stringEagerLen strings-eager-len --strings-eager-len bool :default true
  strings eager length lemmas
+option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true
+ check entailment between length terms to reduce splitting
 
 
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 51300bfba..3659350b5 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -233,9 +233,11 @@ void TheoryDatatypes::check(Effort e) {
               //all other cases
               std::vector< bool > pcons;
               getPossibleCons( eqc, n, pcons );
+              //std::map< int, bool > sel_apps;
+              //getSelectorsForCons( n, sel_apps );
               //check if we do not need to resolve the constructor type for this equivalence class.
-              // this is if there are no selectors for this equivalence class, its possible values are infinite,
-              //  and we are not producing a model, then do not split.
+              // this is if there are no selectors for this equivalence class, and its possible values are infinite,
+              //  then do not split.
               int consIndex = -1;
               int fconsIndex = -1;
               bool needSplit = true;
@@ -959,6 +961,17 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   }
 }
 
+void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) {
+  NodeListMap::iterator sel_i = d_selector_apps.find( r );
+  if( sel_i != d_selector_apps.end() ){
+    NodeList* sel = (*sel_i).second;
+    for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
+      int sindex = Datatype::indexOf( (*j).getOperator().toExpr() );
+      sels[sindex] = true;
+    }
+  }
+}
+
 void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
   if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){
     std::stringstream ss;
@@ -2095,6 +2108,40 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   return false;
 }
 
+std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {
+  Trace("dt-entail") << "Check entailed : " << lit << std::endl;
+  Node atom = lit.getKind()==NOT ? lit[0] : lit;
+  bool pol = lit.getKind()!=NOT;
+  if( atom.getKind()==APPLY_TESTER ){
+    Node n = atom[0];
+    if( hasTerm( n ) ){
+      Node r = d_equalityEngine.getRepresentative( n );
+      EqcInfo * ei = getOrMakeEqcInfo( r, false );
+      int l_index = getLabelIndex( ei, r );
+      int t_index = (int)Datatype::indexOf( atom.getOperator().toExpr() );
+      Trace("dt-entail") << "  Tester indices are " << t_index << " and " << l_index << std::endl;
+      if( l_index!=-1 && (l_index==t_index)==pol ){
+        std::vector< TNode > exp_c;
+        if( ei && !ei->d_constructor.get().isNull() ){
+          explainEquality( n, ei->d_constructor.get(), true, exp_c );
+        }else{
+          Node lbl = getLabel( n );
+          Assert( !lbl.isNull() );
+          exp_c.push_back( lbl );
+          Assert( areEqual( n, lbl[0] ) );
+          explainEquality( n, lbl[0], true, exp_c );
+        }
+        Node exp = mkAnd( exp_c );
+        Trace("dt-entail") << "  entailed, explanation is " << exp << std::endl;
+        return make_pair(true, exp);
+      }
+    }
+  }else{
+
+  }
+  return make_pair(false, Node::null());
+}
+
 } /* namepsace CVC4::theory::datatypes */
 } /* namepsace CVC4::theory */
 } /* namepsace CVC4 */
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index d56538b2a..2f6c6e6bb 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -131,6 +131,7 @@ private:
   bool hasTester( Node n );
   /** get the possible constructors for n */
   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
+  void getSelectorsForCons( Node r, std::map< int, bool >& sels );
   /** mkExpDefSkolem */
   void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );  
   /** skolems for terms */  
@@ -260,6 +261,8 @@ public:
   std::string identify() const { return std::string("TheoryDatatypes"); }
   /** debug print */
   void printModelDebug( const char* c );
+  /** entailment check */
+  virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
 private:
   /** add tester to equivalence class info */
   void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 5cff55d21..779c0c44e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -477,7 +477,22 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
     Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
     return false;
   }else if( rew!=p->d_true ){
-    //if checking for conflicts, we must be sure that the constraint is entailed
+    //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed 
+    if( !chEnt ){
+      rew = Rewriter::rewrite( rew.negate() );
+    }
+    //check if it is entailed
+    Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
+    std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
+    ++(p->d_statistics.d_entailment_checks);
+    Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
+    if( !et.first ){
+      Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
+      return !chEnt;
+    }else{
+      return chEnt;
+    }
+/*
     if( chEnt ){
       //check if it is entailed
       Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
@@ -494,6 +509,7 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
       Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
       return true;
     }
+*/
   }else{
     Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
     return true;
@@ -1681,6 +1697,8 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 bool MatchGen::isHandledUfTerm( TNode n ) {
   //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
   //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
+  //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
+  //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
   return inst::Trigger::isAtomicTriggerKind( n.getKind() );
 }
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 529e69e82..a4ebe5e97 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2012,11 +2012,28 @@ bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
                       antec_new_lits.push_back( xgtz );
                     }
                   }
-
                   Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
                   Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
                   Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
-                  conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
+                  if( options::stringCheckEntailLen() ){
+                    //check entailment
+                    for( unsigned e=0; e<2; e++ ){
+                      Node lt1 = e==0 ? length_term_i : length_term_j;
+                      Node lt2 = e==0 ? length_term_j : length_term_i;
+                      Node ent_lit = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, lt1, lt2 ) );
+                      std::pair<bool, Node> et = d_valuation.entailmentCheck(THEORY_OF_TYPE_BASED, ent_lit );
+                      if( et.first ){
+                        Trace("strings-entail") << "Strings entailment : " << ent_lit << " is entailed in the current context." << std::endl;
+                        Trace("strings-entail") << "  explanation was : " << et.second << std::endl;
+                        conc = e==0 ? eq1 : eq2;
+                        antec_new_lits.push_back( et.second );
+                      }
+                    }
+                  }
+                  if( conc.isNull() ){
+                    conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
+                  }
+
 
                   Node ant = mkExplain( antec, antec_new_lits );
                   sendLemma( ant, conc, "S-Split(VAR)" );
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 3ed1c4d40..661c67354 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1346,7 +1346,7 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
               for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
                 eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
               }
-              Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+              Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs );
               Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
               Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
               d_thss->getOutputChannel().lemma( lem );