src/theory/quantifiers/ce_guided_instantiation.h

   1 /*********************                                                        */
   2 /*! \file ce_guided_instantiation.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 counterexample guided instantiation class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CE_GUIDED_INSTANTIATION_H
  18 #define CE_GUIDED_INSTANTIATION_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "context/cdchunk_list.h"
  22 #include "theory/quantifiers_engine.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28
  29
  30 class CegInstantiation : public QuantifiersModule
  31 {
  32   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  33 private:
  34   class CegConjecture {
  35   public:
  36     CegConjecture();
  37     /** quantified formula */
  38     Node d_quant;
  39     /** guard */
  40     Node d_guard;
  41     /** base instantiation */
  42     Node d_base_inst;
  43     /** guard split */
  44     Node d_guard_split;
  45     /** list of constants for quantified formula */
  46     std::vector< Node > d_candidates;
  47     /** list of variables on inner quantification */
  48     std::vector< Node > d_inner_vars;
  49     /** is assigned */
  50     bool isAssigned() { return !d_quant.isNull(); }
  51     /** assign */
  52     void assign( Node q );
  53     /** initialize guard */
  54     void initializeGuard( QuantifiersEngine * qe );
  55   };
  56   /** the quantified formula stating the synthesis conjecture */
  57   CegConjecture d_conj;
  58   /** is conjecture active */
  59   context::CDO< bool > d_conj_active;
  60   /** is conjecture infeasible */
  61   context::CDO< bool > d_conj_infeasible;
  62   /** assertions for guards */
  63   NodeBoolMap d_guard_assertions;
  64 private:
  65   /** check conjecture */
  66   void checkCegConjecture( CegConjecture * conj );
  67   /** get model value */
  68   Node getModelValue( Node n );
  69   /** get model term */
  70   Node getModelTerm( Node n );
  71 public:
  72   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
  73 public:
  74   bool needsCheck( Theory::Effort e );
  75   /* Call during quantifier engine's check */
  76   void check( Theory::Effort e, unsigned quant_e );
  77   /* Called for new quantifiers */
  78   void registerQuantifier( Node q );
  79   void assertNode( Node n );
  80   Node getNextDecisionRequest();
  81   /** Identify this module (for debugging, dynamic configuration, etc..) */
  82   std::string identify() const { return "CegInstantiation"; }
  83 };
  84
  85 }
  86 }
  87 }
  88
  89 #endif