Branch data     Line data    Source code

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