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
  74
  75   // NotifyClass for equality engine
  76   class NotifyClass : public eq::EqualityEngineNotify {
  77     TheoryStrings& d_str;
  78   public:
  79     NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
  80     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  81       Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  82       if (value) {
  83         return d_str.propagate(equality);
  84       } else {
  85         // We use only literal triggers so taking not is safe
  86         return d_str.propagate(equality.notNode());
  87       }
  88     }
  89     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  90       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  91       if (value) {
  92         return d_str.propagate(predicate);
  93       } else {
  94          return d_str.propagate(predicate.notNode());
  95       }
  96     }
  97     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  98       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  99       if (value) {
 100       return d_str.propagate(t1.eqNode(t2));
 101       } else {
 102       return d_str.propagate(t1.eqNode(t2).notNode());
 103       }
 104     }
 105     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 106       Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 107       d_str.conflict(t1, t2);
 108     }
 109     void eqNotifyNewClass(TNode t) {
 110       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
 111       d_str.eqNotifyNewClass(t);
 112     }
 113     void eqNotifyPreMerge(TNode t1, TNode t2) {
 114       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
 115       d_str.eqNotifyPreMerge(t1, t2);
 116     }
 117     void eqNotifyPostMerge(TNode t1, TNode t2) {
 118       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 119       d_str.eqNotifyPostMerge(t1, t2);
 120     }
 121     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 122       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
 123       d_str.eqNotifyDisequal(t1, t2, reason);
 124     }
 125   };/* class TheoryStrings::NotifyClass */
 126
 127 private:
 128   // Constants
 129   Node d_emptyString;
 130   Node d_emptyRegexp;
 131   Node d_true;
 132   Node d_false;
 133   Node d_zero;
 134   Node d_one;
 135   CVC4::Rational RMAXINT;
 136   unsigned d_card_size;
 137   // Helper functions
 138   Node getRepresentative( Node t );
 139   bool hasTerm( Node a );
 140   bool areEqual( Node a, Node b );
 141   bool areDisequal( Node a, Node b );
 142   // t is representative, te = t, add lt = te to explanation exp
 143   Node getLengthExp( Node t, std::vector< Node >& exp, Node te );
 144   Node getLength( Node t, std::vector< Node >& exp );
 145
 146 private:
 147   /** The notify class */
 148   NotifyClass d_notify;
 149   /** Equaltity engine */
 150   eq::EqualityEngine d_equalityEngine;
 151   /** Are we in conflict */
 152   context::CDO<bool> d_conflict;
 153   //list of pairs of nodes to merge
 154   std::map< Node, Node > d_pending_exp;
 155   std::vector< Node > d_pending;
 156   std::vector< Node > d_lemma_cache;
 157   std::map< Node, bool > d_pending_req_phase;
 158   /** inferences: maintained to ensure ref count for internally introduced nodes */
 159   NodeList d_infer;
 160   NodeList d_infer_exp;
 161   /** normal forms */
 162   std::map< Node, Node > d_normal_forms_base;
 163   std::map< Node, std::vector< Node > > d_normal_forms;
 164   std::map< Node, std::vector< Node > > d_normal_forms_exp;
 165   std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend;
 166   //map of pairs of terms that have the same normal form
 167   NodeIntMap d_nf_pairs;
 168   std::map< Node, std::vector< Node > > d_nf_pairs_data;
 169   void addNormalFormPair( Node n1, Node n2 );
 170   bool isNormalFormPair( Node n1, Node n2 );
 171   bool isNormalFormPair2( Node n1, Node n2 );
 172   // loop ant
 173   NodeSet d_loop_antec;
 174   NodeSet d_length_intro_vars;
 175   // preReg cache
 176   NodeSet d_pregistered_terms_cache;
 177   NodeSet d_registered_terms_cache;
 178   // preprocess cache
 179   StringsPreprocess d_preproc;
 180   NodeBoolMap d_preproc_cache;
 181   // extended functions inferences cache
 182   NodeSet d_extf_infer_cache;
 183   std::vector< Node > d_empty_vec;
 184   //
 185   NodeList d_ee_disequalities;
 186 private:
 187   NodeSet d_congruent;
 188   std::map< Node, Node > d_eqc_to_const;
 189   std::map< Node, Node > d_eqc_to_const_base;
 190   std::map< Node, Node > d_eqc_to_const_exp;
 191   std::map< Node, Node > d_eqc_to_len_term;
 192   std::vector< Node > d_strings_eqc;
 193   Node d_emptyString_r;
 194   class TermIndex {
 195   public:
 196     Node d_data;
 197     std::map< Node, TermIndex > d_children;
 198     Node add( Node n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c );
 199     void clear(){ d_children.clear(); }
 200   };
 201   std::map< Kind, TermIndex > d_term_index;
 202   //list of non-congruent concat terms in each eqc
 203   std::map< Node, std::vector< Node > > d_eqc;
 204   std::map< Node, std::vector< Node > > d_flat_form;
 205   std::map< Node, std::vector< int > > d_flat_form_index;
 206
 207   void debugPrintFlatForms( const char * tc );
 208   /////////////////////////////////////////////////////////////////////////////
 209   // MODEL GENERATION
 210   /////////////////////////////////////////////////////////////////////////////
 211 public:
 212   void collectModelInfo(TheoryModel* m, bool fullModel);
 213
 214   /////////////////////////////////////////////////////////////////////////////
 215   // NOTIFICATIONS
 216   /////////////////////////////////////////////////////////////////////////////
 217 public:
 218   void presolve();
 219   void shutdown() { }
 220
 221   /////////////////////////////////////////////////////////////////////////////
 222   // MAIN SOLVER
 223   /////////////////////////////////////////////////////////////////////////////
 224 private:
 225   void addSharedTerm(TNode n);
 226   EqualityStatus getEqualityStatus(TNode a, TNode b);
 227
 228 private:
 229   class EqcInfo {
 230   public:
 231     EqcInfo( context::Context* c );
 232     ~EqcInfo(){}
 233     //constant in this eqc
 234     context::CDO< Node > d_const_term;
 235     context::CDO< Node > d_length_term;
 236     context::CDO< unsigned > d_cardinality_lem_k;
 237     // 1 = added length lemma
 238     context::CDO< Node > d_normalized_length;
 239   };
 240   /** map from representatives to information necessary for equivalence classes */
 241   std::map< Node, EqcInfo* > d_eqc_info;
 242   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 243   //maintain which concat terms have the length lemma instantiated
 244   NodeNodeMap d_proxy_var;
 245   NodeNodeMap d_proxy_var_to_length;
 246   /** All the function terms that the theory has seen */
 247   context::CDList<TNode> d_functionsTerms;
 248 private:
 249   //initial check
 250   void checkInit();
 251   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
 252   //extended functions evaluation check
 253   void checkExtendedFuncsEval( int effort = 0 );
 254   void checkExtfInference( Node n, Node nr, int effort );
 255   void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
 256   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
 257   //check extf reduction
 258   void checkExtfReduction( int effort );
 259   void checkReduction( Node atom, int pol, int effort );
 260   //flat forms check
 261   void checkFlatForms();
 262   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
 263   //normal forms check
 264   void checkNormalForms();
 265   bool normalizeEquivalenceClass( Node n, std::vector< Node > & nf, std::vector< Node > & nf_exp );
 266   bool getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 267                        std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend);
 268   bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
 269         int i, int j, int index, int &loop_in_i, int &loop_in_j);
 270   bool processLoop(std::vector< Node > &antec,
 271         std::vector< std::vector< Node > > &normal_forms,
 272         std::vector< Node > &normal_form_src,
 273         int i, int j, int loop_n_index, int other_n_index,
 274         int loop_index, int index);
 275   bool processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 276                     std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend );
 277   bool processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 278                           std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 279                           unsigned i, unsigned j );
 280   bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 281                          std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 282                          unsigned i, unsigned j, unsigned& index, bool isRev );
 283   bool processDeq( Node n1, Node n2 );
 284   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 285   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 286   void checkDeqNF();
 287
 288   void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
 289                                       std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
 290                                       unsigned i, unsigned j, int index, bool isRev, std::vector< Node >& curr_exp );
 291
 292   //check membership constraints
 293   Node mkRegExpAntec(Node atom, Node ant);
 294   Node normalizeRegexp(Node r);
 295   bool normalizePosMemberships( std::map< Node, std::vector< Node > > &memb_with_exps );
 296   bool applyRConsume( CVC4::String &s, Node &r );
 297   Node applyRSplit( Node s1, Node s2, Node r );
 298   bool applyRLen( std::map< Node, std::vector< Node > > &XinR_with_exps );
 299   bool checkMembershipsWithoutLength( std::map< Node, std::vector< Node > > &memb_with_exps,
 300                                       std::map< Node, std::vector< Node > > &XinR_with_exps);
 301   void checkMemberships();
 302   bool checkMemberships2();
 303   bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma,
 304                          std::vector< Node > &processed, std::vector< Node > &cprocessed,
 305                          std::vector< Node > &nf_exp);
 306   //check contains
 307   void checkPosContains( std::vector< Node >& posContains );
 308   void checkNegContains( std::vector< Node >& negContains );
 309   //lengths normalize check
 310   void checkLengthsEqc();
 311   //cardinality check
 312   void checkCardinality();
 313
 314 private:
 315   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 316 public:
 317   /** preregister term */
 318   void preRegisterTerm(TNode n);
 319   /** Expand definition */
 320   Node expandDefinition(LogicRequest &logicRequest, Node n);
 321   /** Check at effort e */
 322   void check(Effort e);
 323   /** needs check last effort */
 324   bool needsCheckLastEffort();
 325   /** Conflict when merging two constants */
 326   void conflict(TNode a, TNode b);
 327   /** called when a new equivalence class is created */
 328   void eqNotifyNewClass(TNode t);
 329   /** called when two equivalence classes will merge */
 330   void eqNotifyPreMerge(TNode t1, TNode t2);
 331   /** called when two equivalence classes have merged */
 332   void eqNotifyPostMerge(TNode t1, TNode t2);
 333   /** called when two equivalence classes are made disequal */
 334   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 335   /** get preprocess */
 336   StringsPreprocess * getPreprocess() { return &d_preproc; }
 337 protected:
 338   /** compute care graph */
 339   void computeCareGraph();
 340
 341   //do pending merges
 342   void assertPendingFact(Node atom, bool polarity, Node exp);
 343   void doPendingFacts();
 344   void doPendingLemmas();
 345   bool hasProcessed();
 346   void addToExplanation( Node a, Node b, std::vector< Node >& exp );
 347   void addToExplanation( Node lit, std::vector< Node >& exp );
 348
 349   //register term
 350   void registerTerm( Node n, int effort );
 351   //send lemma
 352   void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false );
 353   void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false );
 354   void sendLemma( Node ant, Node conc, const char * c );
 355   void sendInfer( Node eq_exp, Node eq, const char * c );
 356   void sendSplit( Node a, Node b, const char * c, bool preq = true );
 357   void sendLengthLemma( Node n );
 358   /** mkConcat **/
 359   inline Node mkConcat( Node n1, Node n2 );
 360   inline Node mkConcat( Node n1, Node n2, Node n3 );
 361   inline Node mkConcat( const std::vector< Node >& c );
 362   inline Node mkLength( Node n );
 363   //mkSkolem
 364   enum {
 365     sk_id_c_spt,
 366     sk_id_vc_spt,
 367     sk_id_v_spt,
 368     sk_id_ctn_pre,
 369     sk_id_ctn_post,
 370     sk_id_deq_x,
 371     sk_id_deq_y,
 372     sk_id_deq_z,
 373   };
 374   std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
 375   Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
 376   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
 377   //inline Node mkSkolemI(const char * c);
 378   /** mkExplain **/
 379   Node mkExplain( std::vector< Node >& a );
 380   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 381   /** mkAnd **/
 382   Node mkAnd( std::vector< Node >& a );
 383   /** get concat vector */
 384   void getConcatVec( Node n, std::vector< Node >& c );
 385
 386   //get equivalence classes
 387   void getEquivalenceClasses( std::vector< Node >& eqcs );
 388   //get final normal form
 389   void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 390
 391   //separate into collections with equal length
 392   void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 393   void printConcat( std::vector< Node >& n, const char * c );
 394
 395   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
 396 private:
 397   //extended string terms and whether they have been reduced
 398   NodeBoolMap d_ext_func_terms;
 399   std::map< Node, std::map< Node, std::vector< Node > > > d_extf_vars;
 400   // list of terms that something (does not) contain and their explanation
 401   class ExtfInfo {
 402   public:
 403     std::map< bool, std::vector< Node > > d_ctn;
 404     std::map< bool, std::vector< Node > > d_ctn_from;
 405   };
 406   std::map< Node, int > d_extf_pol;
 407   std::map< Node, std::vector< Node > > d_extf_exp;
 408   std::map< Node, ExtfInfo > d_extf_info;
 409   //collect extended operator terms
 410   void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
 411
 412   // Symbolic Regular Expression
 413 private:
 414   // regular expression memberships
 415   NodeList d_regexp_memberships;
 416   NodeSet d_regexp_ucached;
 417   NodeSet d_regexp_ccached;
 418   // stored assertions
 419   NodeIntMap d_pos_memberships;
 420   std::map< Node, std::vector< Node > > d_pos_memberships_data;
 421   NodeIntMap d_neg_memberships;
 422   std::map< Node, std::vector< Node > > d_neg_memberships_data;
 423   unsigned getNumMemberships( Node n, bool isPos );
 424   Node getMembership( Node n, bool isPos, unsigned i );
 425   // semi normal forms for symbolic expression
 426   std::map< Node, Node > d_nf_regexps;
 427   std::map< Node, std::vector< Node > > d_nf_regexps_exp;
 428   // intersection
 429   NodeNodeMap d_inter_cache;
 430   NodeIntMap d_inter_index;
 431   // processed memberships
 432   NodeSet d_processed_memberships;
 433   // antecedant for why regexp membership must be true
 434   NodeNodeMap d_regexp_ant;
 435   // membership length
 436   //std::map< Node, bool > d_membership_length;
 437   // regular expression operations
 438   RegExpOpr d_regexp_opr;
 439
 440   CVC4::String getHeadConst( Node x );
 441   bool deriveRegExp( Node x, Node r, Node ant );
 442   void addMembership(Node assertion);
 443   Node getNormalString(Node x, std::vector<Node> &nf_exp);
 444   Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 445
 446
 447   // Finite Model Finding
 448 private:
 449   NodeSet d_input_vars;
 450   context::CDO< Node > d_input_var_lsum;
 451   context::CDHashMap< int, Node > d_cardinality_lits;
 452   context::CDO< int > d_curr_cardinality;
 453 public:
 454   //for finite model finding
 455   Node getNextDecisionRequest();
 456   //ppRewrite
 457   Node ppRewrite(TNode atom);
 458 public:
 459 /** statistics class */
 460   class Statistics {
 461   public:
 462     IntStat d_splits;
 463     IntStat d_eq_splits;
 464     IntStat d_deq_splits;
 465     IntStat d_loop_lemmas;
 466     IntStat d_new_skolems;
 467     Statistics();
 468     ~Statistics();
 469   };/* class TheoryStrings::Statistics */
 470   Statistics d_statistics;
 471 };/* class TheoryStrings */
 472
 473 }/* CVC4::theory::strings namespace */
 474 }/* CVC4::theory namespace */
 475 }/* CVC4 namespace */
 476
 477 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */