Public Member Functions
	ClauseTest ()
void	testBug ()
void	testClauseActivity ()
void	testClauseCtorAddsWatches ()
void	testClauseSatisfied ()
void	testClauseTypes ()
void	testClone ()
void	testContraction ()
void	testLoopFormulaAtomConflict ()
void	testLoopFormulaBodyConflict ()
void	testLoopFormulaBugEq ()
void	testLoopFormulaDontChangeSat ()
void	testLoopFormulaInitialWatches ()
void	testLoopFormulaPropagateAtoms ()
void	testLoopFormulaPropagateAtoms2 ()
void	testLoopFormulaPropagateBody ()
void	testLoopFormulaPropagateBody2 ()
void	testLoopFormulaPropTrueAtomInSatClause ()
void	testLoopFormulaSatisfied ()
void	testNewContractedClause ()
void	testPropAlreadySatisfied ()
void	testPropGenericClause ()
void	testPropGenericClauseConflict ()
void	testPropRandomClauses ()
void	testReasonBumpsActivityIfLearnt ()
void	testSimplifyLFIfAllAtomsFalse ()
void	testSimplifyLFIfOneBodyTrue ()
void	testSimplifyLFRemovesFalseAtoms ()
void	testSimplifyLFRemovesFalseBodies ()
void	testSimplifyLFRemovesTrueAtoms ()
void	testSimplifyRemovesFalseLitsBeg ()
void	testSimplifyRemovesFalseLitsEnd ()
void	testSimplifyRemovesFalseLitsMid ()
void	testSimplifySAT ()
void	testSimplifyShortRemovesFalseLitsBeg ()
void	testSimplifyShortRemovesFalseLitsEnd ()
void	testSimplifyShortRemovesFalseLitsMid ()
void	testSimplifyTagged ()
void	testSimplifyUnitButNotLocked ()
void	testStrengthen ()
void	testStrengthenBug ()
void	testStrengthenContracted ()
void	testStrengthenContractedNoExtend ()
void	testStrengthenLocked ()
void	testStrengthenLockedEarly ()
void	testStrengthenToUnary ()
Private Member Functions
void	check (Clause &c)
int	countWatches (const Solver &s, ClauseHead *c, const LitVec &lits)
	CPPUNIT_TEST (testClauseCtorAddsWatches)
	CPPUNIT_TEST (testClauseTypes)
	CPPUNIT_TEST (testClauseActivity)
	CPPUNIT_TEST (testPropGenericClause)
	CPPUNIT_TEST (testPropGenericClauseConflict)
	CPPUNIT_TEST (testPropAlreadySatisfied)
	CPPUNIT_TEST (testPropRandomClauses)
	CPPUNIT_TEST (testReasonBumpsActivityIfLearnt)
	CPPUNIT_TEST (testSimplifySAT)
	CPPUNIT_TEST (testSimplifyUnitButNotLocked)
	CPPUNIT_TEST (testSimplifyRemovesFalseLitsBeg)
	CPPUNIT_TEST (testSimplifyRemovesFalseLitsMid)
	CPPUNIT_TEST (testSimplifyRemovesFalseLitsEnd)
	CPPUNIT_TEST (testSimplifyShortRemovesFalseLitsBeg)
	CPPUNIT_TEST (testSimplifyShortRemovesFalseLitsMid)
	CPPUNIT_TEST (testSimplifyShortRemovesFalseLitsEnd)
	CPPUNIT_TEST (testStrengthen)
	CPPUNIT_TEST (testStrengthenToUnary)
	CPPUNIT_TEST (testStrengthenContracted)
	CPPUNIT_TEST (testStrengthenBug)
	CPPUNIT_TEST (testStrengthenContractedNoExtend)
	CPPUNIT_TEST (testStrengthenLocked)
	CPPUNIT_TEST (testStrengthenLockedEarly)
	CPPUNIT_TEST (testSimplifyTagged)
	CPPUNIT_TEST (testClauseSatisfied)
	CPPUNIT_TEST (testContraction)
	CPPUNIT_TEST (testNewContractedClause)
	CPPUNIT_TEST (testClone)
	CPPUNIT_TEST (testBug)
	CPPUNIT_TEST (testLoopFormulaInitialWatches)
	CPPUNIT_TEST (testSimplifyLFIfOneBodyTrue)
	CPPUNIT_TEST (testSimplifyLFIfAllAtomsFalse)
	CPPUNIT_TEST (testSimplifyLFRemovesFalseBodies)
	CPPUNIT_TEST (testSimplifyLFRemovesFalseAtoms)
	CPPUNIT_TEST (testSimplifyLFRemovesTrueAtoms)
	CPPUNIT_TEST (testLoopFormulaPropagateBody)
	CPPUNIT_TEST (testLoopFormulaPropagateBody2)
	CPPUNIT_TEST (testLoopFormulaPropagateAtoms)
	CPPUNIT_TEST (testLoopFormulaPropagateAtoms2)
	CPPUNIT_TEST (testLoopFormulaBodyConflict)
	CPPUNIT_TEST (testLoopFormulaAtomConflict)
	CPPUNIT_TEST (testLoopFormulaDontChangeSat)
	CPPUNIT_TEST (testLoopFormulaPropTrueAtomInSatClause)
	CPPUNIT_TEST (testLoopFormulaSatisfied)
	CPPUNIT_TEST (testLoopFormulaBugEq)
	CPPUNIT_TEST_SUITE (ClauseTest)
	CPPUNIT_TEST_SUITE_END ()
Clause *	createClause (LitVec &lits, const ClauseInfo &info)
Clause *	createClause (int pos, int neg, ConstraintType t=Constraint_t::static_constraint)
Clause *	createRandomClause (int size)
LoopFormula *	lfTestInit ()
std::string	toString (const LitVec &c)
Private Attributes
Literal	a1
Literal	a2
Literal	a3
Literal	b1
Literal	b2
Literal	b3
LitVec	clLits
SharedContext	ctx
Solver *	solver

Detailed Description

Definition at line 33 of file clause_test.cpp.

Constructor & Destructor Documentation

Clasp::Test::ClauseTest::ClauseTest ( ) [inline]

Definition at line 95 of file clause_test.cpp.

Member Function Documentation

void Clasp::Test::ClauseTest::check ( Clause & c ) [inline, private]

Definition at line 966 of file clause_test.cpp.

int Clasp::Test::ClauseTest::countWatches	(	const Solver &	s,
		ClauseHead *	c,
		const LitVec &	lits
	)		`[inline, private]`

Definition at line 959 of file clause_test.cpp.

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testClauseCtorAddsWatches ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testClauseTypes ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testClauseActivity ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testPropGenericClause ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testPropGenericClauseConflict ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testPropAlreadySatisfied ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testPropRandomClauses ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testReasonBumpsActivityIfLearnt ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifySAT ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyUnitButNotLocked ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyRemovesFalseLitsBeg ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyRemovesFalseLitsMid ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyRemovesFalseLitsEnd ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyShortRemovesFalseLitsBeg ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyShortRemovesFalseLitsMid ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyShortRemovesFalseLitsEnd ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthen ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenToUnary ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenContracted ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenBug ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenContractedNoExtend ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenLocked ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testStrengthenLockedEarly ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyTagged ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testClauseSatisfied ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testContraction ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testNewContractedClause ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testClone ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testBug ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaInitialWatches ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyLFIfOneBodyTrue ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyLFIfAllAtomsFalse ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyLFRemovesFalseBodies ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyLFRemovesFalseAtoms ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testSimplifyLFRemovesTrueAtoms ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaPropagateBody ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaPropagateBody2 ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaPropagateAtoms ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaPropagateAtoms2 ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaBodyConflict ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaAtomConflict ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaDontChangeSat ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaPropTrueAtomInSatClause ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaSatisfied ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST ( testLoopFormulaBugEq ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST_SUITE ( ClauseTest ) [private]

Clasp::Test::ClauseTest::CPPUNIT_TEST_SUITE_END ( ) [private]

Clause* Clasp::Test::ClauseTest::createClause	(	LitVec &	lits,
		const ClauseInfo &	info
	)		`[inline, private]`

Definition at line 1001 of file clause_test.cpp.

Clause* Clasp::Test::ClauseTest::createClause	(	int	pos,
		int	neg,
		ConstraintType	t = `Constraint_t::static_constraint`
	)		`[inline, private]`

Definition at line 1005 of file clause_test.cpp.

Clause* Clasp::Test::ClauseTest::createRandomClause ( int size ) [inline, private]

Definition at line 1020 of file clause_test.cpp.

LoopFormula* Clasp::Test::ClauseTest::lfTestInit ( ) [inline, private]

Definition at line 1025 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testBug ( ) [inline]

Definition at line 597 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testClauseActivity ( ) [inline]

Definition at line 130 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testClauseCtorAddsWatches ( ) [inline]

Definition at line 109 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testClauseSatisfied ( ) [inline]

Definition at line 531 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testClauseTypes ( ) [inline]

Definition at line 118 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testClone ( ) [inline]

Definition at line 624 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testContraction ( ) [inline]

Definition at line 555 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaAtomConflict ( ) [inline]

Definition at line 854 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaBodyConflict ( ) [inline]

Definition at line 834 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaBugEq ( ) [inline]

Definition at line 922 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaDontChangeSat ( ) [inline]

Definition at line 882 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaInitialWatches ( ) [inline]

Definition at line 650 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaPropagateAtoms ( ) [inline]

Definition at line 778 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaPropagateAtoms2 ( ) [inline]

Definition at line 803 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaPropagateBody ( ) [inline]

Definition at line 729 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaPropagateBody2 ( ) [inline]

Definition at line 751 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaPropTrueAtomInSatClause ( ) [inline]

Definition at line 943 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testLoopFormulaSatisfied ( ) [inline]

Definition at line 900 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testNewContractedClause ( ) [inline]

Definition at line 574 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testPropAlreadySatisfied ( ) [inline]

Definition at line 189 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testPropGenericClause ( ) [inline]

Definition at line 150 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testPropGenericClauseConflict ( ) [inline]

Definition at line 173 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testPropRandomClauses ( ) [inline]

Definition at line 205 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testReasonBumpsActivityIfLearnt ( ) [inline]

Definition at line 218 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyLFIfAllAtomsFalse ( ) [inline]

Definition at line 669 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyLFIfOneBodyTrue ( ) [inline]

Definition at line 658 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyLFRemovesFalseAtoms ( ) [inline]

Definition at line 693 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyLFRemovesFalseBodies ( ) [inline]

Definition at line 683 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyLFRemovesTrueAtoms ( ) [inline]

Definition at line 711 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyRemovesFalseLitsBeg ( ) [inline]

Definition at line 260 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyRemovesFalseLitsEnd ( ) [inline]

Definition at line 516 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyRemovesFalseLitsMid ( ) [inline]

Definition at line 276 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifySAT ( ) [inline]

Definition at line 240 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyShortRemovesFalseLitsBeg ( ) [inline]

Definition at line 292 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyShortRemovesFalseLitsEnd ( ) [inline]

Definition at line 318 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyShortRemovesFalseLitsMid ( ) [inline]

Definition at line 305 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyTagged ( ) [inline]

Definition at line 500 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testSimplifyUnitButNotLocked ( ) [inline]

Definition at line 249 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthen ( ) [inline]

Definition at line 331 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenBug ( ) [inline]

Definition at line 414 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenContracted ( ) [inline]

Definition at line 379 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenContractedNoExtend ( ) [inline]

Definition at line 436 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenLocked ( ) [inline]

Definition at line 455 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenLockedEarly ( ) [inline]

Definition at line 477 of file clause_test.cpp.

void Clasp::Test::ClauseTest::testStrengthenToUnary ( ) [inline]

Definition at line 350 of file clause_test.cpp.

std::string Clasp::Test::ClauseTest::toString ( const LitVec & c ) [inline, private]

Definition at line 989 of file clause_test.cpp.

Member Data Documentation

Literal Clasp::Test::ClauseTest::a1 [private]

Definition at line 1043 of file clause_test.cpp.

Literal Clasp::Test::ClauseTest::a2 [private]

Definition at line 1043 of file clause_test.cpp.

Literal Clasp::Test::ClauseTest::a3 [private]

Definition at line 1043 of file clause_test.cpp.

Literal Clasp::Test::ClauseTest::b1 [private]

Definition at line 1043 of file clause_test.cpp.

Literal Clasp::Test::ClauseTest::b2 [private]

Definition at line 1043 of file clause_test.cpp.

Literal Clasp::Test::ClauseTest::b3 [private]

Definition at line 1043 of file clause_test.cpp.

LitVec Clasp::Test::ClauseTest::clLits [private]

Definition at line 1044 of file clause_test.cpp.

SharedContext Clasp::Test::ClauseTest::ctx [private]

Definition at line 957 of file clause_test.cpp.

Solver* Clasp::Test::ClauseTest::solver [private]

Definition at line 958 of file clause_test.cpp.

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

clause_test.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation