src/theory/decision_strategy.cpp

   1 /*********************                                                        */
   2 /*! \file decision_strategy.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Implementation of base classes for decision strategies used by theory
  13  ** solvers for use in the DecisionManager of TheoryEngine.
  14  **/
  15
  16 #include "theory/decision_strategy.h"
  17
  18 #include "theory/rewriter.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24
  25 DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext,
  26                                          Valuation valuation)
  27     : d_valuation(valuation),
  28       d_has_curr_literal(false, satContext),
  29       d_curr_literal(0, satContext)
  30 {
  31 }
  32
  33 void DecisionStrategyFmf::initialize() { d_literals.clear(); }
  34
  35 Node DecisionStrategyFmf::getNextDecisionRequest()
  36 {
  37   Trace("dec-strategy-debug")
  38       << "Get next decision request " << identify() << "..." << std::endl;
  39   if (d_has_curr_literal.get())
  40   {
  41     Trace("dec-strategy-debug") << "...already has decision" << std::endl;
  42     return Node::null();
  43   }
  44   bool success;
  45   unsigned curr_lit = d_curr_literal.get();
  46   do
  47   {
  48     success = true;
  49     // get the current literal
  50     Node lit = getLiteral(curr_lit);
  51     Trace("dec-strategy-debug")
  52         << "...check literal #" << curr_lit << " : " << lit << std::endl;
  53     // if out of literals, we are done in the current SAT context
  54     if (!lit.isNull())
  55     {
  56       bool value;
  57       if (!d_valuation.hasSatValue(lit, value))
  58       {
  59         Trace("dec-strategy-debug") << "...not assigned, return." << std::endl;
  60         // if it has not been decided, return it
  61         return lit;
  62       }
  63       else if (!value)
  64       {
  65         Trace("dec-strategy-debug")
  66             << "...assigned false, increment." << std::endl;
  67         // asserted false, the current literal is incremented
  68         curr_lit = d_curr_literal.get() + 1;
  69         d_curr_literal.set(curr_lit);
  70         // repeat
  71         success = false;
  72       }
  73       else
  74       {
  75         Trace("dec-strategy-debug") << "...already assigned true." << std::endl;
  76       }
  77     }
  78     else
  79     {
  80       Trace("dec-strategy-debug") << "...exhausted literals." << std::endl;
  81     }
  82   } while (!success);
  83   // the current literal has been decided with the right polarity, we are done
  84   d_has_curr_literal = true;
  85   return Node::null();
  86 }
  87
  88 bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const
  89 {
  90   if (d_has_curr_literal.get())
  91   {
  92     i = d_curr_literal.get();
  93     return true;
  94   }
  95   return false;
  96 }
  97
  98 Node DecisionStrategyFmf::getAssertedLiteral()
  99 {
 100   if (d_has_curr_literal.get())
 101   {
 102     Assert(d_curr_literal.get() < d_literals.size());
 103     return getLiteral(d_curr_literal.get());
 104   }
 105   return Node::null();
 106 }
 107
 108 Node DecisionStrategyFmf::getLiteral(unsigned n)
 109 {
 110   // allocate until the index is valid
 111   while (n >= d_literals.size())
 112   {
 113     Node lit = mkLiteral(d_literals.size());
 114     if (!lit.isNull())
 115     {
 116       lit = Rewriter::rewrite(lit);
 117     }
 118     d_literals.push_back(lit);
 119   }
 120   Node ret = d_literals[n];
 121   if (!ret.isNull())
 122   {
 123     // always ensure it is in the CNF stream
 124     ret = d_valuation.ensureLiteral(ret);
 125   }
 126   return ret;
 127 }
 128
 129 DecisionStrategySingleton::DecisionStrategySingleton(
 130     const char* name,
 131     Node lit,
 132     context::Context* satContext,
 133     Valuation valuation)
 134     : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit)
 135 {
 136 }
 137
 138 Node DecisionStrategySingleton::mkLiteral(unsigned n)
 139 {
 140   if (n == 0)
 141   {
 142     return d_literal;
 143   }
 144   return Node::null();
 145 }
 146
 147 Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; }
 148
 149 }  // namespace theory
 150 }  // namespace CVC4