GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/decision/justification_heuristic.h Lines: 0 3 0.0 %
Date: 2021-03-23 Branches: 0 6 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file justification_heuristic.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Gereon Kremer, Andres Noetzli
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 Justification heuristic for decision making
13
 **
14
 ** A ATGP-inspired justification-based decision heuristic. See
15
 ** [insert reference] for more details. This code is, or not, based
16
 ** on the CVC3 implementation of the same heuristic.
17
 **
18
 ** It needs access to the simplified but non-clausal formula.
19
 **/
20
21
#include "cvc4_private.h"
22
23
#ifndef CVC4__DECISION__JUSTIFICATION_HEURISTIC
24
#define CVC4__DECISION__JUSTIFICATION_HEURISTIC
25
26
#include <unordered_set>
27
#include <utility>
28
29
#include "context/cdhashmap.h"
30
#include "context/cdhashset.h"
31
#include "context/cdlist.h"
32
#include "context/cdo.h"
33
#include "decision/decision_strategy.h"
34
#include "expr/node.h"
35
#include "options/decision_weight.h"
36
#include "prop/sat_solver_types.h"
37
#include "util/statistics_registry.h"
38
#include "util/stats_timer.h"
39
40
namespace CVC4 {
41
namespace decision {
42
43
class JustificationHeuristic : public ITEDecisionStrategy {
44
  //                   TRUE           FALSE         MEH
45
  enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
46
47
  typedef std::vector<std::pair<Node, Node> > SkolemList;
48
  typedef context::CDHashMap<Node, SkolemList, NodeHashFunction> SkolemCache;
49
  typedef std::vector<Node> ChildList;
50
  typedef context::
51
      CDHashMap<Node, std::pair<ChildList, ChildList>, NodeHashFunction>
52
          ChildCache;
53
  typedef context::CDHashMap<Node,Node,NodeHashFunction> SkolemMap;
54
  typedef context::CDHashMap<Node,
55
                             std::pair<DecisionWeight, DecisionWeight>,
56
                             NodeHashFunction>
57
      WeightCache;
58
59
  // being 'justified' is monotonic with respect to decisions
60
  typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
61
  JustifiedSet d_justified;
62
  typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold;
63
  ExploredThreshold d_exploredThreshold;
64
  context::CDO<unsigned>  d_prvsIndex;
65
  context::CDO<unsigned>  d_threshPrvsIndex;
66
67
  IntStat d_helpfulness;
68
  IntStat d_giveup;
69
  TimerStat d_timestat;
70
71
  /**
72
   * A copy of the assertions that need to be justified
73
   * directly. Doesn't have ones introduced during during term removal.
74
   */
75
  context::CDList<Node> d_assertions;
76
77
  /** map from skolems introduced in term removal to the corresponding assertion
78
   */
79
  SkolemMap d_skolemAssertions;
80
81
  /** Cache for skolems present in a atomic formula */
82
  SkolemCache d_skolemCache;
83
84
  /**
85
   * This is used to prevent infinite loop when trying to find a
86
   * splitter. Can happen when exploring assertion corresponding to a
87
   * term-ITE.
88
   */
89
  std::unordered_set<Node,NodeHashFunction> d_visited;
90
91
  /**
92
   * Set to track visited nodes in a dfs search done in computeSkolems
93
   * function
94
   */
95
  std::unordered_set<Node, NodeHashFunction> d_visitedComputeSkolems;
96
97
  /** current decision for the recursive call */
98
  prop::SatLiteral d_curDecision;
99
  /** current threshold for the recursive call */
100
  DecisionWeight d_curThreshold;
101
102
  /** child cache */
103
  ChildCache d_childCache;
104
105
  /** computed polarized weight cache */
106
  WeightCache d_weightCache;
107
108
109
  class myCompareClass {
110
    JustificationHeuristic* d_jh;
111
    bool d_b;
112
  public:
113
    myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {};
114
    bool operator() (TNode n1, TNode n2) {
115
      return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b);
116
    }
117
  };
118
119
public:
120
  JustificationHeuristic(CVC4::DecisionEngine* de,
121
                         context::UserContext *uc,
122
                         context::Context *c);
123
124
  ~JustificationHeuristic();
125
126
  prop::SatLiteral getNext(bool &stopSearch) override;
127
128
  /**
129
   * Notify this class that assertion is an (input) assertion, not corresponding
130
   * to a skolem definition.
131
   */
132
  void addAssertion(TNode assertion) override;
133
  /**
134
   * Notify this class  that lem is the skolem definition for skolem, which is
135
   * a part of the current assertions.
136
   */
137
  void addSkolemDefinition(TNode lem, TNode skolem) override;
138
139
 private:
140
  /* getNext with an option to specify threshold */
141
  prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
142
143
  prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal);
144
145
  /**
146
   * Do all the hard work.
147
   */
148
  SearchResult findSplitterRec(TNode node, prop::SatValue value);
149
150
  /* Helper functions */
151
  void setJustified(TNode);
152
  bool checkJustified(TNode);
153
  DecisionWeight getExploredThreshold(TNode);
154
  void setExploredThreshold(TNode);
155
  void setPrvsIndex(int);
156
  int  getPrvsIndex();
157
  DecisionWeight getWeightPolarized(TNode n, bool polarity);
158
  DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
159
  static DecisionWeight getWeight(TNode);
160
  bool compareByWeightFalse(TNode, TNode);
161
  bool compareByWeightTrue(TNode, TNode);
162
  TNode getChildByWeight(TNode n, int i, bool polarity);
163
164
  /* If literal exists corresponding to the node return
165
     that. Otherwise an UNKNOWN */
166
  prop::SatValue tryGetSatValue(Node n);
167
168
  /* Get list of all term-ITEs for the atomic formula v */
169
  JustificationHeuristic::SkolemList getSkolems(TNode n);
170
171
  /**
172
   * For big and/or nodes, a cache to save starting index into children
173
   * for efficiently.
174
   */
175
  typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
176
  StartIndexCache d_startIndexCache;
177
  int getStartIndex(TNode node);
178
  void saveStartIndex(TNode node, int val);
179
180
  /* Compute all term-removal skolems in a node recursively */
181
  void computeSkolems(TNode n, SkolemList& l);
182
183
  SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal);
184
  SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal);
185
  SearchResult handleBinaryEasy(TNode node1,
186
                                prop::SatValue desiredVal1,
187
                                TNode node2,
188
                                prop::SatValue desiredVal2);
189
  SearchResult handleBinaryHard(TNode node1,
190
                                prop::SatValue desiredVal1,
191
                                TNode node2,
192
                                prop::SatValue desiredVal2);
193
  SearchResult handleITE(TNode node, prop::SatValue desiredVal);
194
  SearchResult handleEmbeddedSkolems(TNode node);
195
};/* class JustificationHeuristic */
196
197
}/* namespace decision */
198
}/* namespace CVC4 */
199
200
#endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */