src/theory/strings/theory_strings.h

   1 /*********************                                                        */
   2 /*! \file theory_strings.h
   3  ** \verbatim
   4  ** Original author: Tianyi Liang
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace strings {
  33
  34 /**
  35  * Decision procedure for strings.
  36  *
  37  */
  38
  39 class TheoryStrings : public Theory {
  40   typedef context::CDChunkList<Node> NodeList;
  41   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
  42   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  43   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  44   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  45   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  46
  47 public:
  48   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  49   ~TheoryStrings();
  50
  51   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  52
  53   std::string identify() const { return std::string("TheoryStrings"); }
  54
  55 public:
  56   void propagate(Effort e);
  57   bool propagate(TNode literal);
  58   void explain( TNode literal, std::vector<TNode>& assumptions );
  59   Node explain( TNode literal );
  60
  61
  62   // NotifyClass for equality engine
  63   class NotifyClass : public eq::EqualityEngineNotify {
  64     TheoryStrings& d_str;
  65   public:
  66     NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
  67     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  68       Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  69       if (value) {
  70         return d_str.propagate(equality);
  71       } else {
  72         // We use only literal triggers so taking not is safe
  73         return d_str.propagate(equality.notNode());
  74       }
  75     }
  76     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  77       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  78       if (value) {
  79         return d_str.propagate(predicate);
  80       } else {
  81          return d_str.propagate(predicate.notNode());
  82       }
  83     }
  84     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  85       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  86       if (value) {
  87       return d_str.propagate(t1.eqNode(t2));
  88       } else {
  89       return d_str.propagate(t1.eqNode(t2).notNode());
  90       }
  91     }
  92     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  93       Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  94       d_str.conflict(t1, t2);
  95     }
  96     void eqNotifyNewClass(TNode t) {
  97       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
  98       d_str.eqNotifyNewClass(t);
  99     }
 100     void eqNotifyPreMerge(TNode t1, TNode t2) {
 101       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
 102       d_str.eqNotifyPreMerge(t1, t2);
 103     }
 104     void eqNotifyPostMerge(TNode t1, TNode t2) {
 105       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 106       d_str.eqNotifyPostMerge(t1, t2);
 107     }
 108     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 109       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
 110       d_str.eqNotifyDisequal(t1, t2, reason);
 111     }
 112   };/* class TheoryStrings::NotifyClass */
 113
 114 private:
 115   /**
 116    * Function symbol used to implement uninterpreted undefined string
 117    * semantics.  Needed to deal with partial charat/substr function.
 118    */
 119   Node d_ufSubstr;
 120
 121   // Constants
 122   Node d_emptyString;
 123   Node d_emptyRegexp;
 124   Node d_true;
 125   Node d_false;
 126   Node d_zero;
 127   Node d_one;
 128   // Options
 129   bool d_opt_fmf;
 130   bool d_opt_regexp_gcd;
 131   // Helper functions
 132   Node getRepresentative( Node t );
 133   bool hasTerm( Node a );
 134   bool areEqual( Node a, Node b );
 135   bool areDisequal( Node a, Node b );
 136   Node getLengthTerm( Node t );
 137   Node getLength( Node t );
 138
 139 private:
 140   /** The notify class */
 141   NotifyClass d_notify;
 142   /** Equaltity engine */
 143   eq::EqualityEngine d_equalityEngine;
 144   /** Are we in conflict */
 145   context::CDO<bool> d_conflict;
 146   //list of pairs of nodes to merge
 147   std::map< Node, Node > d_pending_exp;
 148   std::vector< Node > d_pending;
 149   std::vector< Node > d_lemma_cache;
 150   std::map< Node, bool > d_pending_req_phase;
 151   /** inferences */
 152   NodeList d_infer;
 153   NodeList d_infer_exp;
 154   /** normal forms */
 155   std::map< Node, Node > d_normal_forms_base;
 156   std::map< Node, std::vector< Node > > d_normal_forms;
 157   std::map< Node, std::vector< Node > > d_normal_forms_exp;
 158   //map of pairs of terms that have the same normal form
 159   NodeListMap d_nf_pairs;
 160   void addNormalFormPair( Node n1, Node n2 );
 161   bool isNormalFormPair( Node n1, Node n2 );
 162   bool isNormalFormPair2( Node n1, Node n2 );
 163   // loop ant
 164   NodeSet d_loop_antec;
 165   NodeSet d_length_intro_vars;
 166   // preReg cache
 167   NodeSet d_registed_terms_cache;
 168   // term cache
 169   std::vector< Node > d_terms_cache;
 170   void collectTerm( Node n );
 171   void appendTermLemma();
 172
 173   /////////////////////////////////////////////////////////////////////////////
 174   // MODEL GENERATION
 175   /////////////////////////////////////////////////////////////////////////////
 176 public:
 177   void collectModelInfo(TheoryModel* m, bool fullModel);
 178
 179   /////////////////////////////////////////////////////////////////////////////
 180   // NOTIFICATIONS
 181   /////////////////////////////////////////////////////////////////////////////
 182 public:
 183   void presolve();
 184   void shutdown() { }
 185
 186   /////////////////////////////////////////////////////////////////////////////
 187   // MAIN SOLVER
 188   /////////////////////////////////////////////////////////////////////////////
 189 private:
 190   void addSharedTerm(TNode n);
 191   EqualityStatus getEqualityStatus(TNode a, TNode b);
 192
 193 private:
 194   class EqcInfo {
 195   public:
 196     EqcInfo( context::Context* c );
 197     ~EqcInfo(){}
 198     //constant in this eqc
 199     context::CDO< Node > d_const_term;
 200     context::CDO< Node > d_length_term;
 201     context::CDO< unsigned > d_cardinality_lem_k;
 202     // 1 = added length lemma
 203     context::CDO< Node > d_normalized_length;
 204   };
 205   /** map from representatives to information necessary for equivalence classes */
 206   std::map< Node, EqcInfo* > d_eqc_info;
 207   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 208   //maintain which concat terms have the length lemma instantiated
 209   NodeSet d_length_nodes;
 210   NodeNodeMap d_length_inst;
 211 private:
 212   void mergeCstVec(std::vector< Node > &vec_strings);
 213   bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
 214         std::vector< std::vector< Node > > &normal_forms,
 215         std::vector< std::vector< Node > > &normal_forms_exp,
 216         std::vector< Node > &normal_form_src);
 217   bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
 218         int i, int j, int index_i, int index_j,
 219         int &loop_in_i, int &loop_in_j);
 220   bool processLoop(std::vector< Node > &antec,
 221         std::vector< std::vector< Node > > &normal_forms,
 222         std::vector< Node > &normal_form_src,
 223         int i, int j, int loop_n_index, int other_n_index,
 224         int loop_index, int index, int other_index);
 225   bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
 226         std::vector< std::vector< Node > > &normal_forms_exp,
 227         std::vector< Node > &normal_form_src);
 228   bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
 229         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
 230   bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
 231         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
 232         unsigned& index_i, unsigned& index_j, bool isRev );
 233   bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
 234   bool processDeq( Node n1, Node n2 );
 235   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 236   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 237   //bool unrollStar( Node atom );
 238   Node mkRegExpAntec(Node atom, Node ant);
 239
 240   bool checkSimple();
 241   bool checkNormalForms();
 242   void checkDeqNF();
 243   bool checkLengthsEqc();
 244   bool checkCardinality();
 245   bool checkInductiveEquations();
 246   bool checkMemberships();
 247   bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
 248     std::vector< Node > &processed, std::vector< Node > &cprocessed,
 249     std::vector< Node > &nf_exp);
 250   bool checkContains();
 251   bool checkPosContains();
 252   bool checkNegContains();
 253
 254 public:
 255   void preRegisterTerm(TNode n);
 256   Node expandDefinition(LogicRequest &logicRequest, Node n);
 257   void check(Effort e);
 258
 259   /** Conflict when merging two constants */
 260   void conflict(TNode a, TNode b);
 261   /** called when a new equivalence class is created */
 262   void eqNotifyNewClass(TNode t);
 263   /** called when two equivalence classes will merge */
 264   void eqNotifyPreMerge(TNode t1, TNode t2);
 265   /** called when two equivalence classes have merged */
 266   void eqNotifyPostMerge(TNode t1, TNode t2);
 267   /** called when two equivalence classes are made disequal */
 268   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 269 protected:
 270   /** compute care graph */
 271   void computeCareGraph();
 272
 273   //do pending merges
 274   void assertPendingFact(Node fact, Node exp);
 275   void doPendingFacts();
 276   void doPendingLemmas();
 277
 278   //register term
 279   bool registerTerm( Node n );
 280   //send lemma
 281   void sendLemma( Node ant, Node conc, const char * c );
 282   void sendInfer( Node eq_exp, Node eq, const char * c );
 283   void sendSplit( Node a, Node b, const char * c, bool preq = true );
 284   /** mkConcat **/
 285   inline Node mkConcat( Node n1, Node n2 );
 286   inline Node mkConcat( Node n1, Node n2, Node n3 );
 287   inline Node mkConcat( const std::vector< Node >& c );
 288   //mkSkolem
 289   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
 290   //inline Node mkSkolemI(const char * c);
 291   /** mkExplain **/
 292   Node mkExplain( std::vector< Node >& a );
 293   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 294   /** mkAnd **/
 295   Node mkAnd( std::vector< Node >& a );
 296   /** get concat vector */
 297   void getConcatVec( Node n, std::vector< Node >& c );
 298
 299   //get equivalence classes
 300   void getEquivalenceClasses( std::vector< Node >& eqcs );
 301   //get final normal form
 302   void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 303
 304   //separate into collections with equal length
 305   void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 306   void printConcat( std::vector< Node >& n, const char * c );
 307
 308 private:
 309   Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 310
 311   // Special String Functions
 312   NodeList d_str_pos_ctn;
 313   NodeList d_str_neg_ctn;
 314   NodeSet d_neg_ctn_eqlen;
 315   NodeSet d_neg_ctn_ulen;
 316   NodeSet d_pos_ctn_cached;
 317   NodeSet d_neg_ctn_cached;
 318
 319   // Symbolic Regular Expression
 320 private:
 321   // regular expression memberships
 322   NodeList d_regexp_memberships;
 323   NodeSet d_regexp_ucached;
 324   NodeSet d_regexp_ccached;
 325   // intersection
 326   NodeListMap d_str_re_map;
 327   NodeNodeMap d_inter_cache;
 328   NodeIntMap d_inter_index;
 329   // antecedant for why regexp membership must be true
 330   NodeNodeMap d_regexp_ant;
 331   // membership length
 332   //std::map< Node, bool > d_membership_length;
 333   // regular expression operations
 334   RegExpOpr d_regexp_opr;
 335
 336   CVC4::String getHeadConst( Node x );
 337   bool deriveRegExp( Node x, Node r, Node ant );
 338   bool addMembershipLength(Node atom);
 339   void addMembership(Node assertion);
 340   Node getNormalString(Node x, std::vector<Node> &nf_exp);
 341   Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 342
 343
 344   // Finite Model Finding
 345 private:
 346   NodeSet d_input_vars;
 347   context::CDO< Node > d_input_var_lsum;
 348   context::CDHashMap< int, Node > d_cardinality_lits;
 349   context::CDO< int > d_curr_cardinality;
 350 public:
 351   //for finite model finding
 352   Node getNextDecisionRequest();
 353   void assertNode( Node lit );
 354
 355 public:
 356 /** statistics class */
 357   class Statistics {
 358   public:
 359     IntStat d_splits;
 360     IntStat d_eq_splits;
 361     IntStat d_deq_splits;
 362     IntStat d_loop_lemmas;
 363     IntStat d_new_skolems;
 364     Statistics();
 365     ~Statistics();
 366   };/* class TheoryStrings::Statistics */
 367   Statistics d_statistics;
 368 };/* class TheoryStrings */
 369
 370 }/* CVC4::theory::strings namespace */
 371 }/* CVC4::theory namespace */
 372 }/* CVC4 namespace */
 373
 374 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */