GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/decision_strategy.cpp Lines: 59 62 95.2 %
Date: 2021-03-23 Branches: 85 160 53.1 %

Line Exec Source
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-2021 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
6208
DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext,
26
6208
                                         Valuation valuation)
27
    : d_valuation(valuation),
28
      d_has_curr_literal(false, satContext),
29
6208
      d_curr_literal(0, satContext)
30
{
31
6208
}
32
33
4639
void DecisionStrategyFmf::initialize() { d_literals.clear(); }
34
35
2387245
Node DecisionStrategyFmf::getNextDecisionRequest()
36
{
37
4774490
  Trace("dec-strategy-debug")
38
2387245
      << "Get next decision request " << identify() << "..." << std::endl;
39
2387245
  if (d_has_curr_literal.get())
40
  {
41
2303873
    Trace("dec-strategy-debug") << "...already has decision" << std::endl;
42
2303873
    return Node::null();
43
  }
44
  bool success;
45
83372
  unsigned curr_lit = d_curr_literal.get();
46
34501
  do
47
  {
48
117873
    success = true;
49
    // get the current literal
50
194102
    Node lit = getLiteral(curr_lit);
51
235738
    Trace("dec-strategy-debug")
52
117869
        << "...check literal #" << curr_lit << " : " << lit << std::endl;
53
    // if out of literals, we are done in the current SAT context
54
117869
    if (!lit.isNull())
55
    {
56
      bool value;
57
115504
      if (!d_valuation.hasSatValue(lit, value))
58
      {
59
41640
        Trace("dec-strategy-debug") << "...not assigned, return." << std::endl;
60
        // if it has not been decided, return it
61
41640
        return lit;
62
      }
63
73864
      else if (!value)
64
      {
65
69002
        Trace("dec-strategy-debug")
66
34501
            << "...assigned false, increment." << std::endl;
67
        // asserted false, the current literal is incremented
68
34501
        curr_lit = d_curr_literal.get() + 1;
69
34501
        d_curr_literal.set(curr_lit);
70
        // repeat
71
34501
        success = false;
72
      }
73
      else
74
      {
75
39363
        Trace("dec-strategy-debug") << "...already assigned true." << std::endl;
76
      }
77
    }
78
    else
79
    {
80
2365
      Trace("dec-strategy-debug") << "...exhausted literals." << std::endl;
81
    }
82
76229
  } while (!success);
83
  // the current literal has been decided with the right polarity, we are done
84
41728
  d_has_curr_literal = true;
85
41728
  return Node::null();
86
}
87
88
7044
bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const
89
{
90
7044
  if (d_has_curr_literal.get())
91
  {
92
7044
    i = d_curr_literal.get();
93
7044
    return true;
94
  }
95
  return false;
96
}
97
98
2982
Node DecisionStrategyFmf::getAssertedLiteral()
99
{
100
2982
  if (d_has_curr_literal.get())
101
  {
102
2982
    Assert(d_curr_literal.get() < d_literals.size());
103
2982
    return getLiteral(d_curr_literal.get());
104
  }
105
  return Node::null();
106
}
107
108
129682
Node DecisionStrategyFmf::getLiteral(unsigned n)
109
{
110
  // allocate until the index is valid
111
136858
  while (n >= d_literals.size())
112
  {
113
14356
    Node lit = mkLiteral(d_literals.size());
114
7176
    if (!lit.isNull())
115
    {
116
6445
      lit = Rewriter::rewrite(lit);
117
    }
118
7176
    d_literals.push_back(lit);
119
  }
120
122502
  Node ret = d_literals[n];
121
122502
  if (!ret.isNull())
122
  {
123
    // always ensure it is in the CNF stream
124
120137
    ret = d_valuation.ensureLiteral(ret);
125
  }
126
122502
  return ret;
127
}
128
129
2540
DecisionStrategySingleton::DecisionStrategySingleton(
130
    const char* name,
131
    Node lit,
132
    context::Context* satContext,
133
2540
    Valuation valuation)
134
2540
    : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit)
135
{
136
2540
}
137
138
3165
Node DecisionStrategySingleton::mkLiteral(unsigned n)
139
{
140
3165
  if (n == 0)
141
  {
142
2434
    return d_literal;
143
  }
144
731
  return Node::null();
145
}
146
147
Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; }
148
149
}  // namespace theory
150
26685
}  // namespace CVC4