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                 :            :  * Implementation of base classes for decision strategies used by theory
      11                 :            :  * solvers for use in the DecisionManager of TheoryEngine.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "theory/decision_strategy.h"
      15                 :            : 
      16                 :            : #include "theory/rewriter.h"
      17                 :            : 
      18                 :            : using namespace cvc5::internal::kind;
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : 
      23                 :      10910 : DecisionStrategyFmf::DecisionStrategyFmf(Env& env, Valuation valuation)
      24                 :            :     : DecisionStrategy(env),
      25                 :      10910 :       d_valuation(valuation),
      26                 :      10910 :       d_has_curr_literal(context(), false),
      27                 :      21820 :       d_curr_literal(context(), 0)
      28                 :            : {
      29                 :      10910 : }
      30                 :            : 
      31                 :       7821 : void DecisionStrategyFmf::initialize() { d_literals.clear(); }
      32                 :            : 
      33                 :    2883888 : Node DecisionStrategyFmf::getNextDecisionRequest()
      34                 :            : {
      35         [ +  - ]:    5767776 :   Trace("dec-strategy-debug")
      36 [ -  + ][ -  - ]:    2883888 :       << "Get next decision request " << identify() << "..." << std::endl;
      37         [ +  + ]:    2883888 :   if (d_has_curr_literal.get())
      38                 :            :   {
      39         [ +  - ]:    2486621 :     Trace("dec-strategy-debug") << "...already has decision" << std::endl;
      40                 :    2486621 :     return Node::null();
      41                 :            :   }
      42                 :            :   bool success;
      43                 :     397267 :   unsigned curr_lit = d_curr_literal.get();
      44                 :            :   do
      45                 :            :   {
      46                 :     451807 :     success = true;
      47                 :            :     // get the current literal
      48                 :     451807 :     Node lit = getLiteral(curr_lit);
      49         [ +  - ]:     903606 :     Trace("dec-strategy-debug")
      50                 :     451803 :         << "...check literal #" << curr_lit << " : " << lit << std::endl;
      51                 :            :     // if out of literals, we are done in the current SAT context
      52         [ +  + ]:     451803 :     if (!lit.isNull())
      53                 :            :     {
      54                 :            :       bool value;
      55         [ +  + ]:     197565 :       if (!d_valuation.hasSatValue(lit, value))
      56                 :            :       {
      57         [ +  - ]:      72044 :         Trace("dec-strategy-debug") << "...not assigned, return." << std::endl;
      58                 :            :         // if it has not been decided, return it
      59                 :      72044 :         return lit;
      60                 :            :       }
      61         [ +  + ]:     125521 :       else if (!value)
      62                 :            :       {
      63         [ +  - ]:     109080 :         Trace("dec-strategy-debug")
      64                 :      54540 :             << "...assigned false, increment." << std::endl;
      65                 :            :         // asserted false, the current literal is incremented
      66                 :      54540 :         curr_lit = d_curr_literal.get() + 1;
      67                 :      54540 :         d_curr_literal.set(curr_lit);
      68                 :            :         // repeat
      69                 :      54540 :         success = false;
      70                 :            :       }
      71                 :            :       else
      72                 :            :       {
      73         [ +  - ]:      70981 :         Trace("dec-strategy-debug") << "...already assigned true." << std::endl;
      74                 :            :         // the current literal has been decided with the right polarity, we are
      75                 :            :         // done
      76                 :      70981 :         d_has_curr_literal = true;
      77                 :            :       }
      78                 :            :     }
      79                 :            :     else
      80                 :            :     {
      81         [ +  - ]:     254238 :       Trace("dec-strategy-debug") << "...exhausted literals." << std::endl;
      82                 :            :     }
      83 [ +  + ][ +  + ]:     831562 :   } while (!success);
      84                 :     325219 :   return Node::null();
      85                 :            : }
      86                 :            : 
      87                 :      13966 : bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const
      88                 :            : {
      89         [ +  - ]:      13966 :   if (d_has_curr_literal.get())
      90                 :            :   {
      91                 :      13966 :     i = d_curr_literal.get();
      92                 :      13966 :     return true;
      93                 :            :   }
      94                 :          0 :   return false;
      95                 :            : }
      96                 :            : 
      97                 :       5264 : Node DecisionStrategyFmf::getAssertedLiteral()
      98                 :            : {
      99         [ +  - ]:       5264 :   if (d_has_curr_literal.get())
     100                 :            :   {
     101 [ -  + ][ -  + ]:       5264 :     Assert(d_curr_literal.get() < d_literals.size());
                 [ -  - ]
     102                 :       5264 :     return getLiteral(d_curr_literal.get());
     103                 :            :   }
     104                 :          0 :   return Node::null();
     105                 :            : }
     106                 :            : 
     107                 :     460009 : Node DecisionStrategyFmf::getLiteral(unsigned n)
     108                 :            : {
     109                 :            :   // allocate until the index is valid
     110         [ +  + ]:     471249 :   while (n >= d_literals.size())
     111                 :            :   {
     112                 :     265482 :     Node lit = mkLiteral(d_literals.size());
     113         [ +  + ]:     265478 :     if (lit.isNull())
     114                 :            :     {
     115                 :            :       // literal is not ready yet, return null
     116                 :            :       // note we assume that mkLiteral is dynamic here.
     117                 :     254238 :       return lit;
     118                 :            :     }
     119                 :      11240 :     lit = rewrite(lit);
     120                 :      11240 :     d_literals.push_back(lit);
     121         [ +  + ]:     265478 :   }
     122                 :     205767 :   Node ret = d_literals[n];
     123                 :            :   // always ensure it is in the CNF stream
     124                 :     205767 :   return d_valuation.ensureLiteral(ret);
     125                 :     205767 : }
     126                 :            : 
     127                 :       4248 : DecisionStrategySingleton::DecisionStrategySingleton(Env& env,
     128                 :            :                                                      const char* name,
     129                 :            :                                                      Node lit,
     130                 :       4248 :                                                      Valuation valuation)
     131                 :       4248 :     : DecisionStrategyFmf(env, valuation), d_name(name), d_literal(lit)
     132                 :            : {
     133                 :       4248 : }
     134                 :            : 
     135                 :     258348 : Node DecisionStrategySingleton::mkLiteral(unsigned n)
     136                 :            : {
     137         [ +  + ]:     258348 :   if (n == 0)
     138                 :            :   {
     139                 :       4132 :     return d_literal;
     140                 :            :   }
     141                 :     254216 :   return Node::null();
     142                 :            : }
     143                 :            : 
     144                 :          0 : Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; }
     145                 :            : 
     146                 :          9 : DecisionStrategyVector::DecisionStrategyVector(Env& env,
     147                 :            :                                                const char* name,
     148                 :          9 :                                                Valuation valuation)
     149                 :          9 :     : DecisionStrategyFmf(env, valuation), d_name(name)
     150                 :            : {
     151                 :          9 : }
     152                 :            : 
     153                 :         38 : Node DecisionStrategyVector::mkLiteral(unsigned n)
     154                 :            : {
     155         [ +  + ]:         38 :   if (n < d_literals.size())
     156                 :            :   {
     157                 :         16 :     return d_literals[n];
     158                 :            :   }
     159                 :         22 :   return Node::null();
     160                 :            : }
     161                 :            : 
     162                 :         20 : void DecisionStrategyVector::addLiteral(const Node& n)
     163                 :            : {
     164                 :         20 :   d_literals.push_back(n);
     165                 :         20 : }
     166                 :            : 
     167                 :            : }  // namespace theory
     168                 :            : }  // namespace cvc5::internal