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-2013  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 namespace fmcheck {
  35   class FirstOrderModelFmc;
  36 }
  37 class FirstOrderModelQInt;
  38
  39 struct IsStarAttributeId {};
  40 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
  41
  42 class FirstOrderModel : public TheoryModel
  43 {
  44 protected:
  45   /** quant engine */
  46   QuantifiersEngine * d_qe;
  47   /** whether an axiom is asserted */
  48   context::CDO< bool > d_axiom_asserted;
  49   /** list of quantifiers asserted in the current context */
  50   context::CDList<Node> d_forall_asserts;
  51   /** is model set */
  52   context::CDO< bool > d_isModelSet;
  53   /** get variable id */
  54   std::map< Node, std::map< Node, int > > d_quant_var_id;
  55   /** get current model value */
  56   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
  57 public: //for Theory Quantifiers:
  58   /** assert quantifier */
  59   void assertQuantifier( Node n );
  60   /** get number of asserted quantifiers */
  61   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
  62   /** get asserted quantifier */
  63   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
  64   /** bool axiom asserted */
  65   bool isAxiomAsserted() { return d_axiom_asserted; }
  66   /** initialize model for term */
  67   void initializeModelForTerm( Node n );
  68   virtual void processInitializeModelForTerm( Node n ) = 0;
  69   virtual void processInitializeQuantifier( Node q ) {}
  70 public:
  71   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
  72   virtual ~FirstOrderModel(){}
  73   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
  74   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
  75   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
  76   // initialize the model
  77   void initialize( bool considerAxioms = true );
  78   virtual void processInitialize( bool ispre ) = 0;
  79   /** mark model set */
  80   void markModelSet() { d_isModelSet = true; }
  81   /** is model set */
  82   bool isModelSet() { return d_isModelSet; }
  83   /** get current model value */
  84   Node getCurrentModelValue( Node n, bool partial = false );
  85   /** get variable id */
  86   int getVariableId(Node f, Node n) {
  87     return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1;
  88   }
  89   /** get some domain element */
  90   Node getSomeDomainElement(TypeNode tn);
  91 };/* class FirstOrderModel */
  92
  93
  94 class FirstOrderModelIG : public FirstOrderModel
  95 {
  96 public: //for Theory UF:
  97   //models for each UF operator
  98   std::map< Node, uf::UfModelTree > d_uf_model_tree;
  99   //model generators
 100   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
 101 private:
 102   //map from terms to the models used to calculate their value
 103   std::map< Node, bool > d_eval_uf_use_default;
 104   std::map< Node, uf::UfModelTree > d_eval_uf_model;
 105   void makeEvalUfModel( Node n );
 106   //index ordering to use for each term
 107   std::map< Node, std::vector< int > > d_eval_term_index_order;
 108   void makeEvalUfIndexOrder( Node n );
 109   /** get current model value */
 110   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 111 //the following functions are for evaluating quantifier bodies
 112 public:
 113   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 114   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
 115   // initialize the model
 116   void processInitialize( bool ispre );
 117   //for initialize model
 118   void processInitializeModelForTerm( Node n );
 119   /** reset evaluation */
 120   void resetEvaluate();
 121   /** evaluate functions */
 122   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 123   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 124 public:
 125   //statistics
 126   int d_eval_formulas;
 127   int d_eval_uf_terms;
 128   int d_eval_lits;
 129   int d_eval_lits_unknown;
 130 private:
 131   //default evaluate term function
 132   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 133   //temporary storing which literals have failed
 134   void clearEvalFailed( int index );
 135   std::map< Node, bool > d_eval_failed;
 136   std::map< int, std::vector< Node > > d_eval_failed_lits;
 137 };
 138
 139
 140 namespace fmcheck {
 141
 142 class Def;
 143
 144 class FirstOrderModelFmc : public FirstOrderModel
 145 {
 146   friend class FullModelChecker;
 147 private:
 148   /** models for UF */
 149   std::map<Node, Def * > d_models;
 150   std::map<TypeNode, Node > d_model_basis_rep;
 151   std::map<TypeNode, Node > d_type_star;
 152   Node intervalOp;
 153   Node getUsedRepresentative(Node n, bool strict = false);
 154   /** get current model value */
 155   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 156   void processInitializeModelForTerm(Node n);
 157 public:
 158   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 159   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
 160   // initialize the model
 161   void processInitialize( bool ispre );
 162   Node getFunctionValue(Node op, const char* argPrefix );
 163
 164   bool isStar(Node n);
 165   Node getStar(TypeNode tn);
 166   Node getStarElement(TypeNode tn);
 167   bool isModelBasisTerm(Node n);
 168   Node getModelBasisTerm(TypeNode tn);
 169   bool isInterval(Node n);
 170   Node getInterval( Node lb, Node ub );
 171   bool isInRange( Node v, Node i );
 172 };
 173
 174 }
 175
 176
 177 class QIntDef;
 178 class QuantVarOrder;
 179 class FirstOrderModelQInt : public FirstOrderModel
 180 {
 181   friend class QIntervalBuilder;
 182 private:
 183   /** uf op to some representation */
 184   std::map<Node, QIntDef * > d_models;
 185   /** representatives to ids */
 186   std::map< Node, int > d_rep_id;
 187   std::map< TypeNode, Node > d_min;
 188   std::map< TypeNode, Node > d_max;
 189   /** quantifiers to information regarding variable ordering */
 190   std::map<Node, QuantVarOrder * > d_var_order;
 191   /** get current model value */
 192   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 193   void processInitializeModelForTerm(Node n);
 194 public:
 195   FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
 196   FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
 197   void processInitialize( bool ispre );
 198   Node getFunctionValue(Node op, const char* argPrefix );
 199
 200   Node getUsedRepresentative( Node n );
 201   int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
 202   bool isLessThan( Node v1, Node v2 );
 203   Node getMin( Node v1, Node v2 );
 204   Node getMax( Node v1, Node v2 );
 205   Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
 206   Node getMaximum( TypeNode tn );
 207   bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
 208   bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
 209   Node getNext( TypeNode tn, Node v );
 210   Node getPrev( TypeNode tn, Node v );
 211   bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
 212   QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
 213
 214   void processInitializeQuantifier( Node q ) ;
 215   unsigned getOrderedNumVars( Node q );
 216   TypeNode getOrderedVarType( Node q, int i );
 217   int getOrderedVarNumToVarNum( Node q, int i );
 218 };
 219
 220
 221 }/* CVC4::theory::quantifiers namespace */
 222 }/* CVC4::theory namespace */
 223 }/* CVC4 namespace */
 224
 225 #endif /* __CVC4__FIRST_ORDER_MODEL_H */