CVC3::TheoryArithOld::DifferenceLogicGraph

CVC3::TheoryArithOld::DifferenceLogicGraph Class Reference

Collaboration diagram for CVC3::TheoryArithOld::DifferenceLogicGraph:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Classes

Detailed Description

Definition at line 456 of file theory_arith_old.h.

Member Typedef Documentation

typedef CDMap<Expr, EdgeInfo> CVC3::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::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(), incomingEdges, and 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.

References DebugAssert, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, getEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, sourceVertex, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by analyseConflict(), CVC3::TheoryArithOld::tryPropagate(), and 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 existsEdge(), CVC3::CDOmap< Key, Data, HashFcn >::get(), getEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, and CVC3::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(), incomingEdges, CVC3::Expr::isNull(), CVC3::CDList< T >::size(), and 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(), 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 core, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::CDOmap< Key, Data, HashFcn >::get(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::TheoryCore::getResource(), incomingEdges, leGraph, and outgoingEdges.

Referenced by addEdge(), analyseConflict(), getEdgeTheorems(), getEdgeWeight(), getValuation(), and 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.

References CVC3::ArithProofRules::addInequalities(), analyseConflict(), arith, biggestEpsilon, core, d_pathLenghtThres, CVC3::TheoryCore::enqueueFact(), existsEdge(), getEdge(), getEdgeTheorems(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::getType(), CVC3::ArithProofRules::implyEqualities(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::in_path_vertex, CVC3::TheoryArith::intType(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), isUnsat(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::TheoryCore::okToEnqueue(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, rules, smallestPathDifference, sourceVertex, CVC3::Expr::toString(), CVC3::TRACE, CVC3::TheoryArithOld::tryPropagate(), varInCycle, and CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::Zero.

Referenced by 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(), 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(), 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.

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

Definition at line 5124 of file theory_arith_old.cpp.

References addEdge(), arith, CVC3::ExprMap< Data >::begin(), core, CVC3::ExprMap< Data >::end(), existsEdge(), CVC3::Theory::find(), CVC3::Theory::getCommonRules(), CVC3::Theorem::getRHS(), incomingEdges, CVC3::Expr::isNull(), outgoingEdges, sourceVertex, CVC3::CommonProofRules::varIntroSkolem(), and CVC3::TheoryArithOld::zero.

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

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

Definition at line 5163 of file theory_arith_old.cpp.

References arith, biggestEpsilon, getEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, smallestPathDifference, sourceVertex, CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoryArithOld::zero.

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

References arith, biggestEpsilon, core, DebugAssert, existsEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::explanation, CVC3::Theory::find(), CVC3::CDOmap< Key, Data, HashFcn >::get(), getEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, incomingEdges, CVC3::Theorem::isAssump(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::isDefined(), CVC3::Theorem::isNull(), isUnsat(), CVC3::LE, CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::length, CVC3::LT, outgoingEdges, CVC3::TheoryCore::outOfResources(), CVC3::TheoryArithOld::DifferenceLogicGraph::EdgeInfo::path_length_in_edges, CVC3::CDList< T >::size(), smallestPathDifference, CVC3::Expr::toString(), CVC3::TRACE, tryUpdate(), varInCycle, and CVC3::TheoryArithOld::zero.

Referenced by CVC3::TheoryArithOld::addToBuffer(), and 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(), and leGraph.

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

Referenced by tryUpdate().

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.

Referenced by tryUpdate().

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 addEdge(), computeModel(), getValuation(), setArith(), and tryUpdate().

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

The core theory

Definition at line 756 of file theory_arith_old.h.

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

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 analyseConflict(), setRules(), and tryUpdate().

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

The unsat theorem if available

Definition at line 762 of file theory_arith_old.h.

Referenced by analyseConflict(), and getUnsatTheorem().

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.

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

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.

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

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

Graph of <= paths

Definition at line 774 of file theory_arith_old.h.

Referenced by existsEdge(), and getEdge().

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

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

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

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

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.

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

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

Definition at line 873 of file theory_arith_old.h.

Referenced by computeModel(), getEdgeTheorems(), getValuation(), getVariables(), hasIncoming(), and tryUpdate().

The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:16:38 2009 for CVC3 by  doxygen 1.5.2