Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/shared_terms_database.h	Lines:	25	25	100.0 %
Date:	2021-11-07	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 Env;
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:
  /** Reference to the env */
  Env& d_env;

  /** 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(Env& env, TheoryEngine* theoryEngine);

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