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   //add term function
  46   void addTerm( Node n );
  47   //for initialize model
  48   void initializeModelForTerm( Node n );
  49   /** whether an axiom is asserted */
  50   context::CDO< bool > d_axiom_asserted;
  51   /** list of quantifiers asserted in the current context */
  52   context::CDList<Node> d_forall_asserts;
  53 public: //for Theory UF:
  54   //models for each UF operator
  55   std::map< Node, uf::UfModelTree > d_uf_model_tree;
  56   //model generators
  57   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
  58 private:
  59   //map from terms to the models used to calculate their value
  60   std::map< Node, bool > d_eval_uf_use_default;
  61   std::map< Node, uf::UfModelTree > d_eval_uf_model;
  62   void makeEvalUfModel( Node n );
  63   //index ordering to use for each term
  64   std::map< Node, std::vector< int > > d_eval_term_index_order;
  65   void makeEvalUfIndexOrder( Node n );
  66 public: //for Theory Arrays:
  67   //default value for each non-store array
  68   std::map< Node, arrays::ArrayModel > d_array_model;
  69 public: //for Theory Quantifiers:
  70   /** assert quantifier */
  71   void assertQuantifier( Node n );
  72   /** get number of asserted quantifiers */
  73   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
  74   /** get asserted quantifier */
  75   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
  76   /** bool axiom asserted */
  77   bool isAxiomAsserted() { return d_axiom_asserted; }
  78 public:
  79   FirstOrderModel( context::Context* c, std::string name );
  80   virtual ~FirstOrderModel(){}
  81   // reset the model
  82   void reset();
  83   /** get interpreted value */
  84   Node getInterpretedValue( TNode n );
  85 public:
  86   // initialize the model
  87   void initialize( bool considerAxioms = true );
  88   /** to stream function */
  89   void toStream( std::ostream& out );
  90 //the following functions are for evaluating quantifier bodies
  91 public:
  92   /** reset evaluation */
  93   void resetEvaluate();
  94   /** evaluate functions */
  95   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
  96   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
  97 public:
  98   //statistics
  99   int d_eval_formulas;
 100   int d_eval_uf_terms;
 101   int d_eval_lits;
 102   int d_eval_lits_unknown;
 103 private:
 104   //default evaluate term function
 105   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 106   //temporary storing which literals have failed
 107   void clearEvalFailed( int index );
 108   std::map< Node, bool > d_eval_failed;
 109   std::map< int, std::vector< Node > > d_eval_failed_lits;
 110 };/* class FirstOrderModel */
 111
 112 }/* CVC4::theory::quantifiers namespace */
 113 }/* CVC4::theory namespace */
 114 }/* CVC4 namespace */
 115
 116 #endif /* __CVC4__FIRST_ORDER_MODEL_H */