Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Model-based quantifier instantiation
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H
      20                 :            : 
      21                 :            : #include <map>
      22                 :            : #include <unordered_map>
      23                 :            : #include <unordered_set>
      24                 :            : 
      25                 :            : #include "context/cdhashset.h"
      26                 :            : #include "theory/quantifiers/quant_module.h"
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            :     
      30                 :            : class SolverEngine;
      31                 :            : 
      32                 :            : namespace theory {
      33                 :            : namespace quantifiers {
      34                 :            : 
      35                 :            : class MbqiEnum;
      36                 :            : 
      37                 :            : /**
      38                 :            :  * InstStrategyMbqi
      39                 :            :  *
      40                 :            :  * A basic implementation of Ge/de Moura CAV 2009. This class can be used to
      41                 :            :  * check whether the current model satisfies quantified formulas using
      42                 :            :  * subsolvers. The negation of the quantified formula is added as an assertion,
      43                 :            :  * along with embeddings of the models of uninterpreted sorts. If the query
      44                 :            :  * to the subsolver is unsat, then the quantified formula is satisfied.
      45                 :            :  * Otherwise, the model from the subsolver is used to construct an
      46                 :            :  * instantiation.
      47                 :            :  */
      48                 :            : class InstStrategyMbqi : public QuantifiersModule
      49                 :            : {
      50                 :            :   friend class MbqiEnum;
      51                 :            :  public:
      52                 :            :   InstStrategyMbqi(Env& env,
      53                 :            :                    QuantifiersState& qs,
      54                 :            :                    QuantifiersInferenceManager& qim,
      55                 :            :                    QuantifiersRegistry& qr,
      56                 :            :                    TermRegistry& tr);
      57                 :       1034 :   ~InstStrategyMbqi() {}
      58                 :            :   /** reset round */
      59                 :            :   void reset_round(Theory::Effort e) override;
      60                 :            :   /** needs check */
      61                 :            :   bool needsCheck(Theory::Effort e) override;
      62                 :            :   /** needs model */
      63                 :            :   QEffort needsModel(Theory::Effort e) override;
      64                 :            :   /** check */
      65                 :            :   void check(Theory::Effort e, QEffort quant_e) override;
      66                 :            :   /** Check was complete for quantified formula q */
      67                 :            :   bool checkCompleteFor(Node q) override;
      68                 :            :   /** For collecting global terms from all available assertions. */
      69                 :            :   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
      70                 :            :   /** Get the symbols appearing in assertions */
      71                 :            :   const context::CDHashSet<Node>& getGlobalSyms() const;
      72                 :            :   /** identify */
      73                 :          0 :   std::string identify() const override { return "mbqi"; }
      74                 :            : 
      75                 :            :  private:
      76                 :            :   /**
      77                 :            :    * Process quantified formula q, which may add q to d_quantChecked, add an
      78                 :            :    * instantiation for q, or do nothing if something went wrong (e.g. if the
      79                 :            :    * query to the subsolver could not be constructed).
      80                 :            :    */
      81                 :            :   void process(Node q);
      82                 :            :   /**
      83                 :            :    * Convert to query.
      84                 :            :    *
      85                 :            :    * This converts term t that is the body of a quantified
      86                 :            :    * formula into a term that can be sent to the subsolver. Its free constants
      87                 :            :    * are replaced by their model values. The map freshVarType maintains fresh
      88                 :            :    * variables that were introduced corresponding to values of uninterpreted
      89                 :            :    * sort constants.
      90                 :            :    *
      91                 :            :    * cmap caches the results of the conversion.
      92                 :            :    */
      93                 :            :   Node convertToQuery(
      94                 :            :       Node t,
      95                 :            :       std::unordered_map<Node, Node>& cmap,
      96                 :            :       std::map<TypeNode, std::unordered_set<Node> >& freshVarType);
      97                 :            :   /**
      98                 :            :    * Convert from model
      99                 :            :    *
     100                 :            :    * This converts a term t that was returned as a model
     101                 :            :    * value by a subsolver. We use the mapping mvToFreshVar to convert
     102                 :            :    * uninterpreted constants to the fresh variables that were used for
     103                 :            :    * that value in the model from the subsolver.
     104                 :            :    *
     105                 :            :    * cmap caches the results of the conversion.
     106                 :            :    */
     107                 :            :   Node convertFromModel(Node t,
     108                 :            :                         std::unordered_map<Node, Node>& cmap,
     109                 :            :                         const std::map<Node, Node>& mvToFreshVar);
     110                 :            :   /**
     111                 :            :    * Make skolem for term. We use a separate skolem identifier MBQI_INPUT
     112                 :            :    * to refer to the variables of a quantified formula. While purification
     113                 :            :    * skolems could also suffice, this avoids further complications due to
     114                 :            :    * purification skolems for Boolean variables being treated as UF atoms,
     115                 :            :    * which can lead to logic exceptions in subsolvers.
     116                 :            :    */
     117                 :            :   Node mkMbqiSkolem(const Node& t);
     118                 :            :   /**
     119                 :            :    * Return the model value for term t from the solver, possibly post-processing
     120                 :            :    * it with modules maintained by this class (e.g. d_msenum).
     121                 :            :    * @param q The quantified formula we are instantiating.
     122                 :            :    * @param query The query used to find the model-based instantiation.
     123                 :            :    * @param smt The subsolver the query was made on.
     124                 :            :    * @param vars The variables we are instantiating.
     125                 :            :    * @param mvs The model values found for vars by the subsolver. This vector
     126                 :            :    * may be modified based on modules maintained by this class.
     127                 :            :    * @param mvToFreshVar Used for representing values for uninterpreted sorts.
     128                 :            :    */
     129                 :            :   void modelValueFromQuery(const Node& q,
     130                 :            :                            const Node& query,
     131                 :            :                            SolverEngine& smt,
     132                 :            :                            const std::vector<Node>& vars,
     133                 :            :                            std::vector<Node>& mvs,
     134                 :            :                            const std::map<Node, Node>& mvToFreshVar);
     135                 :            :   /** The quantified formulas that we succeeded in checking */
     136                 :            :   std::unordered_set<Node> d_quantChecked;
     137                 :            :   /** Kinds that cannot appear in queries */
     138                 :            :   std::unordered_set<Kind, kind::KindHashFunction> d_nonClosedKinds;
     139                 :            :   /** Submodule for sygus enum */
     140                 :            :   std::unique_ptr<MbqiEnum> d_msenum;
     141                 :            :   /** The options for subsolver calls */
     142                 :            :   Options d_subOptions;
     143                 :            :   /* Set of global ground terms in assertions (outside of quantifiers). */
     144                 :            :   context::CDHashSet<Node> d_globalSyms;
     145                 :            : };
     146                 :            : 
     147                 :            : }  // namespace quantifiers
     148                 :            : }  // namespace theory
     149                 :            : }  // namespace cvc5::internal
     150                 :            : 
     151                 :            : #endif /* CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_MBQI_H */