Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bv_inequality_graph.h	Lines:	41	41	100.0 %
Date:	2021-05-24	Branches:	23	82	28.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Mathias Preiner, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Algebraic solver.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H

#include <queue>
#include <unordered_map>
#include <unordered_set>

#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "context/cdqueue.h"
#include "context/context.h"

namespace cvc5 {
namespace theory {
namespace bv {

typedef unsigned TermId;
typedef unsigned ReasonId;
extern const TermId UndefinedTermId;
extern const ReasonId UndefinedReasonId;
extern const ReasonId AxiomReasonId;

class InequalityGraph : public context::ContextNotifyObj{

  struct InequalityEdge {
    TermId next;
    ReasonId reason;
    bool strict;
    InequalityEdge(TermId n, bool s, ReasonId r)
      : next(n),
        reason(r),
        strict(s)
    {}
    bool operator==(const InequalityEdge& other) const {
      return next == other.next && reason == other.reason && strict == other.strict;
    }
  };

  class InequalityNode {
    TermId d_id;
    unsigned d_bitwidth;
    bool d_isConstant;
  public:
    InequalityNode(TermId id, unsigned bitwidth, bool isConst)
      : d_id(id),
        d_bitwidth(bitwidth),
        d_isConstant(isConst)
    {}
    TermId getId() const { return d_id; }
    unsigned getBitwidth() const { return d_bitwidth; }
    bool isConstant() const { return d_isConstant; }
  };

  struct ModelValue {
    TermId parent;
    ReasonId reason;
    BitVector value;
    ModelValue()
      : parent(UndefinedTermId),
        reason(UndefinedReasonId),
        value(0, 0u)
    {}

    ModelValue(const BitVector& val, TermId p, ReasonId r)
      : parent(p),
        reason(r),
        value(val)
    {}
  };

  typedef context::CDHashMap<TermId, ModelValue> ModelValues;

  struct QueueComparator {
    const ModelValues* d_model;
    QueueComparator(const ModelValues* model)
      : d_model(model)
    {}
    bool operator() (TermId left, TermId right) const {
      Assert(d_model->find(left) != d_model->end()
             && d_model->find(right) != d_model->end());

      return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value;
    }
  };

  typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap;
  typedef std::unordered_map<TNode, TermId> TermNodeToIdMap;

  typedef std::vector<InequalityEdge> Edges;
  typedef std::unordered_set<TermId> TermIdSet;

  typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator>
      BFSQueue;
  typedef std::unordered_set<TNode> TNodeSet;
  typedef std::unordered_set<Node> NodeSet;

  std::vector<InequalityNode> d_ineqNodes;
  std::vector< Edges > d_ineqEdges;

  // to keep the explanation nodes alive
  NodeSet d_reasonSet;
  std::vector<TNode> d_reasonNodes;
  ReasonToIdMap d_reasonToIdMap;

  std::vector<Node> d_termNodes;
  TermNodeToIdMap d_termNodeToIdMap;

  context::CDO<bool> d_inConflict;
  std::vector<TNode> d_conflict;

  ModelValues  d_modelValues;
  void initializeModelValue(TNode node);
  void setModelValue(TermId term, const ModelValue& mv);
  ModelValue getModelValue(TermId term) const;
  bool hasModelValue(TermId id) const;
  bool hasReason(TermId id) const;

  /**
   * Registers the term by creating its corresponding InequalityNode
   * and adding the min <= term <= max default edges.
   *
   * @param term
   *
   * @return
   */
  TermId registerTerm(TNode term);
  TNode getTermNode(TermId id) const;
  TermId getTermId(TNode node) const;
  bool isRegistered(TNode term) const;

  ReasonId registerReason(TNode reason);
  TNode getReasonNode(ReasonId id) const;

  Edges& getEdges(TermId id)
  {
    Assert(id < d_ineqEdges.size());
    return d_ineqEdges[id];
  }
  InequalityNode& getInequalityNode(TermId id)
  {
    Assert(id < d_ineqNodes.size());
    return d_ineqNodes[id];
  }
  const InequalityNode& getInequalityNode(TermId id) const
  {
    Assert(id < d_ineqNodes.size());
    return d_ineqNodes[id];
  }
  unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
  bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }

  BitVector getValue(TermId id) const;

  void addEdge(TermId a, TermId b, bool strict, TermId reason);

  void setConflict(const std::vector<ReasonId>& conflict);
  /**
   * If necessary update the value in the model of the current queue element.
   *
   * @param id current queue element we are updating
   * @param start node we started with, to detect cycles
   *
   * @return
   */
  bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed);
  /**
   * Update the current model starting with the start term.
   *
   * @param queue
   * @param start
   *
   * @return
   */
  bool processQueue(BFSQueue& queue, TermId start);
  /**
   * Return the reasons why from <= to. If from is undefined we just
   * explain the current value of to.
   *
   * @param from
   * @param to
   * @param explanation
   */
  void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation);
  //  void splitDisequality(TNode diseq);

  /**
     Disequality reasoning
   */

  /*** The currently asserted disequalities */
  context::CDQueue<TNode> d_disequalities;
  typedef context::CDHashSet<Node> CDNodeSet;
  CDNodeSet d_disequalitiesAlreadySplit;
  Node makeDiseqSplitLemma(TNode diseq);
  /** Backtracking mechanisms **/
  std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
  context::CDO<unsigned> d_undoStackIndex;

  void contextNotifyPop() override { backtrack(); }

  void backtrack();

public:

  InequalityGraph(context::Context* c, context::Context* u, bool s = false)
    : ContextNotifyObj(c),
      d_ineqNodes(),
      d_ineqEdges(),
      d_inConflict(c, false),
      d_conflict(),
      d_modelValues(c),
      d_disequalities(c),
      d_disequalitiesAlreadySplit(u),
      d_undoStack(),
      d_undoStackIndex(c)
  {}
  /**
   * Add a new inequality to the graph
   *
   * @param a
   * @param b
   * @param strict
   * @param reason
   *
   * @return
   */
  bool addInequality(TNode a, TNode b, bool strict, TNode reason);
  /**
   * Add a new disequality to the graph. This may lead in a lemma.
   *
   * @param a
   * @param b
   * @param reason
   *
   * @return
   */
  bool addDisequality(TNode a, TNode b, TNode reason);
  void getConflict(std::vector<TNode>& conflict);
  virtual ~InequalityGraph() {}
  /**
   * Check that the currently asserted disequalities that have not been split on
   * are still true in the current model.
   */
  void checkDisequalities(std::vector<Node>& lemmas);
  /**
   * Return true if a < b is entailed by the current set of assertions.
   *
   * @param a
   * @param b
   *
   * @return
   */
  bool isLessThan(TNode a, TNode b);
  /**
   * Returns true if the term has a value in the model (i.e. if we have seen it)
   *
   * @param a
   *
   * @return
   */
  bool hasValueInModel(TNode a) const;
  /**
   * Return the value of a in the current model.
   *
   * @param a
   *
   * @return
   */
  BitVector getValueInModel(TNode a) const;

  void getAllValuesInModel(std::vector<Node>& assignments);
};

}
}
}  // namespace cvc5

