src/theory/quantifiers/cegqi/inst_strategy_cbqi.h

   1 /*********************                                                        */
   2 /*! \file inst_strategy_cbqi.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief counterexample-guided quantifier instantiation
  13  **/
  14
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef __CVC4__INST_STRATEGY_CBQI_H
  19 #define __CVC4__INST_STRATEGY_CBQI_H
  20
  21 #include "theory/arith/arithvar.h"
  22 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
  23 #include "theory/quantifiers/ematching/instantiation_engine.h"
  24 #include "util/statistics_registry.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 namespace arith {
  30   class TheoryArith;
  31 }
  32
  33 namespace quantifiers {
  34
  35 class InstStrategyCbqi : public QuantifiersModule {
  36   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  37   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
  38
  39  protected:
  40   bool d_cbqi_set_quant_inactive;
  41   bool d_incomplete_check;
  42   /** whether we have added cbqi lemma */
  43   NodeSet d_added_cbqi_lemma;
  44   /** whether we have added cbqi lemma */
  45   NodeSet d_elim_quants;
  46   /** parent guards */
  47   std::map< Node, std::vector< Node > > d_parent_quant;
  48   std::map< Node, std::vector< Node > > d_children_quant;
  49   std::map< Node, bool > d_active_quant;
  50   /** Whether cegqi handles each quantified formula. */
  51   std::map<Node, CegHandledStatus> d_do_cbqi;
  52   /** register ce lemma */
  53   bool registerCbqiLemma( Node q );
  54   virtual void registerCounterexampleLemma( Node q, Node lem );
  55   /** has added cbqi lemma */
  56   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
  57   /** get next decision request with dependency checking */
  58   Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );
  59   /** process functions */
  60   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
  61   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
  62
  63  protected:
  64   //for identification
  65   uint64_t d_qid_count;
  66   //nested qe map
  67   std::map< Node, Node > d_nested_qe;
  68   //mark ids on quantifiers
  69   Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
  70   // id to ce quant
  71   std::map< Node, Node > d_id_to_ce_quant;
  72   std::map< Node, Node > d_ce_quant_to_id;
  73   //do nested quantifier elimination recursive
  74   Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
  75   Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
  76   //elimination information (for delayed elimination)
  77   class NestedQEInfo {
  78   public:
  79     NestedQEInfo() : d_doVts(false){}
  80     ~NestedQEInfo(){}
  81     Node d_q;
  82     std::vector< Node > d_inst_terms;
  83     bool d_doVts;
  84   };
  85   std::map< Node, NestedQEInfo > d_nested_qe_info;
  86   NodeIntMap d_nested_qe_waitlist_size;
  87   NodeIntMap d_nested_qe_waitlist_proc;
  88   std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
  89
  90  public:
  91   //do nested quantifier elimination
  92   Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
  93
  94  public:
  95   InstStrategyCbqi( QuantifiersEngine * qe );
  96
  97   /** whether to do CBQI for quantifier q */
  98   bool doCbqi( Node q );
  99   /** process functions */
 100   bool needsCheck(Theory::Effort e) override;
 101   QEffort needsModel(Theory::Effort e) override;
 102   void reset_round(Theory::Effort e) override;
 103   void check(Theory::Effort e, QEffort quant_e) override;
 104   bool checkComplete() override;
 105   bool checkCompleteFor(Node q) override;
 106   void preRegisterQuantifier(Node q) override;
 107   void registerQuantifier(Node q) override;
 108   /** get next decision request */
 109   Node getNextDecisionRequest(unsigned& priority) override;
 110 };
 111
 112 //generalized counterexample guided quantifier instantiation
 113
 114 class InstStrategyCegqi;
 115
 116 class CegqiOutputInstStrategy : public CegqiOutput {
 117 public:
 118   CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
 119   InstStrategyCegqi * d_out;
 120   bool doAddInstantiation(std::vector<Node>& subs) override;
 121   bool isEligibleForInstantiation(Node n) override;
 122   bool addLemma(Node lem) override;
 123 };
 124
 125 class InstStrategyCegqi : public InstStrategyCbqi {
 126  protected:
 127   CegqiOutputInstStrategy * d_out;
 128   std::map< Node, CegInstantiator * > d_cinst;
 129   Node d_small_const;
 130   Node d_curr_quant;
 131   bool d_check_vts_lemma_lc;
 132   /** process functions */
 133   void processResetInstantiationRound(Theory::Effort effort) override;
 134   void process(Node f, Theory::Effort effort, int e) override;
 135   /** register ce lemma */
 136   void registerCounterexampleLemma(Node q, Node lem) override;
 137
 138  public:
 139   InstStrategyCegqi( QuantifiersEngine * qe );
 140   ~InstStrategyCegqi() override;
 141
 142   bool doAddInstantiation( std::vector< Node >& subs );
 143   bool isEligibleForInstantiation( Node n );
 144   bool addLemma( Node lem );
 145   /** identify */
 146   std::string identify() const override { return std::string("Cegqi"); }
 147
 148   //get instantiator for quantifier
 149   CegInstantiator * getInstantiator( Node q );
 150   //register quantifier
 151   void registerQuantifier(Node q) override;
 152   //presolve
 153   void presolve() override;
 154 };
 155
 156 }
 157 }
 158 }
 159
 160 #endif