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                 :            :  * A cache to remember what is justified
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "decision/justify_cache.h"
      17                 :            : 
      18                 :            : #include "expr/node_algorithm.h"
      19                 :            : 
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : using namespace cvc5::internal::prop;
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace decision {
      25                 :            : 
      26                 :      41566 : JustifyCache::JustifyCache(context::Context* c,
      27                 :            :                            prop::CDCLTSatSolver* ss,
      28                 :      41566 :                            prop::CnfStream* cs)
      29                 :      41566 :     : d_justified(c), d_satSolver(ss), d_cnfStream(cs)
      30                 :            : {
      31                 :      41566 : }
      32                 :            : 
      33                 :  213500000 : prop::SatValue JustifyCache::lookupValue(TNode n)
      34                 :            : {
      35                 :  213500000 :   bool pol = n.getKind() != Kind::NOT;
      36         [ +  + ]:  427001000 :   TNode atom = pol ? n : n[0];
      37 [ -  + ][ -  + ]:  213500000 :   Assert(atom.getKind() != Kind::NOT);
                 [ -  - ]
      38                 :            :   // check if we have already determined the value
      39                 :            :   // notice that d_justified may contain nodes that are not assigned SAT values,
      40                 :            :   // since this class infers when the value of nodes can be determined.
      41                 :  213500000 :   auto jit = d_justified.find(atom);
      42         [ +  + ]:  213500000 :   if (jit != d_justified.end())
      43                 :            :   {
      44         [ +  + ]:   95439900 :     return pol ? jit->second : invertValue(jit->second);
      45                 :            :   }
      46                 :            :   // Notice that looking up values for non-theory atoms may lead to
      47                 :            :   // an incomplete strategy where a formula is asserted but not justified
      48                 :            :   // via its theory literal subterms. This is the case because the justification
      49                 :            :   // heuristic is not the only source of decisions, as the theory may request
      50                 :            :   // them.
      51         [ +  + ]:  118061000 :   if (expr::isTheoryAtom(atom))
      52                 :            :   {
      53                 :   54852800 :     SatLiteral nsl = d_cnfStream->getLiteral(atom);
      54                 :   54852800 :     prop::SatValue val = d_satSolver->value(nsl);
      55         [ +  + ]:   54852800 :     if (val != SAT_VALUE_UNKNOWN)
      56                 :            :     {
      57                 :            :       // this is the moment where we realize a skolem definition is relevant,
      58                 :            :       // add now.
      59                 :            :       // NOTE: if we enable skolems when they are justified, we could call
      60                 :            :       // a method notifyJustified(atom) here
      61                 :   29719800 :       d_justified.insert(atom, val);
      62         [ +  + ]:   29719800 :       return pol ? val : invertValue(val);
      63                 :            :     }
      64                 :            :   }
      65                 :   88340700 :   return SAT_VALUE_UNKNOWN;
      66                 :            : }
      67                 :            : 
      68                 :          0 : bool JustifyCache::hasValue(TNode n) const
      69                 :            : {
      70                 :          0 :   return d_justified.find(n) != d_justified.end();
      71                 :            : }
      72                 :            : 
      73                 :   44366000 : void JustifyCache::setValue(const Node& n, prop::SatValue value)
      74                 :            : {
      75                 :   44366000 :   d_justified.insert(n, value);
      76                 :   44366000 : }
      77                 :            : 
      78                 :            : }  // namespace decision
      79                 :            : }  // namespace cvc5::internal