CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference

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 4724 of file theory_arith_old.cpp.

TheoryArithOld::DifferenceLogicGraph::~DifferenceLogicGraph (  ) 

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 
)
bool TheoryArithOld::DifferenceLogicGraph::hasIncoming ( const Expr x  ) 
bool TheoryArithOld::DifferenceLogicGraph::hasOutgoing ( const Expr x  ) 

Returns whether a vertex has outgoing edges.

Definition at line 5838 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), outgoingEdges, and CVC3::CDList< T >::size().

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

TheoryArithOld::DifferenceLogicGraph::Graph::ElementReference TheoryArithOld::DifferenceLogicGraph::getEdge ( const Expr x,
const Expr y 
) [protected]
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 5853 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::end(), incomingEdges, outgoingEdges, and sourceVertex.

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

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

Definition at line 806 of file theory_arith_old.h.

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

void CVC3::TheoryArithOld::DifferenceLogicGraph::setArith ( TheoryArithOld arith  )  [inline]

Definition at line 810 of file theory_arith_old.h.

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 4737 of file theory_arith_old.cpp.

References unsat_theorem.

Referenced by CVC3::TheoryArithOld::addToBuffer(), and isUnsat().

bool TheoryArithOld::DifferenceLogicGraph::isUnsat (  ) 

Returns true if there is a negative cycle in the graph.

Definition at line 4741 of file theory_arith_old.cpp.

References getUnsatTheorem(), and CVC3::Theorem::isNull().

Referenced by addEdge(), CVC3::TheoryArithOld::addToBuffer(), and tryUpdate().

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 
)
bool TheoryArithOld::DifferenceLogicGraph::inCycle ( const Expr x  ) 
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 5033 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:
x the variable to use for the conflict
kind the kind of edges to consider

Definition at line 4920 of file theory_arith_old.cpp.

References CVC3::ArithProofRules::cycleConflict(), DebugAssert, CVC3::CDOmap< Key, Data, HashFcn >::get(), getEdge(), getEdgeTheorems(), CVC3::int2string(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), rules, CVC3::TRACE, and unsat_theorem.

Referenced by tryUpdate().


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.

Referenced by tryUpdate().

The arithmetic that's using this graph

Definition at line 753 of file theory_arith_old.h.

Referenced by addEdge(), computeModel(), getValuation(), and tryUpdate().

The core theory

Definition at line 756 of file theory_arith_old.h.

Referenced by addEdge(), computeModel(), getEdge(), and tryUpdate().

The arithmetic that is using u us

Definition at line 759 of file theory_arith_old.h.

Referenced by analyseConflict(), and tryUpdate().

The unsat theorem if available

Definition at line 762 of file theory_arith_old.h.

Referenced by analyseConflict(), and getUnsatTheorem().

The biggest epsilon from EpsRational we used in paths

Definition at line 765 of file theory_arith_old.h.

Referenced by addEdge(), getValuation(), and tryUpdate().

The smallest rational difference we used in path relaxation

Definition at line 768 of file theory_arith_old.h.

Referenced by addEdge(), getValuation(), and tryUpdate().

Graph of <= paths

Definition at line 774 of file theory_arith_old.h.

Referenced by existsEdge(), and getEdge().

List of vertices adjacent backwards to a vertex

Definition at line 779 of file theory_arith_old.h.

Referenced by addEdge(), computeModel(), getEdge(), getVariables(), hasIncoming(), writeGraph(), and ~DifferenceLogicGraph().

List of vertices adjacent forward to a vertex

Definition at line 781 of file theory_arith_old.h.

Referenced by addEdge(), computeModel(), getEdge(), getVariables(), hasOutgoing(), and ~DifferenceLogicGraph().

Whether the variable is in a cycle

Definition at line 871 of file theory_arith_old.h.

Referenced by addEdge(), inCycle(), and tryUpdate().


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

Generated on 19 Apr 2010 for CVC3 by  doxygen 1.6.1