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                 :            :  * The solver for quantifier elimination queries.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "smt/quant_elim_solver.h"
      14                 :            : 
      15                 :            : #include "base/modal_exception.h"
      16                 :            : #include "expr/node_algorithm.h"
      17                 :            : #include "expr/skolem_manager.h"
      18                 :            : #include "expr/subs.h"
      19                 :            : #include "expr/subtype_elim_node_converter.h"
      20                 :            : #include "smt/smt_driver.h"
      21                 :            : #include "smt/smt_solver.h"
      22                 :            : #include "theory/quantifiers/cegqi/nested_qe.h"
      23                 :            : #include "theory/quantifiers_engine.h"
      24                 :            : #include "theory/theory_engine.h"
      25                 :            : #include "util/string.h"
      26                 :            : 
      27                 :            : using namespace cvc5::internal::theory;
      28                 :            : using namespace cvc5::internal::kind;
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : namespace smt {
      32                 :            : 
      33                 :      75822 : QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms, ContextManager* ctx)
      34                 :      75822 :     : EnvObj(env), d_smtSolver(sms), d_ctx(ctx)
      35                 :            : {
      36                 :      75822 : }
      37                 :            : 
      38                 :     141566 : QuantElimSolver::~QuantElimSolver() {}
      39                 :            : 
      40                 :        415 : Node QuantElimSolver::getQuantifierElimination(Node q,
      41                 :            :                                                bool doFull,
      42                 :            :                                                bool isInternalSubsolver)
      43                 :            : {
      44         [ +  - ]:        415 :   Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
      45 [ +  + ][ +  + ]:        415 :   if (q.getKind() != Kind::EXISTS && q.getKind() != Kind::FORALL)
                 [ +  + ]
      46                 :            :   {
      47                 :          4 :     throw ModalException(
      48                 :          8 :         "Expecting a quantified formula as argument to get-qe.");
      49                 :            :   }
      50                 :        411 :   NodeManager* nm = nodeManager();
      51                 :            :   // ensure the body is rewritten
      52                 :        411 :   q = nm->mkNode(q.getKind(), q[0], rewrite(q[1]));
      53                 :            :   // do nested quantifier elimination if necessary
      54                 :        411 :   q = quantifiers::NestedQe::doNestedQe(d_env, q, true);
      55         [ +  - ]:        822 :   Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
      56                 :        411 :                   << q << std::endl;
      57                 :            :   Node keyword =
      58         [ +  + ]:        411 :       nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial"));
      59                 :        411 :   Node n_attr = nm->mkNode(Kind::INST_ATTRIBUTE, keyword);
      60                 :            :   // Polarity is the Boolean constant we return if the subquery is "sat".
      61                 :        411 :   bool polarity = (q.getKind() != Kind::EXISTS);
      62                 :        411 :   Node ne;
      63                 :            :   // Special case: if we have no free symbols, just use a quantifier-free
      64                 :            :   // query. This ensures we don't depend on quantifier instantiation in
      65                 :            :   // these cases, which is especially important if the theory does not admit
      66                 :            :   // QE, e.g. strings.
      67                 :        411 :   std::unordered_set<Node> syms;
      68                 :        411 :   expr::getSymbols(q, syms);
      69                 :        411 :   bool closed = false;
      70         [ +  + ]:        411 :   if (syms.empty())
      71                 :            :   {
      72                 :            :     // Partial elimination is irrelevant since we have a closed formula, so we
      73                 :            :     // assume we are doing full elimination.
      74                 :        368 :     doFull = true;
      75                 :        368 :     closed = true;
      76                 :        368 :     Subs sq;
      77                 :        368 :     SkolemManager* sm = nm->getSkolemManager();
      78         [ +  + ]:        756 :     for (const Node& v : q[0])
      79                 :            :     {
      80                 :        388 :       Node k = sm->mkInternalSkolemFunction(
      81                 :        776 :           InternalSkolemId::QE_CLOSED_INPUT, v.getType(), {v});
      82                 :        388 :       sq.add(v, k);
      83                 :        756 :     }
      84                 :        368 :     ne = sq.apply(q[1]);
      85                 :            :     // We are skolemizing, so we flip the polarity
      86                 :        368 :     polarity = !polarity;
      87         [ +  + ]:        368 :     if (q.getKind() == Kind::EXISTS)
      88                 :            :     {
      89                 :          5 :       ne = ne.negate();
      90                 :            :     }
      91                 :        368 :   }
      92                 :            :   else
      93                 :            :   {
      94                 :            :     // tag the quantified formula with the quant-elim attribute
      95                 :         43 :     TypeNode t = nm->booleanType();
      96                 :         43 :     n_attr = nm->mkNode(Kind::INST_PATTERN_LIST, n_attr);
      97                 :         43 :     std::vector<Node> children;
      98                 :         43 :     children.push_back(q[0]);
      99 [ +  + ][ +  + ]:         43 :     children.push_back(q.getKind() == Kind::EXISTS ? q[1] : q[1].negate());
                 [ -  - ]
     100                 :         43 :     children.push_back(n_attr);
     101                 :         43 :     ne = nm->mkNode(Kind::EXISTS, children);
     102 [ -  + ][ -  + ]:         43 :     Assert(ne.getNumChildren() == 3);
                 [ -  - ]
     103                 :         43 :   }
     104         [ +  - ]:        822 :   Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne
     105                 :        411 :                         << std::endl;
     106                 :            :   // use a single call driver
     107                 :        411 :   SmtDriverSingleCall sdsc(d_env, d_smtSolver, d_ctx);
     108                 :       1233 :   Result r = sdsc.checkSat(std::vector<Node>{ne.notNode()});
     109         [ +  - ]:        411 :   Trace("smt-qe") << "Query returned " << r << std::endl;
     110         [ +  + ]:        411 :   if (r.getStatus() != Result::UNSAT)
     111                 :            :   {
     112 [ +  + ][ -  + ]:         36 :     if (r.getStatus() != Result::SAT && doFull)
                 [ -  + ]
     113                 :            :     {
     114                 :          0 :       verbose(1)
     115                 :          0 :           << "While performing quantifier elimination, unexpected result : "
     116                 :          0 :           << r << " for query." << std::endl;
     117                 :            :       // failed, return original
     118                 :          0 :       return q;
     119                 :            :     }
     120                 :            :     // must use original quantified formula to compute QE, which ensures that
     121                 :            :     // e.g. term formula removal is not run on the body. Notice that we assume
     122                 :            :     // that the (single) quantified formula is preprocessed, rewritten
     123                 :            :     // version of the input quantified formula q.
     124                 :         36 :     std::vector<Node> inst_qs;
     125                 :         36 :     Node topq;
     126                 :         36 :     Node ret;
     127         [ +  + ]:         36 :     if (!closed)
     128                 :            :     {
     129                 :         32 :       TheoryEngine* te = d_smtSolver.getTheoryEngine();
     130 [ -  + ][ -  + ]:         32 :       Assert(te != nullptr);
                 [ -  - ]
     131                 :         32 :       QuantifiersEngine* qe = te->getQuantifiersEngine();
     132                 :         32 :       qe->getInstantiatedQuantifiedFormulas(inst_qs);
     133                 :            :       // Find the quantified formula corresponding to the quantifier elimination
     134         [ +  - ]:         33 :       for (const Node& qinst : inst_qs)
     135                 :            :       {
     136                 :            :         // Should have the same attribute mark as above
     137 [ +  + ][ +  - ]:         33 :         if (qinst.getNumChildren() == 3 && qinst[2] == n_attr)
         [ +  + ][ +  + ]
                 [ -  - ]
     138                 :            :         {
     139                 :         32 :           topq = qinst;
     140                 :         32 :           break;
     141                 :            :         }
     142                 :            :       }
     143         [ +  - ]:         32 :       if (!topq.isNull())
     144                 :            :       {
     145 [ -  + ][ -  + ]:         32 :         Assert(topq.getKind() == Kind::FORALL);
                 [ -  - ]
     146         [ +  - ]:         64 :         Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
     147                 :         32 :                         << topq << std::endl;
     148                 :         32 :         std::vector<Node> insts;
     149                 :         32 :         qe->getInstantiations(topq, insts);
     150                 :            :         // note we do not convert to witness form here, since we could be
     151                 :            :         // an internal subsolver (SolverEngine::isInternalSubsolver).
     152                 :         32 :         ret = nm->mkAnd(insts);
     153         [ +  - ]:         32 :         Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
     154         [ +  + ]:         32 :         if (q.getKind() == Kind::EXISTS)
     155                 :            :         {
     156                 :         27 :           ret = rewrite(ret.negate());
     157                 :            :         }
     158                 :            :         // do extended rewrite to minimize the size of the formula aggressively
     159                 :         32 :         ret = extendedRewrite(ret);
     160                 :            :         // if we are not an internal subsolver, convert to witness form, since
     161                 :            :         // internally generated skolems should not escape
     162         [ +  + ]:         32 :         if (!isInternalSubsolver)
     163                 :            :         {
     164                 :         12 :           ret = SkolemManager::getOriginalForm(ret);
     165                 :            :         }
     166                 :            :         // make so that the returned formula does not involve arithmetic
     167                 :            :         // subtyping
     168                 :         32 :         SubtypeElimNodeConverter senc(nodeManager());
     169                 :         32 :         ret = senc.convert(ret);
     170                 :         32 :       }
     171                 :            :     }
     172                 :            :     // If we are closed, or the quantified formula was not instantiated in the
     173                 :            :     // subsolver, then we are a constant.
     174         [ +  + ]:         36 :     if (ret.isNull())
     175                 :            :     {
     176                 :          4 :       ret = nm->mkConst(polarity);
     177                 :            :     }
     178                 :         36 :     return ret;
     179                 :         36 :   }
     180                 :            :   // otherwise, just true/false
     181                 :        750 :   return nm->mkConst(!polarity);
     182                 :        411 : }
     183                 :            : 
     184                 :            : }  // namespace smt
     185                 :            : }  // namespace cvc5::internal