#include <implicative.hh>
Inherits QSpace.
Inheritance diagram for Implicative:
Public Member Functions | |
| Implicative (int ns, bool firstQ, int *nv, int prop) | |
| Default constructor for a restricted-quantified space. This is the first step for building a restricted-quantified space. The prefix is defined here. | |
| Implicative (Implicative &im) | |
| virtual | ~Implicative () |
| int | spaces () |
| Number of "rules" the quantified space contains. Returns the number of rules the quantified space contains. This is equal to the number of quantifier alternations in the prefix. | |
| void | QIntVar (int var, int min, int max) |
| Defines an integer variable in a quantified space. Defines an integer variable in the quantified space with an interval domain. | |
| void | QIntVar (int var, IntSet dom) |
| Defines an integer variable in the quantified space. Defines an integer variable in the quantifies space using a fully declared domain. | |
| void | QBoolVar (int var, int min, int max) |
| Defines a boolean variable in the quantified space. Defines a boolean variable in the quantified space, uning a min and a max domain value (with false < true). | |
| void | QBoolVar (int var) |
| Defines a boolean variable in the quantified space. Defines a boolean variable with a full initial domain in the quantified space. | |
| MySpace * | getRuleSpace (int sp) |
| Returns one of the restrictor space. Returns one of the restrictor space. Deprecated : use space() and nextScope instead for constraint posting. | |
| MySpace * | getGoalSpace () |
| Returns the goal space. Returns the goal space. Deprecated : use space() and nextScope instead for constraint posting. | |
| MySpace * | space () |
| Returns the current declarating space. Return the space we are currently declarating constraints in. nextScope() is used to set the nextspace as the current one. | |
| IntVar | var (int n) |
| Returns an integer variable from the space we are currently declaring. Returns an integer variable from the cpace we are currently declaring. If the variable had been declared as boolean, will return an integer variable with domain at most {0,1}. | |
| BoolVar | bvar (int n) |
| Returns a boolean variable from the space we are currently declaring. Returns a boolean variable from the space we are currently declaring. Will do strange things if the variable had been declared as integer. | |
| int | nextScope () |
| Switch to the next space for constraint declaration. Switches to the next space for constraint declaration. var, bvar and space methods will now refer to the next rule space (or to the goal space if the current space was the last rule one). Returns the new space number, or -1 if it was called while there was no next space to declare constraints in. | |
| void | makeStructure () |
| Finalizes the restricted-quantified space construction. Finalizes the restricted-quantified space construction. Must be invoked once all the variable and all the constraints have been declared, and before the search is performed on this space. | |
| virtual void | print () |
| Prints the current state of an implicative object. Prints the variable domains of all the spaces (if defined). Does not perform an ounce of propagation. | |
| virtual bool | quantification (int v) |
| Returns a variable quantificaion. Returns wether a variable is quantified existentially (false) or universally (true). | |
| virtual int | status (int var, unsigned long int &propsteps) |
| Returns the current partial status of the quantified space. Returns the current status of the quantified space, but limits the computation of this status at the variable given in parameter. So, this method will return "don't know" more often than a complete status computation. Returns 1 for "true", 0 for "false", and -1 for "Don't know, try a next variable". A "Don't know" answer while all the variables have been assigned can be considered as a "true". | |
| virtual int | finalStatus (unsigned long int &propsteps) |
| Returns the thuth value of a completely assigned problem. Performs the last checks to return in a complete way the truth value of the problem. All non-subsumes variables must be assigned for this method to be correct. | |
| virtual bool | subsumed (int var) |
| Returns wether a variable is subsumed or not. A variable is subsumed if it is assigned or it is bound by no more constraint. The answer must be correct, but not complete (so, a "not sure" must return False for the solver to remain correct. | |
| virtual Implicative * | clone () |
| virtual void | assign (int var, int **vals, int nbVals) |
| Assigns a value to a variable. assigns a value to a variable. Only this method will be used by the search engine. | |
| virtual void | remove (int var, int **vals, int nbVals) |
| virtual void | backtrack () |
| Method called when the solver backtracks to this quantified space. This method is useful to indicate some new information to the branchong heuristic, like simply updating the scores. | |
| virtual void | indicateBranchingHeuristic (BranchingHeuristic *bh) |
| Indicates the branching heuristic to be used when performing search. Indicates the branching heuristic to be used when performing search. This method is typically invoked by the solver at its construction. | |
Protected Member Functions | |
| int | cascade (int firstSpace, unsigned long int &propsteps) |
| Cascade propagation. | |
Protected Attributes | |
| bool * | q |
| Quantification of the variables (true for universal, false for existential). | |
| int | nbSpaces |
| Number of rule spaces. | |
| int | currentDeclareSpace |
| The rule space in which we are currently declaring constraints (for declaration part only). | |
| int * | nbVarBySpace |
| Number of variables by rule space. | |
| int * | whichSpaceOwns |
| Indicates in which space a given variable first appears. | |
| MySpace ** | rules |
| The rule spaces. | |
| MySpace * | goal |
| The goal space. | |
| bool * | varInitialised |
| Indicates wether a variable has been initialised or not (for declaration part only). | |
| bool * | ruleDefined |
| Indicates wether a rule space is defind or not. If not, it has a failed or solved value. | |
| int * | ruleStatus |
| Indicates wether a rule space is failed (0), solved (1), or not yet decided (-1). | |
| bool | goalDefined |
| Indicates wether the goal space is defined or not. | |
| int | goalStatus |
| Indicates wether the goal is failed, solved, or not yet decided. | |
| Warner * | w |
| int | prop_power |
Friends | |
| class | valueHeuristic |
Definition at line 38 of file implicative.hh.
| Implicative::Implicative | ( | int | ns, | |
| bool | firstQ, | |||
| int * | nv, | |||
| int | prop | |||
| ) |
Default constructor for a restricted-quantified space. This is the first step for building a restricted-quantified space. The prefix is defined here.
| ns | The number of scope i.e. the number of quantifier alternations in the prefix. | |
| firstQ | Must be set to true if the first quantifier is universal, false otherwise. | |
| nv | Array of integer which contains the number of variables by scope. | |
| prop | Propagation power (0 = UW, 1 = W, 2 = S, 3 = US) |
Definition at line 26 of file implicative.cc.
References currentDeclareSpace, goal, goalDefined, QSpace::n, nbSpaces, nbVarBySpace, prop_power, q, ruleDefined, rules, QSpace::v, varInitialised, and whichSpaceOwns.
Referenced by clone().
| Implicative::Implicative | ( | Implicative & | im | ) |
Copy constructor for a restricted-quantified space.
| im | The space we want to copy. |
Definition at line 62 of file implicative.cc.
References QSpace::n, nbSpaces, nbVarBySpace, prop_power, q, ruleDefined, rules, Warner::update(), varInitialised, w, and whichSpaceOwns.
| Implicative::~Implicative | ( | ) | [virtual] |
Destructor for a restricted-quantified space. This doesn't destruct the shared datastructures between a quantified space and its copy.
Definition at line 109 of file implicative.cc.
References goal, goalDefined, nbSpaces, ruleDefined, and rules.
| int Implicative::cascade | ( | int | firstSpace, | |
| unsigned long int & | propsteps | |||
| ) | [protected] |
Cascade propagation.
Definition at line 241 of file implicative.cc.
References goal, goalDefined, nbSpaces, nbVarBySpace, ruleDefined, rules, status(), QSpace::v, and MySpace::v.
Referenced by status().
| int Implicative::spaces | ( | ) |
Number of "rules" the quantified space contains. Returns the number of rules the quantified space contains. This is equal to the number of quantifier alternations in the prefix.
Definition at line 122 of file implicative.cc.
References nbSpaces.
| void Implicative::QIntVar | ( | int | var, | |
| int | min, | |||
| int | max | |||
| ) |
Defines an integer variable in a quantified space. Defines an integer variable in the quantified space with an interval domain.
| var | number of the variable to be defined. | |
| min | The min element of the domain | |
| max | the max element of the domain |
Definition at line 127 of file implicative.cc.
References goal, nbSpaces, rules, MySpace::v, QSpace::v, varInitialised, and whichSpaceOwns.
| void Implicative::QIntVar | ( | int | var, | |
| IntSet | dom | |||
| ) |
Defines an integer variable in the quantified space. Defines an integer variable in the quantifies space using a fully declared domain.
| var | Number of the variable to be defined. | |
| dom | The initial domain of the variable. |
Definition at line 155 of file implicative.cc.
References goal, nbSpaces, rules, MySpace::v, QSpace::v, varInitialised, and whichSpaceOwns.
| void Implicative::QBoolVar | ( | int | var, | |
| int | min, | |||
| int | max | |||
| ) |
Defines a boolean variable in the quantified space. Defines a boolean variable in the quantified space, uning a min and a max domain value (with false < true).
| var | Number of the variable to be defined. | |
| min | The min element of the domain (0 or 1, respectively for false or true) | |
| min | The max element of the domain (0 or 1, respectively for false or true) |
Definition at line 141 of file implicative.cc.
References goal, nbSpaces, rules, MySpace::v, QSpace::v, varInitialised, and whichSpaceOwns.
Referenced by QBoolVar().
| void Implicative::QBoolVar | ( | int | var | ) | [inline] |
Defines a boolean variable in the quantified space. Defines a boolean variable with a full initial domain in the quantified space.
| var | Number of the variable to be defined. |
Definition at line 112 of file implicative.hh.
References QBoolVar().
| MySpace * Implicative::getRuleSpace | ( | int | sp | ) |
Returns one of the restrictor space. Returns one of the restrictor space. Deprecated : use space() and nextScope instead for constraint posting.
| sp | the number of the restrictor to get (first restrictor is 0). |
Definition at line 196 of file implicative.cc.
References nbSpaces, rules, var(), and varInitialised.
| MySpace * Implicative::getGoalSpace | ( | ) |
Returns the goal space. Returns the goal space. Deprecated : use space() and nextScope instead for constraint posting.
Definition at line 207 of file implicative.cc.
References goal, var(), and varInitialised.
| MySpace * Implicative::space | ( | ) |
Returns the current declarating space. Return the space we are currently declarating constraints in. nextScope() is used to set the nextspace as the current one.
Definition at line 169 of file implicative.cc.
References currentDeclareSpace, goal, nbSpaces, and rules.
| IntVar Implicative::var | ( | int | n | ) |
Returns an integer variable from the space we are currently declaring. Returns an integer variable from the cpace we are currently declaring. If the variable had been declared as boolean, will return an integer variable with domain at most {0,1}.
| n | The number of the variable to return. |
Definition at line 178 of file implicative.cc.
References space(), and MySpace::v.
Referenced by getGoalSpace(), and getRuleSpace().
| BoolVar Implicative::bvar | ( | int | n | ) |
Returns a boolean variable from the space we are currently declaring. Returns a boolean variable from the space we are currently declaring. Will do strange things if the variable had been declared as integer.
| n | The number of the variable to return. |
Definition at line 183 of file implicative.cc.
References space(), and MySpace::v.
| int Implicative::nextScope | ( | ) |
Switch to the next space for constraint declaration. Switches to the next space for constraint declaration. var, bvar and space methods will now refer to the next rule space (or to the goal space if the current space was the last rule one). Returns the new space number, or -1 if it was called while there was no next space to declare constraints in.
Definition at line 188 of file implicative.cc.
References currentDeclareSpace, and nbSpaces.
| void Implicative::makeStructure | ( | ) |
Finalizes the restricted-quantified space construction. Finalizes the restricted-quantified space construction. Must be invoked once all the variable and all the constraints have been declared, and before the search is performed on this space.
Definition at line 217 of file implicative.cc.
References rules, QSpace::v, varInitialised, w, WarningProp::warning(), and whichSpaceOwns.
| void Implicative::print | ( | ) | [virtual] |
Prints the current state of an implicative object. Prints the variable domains of all the spaces (if defined). Does not perform an ounce of propagation.
Implements QSpace.
Definition at line 439 of file implicative.cc.
References goal, goalDefined, nbSpaces, nbVarBySpace, QSpace::nv(), q, ruleDefined, rules, MySpace::v, and QSpace::v.
| bool Implicative::quantification | ( | int | v | ) | [virtual] |
Returns a variable quantificaion. Returns wether a variable is quantified existentially (false) or universally (true).
| v | The variable number. |
Implements QSpace.
Definition at line 236 of file implicative.cc.
References q.
Referenced by status().
| int Implicative::status | ( | int | var, | |
| unsigned long int & | propsteps | |||
| ) | [virtual] |
Returns the current partial status of the quantified space. Returns the current status of the quantified space, but limits the computation of this status at the variable given in parameter. So, this method will return "don't know" more often than a complete status computation. Returns 1 for "true", 0 for "false", and -1 for "Don't know, try a next variable". A "Don't know" answer while all the variables have been assigned can be considered as a "true".
| var | The number of the variable to compute the status around. | |
| propsteps | Will be increased by the number of propagation steps performed (for statistical purposes). |
Implements QSpace.
Definition at line 280 of file implicative.cc.
References cascade(), goal, goalDefined, nbSpaces, prop_power, quantification(), ruleDefined, rules, and whichSpaceOwns.
Referenced by cascade(), and finalStatus().
| int Implicative::finalStatus | ( | unsigned long int & | propsteps | ) | [virtual] |
Returns the thuth value of a completely assigned problem. Performs the last checks to return in a complete way the truth value of the problem. All non-subsumes variables must be assigned for this method to be correct.
| propsteps | Will be increased by the number of propagation steps performed (for statistical purposes). |
Implements QSpace.
Definition at line 333 of file implicative.cc.
References goal, goalDefined, nbSpaces, nbVarBySpace, q, ruleDefined, rules, and status().
| bool Implicative::subsumed | ( | int | var | ) | [virtual] |
Returns wether a variable is subsumed or not. A variable is subsumed if it is assigned or it is bound by no more constraint. The answer must be correct, but not complete (so, a "not sure" must return False for the solver to remain correct.
| var | The variable number. |
Implements QSpace.
Definition at line 359 of file implicative.cc.
References goal, goalDefined, nbSpaces, ruleDefined, rules, QSpace::v, MySpace::v, and whichSpaceOwns.
| Implicative * Implicative::clone | ( | ) | [virtual] |
Returns a clone of the quantified space (possibly after a propagation call)
Implements QSpace.
Definition at line 394 of file implicative.cc.
References Implicative().
| void Implicative::assign | ( | int | var, | |
| int ** | vals, | |||
| int | nbVals | |||
| ) | [virtual] |
Assigns a value to a variable. assigns a value to a variable. Only this method will be used by the search engine.
| var | The number of the variable to assign. | |
| val | The value to assign to this variable. |
Implements QSpace.
Definition at line 400 of file implicative.cc.
References antidom(), nbSpaces, ruleDefined, rules, and whichSpaceOwns.
| void Implicative::remove | ( | int | var, | |
| int ** | vals, | |||
| int | nbVals | |||
| ) | [virtual] |
Implements QSpace.
Definition at line 416 of file implicative.cc.
References antidom(), nbSpaces, ruleDefined, rules, and whichSpaceOwns.
| void Implicative::backtrack | ( | ) | [virtual] |
Method called when the solver backtracks to this quantified space. This method is useful to indicate some new information to the branchong heuristic, like simply updating the scores.
Implements QSpace.
Definition at line 430 of file implicative.cc.
References Warner::update(), and w.
| void Implicative::indicateBranchingHeuristic | ( | BranchingHeuristic * | bh | ) | [virtual] |
Indicates the branching heuristic to be used when performing search. Indicates the branching heuristic to be used when performing search. This method is typically invoked by the solver at its construction.
Implements QSpace.
Definition at line 435 of file implicative.cc.
References Warner::setBH(), and w.
friend class valueHeuristic [friend] |
Definition at line 39 of file implicative.hh.
bool* Implicative::q [protected] |
Quantification of the variables (true for universal, false for existential).
Definition at line 42 of file implicative.hh.
Referenced by finalStatus(), Implicative(), print(), and quantification().
int Implicative::nbSpaces [protected] |
Number of rule spaces.
Definition at line 43 of file implicative.hh.
Referenced by assign(), cascade(), finalStatus(), getRuleSpace(), Implicative(), valueHeuristic::nbSpaces(), nextScope(), print(), QBoolVar(), QIntVar(), remove(), valueHeuristic::scopeDefined(), space(), spaces(), status(), subsumed(), and ~Implicative().
int Implicative::currentDeclareSpace [protected] |
The rule space in which we are currently declaring constraints (for declaration part only).
Definition at line 44 of file implicative.hh.
Referenced by Implicative(), nextScope(), and space().
int* Implicative::nbVarBySpace [protected] |
Number of variables by rule space.
Definition at line 45 of file implicative.hh.
Referenced by cascade(), finalStatus(), Implicative(), and print().
int* Implicative::whichSpaceOwns [protected] |
Indicates in which space a given variable first appears.
Definition at line 46 of file implicative.hh.
Referenced by assign(), Implicative(), makeStructure(), QBoolVar(), QIntVar(), remove(), status(), subsumed(), and valueHeuristic::whichSpaceOwns().
MySpace** Implicative::rules [protected] |
The rule spaces.
Definition at line 47 of file implicative.hh.
Referenced by assign(), cascade(), finalStatus(), getRuleSpace(), valueHeuristic::getVar(), Implicative(), makeStructure(), print(), QBoolVar(), QIntVar(), remove(), space(), status(), subsumed(), and ~Implicative().
MySpace* Implicative::goal [protected] |
The goal space.
Definition at line 48 of file implicative.hh.
Referenced by cascade(), finalStatus(), getGoalSpace(), valueHeuristic::getVar(), Implicative(), print(), QBoolVar(), QIntVar(), space(), status(), subsumed(), and ~Implicative().
bool* Implicative::varInitialised [protected] |
Indicates wether a variable has been initialised or not (for declaration part only).
Definition at line 49 of file implicative.hh.
Referenced by getGoalSpace(), getRuleSpace(), Implicative(), makeStructure(), QBoolVar(), and QIntVar().
bool* Implicative::ruleDefined [protected] |
Indicates wether a rule space is defind or not. If not, it has a failed or solved value.
Definition at line 50 of file implicative.hh.
Referenced by assign(), cascade(), finalStatus(), valueHeuristic::getVar(), Implicative(), print(), remove(), valueHeuristic::scopeDefined(), status(), subsumed(), and ~Implicative().
int* Implicative::ruleStatus [protected] |
Indicates wether a rule space is failed (0), solved (1), or not yet decided (-1).
Definition at line 51 of file implicative.hh.
bool Implicative::goalDefined [protected] |
Indicates wether the goal space is defined or not.
Definition at line 52 of file implicative.hh.
Referenced by cascade(), finalStatus(), valueHeuristic::getVar(), Implicative(), print(), valueHeuristic::scopeDefined(), status(), subsumed(), and ~Implicative().
int Implicative::goalStatus [protected] |
Indicates wether the goal is failed, solved, or not yet decided.
Definition at line 53 of file implicative.hh.
Warner* Implicative::w [protected] |
Definition at line 54 of file implicative.hh.
Referenced by backtrack(), Implicative(), indicateBranchingHeuristic(), and makeStructure().
int Implicative::prop_power [protected] |
Propagation power applied.
Definition at line 55 of file implicative.hh.
Referenced by Implicative(), and status().
1.5.2