Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/shared_terms_database.h	Lines:	25	25	100.0 %
Date:	2021-09-29	Branches:	10	32	31.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#pragma once

#include <unordered_map>

#include "context/cdhashset.h"
#include "expr/node.h"
#include "proof/proof_node_manager.h"
#include "proof/trust_node.h"
#include "theory/ee_setup_info.h"
#include "theory/theory_id.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_equality_engine.h"
#include "util/statistics_stats.h"

namespace cvc5 {

class TheoryEngine;

class SharedTermsDatabase : public context::ContextNotifyObj {
 public:
  /** A container for a list of shared terms */
  typedef std::vector<TNode> shared_terms_list;

  /** The iterator to go through the shared terms list */
  typedef shared_terms_list::const_iterator shared_terms_iterator;

 private:
  /** Some statistics */
  IntStat d_statSharedTerms;

  // Needs to be a map from Nodes as after a backtrack they might not exist
  typedef std::unordered_map<Node, shared_terms_list> SharedTermsMap;

  /** A map from atoms to a list of shared terms */
  SharedTermsMap d_atomsToTerms;

  /** Each time we add a shared term, we add it's parent to this list */
  std::vector<TNode> d_addedSharedTerms;

  /** Context-dependent size of the d_addedSharedTerms list */
  context::CDO<unsigned> d_addedSharedTermsSize;

  /** A map from atoms and subterms to the theories that use it */
  typedef context::CDHashMap<std::pair<Node, TNode>,
                             theory::TheoryIdSet,
                             TNodePairHashFunction>
      SharedTermsTheoriesMap;
  SharedTermsTheoriesMap d_termsToTheories;

  /** Map from term to theories that have already been notified about the shared term */
  typedef context::CDHashMap<TNode, theory::TheoryIdSet> AlreadyNotifiedMap;
  AlreadyNotifiedMap d_alreadyNotifiedMap;

  /** The registered equalities for propagation */
  typedef context::CDHashSet<Node> RegisteredEqualitiesSet;
  RegisteredEqualitiesSet d_registeredEqualities;

 private:
  /** This method removes all the un-necessary stuff from the maps */
  void backtrack();

  // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
  class EENotifyClass : public theory::eq::EqualityEngineNotify {
    SharedTermsDatabase& d_sharedTerms;
  public:
    EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
    {
      Assert(predicate.getKind() == kind::EQUAL);
      d_sharedTerms.propagateEquality(predicate, value);
      return true;
    }

    bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
                                     TNode t1,
                                     TNode t2,
                                     bool value) override
    {
      return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
    }

    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
    {
      d_sharedTerms.conflict(t1, t2, true);
    }

    void eqNotifyNewClass(TNode t) override {}
    void eqNotifyMerge(TNode t1, TNode t2) override {}
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
  };

  /** The notify class for d_equalityEngine */
  EENotifyClass d_EENotify;

  /**
   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
   * the theory. Returns false if there is a direct conflict (via rewrite for example).
   */
  bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);

  /**
   * Called from the equality engine when a trigger equality is deduced.
   */
  bool propagateEquality(TNode equality, bool polarity);

  /** Theory engine */
  TheoryEngine* d_theoryEngine;

  /** Are we in conflict */
  context::CDO<bool> d_inConflict;

  /** Conflicting terms, if any */
  Node d_conflictLHS, d_conflictRHS;

  /** Polarity of the conflict */
  bool d_conflictPolarity;

  /** Called by the equality engine notify to mark the conflict */
  void conflict(TNode lhs, TNode rhs, bool polarity) {
    if (!d_inConflict) {
      // Only remember it if we're not already in conflict
      d_inConflict = true;
      d_conflictLHS = lhs;
      d_conflictRHS = rhs;
      d_conflictPolarity = polarity;
    }
  }

  /**
   * Should be called before any public non-const method in order to
   * enqueue the conflict to the theory engine.
   */
  void checkForConflict();

 public:
  /**
   * @param theoryEngine The parent theory engine
   * @param context The SAT context
   * @param userContext The user context
   * @param pnm The proof node manager to use, which is non-null if proofs
   * are enabled.
   */
  SharedTermsDatabase(TheoryEngine* theoryEngine,
                      context::Context* context,
                      context::UserContext* userContext,
                      ProofNodeManager* pnm);

  //-------------------------------------------- initialization
  /** Called to set the equality engine. */
  void setEqualityEngine(theory::eq::EqualityEngine* ee);
  /**
   * Returns true if we need an equality engine, this has the same contract
   * as Theory::needsEqualityEngine.
   */
  bool needsEqualityEngine(theory::EeSetupInfo& esi);
  //-------------------------------------------- end initialization

  /**
   * Asserts n to the shared terms database with given polarity and reason
   */
  void assertShared(TNode n, bool polarity, TNode reason);

  /**
   * Return whether the equality is alreday known to the engine
   */
  bool isKnown(TNode literal) const;

  /**
   * Returns an explanation of the propagation that came from the database.
   */
  TrustNode explain(TNode literal) const;

  /**
   * Add an equality to propagate.
   */
  void addEqualityToPropagate(TNode equality);

  /**
   * Add a shared term to the database. The shared term is a subterm of the atom and
   * should be associated with the given theory.
   */
  void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories);

  /**
   * Mark that the given theories have been notified of the given shared term.
   */
  void markNotified(TNode term, theory::TheoryIdSet theories);

  /**
   * Returns true if the atom contains any shared terms, false otherwise.
   */
  bool hasSharedTerms(TNode atom) const;

  /**
   * Iterator pointing to the first shared term belonging to the given atom.
   */
  shared_terms_iterator begin(TNode atom) const;

  /**
   * Iterator pointing to the end of the list of shared terms belonging to the given atom.
   */
  shared_terms_iterator end(TNode atom) const;

  /**
   * Get the theories that share the term in a given atom (and have not yet been notified).
   */
  theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const;

  /**
   * Get the theories that share the term and have been notified already.
   */
  theory::TheoryIdSet getNotifiedTheories(TNode term) const;

  /**
   * Returns true if the term is currently registered as shared with some theory.
   */
  bool isShared(TNode term) const {
    return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
  }

  /**
   * Returns true if the literal is an (dis-)equality with both sides registered as shared with
   * some theory.
   */
  bool isSharedEquality(TNode literal) const {
    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
    return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
  }

  /**
   * Returns true if the shared terms a and b are known to be equal.
   */
  bool areEqual(TNode a, TNode b) const;

  /**
   * Retursn true if the shared terms a and b are known to be dis-equal.
   */
  bool areDisequal(TNode a, TNode b) const;

  /**
   * get equality engine
   */
  theory::eq::EqualityEngine* getEqualityEngine();

 protected:
  /**
   * This method gets called on backtracks from the context manager.
   */
  void contextNotifyPop() override { backtrack(); }
  /** The SAT search context. */
  context::Context* d_satContext;
  /** The user level assertion context. */
  context::UserContext* d_userContext;
  /** Equality engine */
  theory::eq::EqualityEngine* d_equalityEngine;
  /** Proof equality engine, if we allocated one */
  std::unique_ptr<theory::eq::ProofEqEngine> d_pfeeAlloc;
  /** The proof equality engine we are using */
  theory::eq::ProofEqEngine* d_pfee;
  /** The proof node manager */
  ProofNodeManager* d_pnm;
};

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Dejan Jovanovic, Andrew Reynolds, Mathias Preiner
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		* [[ Add lengthier description here ]]
14		* \todo document this file
15		*/
16
17		#include "cvc5_private.h"
18
19		#pragma once
20
21		#include <unordered_map>
22
23		#include "context/cdhashset.h"
24		#include "expr/node.h"
25		#include "proof/proof_node_manager.h"
26		#include "proof/trust_node.h"
27		#include "theory/ee_setup_info.h"
28		#include "theory/theory_id.h"
29		#include "theory/uf/equality_engine.h"
30		#include "theory/uf/proof_equality_engine.h"
31		#include "util/statistics_stats.h"
32
33		namespace cvc5 {
34
35		class TheoryEngine;
36
37	6268	class SharedTermsDatabase : public context::ContextNotifyObj {
38		public:
39		/** A container for a list of shared terms */
40		typedef std::vector<TNode> shared_terms_list;
41
42		/** The iterator to go through the shared terms list */
43		typedef shared_terms_list::const_iterator shared_terms_iterator;
44
45		private:
46		/** Some statistics */
47		IntStat d_statSharedTerms;
48
49		// Needs to be a map from Nodes as after a backtrack they might not exist
50		typedef std::unordered_map<Node, shared_terms_list> SharedTermsMap;
51
52		/** A map from atoms to a list of shared terms */
53		SharedTermsMap d_atomsToTerms;
54
55		/** Each time we add a shared term, we add it's parent to this list */
56		std::vector<TNode> d_addedSharedTerms;
57
58		/** Context-dependent size of the d_addedSharedTerms list */
59		context::CDO<unsigned> d_addedSharedTermsSize;
60
61		/** A map from atoms and subterms to the theories that use it */
62		typedef context::CDHashMap<std::pair<Node, TNode>,
63		theory::TheoryIdSet,
64		TNodePairHashFunction>
65		SharedTermsTheoriesMap;
66		SharedTermsTheoriesMap d_termsToTheories;
67
68		/** Map from term to theories that have already been notified about the shared term */
69		typedef context::CDHashMap<TNode, theory::TheoryIdSet> AlreadyNotifiedMap;
70		AlreadyNotifiedMap d_alreadyNotifiedMap;
71
72		/** The registered equalities for propagation */
73		typedef context::CDHashSet<Node> RegisteredEqualitiesSet;
74		RegisteredEqualitiesSet d_registeredEqualities;
75
76		private:
77		/** This method removes all the un-necessary stuff from the maps */
78		void backtrack();
79
80		// EENotifyClass: template helper class for d_equalityEngine - handles call-backs
81	6268	class EENotifyClass : public theory::eq::EqualityEngineNotify {
82		SharedTermsDatabase& d_sharedTerms;
83		public:
84	6271	EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
85	2979706	bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
86		{
87	2979706	Assert(predicate.getKind() == kind::EQUAL);
88	2979706	d_sharedTerms.propagateEquality(predicate, value);
89	2979706	return true;
90		}
91
92	2420579	bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
93		TNode t1,
94		TNode t2,
95		bool value) override
96		{
97	2420579	return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
98		}
99
100	9465	void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
101		{
102	9465	d_sharedTerms.conflict(t1, t2, true);
103	9465	}
104
105	255050	void eqNotifyNewClass(TNode t) override {}
106	4200648	void eqNotifyMerge(TNode t1, TNode t2) override {}
107	900139	void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
108		};
109
110		/** The notify class for d_equalityEngine */
111		EENotifyClass d_EENotify;
112
113		/**
114		* Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
115		* the theory. Returns false if there is a direct conflict (via rewrite for example).
116		*/
117		bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
118
119		/**
120		* Called from the equality engine when a trigger equality is deduced.
121		*/
122		bool propagateEquality(TNode equality, bool polarity);
123
124		/** Theory engine */
125		TheoryEngine* d_theoryEngine;
126
127		/** Are we in conflict */
128		context::CDO<bool> d_inConflict;
129
130		/** Conflicting terms, if any */
131		Node d_conflictLHS, d_conflictRHS;
132
133		/** Polarity of the conflict */
134		bool d_conflictPolarity;
135
136		/** Called by the equality engine notify to mark the conflict */
137	9465	void conflict(TNode lhs, TNode rhs, bool polarity) {
138	9465	if (!d_inConflict) {
139		// Only remember it if we're not already in conflict
140	9465	d_inConflict = true;
141	9465	d_conflictLHS = lhs;
142	9465	d_conflictRHS = rhs;
143	9465	d_conflictPolarity = polarity;
144		}
145	9465	}
146
147		/**
148		* Should be called before any public non-const method in order to
149		* enqueue the conflict to the theory engine.
150		*/
151		void checkForConflict();
152
153		public:
154		/**
155		* @param theoryEngine The parent theory engine
156		* @param context The SAT context
157		* @param userContext The user context
158		* @param pnm The proof node manager to use, which is non-null if proofs
159		* are enabled.
160		*/
161		SharedTermsDatabase(TheoryEngine* theoryEngine,
162		context::Context* context,
163		context::UserContext* userContext,
164		ProofNodeManager* pnm);
165
166		//-------------------------------------------- initialization
167		/** Called to set the equality engine. */
168		void setEqualityEngine(theory::eq::EqualityEngine* ee);
169		/**
170		* Returns true if we need an equality engine, this has the same contract
171		* as Theory::needsEqualityEngine.
172		*/
173		bool needsEqualityEngine(theory::EeSetupInfo& esi);
174		//-------------------------------------------- end initialization
175
176		/**
177		* Asserts n to the shared terms database with given polarity and reason
178		*/
179		void assertShared(TNode n, bool polarity, TNode reason);
180
181		/**
182		* Return whether the equality is alreday known to the engine
183		*/
184		bool isKnown(TNode literal) const;
185
186		/**
187		* Returns an explanation of the propagation that came from the database.
188		*/
189		TrustNode explain(TNode literal) const;
190
191		/**
192		* Add an equality to propagate.
193		*/
194		void addEqualityToPropagate(TNode equality);
195
196		/**
197		* Add a shared term to the database. The shared term is a subterm of the atom and
198		* should be associated with the given theory.
199		*/
200		void addSharedTerm(TNode atom, TNode term, theory::TheoryIdSet theories);
201
202		/**
203		* Mark that the given theories have been notified of the given shared term.
204		*/
205		void markNotified(TNode term, theory::TheoryIdSet theories);
206
207		/**
208		* Returns true if the atom contains any shared terms, false otherwise.
209		*/
210		bool hasSharedTerms(TNode atom) const;
211
212		/**
213		* Iterator pointing to the first shared term belonging to the given atom.
214		*/
215		shared_terms_iterator begin(TNode atom) const;
216
217		/**
218		* Iterator pointing to the end of the list of shared terms belonging to the given atom.
219		*/
220		shared_terms_iterator end(TNode atom) const;
221
222		/**
223		* Get the theories that share the term in a given atom (and have not yet been notified).
224		*/
225		theory::TheoryIdSet getTheoriesToNotify(TNode atom, TNode term) const;
226
227		/**
228		* Get the theories that share the term and have been notified already.
229		*/
230		theory::TheoryIdSet getNotifiedTheories(TNode term) const;
231
232		/**
233		* Returns true if the term is currently registered as shared with some theory.
234		*/
235	1130204	bool isShared(TNode term) const {
236	1130204	return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
237		}
238
239		/**
240		* Returns true if the literal is an (dis-)equality with both sides registered as shared with
241		* some theory.
242		*/
243		bool isSharedEquality(TNode literal) const {
244		TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
245		return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
246		}
247
248		/**
249		* Returns true if the shared terms a and b are known to be equal.
250		*/
251		bool areEqual(TNode a, TNode b) const;
252
253		/**
254		* Retursn true if the shared terms a and b are known to be dis-equal.
255		*/
256		bool areDisequal(TNode a, TNode b) const;
257
258		/**
259		* get equality engine
260		*/
261		theory::eq::EqualityEngine* getEqualityEngine();
262
263		protected:
264		/**
265		* This method gets called on backtracks from the context manager.
266		*/
267	1876656	void contextNotifyPop() override { backtrack(); }
268		/** The SAT search context. */
269		context::Context* d_satContext;
270		/** The user level assertion context. */
271		context::UserContext* d_userContext;
272		/** Equality engine */
273		theory::eq::EqualityEngine* d_equalityEngine;
274		/** Proof equality engine, if we allocated one */
275		std::unique_ptr<theory::eq::ProofEqEngine> d_pfeeAlloc;
276		/** The proof equality engine we are using */
277		theory::eq::ProofEqEngine* d_pfee;
278		/** The proof node manager */
279		ProofNodeManager* d_pnm;
280		};
281
282		} // namespace cvc5