src/theory/quantifiers/first_order_model.h

   1 /*********************                                                        */
   2 /*! \file first_order_model.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Model extended classes
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__FIRST_ORDER_MODEL_H
  20 #define __CVC4__FIRST_ORDER_MODEL_H
  21
  22 #include "theory/model.h"
  23 #include "theory/uf/theory_uf_model.h"
  24 #include "theory/arrays/theory_arrays_model.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 struct ModelBasisAttributeId {};
  30 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
  31 //for APPLY_UF terms, 1 : term has direct child with model basis attribute,
  32 //                    0 : term has no direct child with model basis attribute.
  33 struct ModelBasisArgAttributeId {};
  34 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
  35
  36 class QuantifiersEngine;
  37
  38 namespace quantifiers{
  39
  40 class TermDb;
  41
  42 class FirstOrderModel : public DefaultModel
  43 {
  44 private:
  45   //pointer to term database
  46   TermDb* d_term_db;
  47   //add term function
  48   void addTerm( Node n );
  49   //for initialize model
  50   void initializeModelForTerm( Node n );
  51   /** to stream functions */
  52   void toStreamFunction( Node n, std::ostream& out );
  53   void toStreamType( TypeNode tn, std::ostream& out );
  54 public: //for Theory UF:
  55   //models for each UF operator
  56   std::map< Node, uf::UfModelTree > d_uf_model_tree;
  57   //model generators
  58   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
  59 public: //for Theory Arrays:
  60   //default value for each non-store array
  61   std::map< Node, arrays::ArrayModel > d_array_model;
  62 public: //for Theory Quantifiers:
  63   /** list of quantifiers asserted in the current context */
  64   context::CDList<Node> d_forall_asserts;
  65   /** get number of asserted quantifiers */
  66   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
  67   /** get asserted quantifier */
  68   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
  69 public:
  70   FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
  71   virtual ~FirstOrderModel(){}
  72   // reset the model
  73   void reset();
  74   /** get interpreted value */
  75   Node getInterpretedValue( TNode n );
  76 public:
  77   // initialize the model
  78   void initialize();
  79   /** get term database */
  80   TermDb* getTermDatabase();
  81   /** to stream function */
  82   void toStream( std::ostream& out );
  83 };/* class FirstOrderModel */
  84
  85 }/* CVC4::theory::quantifiers namespace */
  86 }/* CVC4::theory namespace */
  87 }/* CVC4 namespace */
  88
  89 #endif /* __CVC4__FIRST_ORDER_MODEL_H */