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