Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Pool-based instantiation strategy
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
      16                 :            : #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
      17                 :            : 
      18                 :            : #include "smt/env_obj.h"
      19                 :            : #include "theory/quantifiers/quant_module.h"
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : namespace theory {
      23                 :            : namespace quantifiers {
      24                 :            : 
      25                 :            : /**
      26                 :            :  * Pool-based instantiation. This implements a strategy for instantiating
      27                 :            :  * quantifiers based on user-provided pool annotations.
      28                 :            :  *
      29                 :            :  * When check is invoked, this strategy considers each
      30                 :            :  * INST_POOL annotation on quantified formulas. For each annotation, it
      31                 :            :  * instantiates the associated quantified formula with the Cartesian
      32                 :            :  * product of terms currently in the pool, using efficient techniques for
      33                 :            :  * enumerating over tuples of terms, as implemented in the term tuple
      34                 :            :  * enumerator utilities (see quantifiers/term_tuple_enumerator.h).
      35                 :            :  */
      36                 :            : class InstStrategyPool : public QuantifiersModule
      37                 :            : {
      38                 :            :  public:
      39                 :            :   InstStrategyPool(Env& env,
      40                 :            :                    QuantifiersState& qs,
      41                 :            :                    QuantifiersInferenceManager& qim,
      42                 :            :                    QuantifiersRegistry& qr,
      43                 :            :                    TermRegistry& tr);
      44                 :      86380 :   ~InstStrategyPool() {}
      45                 :            :   /** Presolve */
      46                 :            :   void presolve() override;
      47                 :            :   /** Needs check. */
      48                 :            :   bool needsCheck(Theory::Effort e) override;
      49                 :            :   /** Reset round. */
      50                 :            :   void reset_round(Theory::Effort e) override;
      51                 :            :   /** Register quantified formula q */
      52                 :            :   void registerQuantifier(Node q) override;
      53                 :            :   /** Check ownership for q */
      54                 :            :   void checkOwnership(Node q) override;
      55                 :            :   /** Check.
      56                 :            :    * Adds instantiations for all currently asserted
      57                 :            :    * quantified formulas via calls to process(...)
      58                 :            :    */
      59                 :            :   void check(Theory::Effort e, QEffort quant_e) override;
      60                 :            :   /** Identify. */
      61                 :            :   std::string identify() const override;
      62                 :            :   /**
      63                 :            :    * Has standard product semantics. A pool has product semantics for a
      64                 :            :    * quantified formula forall x : S. F if it specifies a list of sets whose
      65                 :            :    * element types are S.
      66                 :            :    */
      67                 :            :   static bool hasProductSemantics(Node q, Node p);
      68                 :            :   /**
      69                 :            :    * Has tuple semantics. A pool has tuple semantics for a quantified formula
      70                 :            :    * forall x : S. F if it specifies a set whose elements are (Tuple S).
      71                 :            :    */
      72                 :            :   static bool hasTupleSemantics(Node q, Node p);
      73                 :            : 
      74                 :            :  private:
      75                 :            :   /** Process quantified formula with user pool, return true if we are in
      76                 :            :    * conflict */
      77                 :            :   bool process(Node q, Node p, uint64_t& addedLemmas);
      78                 :            :   /** Process quantified formula with user pool with tuple semantics, return
      79                 :            :    * true if we are in conflict */
      80                 :            :   bool processTuple(Node q, Node p, uint64_t& addedLemmas);
      81                 :            :   /** Map from quantified formulas to user pools */
      82                 :            :   std::map<Node, std::vector<Node> > d_userPools;
      83                 :            : };
      84                 :            : 
      85                 :            : }  // namespace quantifiers
      86                 :            : }  // namespace theory
      87                 :            : }  // namespace cvc5::internal
      88                 :            : 
      89                 :            : #endif