src/theory/strings/theory_strings.h

   1 /*********************                                                        */
   2 /*! \file theory_strings.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tianyi Liang, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Theory of strings
  13  **
  14  ** Theory of strings.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
  20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
  21
  22 #include "theory/theory.h"
  23 #include "theory/uf/equality_engine.h"
  24 #include "theory/strings/theory_strings_preprocess.h"
  25 #include "theory/strings/regexp_operation.h"
  26
  27 #include "context/cdchunk_list.h"
  28 #include "context/cdhashset.h"
  29 #include "expr/attribute.h"
  30
  31 #include <climits>
  32 #include <deque>
  33
  34 namespace CVC4 {
  35 namespace theory {
  36
  37 namespace quantifiers{
  38   class TermArgTrie;
  39 }
  40
  41 namespace strings {
  42
  43 /**
  44  * Decision procedure for strings.
  45  *
  46  */
  47
  48 struct StringsProxyVarAttributeId {};
  49 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
  50
  51 class TheoryStrings : public Theory {
  52   typedef context::CDChunkList<Node> NodeList;
  53   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  54   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  55   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  56   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  57
  58 public:
  59   TheoryStrings(context::Context* c, context::UserContext* u,
  60                 OutputChannel& out, Valuation valuation,
  61                 const LogicInfo& logicInfo);
  62   ~TheoryStrings();
  63
  64   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  65
  66   std::string identify() const { return std::string("TheoryStrings"); }
  67
  68 public:
  69   void propagate(Effort e);
  70   bool propagate(TNode literal);
  71   void explain( TNode literal, std::vector<TNode>& assumptions );
  72   Node explain( TNode literal );
  73   eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
  74   bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
  75   int getReduction( int effort, Node n, Node& nr );
  76
  77   // NotifyClass for equality engine
  78   class NotifyClass : public eq::EqualityEngineNotify {
  79     TheoryStrings& d_str;
  80   public:
  81     NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
  82     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  83       Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  84       if (value) {
  85         return d_str.propagate(equality);
  86       } else {
  87         // We use only literal triggers so taking not is safe
  88         return d_str.propagate(equality.notNode());
  89       }
  90     }
  91     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  92       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  93       if (value) {
  94         return d_str.propagate(predicate);
  95       } else {
  96          return d_str.propagate(predicate.notNode());
  97       }
  98     }
  99     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 100       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
 101       if (value) {
 102       return d_str.propagate(t1.eqNode(t2));
 103       } else {
 104       return d_str.propagate(t1.eqNode(t2).notNode());
 105       }
 106     }
 107     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 108       Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 109       d_str.conflict(t1, t2);
 110     }
 111     void eqNotifyNewClass(TNode t) {
 112       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
 113       d_str.eqNotifyNewClass(t);
 114     }
 115     void eqNotifyPreMerge(TNode t1, TNode t2) {
 116       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
 117       d_str.eqNotifyPreMerge(t1, t2);
 118     }
 119     void eqNotifyPostMerge(TNode t1, TNode t2) {
 120       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 121       d_str.eqNotifyPostMerge(t1, t2);
 122     }
 123     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 124       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
 125       d_str.eqNotifyDisequal(t1, t2, reason);
 126     }
 127   };/* class TheoryStrings::NotifyClass */
 128
 129 private:
 130   // Constants
 131   Node d_emptyString;
 132   Node d_emptyRegexp;
 133   Node d_true;
 134   Node d_false;
 135   Node d_zero;
 136   Node d_one;
 137   CVC4::Rational RMAXINT;
 138   unsigned d_card_size;
 139   // Helper functions
 140   Node getRepresentative( Node t );
 141   bool hasTerm( Node a );
 142   bool areEqual( Node a, Node b );
 143   bool areDisequal( Node a, Node b );
 144   // t is representative, te = t, add lt = te to explanation exp
 145   Node getLengthExp( Node t, std::vector< Node >& exp, Node te );
 146   Node getLength( Node t, std::vector< Node >& exp );
 147
 148 private:
 149   /** The notify class */
 150   NotifyClass d_notify;
 151   /** Equaltity engine */
 152   eq::EqualityEngine d_equalityEngine;
 153   /** Are we in conflict */
 154   context::CDO<bool> d_conflict;
 155   //list of pairs of nodes to merge
 156   std::map< Node, Node > d_pending_exp;
 157   std::vector< Node > d_pending;
 158   std::vector< Node > d_lemma_cache;
 159   std::map< Node, bool > d_pending_req_phase;
 160   /** inferences: maintained to ensure ref count for internally introduced nodes */
 161   NodeList d_infer;
 162   NodeList d_infer_exp;
 163   /** normal forms */
 164   std::map< Node, Node > d_normal_forms_base;
 165   std::map< Node, std::vector< Node > > d_normal_forms;
 166   std::map< Node, std::vector< Node > > d_normal_forms_exp;
 167   std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
 168   //map of pairs of terms that have the same normal form
 169   NodeIntMap d_nf_pairs;
 170   std::map< Node, std::vector< Node > > d_nf_pairs_data;
 171   void addNormalFormPair( Node n1, Node n2 );
 172   bool isNormalFormPair( Node n1, Node n2 );
 173   bool isNormalFormPair2( Node n1, Node n2 );
 174   // loop ant
 175   NodeSet d_loop_antec;
 176   // preReg cache
 177   NodeSet d_pregistered_terms_cache;
 178   NodeSet d_registered_terms_cache;
 179   NodeSet d_length_lemma_terms_cache;
 180   NodeSet d_skolem_ne_reg_cache;
 181   // preprocess cache
 182   StringsPreprocess d_preproc;
 183   NodeBoolMap d_preproc_cache;
 184   // extended functions inferences cache
 185   NodeSet d_extf_infer_cache;
 186   NodeSet d_extf_infer_cache_u;
 187   std::vector< Node > d_empty_vec;
 188   //
 189   NodeList d_ee_disequalities;
 190 private:
 191   NodeSet d_congruent;
 192   std::map< Node, Node > d_eqc_to_const;
 193   std::map< Node, Node > d_eqc_to_const_base;
 194   std::map< Node, Node > d_eqc_to_const_exp;
 195   Node getConstantEqc( Node eqc );
 196
 197   std::map< Node, Node > d_eqc_to_len_term;
 198   std::vector< Node > d_strings_eqc;
 199   Node d_emptyString_r;
 200   class TermIndex {
 201   public:
 202     Node d_data;
 203     std::map< TNode, TermIndex > d_children;
 204     Node add( TNode n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c );
 205     void clear(){ d_children.clear(); }
 206   };
 207   std::map< Kind, TermIndex > d_term_index;
 208   //list of non-congruent concat terms in each eqc
 209   std::map< Node, std::vector< Node > > d_eqc;
 210   std::map< Node, std::vector< Node > > d_flat_form;
 211   std::map< Node, std::vector< int > > d_flat_form_index;
 212
 213   void debugPrintFlatForms( const char * tc );
 214   void debugPrintNormalForms( const char * tc );
 215   /////////////////////////////////////////////////////////////////////////////
 216   // MODEL GENERATION
 217   /////////////////////////////////////////////////////////////////////////////
 218 public:
 219   void collectModelInfo(TheoryModel* m, bool fullModel);
 220
 221   /////////////////////////////////////////////////////////////////////////////
 222   // NOTIFICATIONS
 223   /////////////////////////////////////////////////////////////////////////////
 224 public:
 225   void presolve();
 226   void shutdown() { }
 227
 228   /////////////////////////////////////////////////////////////////////////////
 229   // MAIN SOLVER
 230   /////////////////////////////////////////////////////////////////////////////
 231 private:
 232   void addSharedTerm(TNode n);
 233   EqualityStatus getEqualityStatus(TNode a, TNode b);
 234
 235 private:
 236   class EqcInfo {
 237   public:
 238     EqcInfo( context::Context* c );
 239     ~EqcInfo(){}
 240     //constant in this eqc
 241     context::CDO< Node > d_length_term;
 242     context::CDO< unsigned > d_cardinality_lem_k;
 243     // 1 = added length lemma
 244     context::CDO< Node > d_normalized_length;
 245   };
 246   /** map from representatives to information necessary for equivalence classes */
 247   std::map< Node, EqcInfo* > d_eqc_info;
 248   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 249   //maintain which concat terms have the length lemma instantiated
 250   NodeNodeMap d_proxy_var;
 251   NodeNodeMap d_proxy_var_to_length;
 252   /** All the function terms that the theory has seen */
 253   context::CDList<TNode> d_functionsTerms;
 254 private:
 255   //any non-reduced extended functions exist
 256   context::CDO< bool > d_has_extf;
 257   // static information about extf
 258   class ExtfInfo {
 259   public:
 260     //all variables in this term
 261     std::vector< Node > d_vars;
 262   };
 263   // non-static information about extf
 264   class ExtfInfoTmp {
 265   public:
 266     void init(){
 267       d_pol = 0;
 268       d_model_active = true;
 269     }
 270     // list of terms that something (does not) contain and their explanation
 271     std::map< bool, std::vector< Node > > d_ctn;
 272     std::map< bool, std::vector< Node > > d_ctn_from;
 273     //polarity
 274     int d_pol;
 275     //explanation
 276     std::vector< Node > d_exp;
 277     //false if it is reduced in the model
 278     bool d_model_active;
 279   };
 280   std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
 281   //collect extended operator terms
 282   void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
 283 private:
 284   class InferInfo {
 285   public:
 286     unsigned d_i;
 287     unsigned d_j;
 288     bool d_rev;
 289     std::vector< Node > d_ant;
 290     std::vector< Node > d_antn;
 291     std::map< int, std::vector< Node > > d_new_skolem;
 292     Node d_conc;
 293     unsigned d_id;
 294     std::map< Node, bool > d_pending_phase;
 295     unsigned d_index;
 296     const char * getId() {
 297       switch( d_id ){
 298       case 1:return "S-Split(CST-P)-prop";break;
 299       case 2:return "S-Split(VAR)-prop";break;
 300       case 3:return "Len-Split(Len)";break;
 301       case 4:return "Len-Split(Emp)";break;
 302       case 5:return "S-Split(CST-P)-binary";break;
 303       case 6:return "S-Split(CST-P)";break;
 304       case 7:return "S-Split(VAR)";break;
 305       case 8:return "F-Loop";break;
 306       default:break;
 307       }
 308       return "";
 309     }
 310     bool sendAsLemma();
 311   };
 312   //initial check
 313   void checkInit();
 314   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
 315   //extended functions evaluation check
 316   void checkExtfEval( int effort = 0 );
 317   void checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort );
 318   void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
 319   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
 320   //check extf reduction
 321   void checkExtfReductions( int effort );
 322   //flat forms check
 323   void checkFlatForms();
 324   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
 325   //normal forms check
 326   void checkNormalForms();
 327   void normalizeEquivalenceClass( Node n );
 328   void getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 329                        std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend );
 330   bool detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc );
 331   bool processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 332                     int i, int j, int loop_n_index, int other_n_index,int loop_index, int index, InferInfo& info );
 333   void processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 334                     std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend );
 335   void processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 336                           std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 337                           unsigned i, unsigned j, unsigned& index, unsigned rproc, std::vector< InferInfo >& pinfer );
 338   void processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 339                          std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 340                          unsigned i, unsigned j, unsigned& index, bool isRev, unsigned rproc, std::vector< InferInfo >& pinfer );
 341   void processDeq( Node n1, Node n2 );
 342   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 343   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 344   void checkDeqNF();
 345   void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 346                                       unsigned i, int index, bool isRev, std::vector< Node >& curr_exp );
 347   void getExplanationVectorForPrefixEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 348                                         std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 349                                         unsigned i, unsigned j, int index_i, int index_j, bool isRev, std::vector< Node >& curr_exp );
 350
 351   Node collectConstantStringAt( std::vector< Node >& vec, int& index, bool isRev );
 352
 353   //check membership constraints
 354   Node mkRegExpAntec(Node atom, Node ant);
 355   Node normalizeRegexp(Node r);
 356   bool normalizePosMemberships( std::map< Node, std::vector< Node > > &memb_with_exps );
 357   bool applyRConsume( CVC4::String &s, Node &r );
 358   Node applyRSplit( Node s1, Node s2, Node r );
 359   bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
 360   bool checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps,
 361                                       std::map< Node, std::vector< Node > > &XinR_with_exps);
 362   void checkMemberships();
 363   bool checkMemberships2();
 364   bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma,
 365                          std::vector< Node > &processed, std::vector< Node > &cprocessed,
 366                          std::vector< Node > &nf_exp);
 367   //check contains
 368   void checkPosContains( std::vector< Node >& posContains );
 369   void checkNegContains( std::vector< Node >& negContains );
 370   //lengths normalize check
 371   void checkLengthsEqc();
 372   //cardinality check
 373   void checkCardinality();
 374
 375 private:
 376   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 377 public:
 378   /** preregister term */
 379   void preRegisterTerm(TNode n);
 380   /** Expand definition */
 381   Node expandDefinition(LogicRequest &logicRequest, Node n);
 382   /** Check at effort e */
 383   void check(Effort e);
 384   /** needs check last effort */
 385   bool needsCheckLastEffort();
 386   /** Conflict when merging two constants */
 387   void conflict(TNode a, TNode b);
 388   /** called when a new equivalence class is created */
 389   void eqNotifyNewClass(TNode t);
 390   /** called when two equivalence classes will merge */
 391   void eqNotifyPreMerge(TNode t1, TNode t2);
 392   /** called when two equivalence classes have merged */
 393   void eqNotifyPostMerge(TNode t1, TNode t2);
 394   /** called when two equivalence classes are made disequal */
 395   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 396   /** get preprocess */
 397   StringsPreprocess * getPreprocess() { return &d_preproc; }
 398 protected:
 399   /** compute care graph */
 400   void computeCareGraph();
 401
 402   //do pending merges
 403   void assertPendingFact(Node atom, bool polarity, Node exp);
 404   void doPendingFacts();
 405   void doPendingLemmas();
 406   bool hasProcessed();
 407   void addToExplanation( Node a, Node b, std::vector< Node >& exp );
 408   void addToExplanation( Node lit, std::vector< Node >& exp );
 409
 410   //register term
 411   void registerTerm( Node n, int effort );
 412   //send lemma
 413   void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false );
 414   void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false );
 415   void sendLemma( Node ant, Node conc, const char * c );
 416   void sendInfer( Node eq_exp, Node eq, const char * c );
 417   void sendSplit( Node a, Node b, const char * c, bool preq = true );
 418   void sendLengthLemma( Node n );
 419   /** mkConcat **/
 420   inline Node mkConcat( Node n1, Node n2 );
 421   inline Node mkConcat( Node n1, Node n2, Node n3 );
 422   inline Node mkConcat( const std::vector< Node >& c );
 423   inline Node mkLength( Node n );
 424   //mkSkolem
 425   enum {
 426     sk_id_c_spt,
 427     sk_id_vc_spt,
 428     sk_id_vc_bin_spt,
 429     sk_id_v_spt,
 430     sk_id_c_spt_rev,
 431     sk_id_vc_spt_rev,
 432     sk_id_vc_bin_spt_rev,
 433     sk_id_v_spt_rev,
 434     sk_id_ctn_pre,
 435     sk_id_ctn_post,
 436     sk_id_dc_spt,
 437     sk_id_dc_spt_rem,
 438     sk_id_deq_x,
 439     sk_id_deq_y,
 440     sk_id_deq_z,
 441   };
 442   std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
 443   Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
 444   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
 445   void registerNonEmptySkolem( Node sk );
 446   //inline Node mkSkolemI(const char * c);
 447   /** mkExplain **/
 448   Node mkExplain( std::vector< Node >& a );
 449   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 450   /** mkAnd **/
 451   Node mkAnd( std::vector< Node >& a );
 452   /** get concat vector */
 453   void getConcatVec( Node n, std::vector< Node >& c );
 454
 455   //get equivalence classes
 456   void getEquivalenceClasses( std::vector< Node >& eqcs );
 457
 458   //separate into collections with equal length
 459   void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 460   void printConcat( std::vector< Node >& n, const char * c );
 461
 462   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
 463
 464   // Symbolic Regular Expression
 465 private:
 466   // regular expression memberships
 467   NodeList d_regexp_memberships;
 468   NodeSet d_regexp_ucached;
 469   NodeSet d_regexp_ccached;
 470   // stored assertions
 471   NodeIntMap d_pos_memberships;
 472   std::map< Node, std::vector< Node > > d_pos_memberships_data;
 473   NodeIntMap d_neg_memberships;
 474   std::map< Node, std::vector< Node > > d_neg_memberships_data;
 475   unsigned getNumMemberships( Node n, bool isPos );
 476   Node getMembership( Node n, bool isPos, unsigned i );
 477   // semi normal forms for symbolic expression
 478   std::map< Node, Node > d_nf_regexps;
 479   std::map< Node, std::vector< Node > > d_nf_regexps_exp;
 480   // intersection
 481   NodeNodeMap d_inter_cache;
 482   NodeIntMap d_inter_index;
 483   // processed memberships
 484   NodeSet d_processed_memberships;
 485   // antecedant for why regexp membership must be true
 486   NodeNodeMap d_regexp_ant;
 487   // membership length
 488   //std::map< Node, bool > d_membership_length;
 489   // regular expression operations
 490   RegExpOpr d_regexp_opr;
 491
 492   CVC4::String getHeadConst( Node x );
 493   bool deriveRegExp( Node x, Node r, Node ant );
 494   void addMembership(Node assertion);
 495   Node getNormalString(Node x, std::vector<Node> &nf_exp);
 496   Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 497
 498
 499   // Finite Model Finding
 500 private:
 501   NodeSet d_input_vars;
 502   context::CDO< Node > d_input_var_lsum;
 503   context::CDHashMap< int, Node > d_cardinality_lits;
 504   context::CDO< int > d_curr_cardinality;
 505 public:
 506   //for finite model finding
 507   Node getNextDecisionRequest();
 508   //ppRewrite
 509   Node ppRewrite(TNode atom);
 510 public:
 511 /** statistics class */
 512   class Statistics {
 513   public:
 514     IntStat d_splits;
 515     IntStat d_eq_splits;
 516     IntStat d_deq_splits;
 517     IntStat d_loop_lemmas;
 518     IntStat d_new_skolems;
 519     Statistics();
 520     ~Statistics();
 521   };/* class TheoryStrings::Statistics */
 522   Statistics d_statistics;
 523
 524 };/* class TheoryStrings */
 525
 526 }/* CVC4::theory::strings namespace */
 527 }/* CVC4::theory namespace */
 528 }/* CVC4 namespace */
 529
 530 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */