Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/booleans/circuit_propagator.h	Lines:	29	29	100.0 %
Date:	2021-11-07	Branches:	52	100	52.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Aina Niemetz, Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * A non-clausal circuit propagator for Boolean simplification.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#define CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H

#include <memory>
#include <unordered_map>
#include <vector>

#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "context/context.h"
#include "expr/node.h"
#include "proof/lazy_proof_chain.h"
#include "proof/trust_node.h"
#include "smt/env_obj.h"

namespace cvc5 {

class ProofGenerator;
class ProofNode;
class EagerProofGenerator;

namespace theory {
namespace booleans {

/**
 * The main purpose of the CircuitPropagator class is to maintain the
 * state of the circuit for subsequent calls to propagate(), so that
 * the same fact is not output twice, so that the same edge in the
 * circuit isn't propagated twice, etc.
 */
class CircuitPropagator : protected EnvObj
{
 public:
  /**
   * Value of a particular node
   */
  enum AssignmentStatus
  {
    /** Node is currently unassigned */
    UNASSIGNED = 0,
    /** Node is assigned to true */
    ASSIGNED_TO_TRUE,
    /** Node is assigned to false */
    ASSIGNED_TO_FALSE,
  };

  typedef std::unordered_map<Node, std::vector<Node>> BackEdgesMap;

  /**
   * Construct a new CircuitPropagator.
   */
  CircuitPropagator(Env& env, bool enableForward = true, bool enableBackward = true);

  /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
  bool getAssignment(TNode n) const
  {
    AssignmentMap::iterator i = d_state.find(n);
    Assert(i != d_state.end() && (*i).second != UNASSIGNED);
    return (*i).second == ASSIGNED_TO_TRUE;
  }

  // Use custom context to ensure propagator is reset after use
  void initialize() { d_context.push(); }

  void setNeedsFinish(bool value) { d_needsFinish = value; }

  bool getNeedsFinish() { return d_needsFinish; }

  std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }

  /** Finish the computation and pop the internal context */
  void finish();

  /** Assert for propagation */
  void assertTrue(TNode assertion);

  /**
   * Propagate through the asserted circuit propagator. New information
   * discovered by the propagator are put in the substitutions vector used in
   * construction.
   *
   * @return a trust node encapsulating the proof for a conflict as a lemma that
   * proves false, or the null trust node otherwise
   */
  CVC5_WARN_UNUSED_RESULT TrustNode propagate();

  /**
   * Get the back edges of this circuit.
   */
  const BackEdgesMap& getBackEdges() const { return d_backEdges; }

  /** Invert a set value */
  static inline AssignmentStatus neg(AssignmentStatus value)
  {
    Assert(value != UNASSIGNED);
    if (value == ASSIGNED_TO_TRUE)
      return ASSIGNED_TO_FALSE;
    else
      return ASSIGNED_TO_TRUE;
  }

  /** True iff Node is assigned in circuit (either true or false). */
  bool isAssigned(TNode n) const
  {
    AssignmentMap::const_iterator i = d_state.find(n);
    return i != d_state.end() && ((*i).second != UNASSIGNED);
  }

  /** True iff Node is assigned to the value. */
  bool isAssignedTo(TNode n, bool value) const
  {
    AssignmentMap::const_iterator i = d_state.find(n);
    if (i == d_state.end()) return false;
    if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
    if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
    return false;
  }
  /**
   * Set proof node manager, context and parent proof generator.
   *
   * If parent is non-null, then it is responsible for the proofs provided
   * to this class.
   */
  void setProof(ProofNodeManager* pnm,
                context::Context* ctx,
                ProofGenerator* defParent);

 private:
  /** A context-notify object that clears out stale data. */
  template <class T>
  class DataClearer : context::ContextNotifyObj
  {
   public:
    DataClearer(context::Context* context, T& data)
        : context::ContextNotifyObj(context), d_data(data)
    {
    }

   protected:
    void contextNotifyPop() override
    {
      Trace("circuit-prop")
          << "CircuitPropagator::DataClearer: clearing data "
          << "(size was " << d_data.size() << ")" << std::endl;
      d_data.clear();
    }

   private:
    T& d_data;
  }; /* class DataClearer<T> */

  /**
   * Assignment status of each node.
   */
  typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap;

  /**
   * Assign Node in circuit with the value and add it to the queue; note
   * conflicts.
   */
  void assignAndEnqueue(TNode n,
                        bool value,
                        std::shared_ptr<ProofNode> proof = nullptr);

  /**
   * Store a conflict for the case that we have derived both n and n.negate()
   * to be true.
   */
  void makeConflict(Node n);

  /**
   * Compute the map from nodes to the nodes that use it.
   */
  void computeBackEdges(TNode node);

  /**
   * Propagate new information forward in circuit to
   * the parents of "in".
   */
  void propagateForward(TNode child, bool assignment);

  /**
   * Propagate new information backward in circuit to
   * the children of "in".
   */
  void propagateBackward(TNode parent, bool assignment);

