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