CVC3
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes

CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference

Collaboration diagram for CVC3::TheoryArithOld::DifferenceLogicGraph:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes


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(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), 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.

References CVC3::Expr::begin().

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

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

Definition at line 750 of file theory_arith_old.h.

The arithmetic that's using this graph

Definition at line 753 of file theory_arith_old.h.

Referenced by setArith().

The core theory

Definition at line 756 of file theory_arith_old.h.

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.

Graph of <= paths

Definition at line 774 of file theory_arith_old.h.

List of vertices adjacent backwards to a vertex

Definition at line 779 of file theory_arith_old.h.

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.

Definition at line 873 of file theory_arith_old.h.


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