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

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_core.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Liana Hadarean, 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 Algebraic solver.
13
 **
14
 ** Algebraic solver.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#pragma once
20
21
#include <unordered_map>
22
#include <unordered_set>
23
24
#include "context/cdhashset.h"
25
#include "theory/bv/bv_subtheory.h"
26
#include "theory/ext_theory.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace bv {
31
32
class Base;
33
34
/** An extended theory callback used by the core solver */
35
8949
class CoreSolverExtTheoryCallback : public ExtTheoryCallback
36
{
37
 public:
38
8952
  CoreSolverExtTheoryCallback() : d_equalityEngine(nullptr) {}
39
  /** Get current substitution based on the underlying equality engine. */
40
  bool getCurrentSubstitution(int effort,
41
                              const std::vector<Node>& vars,
42
                              std::vector<Node>& subs,
43
                              std::map<Node, std::vector<Node> >& exp) override;
44
  /** Get reduction. */
45
  bool getReduction(int effort, Node n, Node& nr, bool& satDep) override;
46
  /** The underlying equality engine */
47
  eq::EqualityEngine* d_equalityEngine;
48
};
49
50
/**
51
 * Bitvector equality solver
52
 */
53
class CoreSolver : public SubtheorySolver {
54
  typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
55
  typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
56
  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
57
58
59
  struct Statistics {
60
    IntStat d_numCallstoCheck;
61
    Statistics();
62
    ~Statistics();
63
  };
64
65
  // NotifyClass: handles call-back from congruence closure module
66
8949
  class NotifyClass : public eq::EqualityEngineNotify {
67
    CoreSolver& d_solver;
68
69
  public:
70
8952
    NotifyClass(CoreSolver& solver): d_solver(solver) {}
71
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
72
    bool eqNotifyTriggerTermEquality(TheoryId tag,
73
                                     TNode t1,
74
                                     TNode t2,
75
                                     bool value) override;
76
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
77
177727
    void eqNotifyNewClass(TNode t) override {}
78
1182169
    void eqNotifyMerge(TNode t1, TNode t2) override {}
79
152520
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
80
  };
81
82
83
  /** The notify class for d_equalityEngine */
84
  NotifyClass d_notify;
85
86
  /** Store a propagation to the bv solver */
87
  bool storePropagation(TNode literal);
88
89
  /** Store a conflict from merging two constants */
90
  void conflict(TNode a, TNode b);
91
92
  context::CDO<bool> d_isComplete;
93
  unsigned d_lemmaThreshold;
94
95
  bool d_preregisterCalled;
96
  bool d_checkCalled;
97
98
  /** Pointer to the parent theory solver that owns this */
99
  BVSolverLazy* d_bv;
100
  /** Pointer to the equality engine of the parent */
101
  eq::EqualityEngine* d_equalityEngine;
102
  /** The extended theory callback */
103
  CoreSolverExtTheoryCallback d_extTheoryCb;
104
  /** Extended theory module, for context-dependent simplification. */
105
  std::unique_ptr<ExtTheory> d_extTheory;
106
107
  /** To make sure we keep the explanations */
108
  context::CDHashSet<Node, NodeHashFunction> d_reasons;
109
  ModelValue d_modelValues;
110
  void buildModel();
111
  bool assertFactToEqualityEngine(TNode fact, TNode reason);
112
  bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
113
  Statistics d_statistics;
114
115
  /** Whether we need a last call effort check */
116
  bool d_needsLastCallCheck;
117
  /** For extended functions */
118
  context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
119
  context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
120
121
  /** do extended function inferences
122
   *
123
   * This method adds lemmas on the output channel of TheoryBV based on
124
   * reasoning about extended functions, such as bv2nat and int2bv. Examples
125
   * of lemmas added by this method include:
126
   *   0 <= ((_ int2bv w) x) < 2^w
127
   *   ((_ int2bv w) (bv2nat x)) = x
128
   *   (bv2nat ((_ int2bv w) x)) == x + k*2^w
129
   * The purpose of these lemmas is to recognize easy conflicts before fully
130
   * reducing extended functions based on their full semantics.
131
   */
132
  bool doExtfInferences(std::vector<Node>& terms);
133
  /** do extended function reductions
134
   *
135
   * This method adds lemmas on the output channel of TheoryBV based on
136
   * reducing all extended function applications that are preregistered to
137
   * this theory and have not already been reduced by context-dependent
138
   * simplification (see theory/ext_theory.h). Examples of lemmas added by
139
   * this method include:
140
   *   (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
141
   *                (ite ((_ extract 1 0) x) 1 0)
142
   */
143
  bool doExtfReductions(std::vector<Node>& terms);
144
145
 public:
146
  CoreSolver(context::Context* c, BVSolverLazy* bv);
147
  ~CoreSolver();
148
  bool needsEqualityEngine(EeSetupInfo& esi);
149
  void finishInit();
150
254492
  bool isComplete() override { return d_isComplete; }
151
  void preRegister(TNode node) override;
152
  bool check(Theory::Effort e) override;
153
  void explain(TNode literal, std::vector<TNode>& assumptions) override;
154
  bool collectModelValues(TheoryModel* m,
155
                          const std::set<Node>& termSet) override;
156
  Node getModelValue(TNode var) override;
157
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
158
  bool hasTerm(TNode node) const;
159
  void addTermToEqualityEngine(TNode node);
160
  /** check extended functions at the given effort */
161
  void checkExtf(Theory::Effort e);
162
  bool needsCheckLastEffort() const;
163
};
164
165
}
166
}
167
}