summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_inequality_graph.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r--src/theory/bv/bv_inequality_graph.h297
1 files changed, 0 insertions, 297 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
deleted file mode 100644
index ba545e48b..000000000
--- a/src/theory/bv/bv_inequality_graph.h
+++ /dev/null
@@ -1,297 +0,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"
-#include "util/bitvector.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 cgit on debian on lair
contact matthew@masot.net with questions or feedback