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 4957 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::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::Expr::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 4847 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 5878 of file theory_arith_old.cpp.

References CVC3::CDList< T >::size().

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

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

Returns whether a vertex has outgoing edges.

Definition at line 5896 of file theory_arith_old.cpp.

References 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 4817 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]`

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

Definition at line 4996 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::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::Expr::toString(), and TRACE.

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

Definition at line 5941 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 5911 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 4793 of file theory_arith_old.cpp.

bool TheoryArithOld::DifferenceLogicGraph::isUnsat ( )

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

Definition at line 4797 of file theory_arith_old.cpp.

void TheoryArithOld::DifferenceLogicGraph::computeModel ( )

Definition at line 5180 of file theory_arith_old.cpp.

References CVC3::Expr::begin(), and CVC3::Theorem::getExpr().

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

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

Definition at line 5219 of file theory_arith_old.cpp.

References CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::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.

Parameters:

x	variable x::Difference
y	variable y
c	rational c
edge_thm	the theorem for this edge

Definition at line 4857 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 >::push_back(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), and TRACE.

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

Check if there is an edge from x to y

Definition at line 4801 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 4813 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 5089 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 4976 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:

CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference

Classes

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation