src/theory/quantifiers/theory_quantifiers.h

   1 /*********************                                                        */
   2 /*! \file theory_quantifiers.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Francois Bobot, Dejan Jovanovic, Andrew Reynolds
   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 Theory of quantifiers.
  13  **
  14  ** Theory of quantifiers.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
  20 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
  21
  22 #include "context/cdhashmap.h"
  23 #include "theory/theory.h"
  24 #include "util/hash.h"
  25 #include "util/statistics_registry.h"
  26
  27 #include <ext/hash_set>
  28 #include <iostream>
  29 #include <map>
  30
  31 namespace CVC4 {
  32 class TheoryEngine;
  33
  34 namespace theory {
  35
  36 namespace quantifiers {
  37
  38 class ModelEngine;
  39 class InstantiationEngine;
  40
  41 class TheoryQuantifiers : public Theory {
  42 private:
  43   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
  44   /** number of instantiations */
  45   int d_numInstantiations;
  46   int d_baseDecLevel;
  47   /** number of restarts */
  48   int d_numRestarts;
  49
  50   KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
  51
  52   eq::EqualityEngine* d_masterEqualityEngine;
  53
  54 public:
  55   TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  56   ~TheoryQuantifiers();
  57
  58   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  59
  60   void addSharedTerm(TNode t);
  61   void notifyEq(TNode lhs, TNode rhs);
  62   void preRegisterTerm(TNode n);
  63   void presolve();
  64   void check(Effort e);
  65   void propagate(Effort level);
  66   Node getNextDecisionRequest();
  67   Node getValue(TNode n);
  68   void collectModelInfo( TheoryModel* m, bool fullModel );
  69   void shutdown() { }
  70   std::string identify() const { return std::string("TheoryQuantifiers"); }
  71   bool flipDecision();
  72   void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
  73   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
  74   bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
  75 private:
  76   void assertUniversal( Node n );
  77   void assertExistential( Node n );
  78   bool restart();
  79 };/* class TheoryQuantifiers */
  80
  81 }/* CVC4::theory::quantifiers namespace */
  82 }/* CVC4::theory namespace */
  83 }/* CVC4 namespace */
  84
  85 #endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */