GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/decision_strategy.h Lines: 5 5 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file decision_strategy.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 Base classes for decision strategies used by theory solvers
13
 ** for use in the DecisionManager of TheoryEngine.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__DECISION_STRATEGY__H
19
#define CVC4__THEORY__DECISION_STRATEGY__H
20
21
#include "context/cdo.h"
22
#include "expr/node.h"
23
#include "theory/valuation.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
/**
29
 * Virtual base class for decision strategies.
30
 */
31
class DecisionStrategy
32
{
33
 public:
34
15201
  DecisionStrategy() {}
35
15196
  virtual ~DecisionStrategy() {}
36
  /**
37
   * Initalize this strategy, This is called once per satisfiability call by
38
   * the DecisionManager, prior to using this strategy.
39
   */
40
  virtual void initialize() = 0;
41
  /**
42
   * If this method returns a non-null node n, then n is the required next
43
   * decision of this strategy. It must be the case that n is a literal in
44
   * the current CNF stream.
45
   */
46
  virtual Node getNextDecisionRequest() = 0;
47
  /** identify this strategy (for debugging) */
48
  virtual std::string identify() const = 0;
49
};
50
51
/**
52
 * Decision strategy finite model finding.
53
 *
54
 * This is a virtual base class for decision strategies that follow the
55
 * "finite model finding" pattern for decisions. Such strategies have the
56
 * distinguishing feature that they are interested in a stream of literals
57
 * L_1, L_2, L_3, ... and so on. At any given time, they request that L_i is
58
 * asserted true for a minimal i.
59
 *
60
 * To enforce this strategy, this class maintains a SAT-context dependent
61
 * index d_curr_literal, which corresponds to the minimal index of a literal
62
 * in the above list that is not asserted false. A call to
63
 * getNextDecisionRequest increments this value until we find a literal L_j
64
 * that is not assigned false. If L_j is unassigned, we return it as a decision,
65
 * otherwise we return no decisions.
66
 */
67
class DecisionStrategyFmf : public DecisionStrategy
68
{
69
 public:
70
  DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
71
6204
  virtual ~DecisionStrategyFmf() {}
72
  /** initialize */
73
  void initialize() override;
74
  /** get next decision request */
75
  Node getNextDecisionRequest() override;
76
  /** Make the n^th literal of this strategy */
77
  virtual Node mkLiteral(unsigned n) = 0;
78
  /**
79
   * This method returns true iff there exists a (minimal) i such that L_i
80
   * is a literal allocated by this class, and is asserted true in the current
81
   * context. If it returns true, the argument i is set to this i.
82
   */
83
  bool getAssertedLiteralIndex(unsigned& i) const;
84
  /**
85
   * This method returns the literal L_i allocated by this class that
86
   * has been asserted true in the current context and is such that i is
87
   * minimal. It returns null if no such literals exist.
88
   */
89
  Node getAssertedLiteral();
90
  /** Get the n^th literal of this strategy */
91
  Node getLiteral(unsigned lit);
92
93
 protected:
94
  /**
95
   * The valuation of this class, used for knowing what literals are asserted,
96
   * and with what polarity.
97
   */
98
  Valuation d_valuation;
99
  /**
100
   * The (SAT-context-dependent) flag that is true if there exists a literal
101
   * of this class that is asserted true in the current context, according to
102
   * d_valuation.
103
   */
104
  context::CDO<bool> d_has_curr_literal;
105
  /**
106
   * The (SAT-context-dependent) index of the current literal of this strategy.
107
   * This corresponds to the first literal that is not asserted false in the
108
   * current context, according to d_valuation.
109
   */
110
  context::CDO<unsigned> d_curr_literal;
111
  /** the list of literals of this strategy */
112
  std::vector<Node> d_literals;
113
};
114
115
/**
116
 * Special case of above where we only wish to allocate a single literal L_1.
117
 */
118
5080
class DecisionStrategySingleton : public DecisionStrategyFmf
119
{
120
 public:
121
  DecisionStrategySingleton(const char* name,
122
                            Node lit,
123
                            context::Context* satContext,
124
                            Valuation valuation);
125
  /**
126
   * Make the n^th literal of this strategy. This method returns d_literal if
127
   * n=0, null otherwise.
128
   */
129
  Node mkLiteral(unsigned n) override;
130
  /** Get single literal */
131
  Node getSingleLiteral();
132
  /** identify */
133
1964750
  std::string identify() const override { return d_name; }
134
135
 private:
136
  /** the name of this strategy */
137
  std::string d_name;
138
  /** the literal to decide on */
139
  Node d_literal;
140
};
141
142
}  // namespace theory
143
}  // namespace CVC4
144
145
#endif /* CVC4__THEORY__DECISION_STRATEGY__H */