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
  37 class FirstOrderModel : public TheoryModel
  38 {
  39 private:
  40   /** whether an axiom is asserted */
  41   context::CDO< bool > d_axiom_asserted;
  42   /** list of quantifiers asserted in the current context */
  43   context::CDList<Node> d_forall_asserts;
  44   /** is model set */
  45   context::CDO< bool > d_isModelSet;
  46   /** get current model value */
  47   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
  48 public: //for Theory Quantifiers:
  49   /** assert quantifier */
  50   void assertQuantifier( Node n );
  51   /** get number of asserted quantifiers */
  52   int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
  53   /** get asserted quantifier */
  54   Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
  55   /** bool axiom asserted */
  56   bool isAxiomAsserted() { return d_axiom_asserted; }
  57   /** initialize model for term */
  58   void initializeModelForTerm( Node n );
  59   virtual void processInitializeModelForTerm( Node n ) = 0;
  60 public:
  61   FirstOrderModel( context::Context* c, std::string name );
  62   virtual ~FirstOrderModel(){}
  63   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
  64   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
  65   // initialize the model
  66   void initialize( bool considerAxioms = true );
  67   virtual void processInitialize() = 0;
  68   /** mark model set */
  69   void markModelSet() { d_isModelSet = true; }
  70   /** is model set */
  71   bool isModelSet() { return d_isModelSet; }
  72   /** get current model value */
  73   Node getCurrentModelValue( Node n, bool partial = false );
  74 };/* class FirstOrderModel */
  75
  76
  77 class FirstOrderModelIG : public FirstOrderModel
  78 {
  79 public: //for Theory UF:
  80   //models for each UF operator
  81   std::map< Node, uf::UfModelTree > d_uf_model_tree;
  82   //model generators
  83   std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
  84 private:
  85   //map from terms to the models used to calculate their value
  86   std::map< Node, bool > d_eval_uf_use_default;
  87   std::map< Node, uf::UfModelTree > d_eval_uf_model;
  88   void makeEvalUfModel( Node n );
  89   //index ordering to use for each term
  90   std::map< Node, std::vector< int > > d_eval_term_index_order;
  91   void makeEvalUfIndexOrder( Node n );
  92   /** get current model value */
  93   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
  94 //the following functions are for evaluating quantifier bodies
  95 public:
  96   FirstOrderModelIG(context::Context* c, std::string name);
  97   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
  98   // initialize the model
  99   void processInitialize();
 100   //for initialize model
 101   void processInitializeModelForTerm( Node n );
 102   /** reset evaluation */
 103   void resetEvaluate();
 104   /** evaluate functions */
 105   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
 106   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
 107 public:
 108   //statistics
 109   int d_eval_formulas;
 110   int d_eval_uf_terms;
 111   int d_eval_lits;
 112   int d_eval_lits_unknown;
 113 private:
 114   //default evaluate term function
 115   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
 116   //temporary storing which literals have failed
 117   void clearEvalFailed( int index );
 118   std::map< Node, bool > d_eval_failed;
 119   std::map< int, std::vector< Node > > d_eval_failed_lits;
 120 };
 121
 122
 123 namespace fmcheck {
 124
 125 class Def;
 126
 127 class FirstOrderModelFmc : public FirstOrderModel
 128 {
 129   friend class FullModelChecker;
 130 private:
 131   /** quant engine */
 132   QuantifiersEngine * d_qe;
 133   /** models for UF */
 134   std::map<Node, Def * > d_models;
 135   std::map<TypeNode, Node > d_model_basis_rep;
 136   std::map<TypeNode, Node > d_type_star;
 137   Node intervalOp;
 138   Node getUsedRepresentative(Node n, bool strict = false);
 139   /** get current model value */
 140   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 141   void processInitializeModelForTerm(Node n);
 142 public:
 143   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
 144   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
 145   // initialize the model
 146   void processInitialize();
 147
 148   Node getFunctionValue(Node op, const char* argPrefix );
 149
 150   bool isStar(Node n);
 151   Node getStar(TypeNode tn);
 152   Node getStarElement(TypeNode tn);
 153   bool isModelBasisTerm(Node n);
 154   Node getModelBasisTerm(TypeNode tn);
 155   Node getSomeDomainElement(TypeNode tn);
 156   bool isInterval(Node n);
 157   Node getInterval( Node lb, Node ub );
 158   bool isInRange( Node v, Node i );
 159 };
 160
 161 }
 162
 163
 164 }/* CVC4::theory::quantifiers namespace */
 165 }/* CVC4::theory namespace */
 166 }/* CVC4 namespace */
 167
 168 #endif /* __CVC4__FIRST_ORDER_MODEL_H */