Unification Class Reference

#include <unification.h>

Collaboration diagram for Unification:

Collaboration graph
[legend]

List of all members.

Public Member Functions

 Unification (Configuration *configuration, Parser *parser)
void run ()
NodeApplyR0 (Node *start=NULL)
bool tryApplyR1 ()
bool tryApplyR2 ()
bool tryApplyR3 ()
bool tryApplyR4 ()
bool tryApplyR5 ()
NodeSetDisjunctiveSystem (Node *start=NULL)
bool checkDefinition ()
void debugDisplay (ostream &s)
bool exploDefinition (Node *n, SimpleSolution *solution)
bool verifValidPresburger (Node *n)
 ~Unification ()

Static Public Member Functions

static int gcd (unsigned int a, unsigned int b)
static bool prefix (const list< unsigned int > &l1, const list< unsigned int > &l2)
static list< unsigned int > append (const list< unsigned int > &l1, const list< unsigned int > &l2)

Public Attributes

Configurationconfiguration
Parserparser
bool result
list< Solution * > solutions


Detailed Description

Definition at line 41 of file unification.h.


Constructor & Destructor Documentation

Unification::Unification ( Configuration configuration,
Parser parser 
)

Definition at line 18 of file unification.cpp.

Unification::~Unification (  ) 

Definition at line 1906 of file unification.cpp.


Member Function Documentation

void Unification::run (  ) 

Node * Unification::ApplyR0 ( Node start = NULL  ) 

Application of rules R0 (simplification)

Definition at line 138 of file unification.cpp.

References Or::branchs, And::branchs, And::conditions, NodeIterator::DEPTH_FIRST, NodeIterator::next(), parser, NodeIterator::replaceBy(), Parser::result, and NodeIterator::setUnderEqual().

Referenced by run(), and SetDisjunctiveSystem().

Here is the call graph for this function:

bool Unification::tryApplyR1 (  ) 

bool Unification::tryApplyR2 (  ) 

bool Unification::tryApplyR3 (  ) 

bool Unification::tryApplyR4 (  ) 

bool Unification::tryApplyR5 (  ) 

Node * Unification::SetDisjunctiveSystem ( Node start = NULL  ) 

transformation in disjonctive normal form

Definition at line 56 of file unification.cpp.

References Or::addBranch(), And::addBranch(), And::addCondition(), ApplyR0(), NodeIterator::BREADTH_FIRST, NodeIterator::next(), parser, NodeIterator::replaceBy(), and Parser::result.

Referenced by run().

Here is the call graph for this function:

bool Unification::checkDefinition (  ) 

check all solutions (and delete the bad ones).

Definition at line 1664 of file unification.cpp.

References configuration, exploDefinition(), SimpleSolution::fail, Parser::numericalvariabletab, parser, Configuration::presBurgerVerif, Parser::result, solutions, Parser::variabletab, and verifValidPresburger().

Referenced by run().

Here is the call graph for this function:

void Unification::debugDisplay ( ostream &  s  ) 

display current state of the memory

Definition at line 27 of file unification.cpp.

References globconfig, Configuration::LATEX, parser, Node::print(), Parser::result, and Configuration::writeMode.

Referenced by run().

Here is the call graph for this function:

bool Unification::exploDefinition ( Node n,
SimpleSolution solution 
)

bool Unification::verifValidPresburger ( Node n  ) 

A function that verifies if a given solution is a real solution, ie. can be satisfied. We then list the solutions. If not, THIS is not a solution but there may be another one that is valid.

Definition at line 1424 of file unification.cpp.

References StatePara::actives, Groupe::autos, Automata::display(), NumericalVar::id, mycout, Condition::n1, ExploPara::statePara, and State::step.

Referenced by checkDefinition().

Here is the call graph for this function:

int Unification::gcd ( unsigned int  a,
unsigned int  b 
) [static]

Definition at line 618 of file unification.cpp.

Referenced by tryApplyR3().

bool Unification::prefix ( const list< unsigned int > &  l1,
const list< unsigned int > &  l2 
) [static]

is l1 a prefix of l2 ?

Definition at line 626 of file unification.cpp.

Referenced by tryApplyR3(), and tryApplyR4().

list< unsigned int > Unification::append ( const list< unsigned int > &  l1,
const list< unsigned int > &  l2 
) [static]

merging of l1 and l2

Definition at line 647 of file unification.cpp.

Referenced by tryApplyR4().


Member Data Documentation

Definition at line 46 of file unification.h.

Referenced by Display::displayResult(), and run().

Definition at line 48 of file unification.h.

Referenced by checkDefinition(), and Display::displayResult().


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

Generated on Thu Jun 19 19:14:38 2008 for unification by  doxygen 1.5.6