  /** Are proofs enabled? */
  bool isProofEnabled() const;

  context::Context d_context;

  /** The propagation queue */
  std::vector<TNode> d_propagationQueue;

  /**
   * We have a propagation queue "clearer" object for when the user
   * context pops.  Normally the propagation queue should be empty,
   * but this keeps us safe in case there's still some rubbish around
   * on the queue.
   */
  DataClearer<std::vector<TNode>> d_propagationQueueClearer;

  /** Are we in conflict? */
  context::CDO<TrustNode> d_conflict;

  /** Map of substitutions */
  std::vector<TrustNode> d_learnedLiterals;

  /**
   * Similar data clearer for learned literals.
   */
  DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;

  /**
   * Back edges from nodes to where they are used.
   */
  BackEdgesMap d_backEdges;

  /**
   * Similar data clearer for back edges.
   */
  DataClearer<BackEdgesMap> d_backEdgesClearer;

  /** Nodes that have been attached already (computed forward edges for) */
  // All the nodes we've visited so far
  context::CDHashSet<Node> d_seen;

  AssignmentMap d_state;

  /** Whether to perform forward propagation */
  const bool d_forwardPropagation;

  /** Whether to perform backward propagation */
  const bool d_backwardPropagation;

  /* Does the current state require a call to finish()? */
  bool d_needsFinish;

  /** Adds a new proof for f, or drops it if we already have a proof */
  void addProof(TNode f, std::shared_ptr<ProofNode> pf);

