GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_inequality.h Lines: 6 6 100.0 %
Date: 2021-03-22 Branches: 5 10 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_inequality.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, Aina Niemetz
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
#ifndef CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
20
#define CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
21
22
#include <unordered_set>
23
24
#include "context/cdhashset.h"
25
#include "expr/attribute.h"
26
#include "theory/bv/bv_inequality_graph.h"
27
#include "theory/bv/bv_subtheory.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace bv {
32
33
/** Cache for InequalitySolver::isInequalityOnly() */
34
struct IneqOnlyAttributeId
35
{
36
};
37
typedef expr::Attribute<IneqOnlyAttributeId, bool> IneqOnlyAttribute;
38
39
/** Whether the above has been computed yet or not for an expr */
40
struct IneqOnlyComputedAttributeId
41
{
42
};
43
typedef expr::Attribute<IneqOnlyComputedAttributeId, bool>
44
    IneqOnlyComputedAttribute;
45
46
17902
class InequalitySolver : public SubtheorySolver
47
{
48
  struct Statistics
49
  {
50
    IntStat d_numCallstoCheck;
51
    TimerStat d_solveTime;
52
    Statistics();
53
    ~Statistics();
54
  };
55
56
  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
57
  InequalityGraph d_inequalityGraph;
58
  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
59
  context::CDO<bool> d_isComplete;
60
  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
61
  NodeSet d_ineqTerms;
62
  bool isInequalityOnly(TNode node);
63
  bool addInequality(TNode a, TNode b, bool strict, TNode fact);
64
  Statistics d_statistics;
65
66
 public:
67
8954
  InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv)
68
8954
      : SubtheorySolver(c, bv),
69
        d_assertionSet(c),
70
        d_inequalityGraph(c, u),
71
        d_explanations(c),
72
        d_isComplete(c, true),
73
        d_ineqTerms(),
74
8954
        d_statistics()
75
  {
76
8954
  }
77
78
  bool check(Theory::Effort e) override;
79
  void propagate(Theory::Effort e) override;
80
  void explain(TNode literal, std::vector<TNode>& assumptions) override;
81
395846
  bool isComplete() override { return d_isComplete; }
82
  bool collectModelValues(TheoryModel* m,
83
                          const std::set<Node>& termSet) override;
84
  Node getModelValue(TNode var) override;
85
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
86
  void assertFact(TNode fact) override;
87
  void preRegister(TNode node) override;
88
};
89
90
}  // namespace bv
91
}  // namespace theory
92
}  // namespace CVC4
93
94
#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */