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                 :            :  * Info per quantified formula in instantiation evaluator.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/ieval/quant_info.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : using namespace cvc5::internal::kind;
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : namespace quantifiers {
      22                 :            : namespace ieval {
      23                 :            : 
      24                 :      68618 : QuantInfo::QuantInfo(context::Context* c)
      25                 :      68618 :     : d_isActive(c, true),
      26                 :      68618 :       d_maybeConflict(c, true),
      27                 :      68618 :       d_unassignedVars(c, 0),
      28                 :     137236 :       d_failReq(c)
      29                 :            : {
      30                 :      68618 : }
      31                 :            : 
      32                 :      68618 : void QuantInfo::initialize(TNode q, Node body)
      33                 :            : {
      34 [ -  + ][ -  + ]:      68618 :   Assert(q.getKind() == Kind::FORALL);
                 [ -  - ]
      35                 :      68618 :   d_quant = q;
      36                 :            : 
      37         [ +  - ]:     137236 :   Trace("ieval-quant-debug")
      38                 :      68618 :       << "Register quant " << d_quant.getId() << " : " << d_quant << std::endl;
      39                 :            : 
      40                 :            :   // canonize the body of the quantified formula
      41         [ +  - ]:      68618 :   Trace("ieval-quant-debug") << "Get body..." << std::endl;
      42                 :      68618 :   d_body = body;
      43                 :            : 
      44                 :            :   // compute matching requirements
      45         [ +  - ]:      68618 :   Trace("ieval-quant-debug") << "Compute constraints..." << std::endl;
      46                 :      68618 :   std::unordered_set<TNode> processed;
      47                 :      68618 :   std::unordered_set<TNode>::iterator itp;
      48                 :      68618 :   std::vector<TNode> visit;
      49                 :      68618 :   TNode cur;
      50                 :      68618 :   visit.push_back(d_body);
      51                 :            :   do
      52                 :            :   {
      53                 :     156965 :     cur = visit.back();
      54                 :     156965 :     visit.pop_back();
      55                 :     156965 :     itp = processed.find(cur);
      56         [ +  - ]:     156965 :     if (itp == processed.end())
      57                 :            :     {
      58                 :     156965 :       processed.insert(cur);
      59                 :            :       // process the match requirement for (disjunct) cur
      60                 :     156965 :       computeMatchReq(cur, visit);
      61                 :            :     }
      62         [ +  + ]:     156965 :   } while (!visit.empty());
      63                 :            : 
      64                 :      68618 :   d_unassignedVars = q[0].getNumChildren();
      65                 :            :   // debug print
      66 [ +  - ][ -  + ]:      68618 :   Trace("ieval-quant") << toStringDebug();
                 [ -  - ]
      67                 :      68618 : }
      68                 :            : 
      69                 :          0 : std::string QuantInfo::toStringDebug() const
      70                 :            : {
      71                 :          0 :   std::stringstream ss;
      72                 :          0 :   ss << "--- QuantInfo for " << d_quant.getId() << std::endl;
      73                 :          0 :   ss << "Body: " << d_body << std::endl;
      74                 :          0 :   ss << "Constraints:" << std::endl;
      75         [ -  - ]:          0 :   if (d_req.empty())
      76                 :            :   {
      77                 :          0 :     ss << "  (none)" << std::endl;
      78                 :            :   }
      79                 :            :   else
      80                 :            :   {
      81         [ -  - ]:          0 :     for (const std::pair<const TNode, bool>& r : d_req)
      82                 :            :     {
      83                 :          0 :       ss << "  " << r.first << " -> " << r.second << std::endl;
      84                 :            :     }
      85                 :            :   }
      86                 :          0 :   return ss.str();
      87                 :          0 : }
      88                 :            : 
      89                 :     156965 : void QuantInfo::computeMatchReq(TNode cur, std::vector<TNode>& visit)
      90                 :            : {
      91 [ -  + ][ -  + ]:     156965 :   Assert(cur.getType().isBoolean());
                 [ -  - ]
      92                 :     156965 :   bool pol = true;
      93                 :     156965 :   Kind k = cur.getKind();
      94 [ -  + ][ -  + ]:     156965 :   Assert(k != Kind::IMPLIES);
                 [ -  - ]
      95         [ +  + ]:     156965 :   if (k == Kind::OR)
      96                 :            :   {
      97                 :            :     // decompose OR
      98                 :      29413 :     visit.insert(visit.end(), cur.begin(), cur.end());
      99                 :      29413 :     return;
     100                 :            :   }
     101         [ +  + ]:     127552 :   else if (k == Kind::NOT)
     102                 :            :   {
     103                 :      55538 :     pol = false;
     104                 :      55538 :     cur = cur[0];
     105                 :      55538 :     k = cur.getKind();
     106                 :            :     // double negations should already be eliminated
     107 [ -  + ][ -  + ]:      55538 :     Assert(k != Kind::NOT);
                 [ -  - ]
     108                 :            :     // should be NNF
     109 [ -  + ][ -  + ]:      55538 :     Assert(k != Kind::AND);
                 [ -  - ]
     110                 :            :   }
     111                 :            :   // required to falsify
     112                 :     127552 :   d_req[cur] = !pol;
     113                 :            : }
     114                 :            : 
     115                 :    2062180 : const std::map<TNode, bool>& QuantInfo::getConstraints() const { return d_req; }
     116                 :            : 
     117                 :          0 : size_t QuantInfo::getNumUnassignedVars() const
     118                 :            : {
     119                 :          0 :   return d_unassignedVars.get();
     120                 :            : }
     121                 :            : 
     122                 :          0 : void QuantInfo::decrementUnassignedVar()
     123                 :            : {
     124                 :          0 :   d_unassignedVars = d_unassignedVars - 1;
     125                 :          0 : }
     126                 :            : 
     127                 :    7678731 : bool QuantInfo::isActive() const { return d_isActive.get(); }
     128                 :            : 
     129                 :    3017509 : void QuantInfo::setActive(bool val) { d_isActive = val; }
     130                 :            : 
     131                 :     864860 : void QuantInfo::setNoConflict() { d_maybeConflict = false; }
     132                 :            : 
     133                 :          0 : bool QuantInfo::isMaybeConflict() const { return d_maybeConflict.get(); }
     134                 :            : 
     135                 :    3017509 : void QuantInfo::setFailureConstraint(TNode c) { d_failReq = c; }
     136                 :            : 
     137                 :      73666 : TNode QuantInfo::getFailureConstraint() const { return d_failReq.get(); }
     138                 :            : 
     139                 :     846020 : bool QuantInfo::isTraverseTerm(TNode n) { return !n.isClosure(); }
     140                 :            : 
     141                 :            : }  // namespace ieval
     142                 :            : }  // namespace quantifiers
     143                 :            : }  // namespace theory
     144                 :            : }  // namespace cvc5::internal