src/theory/datatypes/theory_datatypes.h

   1 /*********************                                                        */
   2 /*! \file theory_datatypes.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, 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 datatypes.
  13  **
  14  ** Theory of datatypes.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
  20 #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
  21
  22 #include <ext/hash_set>
  23 #include <iostream>
  24 #include <map>
  25
  26 #include "context/cdchunk_list.h"
  27 #include "expr/datatype.h"
  28 #include "theory/datatypes/datatypes_sygus.h"
  29 #include "theory/theory.h"
  30 #include "theory/uf/equality_engine.h"
  31 #include "util/hash.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35
  36 namespace quantifiers{
  37   class TermArgTrie;
  38 }
  39
  40 namespace datatypes {
  41
  42 class TheoryDatatypes : public Theory {
  43 private:
  44   typedef context::CDChunkList<Node> NodeList;
  45   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
  46   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  47   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
  48
  49   /** transitive closure to record equivalence/subterm relation.  */
  50   //TransitiveClosureNode d_cycle_check;
  51   /** has seen cycle */
  52   context::CDO< bool > d_hasSeenCycle;
  53   /** inferences */
  54   NodeList d_infer;
  55   NodeList d_infer_exp;
  56   Node d_true;
  57   /** mkAnd */
  58   Node mkAnd( std::vector< TNode >& assumptions );
  59 private:
  60   //notification class for equality engine
  61   class NotifyClass : public eq::EqualityEngineNotify {
  62     TheoryDatatypes& d_dt;
  63   public:
  64     NotifyClass(TheoryDatatypes& dt): d_dt(dt) {}
  65     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  66       Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  67       if (value) {
  68         return d_dt.propagate(equality);
  69       } else {
  70         // We use only literal triggers so taking not is safe
  71         return d_dt.propagate(equality.notNode());
  72       }
  73     }
  74     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  75       Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  76       if (value) {
  77         return d_dt.propagate(predicate);
  78       } else {
  79        return d_dt.propagate(predicate.notNode());
  80       }
  81     }
  82     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  83       Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  84       if (value) {
  85         return d_dt.propagate(t1.eqNode(t2));
  86       } else {
  87         return d_dt.propagate(t1.eqNode(t2).notNode());
  88       }
  89     }
  90     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  91       Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  92       d_dt.conflict(t1, t2);
  93     }
  94     void eqNotifyNewClass(TNode t) {
  95       Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
  96       d_dt.eqNotifyNewClass(t);
  97     }
  98     void eqNotifyPreMerge(TNode t1, TNode t2) {
  99       Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
 100       d_dt.eqNotifyPreMerge(t1, t2);
 101     }
 102     void eqNotifyPostMerge(TNode t1, TNode t2) {
 103       Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
 104       d_dt.eqNotifyPostMerge(t1, t2);
 105     }
 106     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 107       Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
 108       d_dt.eqNotifyDisequal(t1, t2, reason);
 109     }
 110   };/* class TheoryDatatypes::NotifyClass */
 111 private:
 112   /** equivalence class info
 113    * d_inst is whether the instantiate rule has been applied,
 114    * d_constructor is a node of kind APPLY_CONSTRUCTOR (if any) in this equivalence class,
 115    * d_selectors is whether a selector has been applied to this equivalence class.
 116    */
 117   class EqcInfo
 118   {
 119   public:
 120     EqcInfo( context::Context* c );
 121     ~EqcInfo(){}
 122     //whether we have instantiatied this eqc
 123     context::CDO< bool > d_inst;
 124     //constructor equal to this eqc
 125     context::CDO< Node > d_constructor;
 126     //all selectors whose argument is this eqc
 127     context::CDO< bool > d_selectors;
 128   };
 129   /** does eqc of n have a label (do we know its constructor)? */
 130   bool hasLabel( EqcInfo* eqc, Node n );
 131   /** get the label associated to n */
 132   Node getLabel( Node n );
 133   /** get the index of the label associated to n */
 134   int getLabelIndex( EqcInfo* eqc, Node n );
 135   /** does eqc of n have any testers? */
 136   bool hasTester( Node n );
 137   /** get the possible constructors for n */
 138   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
 139   void getSelectorsForCons( Node r, std::map< int, bool >& sels );
 140   /** mkExpDefSkolem */
 141   void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
 142   /** skolems for terms */
 143   NodeMap d_term_sk;
 144   Node getTermSkolemFor( Node n );
 145 private:
 146   /** The notify class */
 147   NotifyClass d_notify;
 148   /** Equaltity engine */
 149   eq::EqualityEngine d_equalityEngine;
 150   /** information necessary for equivalence classes */
 151   std::map< Node, EqcInfo* > d_eqc_info;
 152   /** map from nodes to their instantiated equivalent for each constructor type */
 153   std::map< Node, std::map< int, Node > > d_inst_map;
 154   /** which instantiation lemmas we have sent */
 155   //std::map< Node, std::vector< Node > > d_inst_lemmas;
 156   /** labels for each equivalence class
 157    * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either:
 158    * a list of equations of the form
 159    *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers
 160    *   and n is less than the number of possible constructors for t minus one,
 161    * or a list of equations of the form
 162    *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t )  followed by
 163    *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
 164   */
 165   NodeIntMap d_labels;
 166   std::map< Node, std::vector< Node > > d_labels_data;
 167   /** selector apps for eqch equivalence class */
 168   NodeIntMap d_selector_apps;
 169   std::map< Node, std::vector< Node > > d_selector_apps_data;
 170   /** constructor terms */
 171   //BoolMap d_consEqc;
 172   /** Are we in conflict */
 173   context::CDO<bool> d_conflict;
 174   /** Added lemma ? */
 175   bool d_addedLemma;
 176   bool d_addedFact;
 177   /** The conflict node */
 178   Node d_conflictNode;
 179   /** cache for which terms we have called collectTerms(...) on */
 180   BoolMap d_collectTermsCache;
 181   /** pending assertions/merges */
 182   std::vector< Node > d_pending_lem;
 183   std::vector< Node > d_pending;
 184   std::map< Node, Node > d_pending_exp;
 185   std::vector< Node > d_pending_merge;
 186   /** All the function terms that the theory has seen */
 187   context::CDList<TNode> d_functionTerms;
 188   /** counter for forcing assignments (ensures fairness) */
 189   unsigned d_dtfCounter;
 190   /** expand definition skolem functions */
 191   std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem;
 192   /** sygus utilities */
 193   SygusSplit * d_sygus_split;
 194   SygusSymBreak * d_sygus_sym_break;
 195
 196 private:
 197   /** singleton lemmas (for degenerate co-datatype case) */
 198   std::map< TypeNode, Node > d_singleton_lemma[2];
 199   /** Cache for singleton equalities processed */
 200   BoolMap d_singleton_eq;
 201   /** list of all lemmas produced */
 202   BoolMap d_lemmas_produced_c;
 203 private:
 204   /** assert fact */
 205   void assertFact( Node fact, Node exp );
 206
 207   /** flush pending facts */
 208   void flushPendingFacts();
 209
 210   /** do pending merged */
 211   void doPendingMerges();
 212   /** do send lemma */
 213   bool doSendLemma( Node lem );
 214   /** get or make eqc info */
 215   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 216
 217   /** has eqc info */
 218   bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); }
 219
 220   /** get eqc constructor */
 221   TNode getEqcConstructor( TNode r );
 222
 223 protected:
 224   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
 225   /** compute care graph */
 226   void computeCareGraph();
 227
 228 public:
 229   TheoryDatatypes(context::Context* c, context::UserContext* u,
 230                   OutputChannel& out, Valuation valuation,
 231                   const LogicInfo& logicInfo);
 232   ~TheoryDatatypes();
 233
 234   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 235
 236   /** propagate */
 237   void propagate(Effort effort);
 238   /** propagate */
 239   bool propagate(TNode literal);
 240   /** explain */
 241   void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
 242   void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
 243   void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
 244   void explain( TNode literal, std::vector<TNode>& assumptions );
 245   Node explain( TNode literal );
 246   Node explain( std::vector< Node >& lits );
 247   /** Conflict when merging two constants */
 248   void conflict(TNode a, TNode b);
 249   /** called when a new equivalance class is created */
 250   void eqNotifyNewClass(TNode t);
 251   /** called when two equivalance classes will merge */
 252   void eqNotifyPreMerge(TNode t1, TNode t2);
 253   /** called when two equivalance classes have merged */
 254   void eqNotifyPostMerge(TNode t1, TNode t2);
 255   /** called when two equivalence classes are made disequal */
 256   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 257
 258   void check(Effort e);
 259   void preRegisterTerm(TNode n);
 260   void finishInit();
 261   Node expandDefinition(LogicRequest &logicRequest, Node n);
 262   Node ppRewrite(TNode n);
 263   void presolve();
 264   void addSharedTerm(TNode t);
 265   EqualityStatus getEqualityStatus(TNode a, TNode b);
 266   void collectModelInfo( TheoryModel* m, bool fullModel );
 267   void shutdown() { }
 268   std::string identify() const { return std::string("TheoryDatatypes"); }
 269   /** equality engine */
 270   eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
 271   bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
 272   /** debug print */
 273   void printModelDebug( const char* c );
 274   /** entailment check */
 275   virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
 276 private:
 277   /** add tester to equivalence class info */
 278   void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
 279   /** add selector to equivalence class info */
 280   void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true );
 281   /** add constructor */
 282   void addConstructor( Node c, EqcInfo* eqc, Node n );
 283   /** merge the equivalence class info of t1 and t2 */
 284   void merge( Node t1, Node t2 );
 285   /** collapse selector, s is of the form sel( n ) where n = c */
 286   void collapseSelector( Node s, Node c );
 287   /** for checking if cycles exist */
 288   void checkCycles();
 289   Node searchForCycle( TNode n, TNode on,
 290                        std::map< TNode, bool >& visited,
 291                        std::vector< TNode >& explanation, bool firstTime = true );
 292   /** for checking whether two codatatype terms must be equal */
 293   void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
 294                           std::vector< TNode >& exp,
 295                           std::map< Node, Node >& cn,
 296                           std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp );
 297   /** build model */
 298   Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth );
 299   /** get singleton lemma */
 300   Node getSingletonLemma( TypeNode tn, bool pol );
 301   /** collect terms */
 302   void collectTerms( Node n );
 303   /** get instantiate cons */
 304   Node getInstantiateCons( Node n, const Datatype& dt, int index );
 305   /** process new term that was created internally */
 306   void processNewTerm( Node n );
 307   /** check instantiate */
 308   void instantiate( EqcInfo* eqc, Node n );
 309   /** must communicate fact */
 310   bool mustCommunicateFact( Node n, Node exp );
 311   /** check clash mod eq */
 312   bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
 313   /** get relevant terms */
 314   void getRelevantTerms( std::set<Node>& termSet );
 315 private:
 316   //equality queries
 317   bool hasTerm( TNode a );
 318   bool areEqual( TNode a, TNode b );
 319   bool areDisequal( TNode a, TNode b );
 320   bool areCareDisequal( TNode x, TNode y );
 321   TNode getRepresentative( TNode a );
 322 };/* class TheoryDatatypes */
 323
 324 }/* CVC4::theory::datatypes namespace */
 325 }/* CVC4::theory namespace */
 326 }/* CVC4 namespace */
 327
 328 #endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */