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