Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Mathias Preiner, Andrew Reynolds, Andres Noetzli
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * SyGuS instantiator class.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
      20                 :            : 
      21                 :            : #include <unordered_map>
      22                 :            : #include <unordered_set>
      23                 :            : 
      24                 :            : #include "context/cdhashset.h"
      25                 :            : #include "smt/env_obj.h"
      26                 :            : #include "theory/decision_strategy.h"
      27                 :            : #include "theory/quantifiers/quant_module.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace theory {
      31                 :            : 
      32                 :            : class QuantifiersEngine;
      33                 :            : 
      34                 :            : namespace quantifiers {
      35                 :            : 
      36                 :            : /**
      37                 :            :  * SyGuS quantifier instantion module.
      38                 :            :  *
      39                 :            :  * This module uses SyGuS techniques to find terms for instantiation and
      40                 :            :  * combines it with counterexample guided instantiation. It uses the datatypes
      41                 :            :  * solver to find instantiation for each variable based on a specified SyGuS
      42                 :            :  * grammar.
      43                 :            :  *
      44                 :            :  * The CE lemma generated for a quantified formula
      45                 :            :  *
      46                 :            :  *   \forall x . P[x]
      47                 :            :  *
      48                 :            :  * is
      49                 :            :  *
      50                 :            :  *   ce_lit => ~P[DT_SYGUS_EVAL(dt_x)]
      51                 :            :  *
      52                 :            :  * where ce_lit is a the counterexample literal for the quantified formula and
      53                 :            :  * dt_x is a fresh datatype variable with the SyGuS grammar for x as type.
      54                 :            :  *
      55                 :            :  * While checking, for active quantifiers, we add (full) evaluation unfolding
      56                 :            :  * lemmas as follows (see Reynolds at al. CAV 2019b for more information):
      57                 :            :  *
      58                 :            :  *   explain(dt_x=dt_x^M) => DT_SYGUS_EVAL(dt_x) = t
      59                 :            :  *
      60                 :            :  * where t = sygusToBuiltin(dt_x^M).
      61                 :            :  *
      62                 :            :  * We collect the t_i for each bound variable x_i and use them to instantiate
      63                 :            :  * the quantified formula.
      64                 :            :  */
      65                 :            : class SygusInst : public QuantifiersModule
      66                 :            : {
      67                 :            :  public:
      68                 :            :   SygusInst(Env& env,
      69                 :            :             QuantifiersState& qs,
      70                 :            :             QuantifiersInferenceManager& qim,
      71                 :            :             QuantifiersRegistry& qr,
      72                 :            :             TermRegistry& tr);
      73                 :        304 :   ~SygusInst() = default;
      74                 :            : 
      75                 :            :   bool needsCheck(Theory::Effort e) override;
      76                 :            : 
      77                 :            :   QEffort needsModel(Theory::Effort e) override;
      78                 :            : 
      79                 :            :   void reset_round(Theory::Effort e) override;
      80                 :            : 
      81                 :            :   void check(Theory::Effort e, QEffort quant_e) override;
      82                 :            : 
      83                 :            :   bool checkCompleteFor(Node q) override;
      84                 :            : 
      85                 :            :   /* Called once for every quantifier 'q' globally (not dependent on context).
      86                 :            :    */
      87                 :            :   void registerQuantifier(Node q) override;
      88                 :            : 
      89                 :            :   /* Called once for every quantifier 'q' per context. */
      90                 :            :   void preRegisterQuantifier(Node q) override;
      91                 :            : 
      92                 :            :   /* For collecting global terms from all available assertions. */
      93                 :            :   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
      94                 :            : 
      95                 :            :   std::string identify() const override;
      96                 :            : 
      97                 :            :  private:
      98                 :            :   /* Lookup counterexample literal or create a new one for quantifier 'q'. */
      99                 :            :   Node getCeLiteral(Node q);
     100                 :            : 
     101                 :            :   /* Generate counterexample lemma for quantifier 'q'. This is done once per
     102                 :            :    * quantifier on registerQuantifier() calls. */
     103                 :            :   void registerCeLemma(Node q, std::vector<TypeNode>& dtypes);
     104                 :            : 
     105                 :            :   /* Add counterexample lemma for quantifier 'q'. This is done on every
     106                 :            :    * preRegisterQuantifier() call.*/
     107                 :            :   void addCeLemma(Node q);
     108                 :            : 
     109                 :            :   /* Send evaluation unfolding lemmas and cache them.
     110                 :            :    * Returns true if a new lemma (not cached) was added, and false otherwise.
     111                 :            :    */
     112                 :            :   bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
     113                 :            : 
     114                 :            :   /** Return true if this module should process quantified formula q */
     115                 :            :   bool shouldProcess(Node q);
     116                 :            : 
     117                 :            :   /* Maps quantifiers to a vector of instantiation constants. */
     118                 :            :   std::unordered_map<Node, std::vector<Node>> d_inst_constants;
     119                 :            : 
     120                 :            :   /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */
     121                 :            :   std::unordered_map<Node, std::vector<Node>> d_var_eval;
     122                 :            : 
     123                 :            :   /* Maps quantified formulas to registered counterexample literals. */
     124                 :            :   std::unordered_map<Node, Node> d_ce_lits;
     125                 :            : 
     126                 :            :   /* Decision strategies registered for quantified formulas. */
     127                 :            :   std::unordered_map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
     128                 :            : 
     129                 :            :   /* Currently active quantifiers. */
     130                 :            :   std::unordered_set<Node> d_active_quant;
     131                 :            : 
     132                 :            :   /* Currently inactive quantifiers. */
     133                 :            :   std::unordered_set<Node> d_inactive_quant;
     134                 :            : 
     135                 :            :   /* Registered counterexample lemma cache. */
     136                 :            :   std::unordered_map<Node, Node> d_ce_lemmas;
     137                 :            : 
     138                 :            :   /* Indicates whether a counterexample lemma was added for a quantified
     139                 :            :    * formula in the current context. */
     140                 :            :   context::CDHashSet<Node> d_ce_lemma_added;
     141                 :            : 
     142                 :            :   /* Set of global ground terms in assertions (outside of quantifiers). */
     143                 :            :   context::CDHashMap<TypeNode, std::unordered_set<Node>> d_global_terms;
     144                 :            : 
     145                 :            :   /* Assertions sent by ppNotifyAssertions. */
     146                 :            :   context::CDHashSet<Node> d_notified_assertions;
     147                 :            : };
     148                 :            : 
     149                 :            : }  // namespace quantifiers
     150                 :            : }  // namespace theory
     151                 :            : }  // namespace cvc5::internal
     152                 :            : 
     153                 :            : #endif