src/theory/quantifiers/first_order_model.h

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