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                 :      39621 : QuantDSplit::QuantDSplit(Env& env,
      32                 :            :                          QuantifiersState& qs,
      33                 :            :                          QuantifiersInferenceManager& qim,
      34                 :            :                          QuantifiersRegistry& qr,
      35                 :      39621 :                          TermRegistry& tr)
      36                 :            :     : QuantifiersModule(env, qs, qim, qr, tr),
      37                 :      79242 :       d_quant_to_reduce(userContext()),
      38                 :      39621 :       d_added_split(userContext())
      39                 :            : {
      40                 :      39621 : }
      41                 :            : 
      42                 :      32499 : 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                 :      32499 :   QAttributes qa;
      47                 :      32499 :   QuantAttributes::computeQuantAttributes(q, qa);
      48         [ +  + ]:      32499 :   if (!qa.isStandard())
      49                 :            :   {
      50                 :       3536 :     return;
      51                 :            :   }
      52                 :            :   // do not split if there is a trigger
      53         [ +  + ]:      28963 :   if (qa.d_hasPattern)
      54                 :            :   {
      55                 :       2614 :     return;
      56                 :            :   }
      57                 :      26349 :   bool takeOwnership = false;
      58                 :      26349 :   bool doSplit = false;
      59                 :      26349 :   QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
      60         [ +  - ]:      26349 :   Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
      61         [ +  + ]:      86660 :   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
      62                 :     124264 :     TypeNode tn = q[0][i].getType();
      63         [ +  + ]:      62132 :     if( tn.isDatatype() ){
      64                 :       7492 :       bool isFinite = d_env.isFiniteType(tn);
      65                 :       7492 :       const DType& dt = tn.getDType();
      66         [ +  + ]:       7492 :       if (dt.isRecursiveSingleton(tn))
      67                 :            :       {
      68 [ +  - ][ -  + ]:        450 :         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
                 [ -  - ]
      69                 :            :       }
      70                 :            :       else
      71                 :            :       {
      72                 :       7042 :         if (options().quantifiers.quantDynamicSplit
      73         [ -  + ]:       7042 :             == options::QuantDSplitMode::AGG)
      74                 :            :         {
      75                 :            :           // split if it is a finite datatype
      76                 :          0 :           doSplit = isFinite;
      77                 :            :         }
      78                 :       7042 :         else if (options().quantifiers.quantDynamicSplit
      79         [ +  - ]:       7042 :                  == options::QuantDSplitMode::DEFAULT)
      80                 :            :         {
      81         [ +  + ]:       7042 :           if (!qbi.isFiniteBound(q, q[0][i]))
      82                 :            :           {
      83         [ +  + ]:       6859 :             if (isFinite)
      84                 :            :             {
      85                 :            :               // split if goes from being unhandled -> handled by finite
      86                 :            :               // instantiation. An example is datatypes with uninterpreted sort
      87                 :            :               // fields which are "interpreted finite" but not "finite".
      88                 :         48 :               doSplit = true;
      89                 :            :               // we additionally take ownership of this formula, in other words,
      90                 :            :               // we mark it reduced.
      91                 :         48 :               takeOwnership = true;
      92                 :            :             }
      93 [ +  + ][ +  - ]:       6811 :             else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
                 [ +  + ]
      94                 :            :             {
      95                 :            :               // split if only one constructor
      96                 :       1773 :               doSplit = true;
      97                 :            :             }
      98                 :            :           }
      99                 :            :         }
     100         [ +  + ]:       7042 :         if (doSplit)
     101                 :            :         {
     102                 :            :           // store the index to split
     103                 :       1821 :           d_quant_to_reduce[q] = i;
     104         [ +  - ]:       3642 :           Trace("quant-dsplit-debug")
     105 [ -  + ][ -  - ]:       1821 :               << "Split at index " << i << " based on datatype " << dt.getName()
     106                 :       1821 :               << std::endl;
     107                 :       1821 :           break;
     108                 :            :         }
     109         [ +  - ]:      10442 :         Trace("quant-dsplit-debug")
     110 [ -  + ][ -  - ]:       5221 :             << "Do not split based on datatype " << dt.getName() << std::endl;
     111                 :            :       }
     112                 :            :     }
     113                 :            :   }
     114                 :            : 
     115         [ +  + ]:      26349 :   if (takeOwnership)
     116                 :            :   {
     117         [ +  - ]:         48 :     Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
     118                 :         48 :     d_qreg.setOwner(q, this);
     119                 :            :   }
     120                 :            :   // Notice we may not take ownership in some cases, meaning that both the
     121                 :            :   // original quantified formula and the split one are generated. This may
     122                 :            :   // increase our ability to answer "unsat", since quantifier instantiation
     123                 :            :   // heuristics may be more effective for one or the other (see issues #993
     124                 :            :   // and 3481).
     125                 :            : }
     126                 :            : 
     127                 :            : /* whether this module needs to check this round */
     128                 :     101164 : bool QuantDSplit::needsCheck( Theory::Effort e ) {
     129 [ +  + ][ +  + ]:     101164 :   return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
     130                 :            : }
     131                 :            : 
     132                 :        743 : bool QuantDSplit::checkCompleteFor( Node q ) {
     133                 :            :   // true if we split q
     134                 :        743 :   return d_added_split.find( q )!=d_added_split.end();
     135                 :            : }
     136                 :            : 
     137                 :            : /* Call during quantifier engine's check */
     138                 :       3770 : void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
     139                 :            : {
     140                 :            :   //add lemmas ASAP (they are a reduction)
     141         [ +  + ]:       3770 :   if (quant_e != QEFFORT_CONFLICT)
     142                 :            :   {
     143                 :       2414 :     return;
     144                 :            :   }
     145         [ +  - ]:       1356 :   Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
     146                 :       1356 :   NodeManager* nm = nodeManager();
     147                 :       1356 :   FirstOrderModel* m = d_treg.getModel();
     148                 :       1356 :   std::vector<Node> lemmas;
     149                 :      30162 :   for (NodeIntMap::iterator it = d_quant_to_reduce.begin();
     150         [ +  + ]:      30162 :        it != d_quant_to_reduce.end();
     151                 :      28806 :        ++it)
     152                 :            :   {
     153                 :      28806 :     Node q = it->first;
     154         [ +  - ]:      28806 :     Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
     155         [ +  + ]:      28806 :     if (d_added_split.find(q) != d_added_split.end())
     156                 :            :     {
     157                 :      26891 :       continue;
     158                 :            :     }
     159                 :       1915 :     if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q))
     160                 :            :     {
     161                 :       1795 :       d_added_split.insert(q);
     162                 :       3590 :       std::vector<Node> bvs;
     163         [ +  + ]:       7376 :       for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
     164                 :            :       {
     165         [ +  + ]:       5581 :         if (static_cast<int>(i) != it->second)
     166                 :            :         {
     167                 :       3786 :           bvs.push_back(q[0][i]);
     168                 :            :         }
     169                 :            :       }
     170                 :       3590 :       std::vector<Node> disj;
     171                 :       1795 :       disj.push_back(q.negate());
     172                 :       5385 :       TNode svar = q[0][it->second];
     173                 :       3590 :       TypeNode tn = svar.getType();
     174 [ -  + ][ -  + ]:       1795 :       Assert(tn.isDatatype());
                 [ -  - ]
     175                 :       3590 :       std::vector<Node> cons;
     176                 :       1795 :       const DType& dt = tn.getDType();
     177         [ +  + ]:       3606 :       for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
     178                 :            :       {
     179                 :       3622 :         std::vector<Node> vars;
     180                 :       3622 :         TypeNode dtjtn = dt[j].getInstantiatedConstructorType(tn);
     181 [ -  + ][ -  + ]:       1811 :         Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
                 [ -  - ]
     182         [ +  + ]:       5372 :         for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
     183                 :            :         {
     184                 :       7122 :           TypeNode tns = dtjtn[k];
     185                 :       7122 :           Node v = nm->mkBoundVar(tns);
     186                 :       3561 :           vars.push_back(v);
     187                 :            :         }
     188                 :       3622 :         std::vector<Node> bvs_cmb;
     189                 :       1811 :         bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
     190                 :       1811 :         bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
     191                 :       3622 :         Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
     192                 :       3622 :         TNode ct = c;
     193                 :       5433 :         Node body = q[1].substitute(svar, ct);
     194         [ +  - ]:       1811 :         if (!bvs_cmb.empty())
     195                 :            :         {
     196                 :       3622 :           Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, bvs_cmb);
     197                 :       1811 :           std::vector<Node> children;
     198                 :       1811 :           children.push_back(bvl);
     199                 :       1811 :           children.push_back(body);
     200         [ -  + ]:       1811 :           if (q.getNumChildren() == 3)
     201                 :            :           {
     202                 :          0 :             Node ipls = q[2].substitute(svar, ct);
     203                 :          0 :             children.push_back(ipls);
     204                 :            :           }
     205                 :       1811 :           body = nm->mkNode(Kind::FORALL, children);
     206                 :            :         }
     207                 :       1811 :         cons.push_back(body);
     208                 :            :       }
     209         [ +  + ]:       1795 :       Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(Kind::AND, cons);
     210                 :       1795 :       disj.push_back(conc);
     211         [ -  + ]:       1795 :       lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(Kind::OR, disj));
     212                 :            :     }
     213                 :            :   }
     214                 :            : 
     215                 :            :   // add lemmas to quantifiers engine
     216         [ +  + ]:       3151 :   for (const Node& lem : lemmas)
     217                 :            :   {
     218         [ +  - ]:       1795 :     Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
     219                 :       1795 :     d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_DSPLIT);
     220                 :            :   }
     221         [ +  - ]:       1356 :   Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
     222                 :            : }
     223                 :            : 
     224                 :            : }  // namespace quantifiers
     225                 :            : }  // namespace theory
     226                 :            : }  // namespace cvc5::internal