CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph Class Reference

Collaboration diagram for CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph:

[legend]

List of all members.

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

Detailed Description

Definition at line 456 of file theory_arith_old.h.

Member Typedef Documentation

typedef CDMap<Expr, EdgeInfo> CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::Graph [protected]

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

Definition at line 771 of file theory_arith_old.h.

typedef ExprMap<CDList<Expr>*> CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::EdgesList [protected]

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

Destructor

Definition at line 5037 of file theory_arith_old.cpp.

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

Member Function Documentation

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

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), CVC3::TheoryArithOld::tryPropagate(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

TheoryArithOld::DifferenceLogicGraph::EpsRational TheoryArithOld::DifferenceLogicGraph::getEdgeWeight	(	const Expr &	x,
		const Expr &	y
	)

Returns the current weight of the edge.

Definition at line 4791 of file theory_arith_old.cpp.

References CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::existsEdge(), CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EpsRational::PlusInfinity.

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

bool TheoryArithOld::DifferenceLogicGraph::hasIncoming ( const Expr & x )

Returns whether a vertex has incoming edges.

Definition at line 5820 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::incomingEdges, CVC3::Expr::isNull(), CVC3::CDList< T >::size(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::sourceVertex.

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

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(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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]`

Returns the edge (path) info for the given kind

Parameters:

	x	the starting vertex
	y	the ending vertex

Returns:: the edge information

Definition at line 4761 of file theory_arith_old.cpp.

References CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::core, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::TheoryCore::getResource(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::incomingEdges, CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::leGraph, CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::outgoingEdges, and CVC3::CDList< T >::push_back().

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getValuation(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

bool TheoryArithOld::DifferenceLogicGraph::tryUpdate	(	const Expr &	x,
		const Expr &	y,
		const Expr &	z
	)			`[protected]`

Try to update the shortest path from x to z using y.

Definition at line 4940 of file theory_arith_old.cpp.

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

void TheoryArithOld::DifferenceLogicGraph::writeGraph ( std::ostream & out )

Definition at line 5883 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::end(), std::endl(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::incomingEdges, 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 5853 of file theory_arith_old.cpp.

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

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

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

Definition at line 806 of file theory_arith_old.h.

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

void CVC3::TheoryArithOld::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 CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::unsat_theorem.

Referenced by CVC3::TheoryArithOld::addToBuffer(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::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 CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem(), and CVC3::Theorem::isNull().

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

void TheoryArithOld::DifferenceLogicGraph::computeModel ( )

Definition at line 5124 of file theory_arith_old.cpp.

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

Rational TheoryArithOld::DifferenceLogicGraph::getValuation ( const Expr & x )

Definition at line 5163 of file theory_arith_old.cpp.

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.

Parameters:

	x	variable x::Difference
	y	variable y
	c	rational c
	kind	the kind of inequality (LE or LT)
	edge_thm	the theorem for this edge

Definition at line 4801 of file theory_arith_old.cpp.

Referenced by CVC3::TheoryArithOld::addToBuffer(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel().

bool TheoryArithOld::DifferenceLogicGraph::existsEdge	(	const Expr &	x,
		const Expr &	y
	)

Check if there is an edge from x to y

Definition at line 4745 of file theory_arith_old.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::leGraph.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeWeight(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

bool TheoryArithOld::DifferenceLogicGraph::inCycle ( const Expr & x )

Check if x is in a cycle

Definition at line 4757 of file theory_arith_old.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::varInCycle.

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 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(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::int2string(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::rules, CVC3::TRACE, and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::unsat_theorem.

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

Member Data Documentation

const int* CVC3::TheoryArithOld::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.

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

TheoryArithOld* CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::arith [protected]

The arithmetic that's using this graph

Definition at line 753 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getValuation(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

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

The core theory

Definition at line 756 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

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

The arithmetic that is using u us

Definition at line 759 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

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

The unsat theorem if available

Definition at line 762 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getUnsatTheorem().

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

The biggest epsilon from EpsRational we used in paths

Definition at line 765 of file theory_arith_old.h.

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

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

The smallest rational difference we used in path relaxation

Definition at line 768 of file theory_arith_old.h.

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

Graph CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::leGraph [protected]

Graph of <= paths

Definition at line 774 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::existsEdge(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdge().

EdgesList CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::incomingEdges [protected]

List of vertices adjacent backwards to a vertex

Definition at line 779 of file theory_arith_old.h.

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

EdgesList CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::outgoingEdges [protected]

List of vertices adjacent forward to a vertex

Definition at line 781 of file theory_arith_old.h.

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

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

Whether the variable is in a cycle

Definition at line 872 of file theory_arith_old.h.

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

Expr CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::sourceVertex [protected]

Definition at line 874 of file theory_arith_old.h.

Referenced by CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::getVariables(), CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::hasIncoming(), and CVC3::TheoryArithOld::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

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