CVC3
|
Classes | |
struct | EdgeInfo |
class | EpsRational |
Public Member Functions | |
void | getEdgeTheorems (const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems) |
EpsRational | getEdgeWeight (const Expr &x, const Expr &y) |
bool | hasIncoming (const Expr &x) |
bool | hasOutgoing (const Expr &x) |
void | writeGraph (std::ostream &out) |
void | getVariables (std::vector< Expr > &variables) |
void | setRules (ArithProofRules *rules) |
void | setArith (TheoryArithOld *arith) |
DifferenceLogicGraph (TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context) | |
~DifferenceLogicGraph () | |
Theorem | getUnsatTheorem () |
bool | isUnsat () |
void | computeModel () |
Rational | getValuation (const Expr &x) |
void | addEdge (const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm) |
bool | existsEdge (const Expr &x, const Expr &y) |
bool | inCycle (const Expr &x) |
void | expandSharedTerm (const Expr &x) |
Protected Types | |
typedef CDMap< Expr, EdgeInfo > | Graph |
typedef ExprMap< CDList< Expr > * > | EdgesList |
Protected Member Functions | |
Graph::ElementReference | getEdge (const Expr &x, const Expr &y) |
bool | tryUpdate (const Expr &x, const Expr &y, const Expr &z) |
void | analyseConflict (const Expr &x, int kind) |
Protected Attributes | |
const int * | d_pathLenghtThres |
TheoryArithOld * | arith |
TheoryCore * | core |
ArithProofRules * | rules |
CDO< Theorem > | unsat_theorem |
CDO< Rational > | biggestEpsilon |
CDO< Rational > | smallestPathDifference |
Graph | leGraph |
EdgesList | incomingEdges |
EdgesList | outgoingEdges |
CDMap< Expr, bool > | varInCycle |
Expr | sourceVertex |
Definition at line 456 of file theory_arith_old.h.
|
protected |
The graph itself, maps expressions (x-y) to the edge information
Definition at line 771 of file theory_arith_old.h.
|
protected |
Definition at line 776 of file theory_arith_old.h.
TheoryArithOld::DifferenceLogicGraph::DifferenceLogicGraph | ( | TheoryArithOld * | arith, |
TheoryCore * | core, | ||
ArithProofRules * | rules, | ||
Context * | context | ||
) |
Class constructor.
Definition at line 4711 of file theory_arith_old.cpp.
TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph | ( | ) |
Destructor
Definition at line 5024 of file theory_arith_old.cpp.
References CVC3::ExprMap< Data >::begin().
void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems | ( | const Expr & | x, |
const Expr & | y, | ||
const EdgeInfo & | edgeInfo, | ||
std::vector< Theorem > & | outputTheorems | ||
) |
Given two vertices in the graph and an path edge, reconstruct all the theorems and put them in the output vector
Definition at line 4888 of file theory_arith_old.cpp.
References DebugAssert, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::int2string(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::Expr::toString(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), and TRACE.
Referenced by CVC3::TheoryArithOld::tryPropagate().
TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::getEdgeWeight | ( | const Expr & | x, |
const Expr & | y | ||
) |
Returns the current weight of the edge.
Definition at line 4778 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length.
Referenced by CVC3::TheoryArithOld::computeTermBounds().
bool TheoryArithOld::DifferenceLogicGraph::hasIncoming | ( | const Expr & | x | ) |
Returns whether a vertex has incoming edges.
Definition at line 5809 of file theory_arith_old.cpp.
References CVC3::CDList< T >::size().
Referenced by CVC3::TheoryArithOld::computeTermBounds(), and CVC3::TheoryArithOld::isUnconstrained().
bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing | ( | const Expr & | x | ) |
Returns whether a vertex has outgoing edges.
Definition at line 5827 of file theory_arith_old.cpp.
References CVC3::CDList< T >::size().
Referenced by CVC3::TheoryArithOld::computeTermBounds(), and CVC3::TheoryArithOld::isUnconstrained().
|
protected |
Returns the edge (path) info for the given kind
x | the starting vertex |
y | the ending vertex |
Definition at line 4748 of file theory_arith_old.cpp.
References CVC3::CDOmap< Key, Data, HashFcn >::get(), and CVC3::CDList< T >::push_back().
|
protected |
Try to update the shortest path from x to z using y.
Definition at line 4927 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::getType(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::Expr::toString(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), and TRACE.
void TheoryArithOld::DifferenceLogicGraph::writeGraph | ( | std::ostream & | out | ) |
Definition at line 5872 of file theory_arith_old.cpp.
References std::endl(), CVC3::CDList< T >::size(), and CVC3::Expr::toString().
Referenced by CVC3::TheoryArithOld::computeTermBounds().
void TheoryArithOld::DifferenceLogicGraph::getVariables | ( | std::vector< Expr > & | variables | ) |
Fills the vector with all the variables (vertices) in the graph
Definition at line 5842 of file theory_arith_old.cpp.
Referenced by CVC3::TheoryArithOld::computeTermBounds().
|
inline |
Definition at line 806 of file theory_arith_old.h.
References rules.
Referenced by CVC3::TheoryArithOld::TheoryArithOld().
|
inline |
Definition at line 810 of file theory_arith_old.h.
References arith.
Referenced by CVC3::TheoryArithOld::TheoryArithOld().
Theorem TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem | ( | ) |
Returns the reference to the unsat theorem if there is a negative cycle in the graph.
Definition at line 4724 of file theory_arith_old.cpp.
bool TheoryArithOld::DifferenceLogicGraph::isUnsat | ( | ) |
Returns true if there is a negative cycle in the graph.
Definition at line 4728 of file theory_arith_old.cpp.
void TheoryArithOld::DifferenceLogicGraph::computeModel | ( | ) |
Definition at line 5111 of file theory_arith_old.cpp.
References CVC3::Expr::begin(), and CVC3::Theorem::getExpr().
Referenced by CVC3::TheoryArithOld::assignVariables().
Definition at line 5150 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::Expr::getRational(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::isRational(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryArithOld::assignVariables().
void TheoryArithOld::DifferenceLogicGraph::addEdge | ( | const Expr & | x, |
const Expr & | y, | ||
const Rational & | c, | ||
const Theorem & | edge_thm | ||
) |
Adds an edge corresponding to the constraint x - y <= c.
x | variable x::Difference |
y | variable y |
c | rational c |
edge_thm | the theorem for this edge |
Definition at line 4788 of file theory_arith_old.cpp.
References DebugAssert, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::LT, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::CDList< T >::size(), CVC3::Expr::toString(), and TRACE.
Check if there is an edge from x to y
Definition at line 4732 of file theory_arith_old.cpp.
References CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined().
bool TheoryArithOld::DifferenceLogicGraph::inCycle | ( | const Expr & | x | ) |
Check if x is in a cycle
Definition at line 4744 of file theory_arith_old.cpp.
Referenced by CVC3::TheoryArithOld::computeTermBounds().
void TheoryArithOld::DifferenceLogicGraph::expandSharedTerm | ( | const Expr & | x | ) |
Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides).
Definition at line 5020 of file theory_arith_old.cpp.
|
protected |
Produced the unsat theorem from a cycle x –> x of negative length
x | the variable to use for the conflict |
kind | the kind of edges to consider |
Definition at line 4907 of file theory_arith_old.cpp.
References DebugAssert, CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::int2string(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), and TRACE.
|
protected |
Threshold on path length to process (ignore bigger than and set incomplete)
Definition at line 750 of file theory_arith_old.h.
|
protected |
The arithmetic that's using this graph
Definition at line 753 of file theory_arith_old.h.
Referenced by setArith().
|
protected |
The core theory
Definition at line 756 of file theory_arith_old.h.
|
protected |
The arithmetic that is using u us
Definition at line 759 of file theory_arith_old.h.
Referenced by setRules().
The unsat theorem if available
Definition at line 762 of file theory_arith_old.h.
The biggest epsilon from EpsRational we used in paths
Definition at line 765 of file theory_arith_old.h.
The smallest rational difference we used in path relaxation
Definition at line 768 of file theory_arith_old.h.
|
protected |
Graph of <= paths
Definition at line 774 of file theory_arith_old.h.
|
protected |
List of vertices adjacent backwards to a vertex
Definition at line 779 of file theory_arith_old.h.
|
protected |
List of vertices adjacent forward to a vertex
Definition at line 781 of file theory_arith_old.h.
Whether the variable is in a cycle
Definition at line 871 of file theory_arith_old.h.
|
protected |
Definition at line 873 of file theory_arith_old.h.