src/theory/quantifiers/first_order_model.h

   1 /*********************                                                        */
   2 /*! \file first_order_model.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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/model.h"
  21 #include "theory/uf/theory_uf_model.h"
  22 #include "theory/arrays/theory_arrays_model.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 class QuantifiersEngine;
  28
  29 namespace quantifiers{
  30
  31 class TermDb;
  32
  33 class FirstOrderModel : public TheoryModel
  34 {
  35 private:
  36   //for initialize model
  37   void initializeModelForTerm( Node n );
  38   /** whether an axiom is asserted */
  39   context::CDO< bool > d_axiom_asserted;
  40   /** list of quantifiers asserted in the current context */
  41   context::CDList<Node> d_forall_asserts;
  42   /** is model set */
  43   context::CDO< bool > d_isModelSet;
  44 public: //for Theory UF:
  45   //models for each UF operator
  46   std::map< Node, uf::UfModelTree > d_uf_model_tree;
  47   //model generators
  48   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
  49 private:
  50   //map from terms to the models used to calculate their value
  51   std::map< Node, bool > d_eval_uf_use_default;
  52   std::map< Node, uf::UfModelTree > d_eval_uf_model;
  53   void makeEvalUfModel( Node n );
  54   //index ordering to use for each term
  55   std::map< Node, std::vector< int > > d_eval_term_index_order;
  56   void makeEvalUfIndexOrder( Node n );
  57 public: //for Theory Arrays:
  58   //default value for each non-store array
  59   std::map< Node, arrays::ArrayModel > d_array_model;
  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 public:
  70   FirstOrderModel( context::Context* c, std::string name );
  71   virtual ~FirstOrderModel(){}
  72   // reset the model
  73   void reset();
  74   // initialize the model
  75   void initialize( bool considerAxioms = true );
  76   /** mark model set */
  77   void markModelSet() { d_isModelSet = true; }
  78   /** is model set */
  79   bool isModelSet() { return d_isModelSet; }
  80 //the following functions are for evaluating quantifier bodies
  81 public:
  82   /** reset evaluation */
  83   void resetEvaluate();
  84   /** evaluate functions */
  85   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
  86   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
  87 public:
  88   //statistics
  89   int d_eval_formulas;
  90   int d_eval_uf_terms;
  91   int d_eval_lits;
  92   int d_eval_lits_unknown;
  93 private:
  94   //default evaluate term function
  95   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
  96   //temporary storing which literals have failed
  97   void clearEvalFailed( int index );
  98   std::map< Node, bool > d_eval_failed;
  99   std::map< int, std::vector< Node > > d_eval_failed_lits;
 100 };/* class FirstOrderModel */
 101
 102 }/* CVC4::theory::quantifiers namespace */
 103 }/* CVC4::theory namespace */
 104 }/* CVC4 namespace */
 105
 106 #endif /* __CVC4__FIRST_ORDER_MODEL_H */