Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Andres Noetzli, 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                 :            :  * Implementation of base classes for decision strategies used by theory
      14                 :            :  * solvers for use in the DecisionManager of TheoryEngine.
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "theory/decision_strategy.h"
      18                 :            : 
      19                 :            : #include "theory/rewriter.h"
      20                 :            : 
      21                 :            : using namespace cvc5::internal::kind;
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace theory {
      25                 :            : 
      26                 :      16414 : DecisionStrategyFmf::DecisionStrategyFmf(Env& env, Valuation valuation)
      27                 :            :     : DecisionStrategy(env),
      28                 :            :       d_valuation(valuation),
      29                 :          0 :       d_has_curr_literal(context(), false),
      30                 :      16414 :       d_curr_literal(context(), 0)
      31                 :            : {
      32                 :      16414 : }
      33                 :            : 
      34                 :       9984 : void DecisionStrategyFmf::initialize() { d_literals.clear(); }
      35                 :            : 
      36                 :    6949320 : Node DecisionStrategyFmf::getNextDecisionRequest()
      37                 :            : {
      38         [ +  - ]:   13898600 :   Trace("dec-strategy-debug")
      39 [ -  + ][ -  - ]:    6949320 :       << "Get next decision request " << identify() << "..." << std::endl;
      40         [ +  + ]:    6949320 :   if (d_has_curr_literal.get())
      41                 :            :   {
      42         [ +  - ]:    6254210 :     Trace("dec-strategy-debug") << "...already has decision" << std::endl;
      43                 :    6254210 :     return Node::null();
      44                 :            :   }
      45                 :            :   bool success;
      46                 :     695114 :   unsigned curr_lit = d_curr_literal.get();
      47                 :      72985 :   do
      48                 :            :   {
      49                 :     768099 :     success = true;
      50                 :            :     // get the current literal
      51                 :     768099 :     Node lit = getLiteral(curr_lit);
      52         [ +  - ]:    1536190 :     Trace("dec-strategy-debug")
      53                 :     768095 :         << "...check literal #" << curr_lit << " : " << lit << std::endl;
      54                 :            :     // if out of literals, we are done in the current SAT context
      55         [ +  + ]:     768095 :     if (!lit.isNull())
      56                 :            :     {
      57                 :            :       bool value;
      58         [ +  + ]:     240429 :       if (!d_valuation.hasSatValue(lit, value))
      59                 :            :       {
      60         [ +  - ]:      83357 :         Trace("dec-strategy-debug") << "...not assigned, return." << std::endl;
      61                 :            :         // if it has not been decided, return it
      62                 :      83357 :         return lit;
      63                 :            :       }
      64         [ +  + ]:     157072 :       else if (!value)
      65                 :            :       {
      66         [ +  - ]:     145970 :         Trace("dec-strategy-debug")
      67                 :      72985 :             << "...assigned false, increment." << std::endl;
      68                 :            :         // asserted false, the current literal is incremented
      69                 :      72985 :         curr_lit = d_curr_literal.get() + 1;
      70                 :      72985 :         d_curr_literal.set(curr_lit);
      71                 :            :         // repeat
      72                 :      72985 :         success = false;
      73                 :            :       }
      74                 :            :       else
      75                 :            :       {
      76         [ +  - ]:      84087 :         Trace("dec-strategy-debug") << "...already assigned true." << std::endl;
      77                 :            :         // the current literal has been decided with the right polarity, we are
      78                 :            :         // done
      79                 :      84087 :         d_has_curr_literal = true;
      80                 :            :       }
      81                 :            :     }
      82                 :            :     else
      83                 :            :     {
      84         [ +  - ]:     527666 :       Trace("dec-strategy-debug") << "...exhausted literals." << std::endl;
      85                 :            :     }
      86         [ +  + ]:     684738 :   } while (!success);
      87                 :     611753 :   return Node::null();
      88                 :            : }
      89                 :            : 
      90                 :      13625 : bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const
      91                 :            : {
      92         [ +  + ]:      13625 :   if (d_has_curr_literal.get())
      93                 :            :   {
      94                 :      13623 :     i = d_curr_literal.get();
      95                 :      13623 :     return true;
      96                 :            :   }
      97                 :          2 :   return false;
      98                 :            : }
      99                 :            : 
     100                 :       5054 : Node DecisionStrategyFmf::getAssertedLiteral()
     101                 :            : {
     102         [ +  - ]:       5054 :   if (d_has_curr_literal.get())
     103                 :            :   {
     104 [ -  + ][ -  + ]:       5054 :     Assert(d_curr_literal.get() < d_literals.size());
                 [ -  - ]
     105                 :       5054 :     return getLiteral(d_curr_literal.get());
     106                 :            :   }
     107                 :          0 :   return Node::null();
     108                 :            : }
     109                 :            : 
     110                 :     790131 : Node DecisionStrategyFmf::getLiteral(unsigned n)
     111                 :            : {
     112                 :            :   // allocate until the index is valid
     113         [ +  + ]:     790131 :   while (n >= d_literals.size())
     114                 :            :   {
     115                 :     541617 :     Node lit = mkLiteral(d_literals.size());
     116         [ +  + ]:     541613 :     if (lit.isNull())
     117                 :            :     {
     118                 :            :       // literal is not ready yet, return null
     119                 :            :       // note we assume that mkLiteral is dynamic here.
     120                 :     527666 :       return lit;
     121                 :            :     }
     122                 :      13947 :     lit = rewrite(lit);
     123                 :      13947 :     d_literals.push_back(lit);
     124                 :            :   }
     125                 :     248514 :   Node ret = d_literals[n];
     126                 :            :   // always ensure it is in the CNF stream
     127                 :     248514 :   return d_valuation.ensureLiteral(ret);
     128                 :            : }
     129                 :            : 
     130                 :       5284 : DecisionStrategySingleton::DecisionStrategySingleton(Env& env,
     131                 :            :                                                      const char* name,
     132                 :            :                                                      Node lit,
     133                 :       5284 :                                                      Valuation valuation)
     134                 :       5284 :     : DecisionStrategyFmf(env, valuation), d_name(name), d_literal(lit)
     135                 :            : {
     136                 :       5284 : }
     137                 :            : 
     138                 :     531735 : Node DecisionStrategySingleton::mkLiteral(unsigned n)
     139                 :            : {
     140         [ +  + ]:     531735 :   if (n == 0)
     141                 :            :   {
     142                 :       5144 :     return d_literal;
     143                 :            :   }
     144                 :     526591 :   return Node::null();
     145                 :            : }
     146                 :            : 
     147                 :          0 : Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; }
     148                 :            : 
     149                 :        535 : DecisionStrategyVector::DecisionStrategyVector(Env& env,
     150                 :            :                                                const char* name,
     151                 :        535 :                                                Valuation valuation)
     152                 :        535 :     : DecisionStrategyFmf(env, valuation), d_name(name)
     153                 :            : {
     154                 :        535 : }
     155                 :            : 
     156                 :       1931 : Node DecisionStrategyVector::mkLiteral(unsigned n)
     157                 :            : {
     158         [ +  + ]:       1931 :   if (n < d_literals.size())
     159                 :            :   {
     160                 :        856 :     return d_literals[n];
     161                 :            :   }
     162                 :       1075 :   return Node::null();
     163                 :            : }
     164                 :            : 
     165                 :       1073 : void DecisionStrategyVector::addLiteral(const Node& n)
     166                 :            : {
     167                 :       1073 :   d_literals.push_back(n);
     168                 :       1073 : }
     169                 :            : 
     170                 :            : }  // namespace theory
     171                 :            : }  // namespace cvc5::internal