#endif /* CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Mathias Preiner, Tim King
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		* Algebraic solver.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
19		#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
20
21		#include <queue>
22		#include <unordered_map>
23		#include <unordered_set>
24
25		#include "context/cdhashmap.h"
26		#include "context/cdhashset.h"
27		#include "context/cdo.h"
28		#include "context/cdqueue.h"
29		#include "context/context.h"
30
31		namespace cvc5 {
32		namespace theory {
33		namespace bv {
34
35		typedef unsigned TermId;
36		typedef unsigned ReasonId;
37		extern const TermId UndefinedTermId;
38		extern const ReasonId UndefinedReasonId;
39		extern const ReasonId AxiomReasonId;
40
41		class InequalityGraph : public context::ContextNotifyObj{
42
43		struct InequalityEdge {
44		TermId next;
45		ReasonId reason;
46		bool strict;
47	1158509	InequalityEdge(TermId n, bool s, ReasonId r)
48	1158509	: next(n),
49		reason(r),
50	1158509	strict(s)
51	1158509	{}
52	1158509	bool operator==(const InequalityEdge& other) const {
53	1158509	return next == other.next && reason == other.reason && strict == other.strict;
54		}
55		};
56
57		class InequalityNode {
58		TermId d_id;
59		unsigned d_bitwidth;
60		bool d_isConstant;
61		public:
62	29632	InequalityNode(TermId id, unsigned bitwidth, bool isConst)
63	29632	: d_id(id),
64		d_bitwidth(bitwidth),
65	29632	d_isConstant(isConst)
66	29632	{}
67		TermId getId() const { return d_id; }
68	445227	unsigned getBitwidth() const { return d_bitwidth; }
69	5940016	bool isConstant() const { return d_isConstant; }
70		};
71
72	20736386	struct ModelValue {
73		TermId parent;
74		ReasonId reason;
75		BitVector value;
76	927954	ModelValue()
77	927954	: parent(UndefinedTermId),
78		reason(UndefinedReasonId),
79	927954	value(0, 0u)
80	927954	{}
81
82	5238447	ModelValue(const BitVector& val, TermId p, ReasonId r)
83	5238447	: parent(p),
84		reason(r),
85	5238447	value(val)
86	5238447	{}
87		};
88
89		typedef context::CDHashMap<TermId, ModelValue> ModelValues;
90
91		struct QueueComparator {
92		const ModelValues* d_model;
93	215480	QueueComparator(const ModelValues* model)
94	215480	: d_model(model)
95	215480	{}
96	3687	bool operator() (TermId left, TermId right) const {
97	3687	Assert(d_model->find(left) != d_model->end()
98		&& d_model->find(right) != d_model->end());
99
100	3687	return ((d_model->find(left))).second.value < ((d_model->find(right))).second.value;
101		}
102		};
103
104		typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap;
105		typedef std::unordered_map<TNode, TermId> TermNodeToIdMap;
106
107		typedef std::vector<InequalityEdge> Edges;
108		typedef std::unordered_set<TermId> TermIdSet;
109
110		typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator>
111		BFSQueue;
112		typedef std::unordered_set<TNode> TNodeSet;
113		typedef std::unordered_set<Node> NodeSet;
114
115		std::vector<InequalityNode> d_ineqNodes;
116		std::vector< Edges > d_ineqEdges;
117
118		// to keep the explanation nodes alive
119		NodeSet d_reasonSet;
120		std::vector<TNode> d_reasonNodes;
121		ReasonToIdMap d_reasonToIdMap;
122
123		std::vector<Node> d_termNodes;
124		TermNodeToIdMap d_termNodeToIdMap;
125
126		context::CDO<bool> d_inConflict;
127		std::vector<TNode> d_conflict;
128
129		ModelValues d_modelValues;
130		void initializeModelValue(TNode node);
131		void setModelValue(TermId term, const ModelValue& mv);
132		ModelValue getModelValue(TermId term) const;
133		bool hasModelValue(TermId id) const;
134		bool hasReason(TermId id) const;
135
136		/**
137		* Registers the term by creating its corresponding InequalityNode
138		* and adding the min <= term <= max default edges.
139		*
140		* @param term
141		*
142		* @return
143		*/
144		TermId registerTerm(TNode term);
145		TNode getTermNode(TermId id) const;
146		TermId getTermId(TNode node) const;
147		bool isRegistered(TNode term) const;
148
149		ReasonId registerReason(TNode reason);
150		TNode getReasonNode(ReasonId id) const;
151
152	2762245	Edges& getEdges(TermId id)
153		{
154	2762245	Assert(id < d_ineqEdges.size());
155	2762245	return d_ineqEdges[id];
156		}
157		InequalityNode& getInequalityNode(TermId id)
158		{
159		Assert(id < d_ineqNodes.size());
160		return d_ineqNodes[id];
161		}
162	6385243	const InequalityNode& getInequalityNode(TermId id) const
163		{
164	6385243	Assert(id < d_ineqNodes.size());
165	6385243	return d_ineqNodes[id];
166		}
167	445227	unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); }
168	5940016	bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); }
169
170		BitVector getValue(TermId id) const;
171
172		void addEdge(TermId a, TermId b, bool strict, TermId reason);
173
174		void setConflict(const std::vector<ReasonId>& conflict);
175		/**
176		* If necessary update the value in the model of the current queue element.
177		*
178		* @param id current queue element we are updating
179		* @param start node we started with, to detect cycles
180		*
181		* @return
182		*/
183		bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed);
184		/**
185		* Update the current model starting with the start term.
186		*
187		* @param queue
188		* @param start
189		*
190		* @return
191		*/
192		bool processQueue(BFSQueue& queue, TermId start);
193		/**
194		* Return the reasons why from <= to. If from is undefined we just
195		* explain the current value of to.
196		*
197		* @param from
198		* @param to
199		* @param explanation
200		*/
201		void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation);
202		// void splitDisequality(TNode diseq);
203
204		/**
205		Disequality reasoning
206		*/
207
208		/*** The currently asserted disequalities */
209		context::CDQueue<TNode> d_disequalities;
210		typedef context::CDHashSet<Node> CDNodeSet;
211		CDNodeSet d_disequalitiesAlreadySplit;
212		Node makeDiseqSplitLemma(TNode diseq);
213		/ Backtracking mechanisms /
214		std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
215		context::CDO<unsigned> d_undoStackIndex;
216
217	2239992	void contextNotifyPop() override { backtrack(); }
218
219		void backtrack();
220
221		public:
222
223	9405	InequalityGraph(context::Context* c, context::Context* u, bool s = false)
224	9405	: ContextNotifyObj(c),
225		d_ineqNodes(),
226		d_ineqEdges(),
227		d_inConflict(c, false),
228		d_conflict(),
229		d_modelValues(c),
230		d_disequalities(c),
231		d_disequalitiesAlreadySplit(u),
232		d_undoStack(),
233	9405	d_undoStackIndex(c)
234	9405	{}
235		/**
236		* Add a new inequality to the graph
237		*
238		* @param a
239		* @param b
240		* @param strict
241		* @param reason
242		*
243		* @return
244		*/
245		bool addInequality(TNode a, TNode b, bool strict, TNode reason);
246		/**
247		* Add a new disequality to the graph. This may lead in a lemma.
248		*
249		* @param a
250		* @param b
251		* @param reason
252		*
253		* @return
254		*/
255		bool addDisequality(TNode a, TNode b, TNode reason);
256		void getConflict(std::vector<TNode>& conflict);
257	9405	virtual ~InequalityGraph() {}
258		/**
259		* Check that the currently asserted disequalities that have not been split on
260		* are still true in the current model.
261		*/
262		void checkDisequalities(std::vector<Node>& lemmas);
263		/**
264		* Return true if a < b is entailed by the current set of assertions.
265		*
266		* @param a
267		* @param b
268		*
269		* @return
270		*/
271		bool isLessThan(TNode a, TNode b);
272		/**
273		* Returns true if the term has a value in the model (i.e. if we have seen it)
274		*
275		* @param a
276		*
277		* @return
278		*/
279		bool hasValueInModel(TNode a) const;
280		/**
281		* Return the value of a in the current model.
282		*
283		* @param a
284		*
285		* @return
286		*/
287		BitVector getValueInModel(TNode a) const;
288
289		void getAllValuesInModel(std::vector<Node>& assignments);
290		};
291
292		}
293		}
294		} // namespace cvc5
295
296		#endif /* CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H */