CVC3  2.4.1
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference

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, EdgeInfoGraph
 
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
 
TheoryArithOldarith
 
TheoryCorecore
 
ArithProofRulesrules
 
CDO< Theoremunsat_theorem
 
CDO< RationalbiggestEpsilon
 
CDO< RationalsmallestPathDifference
 
Graph leGraph
 
EdgesList incomingEdges
 
EdgesList outgoingEdges
 
CDMap< Expr, bool > varInCycle
 
Expr sourceVertex
 

Detailed Description

Definition at line 456 of file theory_arith_old.h.

Member Typedef Documentation

The graph itself, maps expressions (x-y) to the edge information

Definition at line 771 of file theory_arith_old.h.

Definition at line 776 of file theory_arith_old.h.

Constructor & Destructor Documentation

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().

Member Function Documentation

void TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems ( const Expr x,
const Expr y,
const EdgeInfo edgeInfo,
std::vector< Theorem > &  outputTheorems 
)
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().

TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference TheoryArithOld::DifferenceLogicGraph::getEdge ( const Expr x,
const Expr y 
)
protected

Returns the edge (path) info for the given kind

Parameters
xthe starting vertex
ythe ending vertex
Returns
the edge information

Definition at line 4748 of file theory_arith_old.cpp.

References CVC3::CDOmap< Key, Data, HashFcn >::get(), and CVC3::CDList< T >::push_back().

bool TheoryArithOld::DifferenceLogicGraph::tryUpdate ( const Expr x,
const Expr y,
const Expr z 
)
protected
void TheoryArithOld::DifferenceLogicGraph::writeGraph ( std::ostream &  out)
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().

void CVC3::TheoryArithOld::DifferenceLogicGraph::setRules ( ArithProofRules rules)
inline

Definition at line 806 of file theory_arith_old.h.

References rules.

Referenced by CVC3::TheoryArithOld::TheoryArithOld().

void CVC3::TheoryArithOld::DifferenceLogicGraph::setArith ( TheoryArithOld arith)
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.

Returns
the unsat theorem

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 ( )
Rational TheoryArithOld::DifferenceLogicGraph::getValuation ( const Expr x)
void TheoryArithOld::DifferenceLogicGraph::addEdge ( const Expr x,
const Expr y,
const Rational c,
const Theorem edge_thm 
)
bool TheoryArithOld::DifferenceLogicGraph::existsEdge ( const Expr x,
const Expr y 
)

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.

void TheoryArithOld::DifferenceLogicGraph::analyseConflict ( const Expr x,
int  kind 
)
protected

Produced the unsat theorem from a cycle x –> x of negative length

Parameters
xthe variable to use for the conflict
kindthe 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.

Member Data Documentation

const int* CVC3::TheoryArithOld::DifferenceLogicGraph::d_pathLenghtThres
protected

Threshold on path length to process (ignore bigger than and set incomplete)

Definition at line 750 of file theory_arith_old.h.

TheoryArithOld* CVC3::TheoryArithOld::DifferenceLogicGraph::arith
protected

The arithmetic that's using this graph

Definition at line 753 of file theory_arith_old.h.

Referenced by setArith().

TheoryCore* CVC3::TheoryArithOld::DifferenceLogicGraph::core
protected

The core theory

Definition at line 756 of file theory_arith_old.h.

ArithProofRules* CVC3::TheoryArithOld::DifferenceLogicGraph::rules
protected

The arithmetic that is using u us

Definition at line 759 of file theory_arith_old.h.

Referenced by setRules().

CDO<Theorem> CVC3::TheoryArithOld::DifferenceLogicGraph::unsat_theorem
protected

The unsat theorem if available

Definition at line 762 of file theory_arith_old.h.

CDO<Rational> CVC3::TheoryArithOld::DifferenceLogicGraph::biggestEpsilon
protected

The biggest epsilon from EpsRational we used in paths

Definition at line 765 of file theory_arith_old.h.

CDO<Rational> CVC3::TheoryArithOld::DifferenceLogicGraph::smallestPathDifference
protected

The smallest rational difference we used in path relaxation

Definition at line 768 of file theory_arith_old.h.

Graph CVC3::TheoryArithOld::DifferenceLogicGraph::leGraph
protected

Graph of <= paths

Definition at line 774 of file theory_arith_old.h.

EdgesList CVC3::TheoryArithOld::DifferenceLogicGraph::incomingEdges
protected

List of vertices adjacent backwards to a vertex

Definition at line 779 of file theory_arith_old.h.

EdgesList CVC3::TheoryArithOld::DifferenceLogicGraph::outgoingEdges
protected

List of vertices adjacent forward to a vertex

Definition at line 781 of file theory_arith_old.h.

CDMap<Expr, bool> CVC3::TheoryArithOld::DifferenceLogicGraph::varInCycle
protected

Whether the variable is in a cycle

Definition at line 871 of file theory_arith_old.h.

Expr CVC3::TheoryArithOld::DifferenceLogicGraph::sourceVertex
protected

Definition at line 873 of file theory_arith_old.h.


The documentation for this class was generated from the following files: