Implicative Class Reference

#include <implicative.hh>

Inherits QSpace.

Inheritance diagram for Implicative:

[legend]Collaboration diagram for Implicative:


Public Member Functions
QECODE_EXPORT	Implicative (int ns, bool firstQ, int *nv)
	Default constructor for a restricted-quantified space. This is the first step for building a restricted-quantified space. The prefix is defined here.
QECODE_EXPORT	Implicative (Implicative &im)
virtual QECODE_EXPORT	~Implicative ()
QECODE_EXPORT 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.
QECODE_EXPORT 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.
QECODE_EXPORT 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.
QECODE_EXPORT 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).
QECODE_EXPORT 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.
QECODE_EXPORT MySpace *	space ()
	Returns one of the restrictor space. Returns one of the restrictor space. Deprecated : use space() and nextScope instead for constraint posting. Returns the goal space. Returns the goal space. Deprecated : use space() and nextScope instead for constraint posting. 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.
QECODE_EXPORT 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. Will abort if the variable is not integer.
QECODE_EXPORT 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 abort if the variable is not boolean.
QECODE_EXPORT 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.
QECODE_EXPORT 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 QECODE_EXPORT 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 QECODE_EXPORT bool	quantification (int v)
	Returns a variable quantificaion. Returns wether a variable is quantified existentially (false) or universally (true).
virtual QECODE_EXPORT 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 QECODE_EXPORT 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 QECODE_EXPORT 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 QECODE_EXPORT Implicative *	clone ()
virtual QECODE_EXPORT void	assign_int (int var, int **vals, int nbVals)
	Assigns a set of value to an integer variable. assigns a set of value to an integer variable. Used only by the search engine.
virtual QECODE_EXPORT void	remove_int (int var, int **vals, int nbVals)
	Removes a set of value to an integer variable. Removes a set of value to an integer variable. Used only by the search engine.
virtual QECODE_EXPORT void	assign_bool (int var, int **vals, int nbVals)
	Assigns a set of value to an integer variable. assigns a set of value to an integer variable. Used only by the search engine.
virtual QECODE_EXPORT void	remove_bool (int var, int **vals, int nbVals)
	Removes a set of value to an boolean variable. Removes a set of value to an boolean variable. Used only by the search engine.
virtual QECODE_EXPORT void	assign_bool (int var, int b)
	Assigns a value to a boolean variable. assigns a set of value to an integer variable. Used only by the search engine.
virtual QECODE_EXPORT void	remove_bool (int var, int b)
	Removes a value to a boolean variable. removes a set of value to an integer variable. Used only by the search engine.
virtual QECODE_EXPORT 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 QECODE_EXPORT 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

Detailed Description

Definition at line 38 of file implicative.hh.

Constructor & Destructor Documentation

Implicative::Implicative	(	int	ns,
		bool	firstQ,
		int *	nv
	)

Default constructor for a restricted-quantified space. This is the first step for building a restricted-quantified space. The prefix is defined here.

Parameters:

	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.

Definition at line 26 of file implicative.cc.

References currentDeclareSpace, goal, goalDefined, QSpace::n, nbSpaces, nbVarBySpace, prop_power, q, ruleDefined, rules, QSpace::type_of_v, QSpace::v, varInitialised, and whichSpaceOwns.

Referenced by clone().

Implicative::Implicative ( Implicative & im )

Copy constructor for a restricted-quantified space.

Parameters:

The space we want to copy.

Definition at line 63 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 110 of file implicative.cc.

References goal, goalDefined, nbSpaces, ruleDefined, and rules.

Member Function Documentation

int Implicative::cascade	(	int	firstSpace,
		unsigned long int &	propsteps
	)			`[protected]`

Cascade propagation.

Definition at line 260 of file implicative.cc.

References goal, goalDefined, nbSpaces, nbVarBySpace, ruleDefined, rules, status(), QSpace::type_of_v, QSpace::v, MySpace::v, VTYPE_BOOL, and VTYPE_INT.

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 123 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.

Parameters:

	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 128 of file implicative.cc.

References goal, nbSpaces, rules, QSpace::type_of_v, MySpace::type_of_v, MySpace::v, QSpace::v, varInitialised, VTYPE_INT, and whichSpaceOwns.

Referenced by main().

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.

Parameters:

	var	Number of the variable to be defined.
	dom	The initial domain of the variable.

Definition at line 162 of file implicative.cc.

References goal, nbSpaces, rules, QSpace::type_of_v, MySpace::type_of_v, MySpace::v, QSpace::v, varInitialised, VTYPE_INT, 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).

Parameters:

	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 145 of file implicative.cc.

References goal, nbSpaces, rules, QSpace::type_of_v, MySpace::type_of_v, MySpace::v, QSpace::v, varInitialised, VTYPE_BOOL, and whichSpaceOwns.

QECODE_EXPORT 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.

Parameters:

var

Number of the variable to be defined.

Definition at line 111 of file implicative.hh.

MySpace * Implicative::space ( )

Returns one of the restrictor space. Returns one of the restrictor space. Deprecated : use space() and nextScope instead for constraint posting. Returns the goal space. Returns the goal space. Deprecated : use space() and nextScope instead for constraint posting. 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 179 of file implicative.cc.

References currentDeclareSpace, goal, nbSpaces, and rules.

Referenced by bvar(), main(), and var().

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. Will abort if the variable is not integer.

Parameters:

The number of the variable to return.

Definition at line 188 of file implicative.cc.

References space(), and MySpace::v.

Referenced by main().

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 abort if the variable is not boolean.

Parameters:

The number of the variable to return.

Definition at line 193 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 198 of file implicative.cc.

References currentDeclareSpace, and nbSpaces.

Referenced by main().

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 227 of file implicative.cc.

References BoolWarningProp::BoolWarning(), IntWarningProp::IntWarning(), rules, QSpace::type_of_v, QSpace::v, varInitialised, VTYPE_BOOL, VTYPE_INT, w, and whichSpaceOwns.

Referenced by main().

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

Parameters:

The variable number.

Implements QSpace.

Definition at line 255 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".

Parameters:

	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 315 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.

Parameters:

propsteps

Will be increased by the number of propagation steps performed (for statistical purposes).

Implements QSpace.

Definition at line 349 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.

Parameters:

var

The variable number.

Implements QSpace.

Definition at line 375 of file implicative.cc.

References goal, goalDefined, nbSpaces, ruleDefined, rules, QSpace::type_of_v, QSpace::v, MySpace::v, VTYPE_BOOL, VTYPE_INT, and whichSpaceOwns.

Implicative * Implicative::clone ( ) [virtual]

Returns a clone of the quantified space (possibly after a propagation call)

Implements QSpace.

Definition at line 458 of file implicative.cc.

References Implicative().

void Implicative::assign_int	(	int	var,
		int **	vals,
		int	nbVals
	)			`[virtual]`

Assigns a set of value to an integer variable. assigns a set of value to an integer variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	vals	The values to assign to this variable (represented y ranges).
	nbVals	The number of ranges in vals.

Implements QSpace.

Definition at line 464 of file implicative.cc.

References myAntidom_int(), nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_INT, and whichSpaceOwns.

void Implicative::remove_int	(	int	var,
		int **	vals,
		int	nbVals
	)			`[virtual]`

Removes a set of value to an integer variable. Removes a set of value to an integer variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	vals	The values to remove from this variable (represented y ranges).
	nbVals	The number of ranges in vals.

Implements QSpace.

Definition at line 484 of file implicative.cc.

References myAntidom_int(), nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_INT, and whichSpaceOwns.

void Implicative::assign_bool	(	int	var,
		int **	vals,
		int	nbVals
	)			`[virtual]`

Assigns a set of value to an integer variable. assigns a set of value to an integer variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	vals	The values to assign to this variable (represented y ranges).
	nbVals	The number of ranges in vals.

Implements QSpace.

Definition at line 501 of file implicative.cc.

References myAntidom_bool(), nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_BOOL, and whichSpaceOwns.

void Implicative::remove_bool	(	int	var,
		int **	vals,
		int	nbVals
	)			`[virtual]`

Removes a set of value to an boolean variable. Removes a set of value to an boolean variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	vals	The values to remove from this variable (represented y ranges).
	nbVals	The number of ranges in vals.

Implements QSpace.

Definition at line 521 of file implicative.cc.

References myAntidom_bool(), nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_BOOL, and whichSpaceOwns.

void Implicative::assign_bool	(	int	var,
		int	b
	)			`[virtual]`

Assigns a value to a boolean variable. assigns a set of value to an integer variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	b	The value to assign to this variable.

Implements QSpace.

Definition at line 538 of file implicative.cc.

References nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_INT, and whichSpaceOwns.

void Implicative::remove_bool	(	int	var,
		int	b
	)			`[virtual]`

Removes a value to a boolean variable. removes a set of value to an integer variable. Used only by the search engine.

Parameters:

	var	The number of the variable to assign.
	b	The value to remove from this variable.

Implements QSpace.

Definition at line 552 of file implicative.cc.

References nbSpaces, ruleDefined, rules, QSpace::type_of_v, VTYPE_INT, 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 567 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 572 of file implicative.cc.

References Warner::setBH(), and w.