Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
       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                 :            :  * Implementation of dynamic quantifiers splitting.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/quantifiers/quant_split.h"
      17                 :            : 
      18                 :            : #include "expr/dtype.h"
      19                 :            : #include "expr/dtype_cons.h"
      20                 :            : #include "options/quantifiers_options.h"
      21                 :            : #include "theory/datatypes/theory_datatypes_utils.h"
      22                 :            : #include "theory/quantifiers/first_order_model.h"
      23                 :            : #include "theory/quantifiers/term_database.h"
      24                 :            : 
      25                 :            : using namespace cvc5::internal::kind;
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace theory {
      29                 :            : namespace quantifiers {
      30                 :            : 
      31                 :      39174 : QuantDSplit::QuantDSplit(Env& env,
      32                 :            :                          QuantifiersState& qs,
      33                 :            :                          QuantifiersInferenceManager& qim,
      34                 :            :                          QuantifiersRegistry& qr,
      35                 :      39174 :                          TermRegistry& tr)
      36                 :            :     : QuantifiersModule(env, qs, qim, qr, tr),
      37                 :      78348 :       d_quant_to_reduce(userContext()),
      38                 :      39174 :       d_added_split(userContext())
      39                 :            : {
      40                 :      39174 : }
      41                 :            : 
      42                 :      33414 : void QuantDSplit::checkOwnership(Node q)
      43                 :            : {
      44                 :            :   // If q is non-standard (marked as sygus, quantifier elimination, etc.), then
      45                 :            :   // do no split it.
      46                 :      33414 :   QAttributes qa;
      47                 :      33414 :   QuantAttributes::computeQuantAttributes(q, qa);
      48         [ +  + ]:      33414 :   if (!qa.isStandard())
      49                 :            :   {
      50                 :       3536 :     return;
      51                 :            :   }
      52                 :      29878 :   bool takeOwnership = false;
      53                 :      29878 :   bool doSplit = false;
      54                 :      29878 :   QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
      55         [ +  - ]:      29878 :   Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
      56         [ +  + ]:      97878 :   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
      57                 :     141214 :     TypeNode tn = q[0][i].getType();
      58         [ +  + ]:      70607 :     if( tn.isDatatype() ){
      59                 :      10340 :       bool isFinite = d_env.isFiniteType(tn);
      60                 :      10340 :       const DType& dt = tn.getDType();
      61         [ +  + ]:      10340 :       if (dt.isRecursiveSingleton(tn))
      62                 :            :       {
      63 [ +  - ][ -  + ]:        450 :         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
                 [ -  - ]
      64                 :            :       }
      65                 :            :       else
      66                 :            :       {
      67                 :       9890 :         if (options().quantifiers.quantDynamicSplit
      68         [ -  + ]:       9890 :             == options::QuantDSplitMode::AGG)
      69                 :            :         {
      70                 :            :           // split if it is a finite datatype
      71                 :          0 :           doSplit = isFinite;
      72                 :            :         }
      73                 :       9890 :         else if (options().quantifiers.quantDynamicSplit
      74         [ +  - ]:       9890 :                  == options::QuantDSplitMode::DEFAULT)
      75                 :            :         {
      76         [ +  + ]:       9890 :           if (!qbi.isFiniteBound(q, q[0][i]))
      77                 :            :           {
      78         [ +  + ]:       9707 :             if (isFinite)
      79                 :            :             {
      80                 :            :               // split if goes from being unhandled -> handled by finite
      81                 :            :               // instantiation. An example is datatypes with uninterpreted sort
      82                 :            :               // fields which are "interpreted finite" but not "finite".
      83                 :         48 :               doSplit = true;
      84                 :            :               // we additionally take ownership of this formula, in other words,
      85                 :            :               // we mark it reduced.
      86                 :         48 :               takeOwnership = true;
      87                 :            :             }
      88 [ +  + ][ +  - ]:       9659 :             else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
                 [ +  + ]
      89                 :            :             {
      90                 :            :               // split if only one constructor
      91                 :       2559 :               doSplit = true;
      92                 :            :             }
      93                 :            :           }
      94                 :            :         }
      95         [ +  + ]:       9890 :         if (doSplit)
      96                 :            :         {
      97                 :            :           // store the index to split
      98                 :       2607 :           d_quant_to_reduce[q] = i;
      99         [ +  - ]:       5214 :           Trace("quant-dsplit-debug")
     100 [ -  + ][ -  - ]:       2607 :               << "Split at index " << i << " based on datatype " << dt.getName()
     101                 :       2607 :               << std::endl;
     102                 :       2607 :           break;
     103                 :            :         }
     104         [ +  - ]:      14566 :         Trace("quant-dsplit-debug")
     105 [ -  + ][ -  - ]:       7283 :             << "Do not split based on datatype " << dt.getName() << std::endl;
     106                 :            :       }
     107                 :            :     }
     108                 :            :   }
     109                 :            : 
     110         [ +  + ]:      29878 :   if (takeOwnership)
     111                 :            :   {
     112         [ +  - ]:         48 :     Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
     113                 :         48 :     d_qreg.setOwner(q, this);
     114                 :            :   }
     115                 :            :   // Notice we may not take ownership in some cases, meaning that both the
     116                 :            :   // original quantified formula and the split one are generated. This may
     117                 :            :   // increase our ability to answer "unsat", since quantifier instantiation
     118                 :            :   // heuristics may be more effective for one or the other (see issues #993
     119                 :            :   // and 3481).
     120                 :            : }
     121                 :            : 
     122                 :            : /* whether this module needs to check this round */
     123                 :     101016 : bool QuantDSplit::needsCheck( Theory::Effort e ) {
     124 [ +  + ][ +  + ]:     101016 :   return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
     125                 :            : }
     126                 :            : 
     127                 :        742 : bool QuantDSplit::checkCompleteFor( Node q ) {
     128                 :            :   // true if we split q
     129                 :        742 :   return d_added_split.find( q )!=d_added_split.end();
     130                 :            : }
     131                 :            : 
     132                 :            : /* Call during quantifier engine's check */
     133                 :       2973 : void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
     134                 :            : {
     135                 :            :   //add lemmas ASAP (they are a reduction)
     136         [ +  + ]:       2973 :   if (quant_e != QEFFORT_CONFLICT)
     137                 :            :   {
     138                 :       1751 :     return;
     139                 :            :   }
     140         [ +  - ]:       1222 :   Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
     141                 :       1222 :   NodeManager* nm = nodeManager();
     142                 :       1222 :   FirstOrderModel* m = d_treg.getModel();
     143                 :       1222 :   std::vector<Node> lemmas;
     144                 :      42060 :   for (NodeIntMap::iterator it = d_quant_to_reduce.begin();
     145         [ +  + ]:      42060 :        it != d_quant_to_reduce.end();
     146                 :      40838 :        ++it)
     147                 :            :   {
     148                 :      40838 :     Node q = it->first;
     149         [ +  - ]:      40838 :     Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
     150         [ +  + ]:      40838 :     if (d_added_split.find(q) != d_added_split.end())
     151                 :            :     {
     152                 :      38131 :       continue;
     153                 :            :     }
     154                 :       2707 :     if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q))
     155                 :            :     {
     156                 :       2581 :       d_added_split.insert(q);
     157                 :       5162 :       std::vector<Node> bvs;
     158         [ +  + ]:      10282 :       for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
     159                 :            :       {
     160         [ +  + ]:       7701 :         if (static_cast<int>(i) != it->second)
     161                 :            :         {
     162                 :       5120 :           bvs.push_back(q[0][i]);
     163                 :            :         }
     164                 :            :       }
     165                 :       5162 :       std::vector<Node> disj;
     166                 :       2581 :       disj.push_back(q.negate());
     167                 :       7743 :       TNode svar = q[0][it->second];
     168                 :       5162 :       TypeNode tn = svar.getType();
     169 [ -  + ][ -  + ]:       2581 :       Assert(tn.isDatatype());
                 [ -  - ]
     170                 :       5162 :       std::vector<Node> cons;
     171                 :       2581 :       const DType& dt = tn.getDType();
     172         [ +  + ]:       5178 :       for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
     173                 :            :       {
     174                 :       5194 :         std::vector<Node> vars;
     175                 :       5194 :         TypeNode dtjtn = dt[j].getInstantiatedConstructorType(tn);
     176 [ -  + ][ -  + ]:       2597 :         Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
                 [ -  - ]
     177         [ +  + ]:       7739 :         for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
     178                 :            :         {
     179                 :      10284 :           TypeNode tns = dtjtn[k];
     180                 :      10284 :           Node v = nm->mkBoundVar(tns);
     181                 :       5142 :           vars.push_back(v);
     182                 :            :         }
     183                 :       5194 :         std::vector<Node> bvs_cmb;
     184                 :       2597 :         bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
     185                 :       2597 :         bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
     186                 :       5194 :         Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
     187                 :       5194 :         TNode ct = c;
     188                 :       7791 :         Node body = q[1].substitute(svar, ct);
     189         [ +  - ]:       2597 :         if (!bvs_cmb.empty())
     190                 :            :         {
     191                 :       5194 :           Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, bvs_cmb);
     192                 :       2597 :           std::vector<Node> children;
     193                 :       2597 :           children.push_back(bvl);
     194                 :       2597 :           children.push_back(body);
     195         [ +  + ]:       2597 :           if (q.getNumChildren() == 3)
     196                 :            :           {
     197                 :       2406 :             Node ipls = q[2].substitute(svar, ct);
     198                 :        802 :             children.push_back(ipls);
     199                 :            :           }
     200                 :       2597 :           body = nm->mkNode(Kind::FORALL, children);
     201                 :            :         }
     202                 :       2597 :         cons.push_back(body);
     203                 :            :       }
     204         [ +  + ]:       2581 :       Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(Kind::AND, cons);
     205                 :       2581 :       disj.push_back(conc);
     206         [ -  + ]:       2581 :       lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(Kind::OR, disj));
     207                 :            :     }
     208                 :            :   }
     209                 :            : 
     210                 :            :   // add lemmas to quantifiers engine
     211         [ +  + ]:       3803 :   for (const Node& lem : lemmas)
     212                 :            :   {
     213         [ +  - ]:       2581 :     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
     214                 :       2581 :     d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_DSPLIT);
     215                 :            :   }
     216         [ +  - ]:       1222 :   Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
     217                 :            : }
     218                 :            : 
     219                 :            : }  // namespace quantifiers
     220                 :            : }  // namespace theory
     221                 :            : }  // namespace cvc5::internal