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                 :            :  * Methods for counterexample-guided quantifier instantiation
      11                 :            :  * based on nested quantifier elimination.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "theory/quantifiers/cegqi/nested_qe.h"
      15                 :            : 
      16                 :            : #include "expr/node_algorithm.h"
      17                 :            : #include "expr/subs.h"
      18                 :            : #include "smt/env.h"
      19                 :            : #include "theory/rewriter.h"
      20                 :            : #include "theory/smt_engine_subsolver.h"
      21                 :            : #include "smt/set_defaults.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace theory {
      25                 :            : namespace quantifiers {
      26                 :            : 
      27                 :         50 : NestedQe::NestedQe(Env& env) : d_env(env), d_qnqe(d_env.getUserContext()) {}
      28                 :            : 
      29                 :         89 : bool NestedQe::process(Node q, std::vector<Node>& lems)
      30                 :            : {
      31                 :         89 :   NodeNodeMap::iterator it = d_qnqe.find(q);
      32         [ +  + ]:         89 :   if (it != d_qnqe.end())
      33                 :            :   {
      34                 :            :     // already processed
      35                 :         35 :     return (*it).second != q;
      36                 :            :   }
      37         [ +  - ]:         54 :   Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl;
      38                 :         54 :   Node qqe = doNestedQe(d_env, q, true);
      39                 :         54 :   d_qnqe[q] = qqe;
      40         [ +  + ]:         54 :   if (qqe == q)
      41                 :            :   {
      42         [ +  - ]:         31 :     Trace("cegqi-nested-qe") << "...did not apply nested QE" << std::endl;
      43                 :         31 :     return false;
      44                 :            :   }
      45         [ +  - ]:         23 :   Trace("cegqi-nested-qe") << "...applied nested QE" << std::endl;
      46         [ +  - ]:         23 :   Trace("cegqi-nested-qe") << "Result is " << qqe << std::endl;
      47                 :            : 
      48                 :            :   // add as lemma
      49                 :         23 :   lems.push_back(q.eqNode(qqe));
      50                 :         23 :   return true;
      51                 :         54 : }
      52                 :            : 
      53                 :          0 : bool NestedQe::hasProcessed(Node q) const
      54                 :            : {
      55                 :          0 :   return d_qnqe.find(q) != d_qnqe.end();
      56                 :            : }
      57                 :            : 
      58                 :        561 : bool NestedQe::getNestedQuantification(Node q, std::unordered_set<Node>& nqs)
      59                 :            : {
      60                 :        561 :   expr::getKindSubterms(q[1], Kind::FORALL, true, nqs);
      61                 :        561 :   return !nqs.empty();
      62                 :            : }
      63                 :            : 
      64                 :         66 : bool NestedQe::hasNestedQuantification(Node q)
      65                 :            : {
      66                 :         66 :   std::unordered_set<Node> nqs;
      67                 :        132 :   return getNestedQuantification(q, nqs);
      68                 :         66 : }
      69                 :            : 
      70                 :        495 : Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel)
      71                 :            : {
      72                 :        495 :   NodeManager* nm = env.getNodeManager();
      73                 :        495 :   Node qOrig = q;
      74                 :        495 :   bool inputExists = false;
      75         [ +  + ]:        495 :   if (q.getKind() == Kind::EXISTS)
      76                 :            :   {
      77                 :         42 :     q = nm->mkNode(Kind::FORALL, q[0], q[1].negate());
      78                 :         42 :     inputExists = true;
      79                 :            :   }
      80 [ -  + ][ -  + ]:        495 :   Assert(q.getKind() == Kind::FORALL);
                 [ -  - ]
      81                 :        495 :   std::unordered_set<Node> nqs;
      82         [ +  + ]:        495 :   if (!getNestedQuantification(q, nqs))
      83                 :            :   {
      84         [ +  - ]:        930 :     Trace("cegqi-nested-qe-debug")
      85                 :        465 :         << "...no nested quantification" << std::endl;
      86         [ +  + ]:        465 :     if (keepTopLevel)
      87                 :            :     {
      88                 :        442 :       return qOrig;
      89                 :            :     }
      90                 :            :     // just do ordinary quantifier elimination
      91                 :         23 :     Node qqe = doQe(env, q);
      92         [ +  - ]:         23 :     Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl;
      93                 :         23 :     return qqe;
      94                 :         23 :   }
      95         [ +  - ]:         60 :   Trace("cegqi-nested-qe-debug")
      96                 :         30 :       << "..." << nqs.size() << " nested quantifiers" << std::endl;
      97                 :            :   // otherwise, skolemize the arguments of this and apply
      98                 :         60 :   std::vector<Node> vars(q[0].begin(), q[0].end());
      99                 :         30 :   Subs sk;
     100                 :         30 :   sk.add(vars);
     101                 :            :   // do nested quantifier elimination on each nested quantifier, skolemizing the
     102                 :            :   // free variables
     103                 :         30 :   Subs snqe;
     104         [ +  + ]:         60 :   for (const Node& nq : nqs)
     105                 :            :   {
     106                 :         30 :     Node nqk = sk.apply(nq);
     107                 :         30 :     Node nqqe = doNestedQe(env, nqk);
     108         [ -  + ]:         30 :     if (nqqe == nqk)
     109                 :            :     {
     110                 :            :       // failed
     111         [ -  - ]:          0 :       Trace("cegqi-nested-qe-debug")
     112                 :          0 :           << "...failed to apply to nested" << std::endl;
     113                 :          0 :       return q;
     114                 :            :     }
     115                 :         30 :     snqe.add(nqk, nqqe);
     116 [ +  - ][ +  - ]:         30 :   }
     117                 :            :   // get the result of nested quantifier elimination
     118                 :         30 :   Node qeBody = sk.apply(q[1]);
     119                 :         30 :   qeBody = snqe.apply(qeBody);
     120                 :            :   // undo the skolemization
     121                 :         30 :   qeBody = sk.rapply(qeBody);
     122                 :         30 :   qeBody = env.getRewriter()->rewrite(qeBody);
     123                 :            :   // reconstruct the body
     124                 :         30 :   std::vector<Node> qargs;
     125                 :         30 :   qargs.push_back(q[0]);
     126         [ -  + ]:         30 :   qargs.push_back(inputExists ? qeBody.negate() : qeBody);
     127         [ -  + ]:         30 :   if (q.getNumChildren() == 3)
     128                 :            :   {
     129                 :          0 :     qargs.push_back(q[2]);
     130                 :            :   }
     131         [ -  + ]:         30 :   return nm->mkNode(inputExists ? Kind::EXISTS : Kind::FORALL, qargs);
     132                 :        495 : }
     133                 :            : 
     134                 :         23 : Node NestedQe::doQe(Env& env, Node q)
     135                 :            : {
     136 [ -  + ][ -  + ]:         23 :   Assert(q.getKind() == Kind::FORALL);
                 [ -  - ]
     137         [ +  - ]:         23 :   Trace("cegqi-nested-qe") << "  Apply qe to " << q << std::endl;
     138                 :         23 :   q = NodeManager::mkNode(Kind::EXISTS, q[0], q[1].negate());
     139                 :         23 :   std::unique_ptr<SolverEngine> smt_qe;
     140                 :         23 :   Options subOptions;
     141                 :         23 :   subOptions.copyValues(env.getOptions());
     142                 :         23 :   smt::SetDefaults::disableChecking(subOptions);
     143                 :         23 :   SubsolverSetupInfo ssi(env, subOptions);
     144                 :         23 :   initializeSubsolver(env.getNodeManager(), smt_qe, ssi);
     145                 :         23 :   Node qqe = smt_qe->getQuantifierElimination(q, true);
     146         [ -  + ]:         23 :   if (expr::hasBoundVar(qqe))
     147                 :            :   {
     148         [ -  - ]:          0 :     Trace("cegqi-nested-qe") << "  ...failed QE" << std::endl;
     149                 :            :     //...failed to apply
     150                 :          0 :     return q;
     151                 :            :   }
     152                 :         23 :   Node res = qqe.negate();
     153         [ +  - ]:         23 :   Trace("cegqi-nested-qe") << "  ...success, result = " << res << std::endl;
     154                 :         23 :   return res;
     155                 :         23 : }
     156                 :            : 
     157                 :            : }  // namespace quantifiers
     158                 :            : }  // namespace theory
     159                 :            : }  // namespace cvc5::internal