src/theory/strings/theory_strings.h

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