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, 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 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   /** is model set */
  59   context::CDO< bool > d_isModelSet;
  60   /** get variable id */
  61   std::map< Node, std::map< Node, int > > d_quant_var_id;
  62   /** get current model value */
  63   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
  64 public: //for Theory Quantifiers:
  65   /** assert quantifier */
  66   void assertQuantifier( Node n );
  67   /** get number of asserted quantifiers */
  68   unsigned getNumAssertedQuantifiers();
  69   /** get asserted quantifier */
  70   Node getAssertedQuantifier( unsigned i, bool ordered = false );
  71   /** initialize model for term */
  72   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
  73   virtual void processInitializeModelForTerm( Node n ) = 0;
  74   virtual void processInitializeQuantifier( Node q ) {}
  75 public:
  76   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
  77   virtual ~FirstOrderModel() throw() {}
  78   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
  79   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
  80   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
  81   virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
  82   // initialize the model
  83   void initialize();
  84   virtual void processInitialize( bool ispre ) = 0;
  85   /** mark model set */
  86   void markModelSet() { d_isModelSet = true; }
  87   /** is model set */
  88   bool isModelSet() { return d_isModelSet; }
  89   /** get current model value */
  90   Node getCurrentModelValue( Node n, bool partial = false );
  91   /** get variable id */
  92   int getVariableId(TNode q, TNode n) {
  93     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
  94   }
  95   /** get some domain element */
  96   Node getSomeDomainElement(TypeNode tn);
  97   /** do we need to do any work? */
  98   bool checkNeeded();
  99 private:
 100   //list of inactive quantified formulas
 101   std::map< TNode, bool > d_quant_active;
 102 public:
 103   /** reset round */
 104   void reset_round();
 105   /** mark quantified formula relevant */
 106   void markRelevant( Node q );
 107   /** get relevance value */
 108   int getRelevanceValue( Node q );
 109   /** set quantified formula active/inactive
 110    * a quantified formula may be set inactive if for instance:
 111    *   - it is entailed by other quantified formulas
 112    */
 113   void setQuantifierActive( TNode q, bool active );
 114   /** is quantified formula active */
 115   bool isQuantifierActive( TNode q );
 116 };/* class FirstOrderModel */
 117
 118
 119 class FirstOrderModelIG : public FirstOrderModel
 120 {
 121 public: //for Theory UF:
 122   //models for each UF operator
 123   std::map< Node, uf::UfModelTree > d_uf_model_tree;
 124   //model generators
 125   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
 126 private:
 127   //map from terms to the models used to calculate their value
 128   std::map< Node, bool > d_eval_uf_use_default;
 129   std::map< Node, uf::UfModelTree > d_eval_uf_model;
 130   void makeEvalUfModel( Node n );
 131   //index ordering to use for each term
 132   std::map< Node, std::vector< int > > d_eval_term_index_order;
 133   void makeEvalUfIndexOrder( Node n );
 134   /** get current model value */
 135   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 136 //the following functions are for evaluating quantifier bodies
 137 public:
 138   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 139   ~FirstOrderModelIG() throw() {}
 140   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
 141   // initialize the model
 142   void processInitialize( bool ispre );
 143   //for initialize model
 144   void processInitializeModelForTerm( Node n );
 145   /** reset evaluation */
 146   void resetEvaluate();
 147   /** evaluate functions */
 148   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 149   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 150 public:
 151   //statistics
 152   int d_eval_formulas;
 153   int d_eval_uf_terms;
 154   int d_eval_lits;
 155   int d_eval_lits_unknown;
 156 private:
 157   //default evaluate term function
 158   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 159   //temporary storing which literals have failed
 160   void clearEvalFailed( int index );
 161   std::map< Node, bool > d_eval_failed;
 162   std::map< int, std::vector< Node > > d_eval_failed_lits;
 163 };/* class FirstOrderModelIG */
 164
 165
 166 namespace fmcheck {
 167
 168 class Def;
 169
 170 class FirstOrderModelFmc : public FirstOrderModel
 171 {
 172   friend class FullModelChecker;
 173 private:
 174   /** models for UF */
 175   std::map<Node, Def * > d_models;
 176   std::map<TypeNode, Node > d_type_star;
 177   Node intervalOp;
 178   Node getUsedRepresentative(Node n, bool strict = false);
 179   /** get current model value */
 180   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 181   void processInitializeModelForTerm(Node n);
 182 public:
 183   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 184   virtual ~FirstOrderModelFmc() throw();
 185   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
 186   // initialize the model
 187   void processInitialize( bool ispre );
 188   Node getFunctionValue(Node op, const char* argPrefix );
 189
 190   bool isStar(Node n);
 191   Node getStar(TypeNode tn);
 192   Node getStarElement(TypeNode tn);
 193   bool isModelBasisTerm(Node n);
 194   Node getModelBasisTerm(TypeNode tn);
 195   bool isInterval(Node n);
 196   Node getInterval( Node lb, Node ub );
 197   bool isInRange( Node v, Node i );
 198 };/* class FirstOrderModelFmc */
 199
 200 }/* CVC4::theory::quantifiers::fmcheck namespace */
 201
 202 class AbsDef;
 203
 204 class FirstOrderModelAbs : public FirstOrderModel
 205 {
 206 public:
 207   std::map< Node, AbsDef * > d_models;
 208   std::map< Node, bool > d_models_valid;
 209   std::map< TNode, unsigned > d_rep_id;
 210   std::map< TypeNode, unsigned > d_domain;
 211   std::map< Node, std::vector< int > > d_var_order;
 212   std::map< Node, std::map< int, int > > d_var_index;
 213 private:
 214   /** get current model value */
 215   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 216   void processInitializeModelForTerm(Node n);
 217   void processInitializeQuantifier( Node q );
 218   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
 219 public:
 220   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
 221   ~FirstOrderModelAbs() throw();
 222   FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
 223   void processInitialize( bool ispre );
 224   unsigned getRepresentativeId( TNode n );
 225   TNode getUsedRepresentative( TNode n );
 226   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
 227   Node getFunctionValue(Node op, const char* argPrefix );
 228   Node getVariable( Node q, unsigned i );
 229 };
 230
 231 }/* CVC4::theory::quantifiers namespace */
 232 }/* CVC4::theory namespace */
 233 }/* CVC4 namespace */
 234
 235 #endif /* __CVC4__FIRST_ORDER_MODEL_H */