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