#include <unification.h>
Public Member Functions | |
Unification (Configuration *configuration, Parser *parser) | |
void | run () |
Node * | ApplyR0 (Node *start=NULL) |
bool | tryApplyR1 () |
bool | tryApplyR2 () |
bool | tryApplyR3 () |
bool | tryApplyR4 () |
bool | tryApplyR5 () |
Node * | SetDisjunctiveSystem (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 | |
Configuration * | configuration |
Parser * | parser |
bool | result |
list< Solution * > | solutions |
Definition at line 41 of file unification.h.
Unification::Unification | ( | Configuration * | configuration, | |
Parser * | parser | |||
) |
Definition at line 18 of file unification.cpp.
Unification::~Unification | ( | ) |
Definition at line 1906 of file unification.cpp.
void Unification::run | ( | ) |
Run unification
Definition at line 1785 of file unification.cpp.
References ApplyR0(), Display::beep(), Configuration::beep, checkDefinition(), Parser::checkSoundness(), configuration, debugDisplay(), Configuration::disjonction, Display::displayTime(), Parser::fonctiontab, globconfig, Configuration::LATEX, mycout, Node::ndterms, Parser::numericalvariabletab, parser, Configuration::pauseEveryStep, Configuration::printRule, Parser::result, result, SetDisjunctiveSystem(), Display::texDi(), Display::texEndl(), tryApplyR1(), tryApplyR2(), tryApplyR3(), tryApplyR4(), tryApplyR5(), Parser::variabletab, and Configuration::writeMode.
Referenced by main().
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().
bool Unification::tryApplyR1 | ( | ) |
Application of rules R1 (basic unification rules)
Definition at line 277 of file unification.cpp.
References And::branchs, configuration, Node::containVar(), NodeIterator::DEPTH_FIRST, Variable::id, Node::isEqual(), Configuration::LATEX, mycout, Equal::n1, Equal::n2, NodeIterator::next(), parser, Configuration::printRule, Node::replace(), NodeIterator::replaceBy(), NodeIterator::reset(), Parser::result, Display::texEndl(), Display::texHspace(), and Configuration::writeMode.
Referenced by run().
bool Unification::tryApplyR2 | ( | ) |
Application of rules R2 (Unfold 1)
Definition at line 496 of file unification.cpp.
References And::addBranch(), And::addCondition(), Expo::buildOne(), configuration, NodeIterator::DEPTH_FIRST, Expo::duplicate(), Node::duplicate(), NumericalVar::duplicate(), Expo::expNum, Expo::free, Parser::genNumericalValName(), Node::holePosition, Configuration::LATEX, mycout, Expo::n1, Equal::n1, Equal::n2, Configuration::NcanbeZero, NodeIterator::next(), parser, Configuration::printRule, NodeIterator::replaceBy(), Parser::result, Display::texHspace(), Expo::var, and Configuration::writeMode.
Referenced by run().
bool Unification::tryApplyR3 | ( | ) |
Application of rules R3 (Unfold 2)
Definition at line 662 of file unification.cpp.
References Or::addBranch(), And::addBranch(), And::addCondition(), Node::buildOneAndReplace(), configuration, NodeIterator::DEPTH_FIRST, And::duplicate(), Expo::duplicate(), Node::duplicate(), gcd(), Parser::genNumericalValName(), NodeIterator::getPosition(), Node::holePosition, Configuration::LATEX, mycout, Equal::n1, Equal::n2, Configuration::NcanbeZero, NodeIterator::next(), parser, prefix(), Configuration::printRule, NodeIterator::replaceBy(), Parser::result, Display::texHspace(), and Configuration::writeMode.
Referenced by run().
bool Unification::tryApplyR4 | ( | ) |
Application of rules R4 (Unfold 3)
Definition at line 896 of file unification.cpp.
References Or::addBranch(), And::addBranch(), And::addCondition(), append(), Or::branchs, And::conditions, configuration, NodeIterator::DEPTH_FIRST, Expo::duplicate(), Expo::expNum, Parser::genNumericalValName(), NodeIterator::getPosition(), Node::holePosition, Configuration::LATEX, mycout, Equal::n1, Equal::n2, Configuration::NcanbeZero, NodeIterator::next(), parser, prefix(), Configuration::printRule, NodeIterator::replaceBy(), Parser::result, Display::texHspace(), Expo::var, and Configuration::writeMode.
Referenced by run().
bool Unification::tryApplyR5 | ( | ) |
Application of rules R5 (Decompose 2)
Definition at line 1100 of file unification.cpp.
References Or::addBranch(), And::addBranch(), And::addCondition(), Or::branchs, Node::buildOneAndReplace(), configuration, NodeIterator::DEPTH_FIRST, Expo::duplicate(), NumericalVar::duplicate(), Node::duplicate(), Function::duplicate(), Expo::expNum, Node::find(), Expo::free, Parser::genContstantValName(), Parser::genNumericalValName(), NodeIterator::getPosition(), Configuration::LATEX, mycout, Equal::n1, Equal::n2, Configuration::NcanbeZero, NodeIterator::next(), parser, Configuration::printRule, NodeIterator::replaceBy(), Parser::result, Display::texHspace(), Expo::var, and Configuration::writeMode.
Referenced by run().
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().
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().
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().
bool Unification::exploDefinition | ( | Node * | n, | |
SimpleSolution * | solution | |||
) |
Explore and check definition (is the current system well define variables)
Definition at line 1320 of file unification.cpp.
References Function::arguments, And::branchs, And::conditions, VariableSolution::definitionc, Expo::free, Variable::id, NumericalVar::id, Expo::n1, Equal::n1, Expo::n2, Equal::n2, SimpleSolution::numericalvariableSolution, VariableSolution::seeoutside, Expo::var, and SimpleSolution::variableSolution.
Referenced by checkDefinition().
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().
int Unification::gcd | ( | unsigned int | a, | |
unsigned int | b | |||
) | [static] |
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] |
Definition at line 44 of file unification.h.
Referenced by Solver::Graph::addVertex(), checkDefinition(), Display::displayResult(), Solver::Graph::explo(), run(), Solver::Graph::run(), tryApplyR1(), tryApplyR2(), tryApplyR3(), tryApplyR4(), and tryApplyR5().
Definition at line 45 of file unification.h.
Referenced by ApplyR0(), checkDefinition(), debugDisplay(), SimpleSolution::display(), Solver::SolverSolution::display(), Solver::Graph::Graph(), run(), SetDisjunctiveSystem(), tryApplyR1(), tryApplyR2(), tryApplyR3(), tryApplyR4(), and tryApplyR5().
bool Unification::result |
list<Solution*> Unification::solutions |
Definition at line 48 of file unification.h.
Referenced by checkDefinition(), and Display::displayResult().