Branch data     Line data    Source code

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