Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/equality_engine_notify.h	Lines:	7	11	63.6 %
Date:	2021-05-21	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The virtual class for notifications from the equality engine.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
#define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace eq {

/**
 * Interface for equality engine notifications. All the notifications
 * are safe as TNodes, but not necessarily for negations.
 */
class EqualityEngineNotify
{
 public:
  virtual ~EqualityEngineNotify(){};

  /**
   * Notifies about a trigger predicate that became true or false. Notice that
   * predicate can be an equality.
   *
   * @param predicate the trigger predicate that became true or false
   * @param value the value of the predicate
   */
  virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0;

  /**
   * Notifies about the merge of two trigger terms.
   *
   * @param tag the theory that both triggers were tagged with
   * @param t1 a term marked as trigger
   * @param t2 a term marked as trigger
   * @param value true if equal, false if dis-equal
   */
  virtual bool eqNotifyTriggerTermEquality(TheoryId tag,
                                           TNode t1,
                                           TNode t2,
                                           bool value) = 0;

  /**
   * Notifies about the merge of two constant terms. After this, all work is
   * suspended and all you can do is ask for explanations.
   *
   * @param t1 a constant term
   * @param t2 a constant term
   */
  virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;

  /**
   * Notifies about the creation of a new equality class.
   *
   * @param t the term forming the new class
   */
  virtual void eqNotifyNewClass(TNode t) = 0;

  /**
   * Notifies about the merge of two classes (just after the merge).
   *
   * @param t1 a term
   * @param t2 a term
   */
  virtual void eqNotifyMerge(TNode t1, TNode t2) = 0;

  /**
   * Notifies about the disequality of two terms.
   *
   * @param t1 a term
   * @param t2 a term
   * @param reason the reason
   */
  virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0;

}; /* class EqualityEngineNotify */

/**
 * Implementation of the notification interface that ignores all the
 * notifications.
 */
class EqualityEngineNotifyNone : public EqualityEngineNotify
{
 public:
  bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
  {
    return true;
  }
  bool eqNotifyTriggerTermEquality(TheoryId tag,
                                   TNode t1,
                                   TNode t2,
                                   bool value) override
  {
    return true;
  }
  void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
  void eqNotifyNewClass(TNode t) override {}
  void eqNotifyMerge(TNode t1, TNode t2) override {}
  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
}; /* class EqualityEngineNotifyNone */

}  // Namespace eq
}  // Namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Dejan Jovanovic, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* The virtual class for notifications from the equality engine.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
19		#define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
20
21		#include "expr/node.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace eq {
26
27		/**
28		* Interface for equality engine notifications. All the notifications
29		* are safe as TNodes, but not necessarily for negations.
30		*/
31	113702	class EqualityEngineNotify
32		{
33		public:
34	122947	virtual ~EqualityEngineNotify(){};
35
36		/**
37		* Notifies about a trigger predicate that became true or false. Notice that
38		* predicate can be an equality.
39		*
40		* @param predicate the trigger predicate that became true or false
41		* @param value the value of the predicate
42		*/
43		virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0;
44
45		/**
46		* Notifies about the merge of two trigger terms.
47		*
48		* @param tag the theory that both triggers were tagged with
49		* @param t1 a term marked as trigger
50		* @param t2 a term marked as trigger
51		* @param value true if equal, false if dis-equal
52		*/
53		virtual bool eqNotifyTriggerTermEquality(TheoryId tag,
54		TNode t1,
55		TNode t2,
56		bool value) = 0;
57
58		/**
59		* Notifies about the merge of two constant terms. After this, all work is
60		* suspended and all you can do is ask for explanations.
61		*
62		* @param t1 a constant term
63		* @param t2 a constant term
64		*/
65		virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
66
67		/**
68		* Notifies about the creation of a new equality class.
69		*
70		* @param t the term forming the new class
71		*/
72		virtual void eqNotifyNewClass(TNode t) = 0;
73
74		/**
75		* Notifies about the merge of two classes (just after the merge).
76		*
77		* @param t1 a term
78		* @param t2 a term
79		*/
80		virtual void eqNotifyMerge(TNode t1, TNode t2) = 0;
81
82		/**
83		* Notifies about the disequality of two terms.
84		*
85		* @param t1 a term
86		* @param t2 a term
87		* @param reason the reason
88		*/
89		virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0;
90
91		}; /* class EqualityEngineNotify */
92
93		/**
94		* Implementation of the notification interface that ignores all the
95		* notifications.
96		*/
97	9245	class EqualityEngineNotifyNone : public EqualityEngineNotify
98		{
99		public:
100		bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
101		{
102		return true;
103		}
104		bool eqNotifyTriggerTermEquality(TheoryId tag,
105		TNode t1,
106		TNode t2,
107		bool value) override
108		{
109		return true;
110		}
111	4	void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
112	1259934	void eqNotifyNewClass(TNode t) override {}
113	630264	void eqNotifyMerge(TNode t1, TNode t2) override {}
114	622	void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
115		}; /* class EqualityEngineNotifyNone */
116
117		} // Namespace eq
118		} // Namespace theory
119		} // namespace cvc5
120
121		#endif