  /** A pointer to the proof manager */
  ProofNodeManager* d_pnm;
  /** Eager proof generator that actually stores the proofs */
  std::unique_ptr<EagerProofGenerator> d_epg;
  /** Connects the proofs to subproofs internally */
  std::unique_ptr<LazyCDProofChain> d_proofInternal;
  /** Connects the proofs to assumptions externally */
  std::unique_ptr<LazyCDProofChain> d_proofExternal;
}; /* class CircuitPropagator */

}  // namespace booleans
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Aina Niemetz, Gereon Kremer
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		* A non-clausal circuit propagator for Boolean simplification.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
19		#define CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
20
21		#include <memory>
22		#include <unordered_map>
23		#include <vector>
24
25		#include "context/cdhashmap.h"
26		#include "context/cdhashset.h"
27		#include "context/cdo.h"
28		#include "context/context.h"
29		#include "expr/node.h"
30		#include "proof/lazy_proof_chain.h"
31		#include "proof/trust_node.h"
32		#include "smt/env_obj.h"
33
34		namespace cvc5 {
35
36		class ProofGenerator;
37		class ProofNode;
38		class EagerProofGenerator;
39
40		namespace theory {
41		namespace booleans {
42
43		/**
44		* The main purpose of the CircuitPropagator class is to maintain the
45		* state of the circuit for subsequent calls to propagate(), so that
46		* the same fact is not output twice, so that the same edge in the
47		* circuit isn't propagated twice, etc.
48		*/
49	15884	class CircuitPropagator : protected EnvObj
50		{
51		public:
52		/**
53		* Value of a particular node
54		*/
55		enum AssignmentStatus
56		{
57		/** Node is currently unassigned */
58		UNASSIGNED = 0,
59		/** Node is assigned to true */
60		ASSIGNED_TO_TRUE,
61		/** Node is assigned to false */
62		ASSIGNED_TO_FALSE,
63		};
64
65		typedef std::unordered_map<Node, std::vector<Node>> BackEdgesMap;
66
67		/**
68		* Construct a new CircuitPropagator.
69		*/
70		CircuitPropagator(Env& env, bool enableForward = true, bool enableBackward = true);
71
72		/** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
73	307761	bool getAssignment(TNode n) const
74		{
75	307761	AssignmentMap::iterator i = d_state.find(n);
76	307761	Assert(i != d_state.end() && (*i).second != UNASSIGNED);
77	307761	return (*i).second == ASSIGNED_TO_TRUE;
78		}
79
80		// Use custom context to ensure propagator is reset after use
81	16303	void initialize() { d_context.push(); }
82
83	32606	void setNeedsFinish(bool value) { d_needsFinish = value; }
84
85	32187	bool getNeedsFinish() { return d_needsFinish; }
86
87	30894	std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
88
89		/** Finish the computation and pop the internal context */
90		void finish();
91
92		/** Assert for propagation */
93		void assertTrue(TNode assertion);
94
95		/**
96		* Propagate through the asserted circuit propagator. New information
97		* discovered by the propagator are put in the substitutions vector used in
98		* construction.
99		*
100		* @return a trust node encapsulating the proof for a conflict as a lemma that
101		* proves false, or the null trust node otherwise
102		*/
103		CVC5_WARN_UNUSED_RESULT TrustNode propagate();
104
105		/**
106		* Get the back edges of this circuit.
107		*/
108	16324	const BackEdgesMap& getBackEdges() const { return d_backEdges; }
109
110		/** Invert a set value */
111		static inline AssignmentStatus neg(AssignmentStatus value)
112		{
113		Assert(value != UNASSIGNED);
114		if (value == ASSIGNED_TO_TRUE)
115		return ASSIGNED_TO_FALSE;
116		else
117		return ASSIGNED_TO_TRUE;
118		}
119
120		/** True iff Node is assigned in circuit (either true or false). */
121	123328	bool isAssigned(TNode n) const
122		{
123	123328	AssignmentMap::const_iterator i = d_state.find(n);
124	123328	return i != d_state.end() && ((*i).second != UNASSIGNED);
125		}
126
127		/** True iff Node is assigned to the value. */
128	20168452	bool isAssignedTo(TNode n, bool value) const
129		{
130	20168452	AssignmentMap::const_iterator i = d_state.find(n);
131	20168452	if (i == d_state.end()) return false;
132	19901600	if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
133	482755	if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
134	40579	return false;
135		}
136		/**
137		* Set proof node manager, context and parent proof generator.
138		*
139		* If parent is non-null, then it is responsible for the proofs provided
140		* to this class.
141		*/
142		void setProof(ProofNodeManager* pnm,
143		context::Context* ctx,
144		ProofGenerator* defParent);
145
146		private:
147		/** A context-notify object that clears out stale data. */
148		template <class T>
149	47652	class DataClearer : context::ContextNotifyObj
150		{
151		public:
152	55899	DataClearer(context::Context* context, T& data)
153	55899	: context::ContextNotifyObj(context), d_data(data)
154		{
155	55899	}
156
157		protected:
158	48909	void contextNotifyPop() override
159		{
160	146727	Trace("circuit-prop")
161	48909	<< "CircuitPropagator::DataClearer: clearing data "
162	97818	<< "(size was " << d_data.size() << ")" << std::endl;
163	48909	d_data.clear();
164	48909	}
165
166		private:
167		T& d_data;
168		}; /* class DataClearer<T> */
169
170		/**
171		* Assignment status of each node.
172		*/
173		typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap;
174
175		/**
176		* Assign Node in circuit with the value and add it to the queue; note
177		* conflicts.
178		*/
179		void assignAndEnqueue(TNode n,
180		bool value,
181		std::shared_ptr<ProofNode> proof = nullptr);
182
183		/**
184		* Store a conflict for the case that we have derived both n and n.negate()
185		* to be true.
186		*/
187		void makeConflict(Node n);
188
189		/**
190		* Compute the map from nodes to the nodes that use it.
191		*/
192		void computeBackEdges(TNode node);
193
194		/**
195		* Propagate new information forward in circuit to
196		* the parents of "in".
197		*/
198		void propagateForward(TNode child, bool assignment);
199
200		/**
201		* Propagate new information backward in circuit to
202		* the children of "in".
203		*/
204		void propagateBackward(TNode parent, bool assignment);
205
206		/** Are proofs enabled? */
207		bool isProofEnabled() const;
208
209		context::Context d_context;
210
211		/** The propagation queue */
212		std::vector<TNode> d_propagationQueue;
213
214		/**
215		* We have a propagation queue "clearer" object for when the user
216		* context pops. Normally the propagation queue should be empty,
217		* but this keeps us safe in case there's still some rubbish around
218		* on the queue.
219		*/
220		DataClearer<std::vector<TNode>> d_propagationQueueClearer;
221
222		/** Are we in conflict? */
223		context::CDO<TrustNode> d_conflict;
224
225		/** Map of substitutions */
226		std::vector<TrustNode> d_learnedLiterals;
227
228		/**
229		* Similar data clearer for learned literals.
230		*/
231		DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
232
233		/**
234		* Back edges from nodes to where they are used.
235		*/
236		BackEdgesMap d_backEdges;
237
238		/**
239		* Similar data clearer for back edges.
240		*/
241		DataClearer<BackEdgesMap> d_backEdgesClearer;
242
243		/** Nodes that have been attached already (computed forward edges for) */
244		// All the nodes we've visited so far
245		context::CDHashSet<Node> d_seen;
246
247		AssignmentMap d_state;
248
249		/** Whether to perform forward propagation */
250		const bool d_forwardPropagation;
251
252		/** Whether to perform backward propagation */
253		const bool d_backwardPropagation;
254
255		/* Does the current state require a call to finish()? */
256		bool d_needsFinish;
257
258		/** Adds a new proof for f, or drops it if we already have a proof */
259		void addProof(TNode f, std::shared_ptr<ProofNode> pf);
260
261		/** A pointer to the proof manager */
262		ProofNodeManager* d_pnm;
263		/** Eager proof generator that actually stores the proofs */
264		std::unique_ptr<EagerProofGenerator> d_epg;
265		/** Connects the proofs to subproofs internally */
266		std::unique_ptr<LazyCDProofChain> d_proofInternal;
267		/** Connects the proofs to assumptions externally */
268		std::unique_ptr<LazyCDProofChain> d_proofExternal;
269		}; /* class CircuitPropagator */
270
271		} // namespace booleans
272		} // namespace theory
273		} // namespace cvc5
274
275		#endif /* CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */