src/theory/quantifiers/first_order_model.h

   1 /*********************                                                        */
   2 /*! \file first_order_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 Model extended classes
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__FIRST_ORDER_MODEL_H
  18 #define __CVC4__FIRST_ORDER_MODEL_H
  19
  20 #include "theory/theory_model.h"
  21 #include "theory/uf/theory_uf_model.h"
  22 #include "expr/attribute.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 class QuantifiersEngine;
  28
  29 namespace quantifiers {
  30
  31 class TermDb;
  32
  33 class FirstOrderModelIG;
  34
  35 namespace fmcheck {
  36   class FirstOrderModelFmc;
  37 }/* CVC4::theory::quantifiers::fmcheck namespace */
  38
  39 class FirstOrderModelQInt;
  40 class FirstOrderModelAbs;
  41
  42 struct IsStarAttributeId {};
  43 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
  44
  45 class FirstOrderModel : public TheoryModel
  46 {
  47 protected:
  48   /** quant engine */
  49   QuantifiersEngine * d_qe;
  50   /** list of quantifiers asserted in the current context */
  51   context::CDList<Node> d_forall_asserts;
  52   /** quantified formulas marked as relevant */
  53   unsigned d_rlv_count;
  54   std::map< Node, unsigned > d_forall_rlv;
  55   std::vector< Node > d_forall_rlv_vec;
  56   Node d_last_forall_rlv;
  57   std::vector< Node > d_forall_rlv_assert;
  58   /** get variable id */
  59   std::map< Node, std::map< Node, int > > d_quant_var_id;
  60   /** get current model value (deprecated) */
  61   //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
  62 public: //for Theory Quantifiers:
  63   /** assert quantifier */
  64   void assertQuantifier( Node n );
  65   /** get number of asserted quantifiers */
  66   unsigned getNumAssertedQuantifiers();
  67   /** get asserted quantifier */
  68   Node getAssertedQuantifier( unsigned i, bool ordered = false );
  69   /** initialize model for term */
  70   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
  71   virtual void processInitializeModelForTerm( Node n ) = 0;
  72   virtual void processInitializeQuantifier( Node q ) {}
  73 public:
  74   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
  75   virtual ~FirstOrderModel() throw() {}
  76   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
  77   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
  78   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
  79   virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
  80   // initialize the model
  81   void initialize();
  82   virtual void processInitialize( bool ispre ) = 0;
  83   /** get variable id */
  84   int getVariableId(TNode q, TNode n) {
  85     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
  86   }
  87   /** get some domain element */
  88   Node getSomeDomainElement(TypeNode tn);
  89   /** do we need to do any work? */
  90   bool checkNeeded();
  91 private:
  92   //list of inactive quantified formulas
  93   std::map< TNode, bool > d_quant_active;
  94 public:
  95   /** reset round */
  96   void reset_round();
  97   /** mark quantified formula relevant */
  98   void markRelevant( Node q );
  99   /** get relevance value */
 100   int getRelevanceValue( Node q );
 101   /** set quantified formula active/inactive
 102    * a quantified formula may be set inactive if for instance:
 103    *   - it is entailed by other quantified formulas
 104    */
 105   void setQuantifierActive( TNode q, bool active );
 106   /** is quantified formula active */
 107   bool isQuantifierActive( TNode q );
 108   /** is quantified formula asserted */
 109   bool isQuantifierAsserted( TNode q );
 110 };/* class FirstOrderModel */
 111
 112
 113 class FirstOrderModelIG : public FirstOrderModel
 114 {
 115 public: //for Theory UF:
 116   //models for each UF operator
 117   std::map< Node, uf::UfModelTree > d_uf_model_tree;
 118   //model generators
 119   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
 120 private:
 121   //map from terms to the models used to calculate their value
 122   std::map< Node, bool > d_eval_uf_use_default;
 123   std::map< Node, uf::UfModelTree > d_eval_uf_model;
 124   void makeEvalUfModel( Node n );
 125   //index ordering to use for each term
 126   std::map< Node, std::vector< int > > d_eval_term_index_order;
 127   void makeEvalUfIndexOrder( Node n );
 128 //the following functions are for evaluating quantifier bodies
 129 public:
 130   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 131   ~FirstOrderModelIG() throw() {}
 132   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
 133   // initialize the model
 134   void processInitialize( bool ispre );
 135   //for initialize model
 136   void processInitializeModelForTerm( Node n );
 137   /** reset evaluation */
 138   void resetEvaluate();
 139   /** evaluate functions */
 140   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 141   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 142 public:
 143   //statistics
 144   int d_eval_formulas;
 145   int d_eval_uf_terms;
 146   int d_eval_lits;
 147   int d_eval_lits_unknown;
 148 private:
 149   //default evaluate term function
 150   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 151   //temporary storing which literals have failed
 152   void clearEvalFailed( int index );
 153   std::map< Node, bool > d_eval_failed;
 154   std::map< int, std::vector< Node > > d_eval_failed_lits;
 155 };/* class FirstOrderModelIG */
 156
 157
 158 namespace fmcheck {
 159
 160 class Def;
 161
 162 class FirstOrderModelFmc : public FirstOrderModel
 163 {
 164   friend class FullModelChecker;
 165 private:
 166   /** models for UF */
 167   std::map<Node, Def * > d_models;
 168   std::map<TypeNode, Node > d_type_star;
 169   Node intervalOp;
 170   /** get current model value */
 171   void processInitializeModelForTerm(Node n);
 172 public:
 173   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 174   virtual ~FirstOrderModelFmc() throw();
 175   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
 176   // initialize the model
 177   void processInitialize( bool ispre );
 178   Node getFunctionValue(Node op, const char* argPrefix );
 179
 180   bool isStar(Node n);
 181   Node getStar(TypeNode tn);
 182   Node getStarElement(TypeNode tn);
 183   bool isModelBasisTerm(Node n);
 184   Node getModelBasisTerm(TypeNode tn);
 185   bool isInterval(Node n);
 186   Node getInterval( Node lb, Node ub );
 187   bool isInRange( Node v, Node i );
 188 };/* class FirstOrderModelFmc */
 189
 190 }/* CVC4::theory::quantifiers::fmcheck namespace */
 191
 192 class AbsDef;
 193
 194 class FirstOrderModelAbs : public FirstOrderModel
 195 {
 196 public:
 197   std::map< Node, AbsDef * > d_models;
 198   std::map< Node, bool > d_models_valid;
 199   std::map< TNode, unsigned > d_rep_id;
 200   std::map< TypeNode, unsigned > d_domain;
 201   std::map< Node, std::vector< int > > d_var_order;
 202   std::map< Node, std::map< int, int > > d_var_index;
 203 private:
 204   /** get current model value */
 205   void processInitializeModelForTerm(Node n);
 206   void processInitializeQuantifier( Node q );
 207   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
 208   TNode getUsedRepresentative( TNode n );
 209 public:
 210   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
 211   ~FirstOrderModelAbs() throw();
 212   FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
 213   void processInitialize( bool ispre );
 214   unsigned getRepresentativeId( TNode n );
 215   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
 216   Node getFunctionValue(Node op, const char* argPrefix );
 217   Node getVariable( Node q, unsigned i );
 218 };
 219
 220 }/* CVC4::theory::quantifiers namespace */
 221 }/* CVC4::theory namespace */
 222 }/* CVC4 namespace */
 223
 224 #endif /* __CVC4__FIRST_ORDER_MODEL_H */