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   /** whether an axiom is asserted */
  51   context::CDO< bool > d_axiom_asserted;
  52   /** list of quantifiers asserted in the current context */
  53   context::CDList<Node> d_forall_asserts;
  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 );
  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   /** bool axiom asserted */
  68   bool isAxiomAsserted() { return d_axiom_asserted; }
  69   /** initialize model for term */
  70   void initializeModelForTerm( Node n );
  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() {}
  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( bool considerAxioms = true );
  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 private:
  96   //list of inactive quantified formulas
  97   std::map< TNode, bool > d_quant_active;
  98 public:
  99   /** reset round */
 100   void reset_round();
 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 };/* class FirstOrderModel */
 109
 110
 111 class FirstOrderModelIG : public FirstOrderModel
 112 {
 113 public: //for Theory UF:
 114   //models for each UF operator
 115   std::map< Node, uf::UfModelTree > d_uf_model_tree;
 116   //model generators
 117   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
 118 private:
 119   //map from terms to the models used to calculate their value
 120   std::map< Node, bool > d_eval_uf_use_default;
 121   std::map< Node, uf::UfModelTree > d_eval_uf_model;
 122   void makeEvalUfModel( Node n );
 123   //index ordering to use for each term
 124   std::map< Node, std::vector< int > > d_eval_term_index_order;
 125   void makeEvalUfIndexOrder( Node n );
 126   /** get current model value */
 127   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 128 //the following functions are for evaluating quantifier bodies
 129 public:
 130   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 131   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
 132   // initialize the model
 133   void processInitialize( bool ispre );
 134   //for initialize model
 135   void processInitializeModelForTerm( Node n );
 136   /** reset evaluation */
 137   void resetEvaluate();
 138   /** evaluate functions */
 139   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 140   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 141 public:
 142   //statistics
 143   int d_eval_formulas;
 144   int d_eval_uf_terms;
 145   int d_eval_lits;
 146   int d_eval_lits_unknown;
 147 private:
 148   //default evaluate term function
 149   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 150   //temporary storing which literals have failed
 151   void clearEvalFailed( int index );
 152   std::map< Node, bool > d_eval_failed;
 153   std::map< int, std::vector< Node > > d_eval_failed_lits;
 154 };/* class FirstOrderModelIG */
 155
 156
 157 namespace fmcheck {
 158
 159 class Def;
 160
 161 class FirstOrderModelFmc : public FirstOrderModel
 162 {
 163   friend class FullModelChecker;
 164 private:
 165   /** models for UF */
 166   std::map<Node, Def * > d_models;
 167   std::map<TypeNode, Node > d_model_basis_rep;
 168   std::map<TypeNode, Node > d_type_star;
 169   Node intervalOp;
 170   Node getUsedRepresentative(Node n, bool strict = false);
 171   /** get current model value */
 172   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 173   void processInitializeModelForTerm(Node n);
 174 public:
 175   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 176   virtual ~FirstOrderModelFmc();
 177   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
 178   // initialize the model
 179   void processInitialize( bool ispre );
 180   Node getFunctionValue(Node op, const char* argPrefix );
 181
 182   bool isStar(Node n);
 183   Node getStar(TypeNode tn);
 184   Node getStarElement(TypeNode tn);
 185   bool isModelBasisTerm(Node n);
 186   Node getModelBasisTerm(TypeNode tn);
 187   bool isInterval(Node n);
 188   Node getInterval( Node lb, Node ub );
 189   bool isInRange( Node v, Node i );
 190 };/* class FirstOrderModelFmc */
 191
 192 }/* CVC4::theory::quantifiers::fmcheck namespace */
 193
 194
 195 class QIntDef;
 196 class QuantVarOrder;
 197 class FirstOrderModelQInt : public FirstOrderModel
 198 {
 199   friend class QIntervalBuilder;
 200 private:
 201   /** uf op to some representation */
 202   std::map<Node, QIntDef * > d_models;
 203   /** representatives to ids */
 204   std::map< Node, int > d_rep_id;
 205   std::map< TypeNode, Node > d_min;
 206   std::map< TypeNode, Node > d_max;
 207   /** quantifiers to information regarding variable ordering */
 208   std::map<Node, QuantVarOrder * > d_var_order;
 209   /** get current model value */
 210   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 211   void processInitializeModelForTerm(Node n);
 212 public:
 213   FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
 214   FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
 215   void processInitialize( bool ispre );
 216   Node getFunctionValue(Node op, const char* argPrefix );
 217
 218   Node getUsedRepresentative( Node n );
 219   int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
 220   bool isLessThan( Node v1, Node v2 );
 221   Node getMin( Node v1, Node v2 );
 222   Node getMax( Node v1, Node v2 );
 223   Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
 224   Node getMaximum( TypeNode tn );
 225   bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
 226   bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
 227   Node getNext( TypeNode tn, Node v );
 228   Node getPrev( TypeNode tn, Node v );
 229   bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
 230   QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
 231
 232   void processInitializeQuantifier( Node q ) ;
 233   unsigned getOrderedNumVars( Node q );
 234   TypeNode getOrderedVarType( Node q, int i );
 235   int getOrderedVarNumToVarNum( Node q, int i );
 236 };/* class FirstOrderModelQInt */
 237
 238 class AbsDef;
 239
 240 class FirstOrderModelAbs : public FirstOrderModel
 241 {
 242 public:
 243   std::map< Node, AbsDef * > d_models;
 244   std::map< Node, bool > d_models_valid;
 245   std::map< TNode, unsigned > d_rep_id;
 246   std::map< TypeNode, unsigned > d_domain;
 247   std::map< Node, std::vector< int > > d_var_order;
 248   std::map< Node, std::map< int, int > > d_var_index;
 249 private:
 250   /** get current model value */
 251   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 252   void processInitializeModelForTerm(Node n);
 253   void processInitializeQuantifier( Node q );
 254   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
 255 public:
 256   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
 257   FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
 258   void processInitialize( bool ispre );
 259   unsigned getRepresentativeId( TNode n );
 260   TNode getUsedRepresentative( TNode n );
 261   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
 262   Node getFunctionValue(Node op, const char* argPrefix );
 263   Node getVariable( Node q, unsigned i );
 264 };
 265
 266 }/* CVC4::theory::quantifiers namespace */
 267 }/* CVC4::theory namespace */
 268 }/* CVC4 namespace */
 269
 270 #endif /* __CVC4__FIRST_ORDER_MODEL_H */