GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_eq_notify.h Lines: 15 19 78.9 %
Date: 2021-03-22 Branches: 14 24 58.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_eq_notify.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 The theory equality notify utility.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__THEORY_EQ_NOTIFY_H
18
#define CVC4__THEORY__THEORY_EQ_NOTIFY_H
19
20
#include "expr/node.h"
21
#include "theory/theory_inference_manager.h"
22
#include "theory/uf/equality_engine_notify.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
/**
28
 * The default class for equality engine callbacks for a theory. This forwards
29
 * calls for trigger predicates, trigger term equalities and conflicts due to
30
 * constant merges to the provided theory inference manager.
31
 */
32
class TheoryEqNotifyClass : public eq::EqualityEngineNotify
33
{
34
 public:
35
44975
  TheoryEqNotifyClass(TheoryInferenceManager& im) : d_im(im) {}
36
44960
  ~TheoryEqNotifyClass() {}
37
38
6111643
  bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
39
  {
40
6111643
    if (value)
41
    {
42
1854739
      return d_im.propagateLit(predicate);
43
    }
44
4256904
    return d_im.propagateLit(predicate.notNode());
45
  }
46
1533712
  bool eqNotifyTriggerTermEquality(TheoryId tag,
47
                                   TNode t1,
48
                                   TNode t2,
49
                                   bool value) override
50
  {
51
1533712
    if (value)
52
    {
53
944052
      return d_im.propagateLit(t1.eqNode(t2));
54
    }
55
589660
    return d_im.propagateLit(t1.eqNode(t2).notNode());
56
  }
57
9500
  void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
58
  {
59
9500
    d_im.conflictEqConstantMerge(t1, t2);
60
9500
  }
61
  void eqNotifyNewClass(TNode t) override
62
  {
63
    // do nothing
64
  }
65
  void eqNotifyMerge(TNode t1, TNode t2) override
66
  {
67
    // do nothing
68
  }
69
223697
  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
70
  {
71
    // do nothing
72
223697
  }
73
74
 protected:
75
  /** Reference to the theory inference manager */
76
  TheoryInferenceManager& d_im;
77
};
78
79
}  // namespace theory
80
}  // namespace CVC4
81
82
#endif