Public Member Functions
	ClauseCreatorTest ()
void	testAddBinaryClause ()
void	testAddGenericClause ()
void	testAddTernaryClause ()
void	testCreateBogusUnit ()
void	testCreateLearntClauseConflict ()
void	testCreateNonAssertingLearntClause ()
void	testCreateNonAssertingLearntClauseAsserting ()
void	testCreatorAddLitBug ()
void	testCreatorAssertsFirstLit ()
void	testCreatorInitsWatches ()
void	testCreatorNotifiesHeuristic ()
void	testCreatorSimplifyBug ()
void	testCreatorSimplifyFindsTauts ()
void	testCreatorSimplifyMovesWatch ()
void	testCreatorSimplifyRemovesDuplicates ()
void	testEmptyClauseIsFalse ()
void	testFactsAreAsserted ()
void	testFactsAreRemovedFromLearnt ()
void	testInitWatches ()
void	testIntegrateAssertingBelowBT ()
void	testIntegrateAssertingConflict ()
void	testIntegrateAssertingConflictBelowRoot ()
void	testIntegrateConflict ()
void	testIntegrateConflictBelowBT ()
void	testIntegrateConflictBelowRoot ()
void	testIntegrateEmpty ()
void	testIntegrateKnownOrderBug ()
void	testIntegrateNotConflictingBug ()
void	testIntegrateSAT ()
void	testIntegrateSATBug1 ()
void	testIntegrateSATBug2 ()
void	testIntegrateSATBug3 ()
void	testIntegrateSATBug4 ()
void	testIntegrateSimplify ()
void	testIntegrateUnit ()
void	testIntegrateUnitSAT ()
void	testIntegrateUnsat ()
void	testTopLevelFalseLitsAreRemoved ()
void	testTopLevelSATClausesAreNotAdded ()
Private Member Functions
	CPPUNIT_TEST (testEmptyClauseIsFalse)
	CPPUNIT_TEST (testFactsAreAsserted)
	CPPUNIT_TEST (testTopLevelSATClausesAreNotAdded)
	CPPUNIT_TEST (testTopLevelFalseLitsAreRemoved)
	CPPUNIT_TEST (testAddBinaryClause)
	CPPUNIT_TEST (testAddTernaryClause)
	CPPUNIT_TEST (testAddGenericClause)
	CPPUNIT_TEST (testCreatorAssertsFirstLit)
	CPPUNIT_TEST (testCreatorInitsWatches)
	CPPUNIT_TEST (testCreatorNotifiesHeuristic)
	CPPUNIT_TEST (testCreatorAddLitBug)
	CPPUNIT_TEST (testCreatorSimplifyRemovesDuplicates)
	CPPUNIT_TEST (testCreatorSimplifyFindsTauts)
	CPPUNIT_TEST (testCreatorSimplifyMovesWatch)
	CPPUNIT_TEST (testCreatorSimplifyBug)
	CPPUNIT_TEST (testCreateNonAssertingLearntClause)
	CPPUNIT_TEST (testCreateLearntClauseConflict)
	CPPUNIT_TEST (testCreateNonAssertingLearntClauseAsserting)
	CPPUNIT_TEST (testCreateBogusUnit)
	CPPUNIT_TEST (testInitWatches)
	CPPUNIT_TEST (testIntegrateEmpty)
	CPPUNIT_TEST (testIntegrateUnit)
	CPPUNIT_TEST (testIntegrateUnitSAT)
	CPPUNIT_TEST (testIntegrateConflict)
	CPPUNIT_TEST (testIntegrateAssertingConflict)
	CPPUNIT_TEST (testIntegrateAssertingConflictBelowRoot)
	CPPUNIT_TEST (testIntegrateConflictBelowRoot)
	CPPUNIT_TEST (testIntegrateSATBug1)
	CPPUNIT_TEST (testIntegrateSATBug2)
	CPPUNIT_TEST (testIntegrateSATBug3)
	CPPUNIT_TEST (testIntegrateSATBug4)
	CPPUNIT_TEST (testIntegrateKnownOrderBug)
	CPPUNIT_TEST (testIntegrateNotConflictingBug)
	CPPUNIT_TEST (testIntegrateSimplify)
	CPPUNIT_TEST (testIntegrateSAT)
	CPPUNIT_TEST (testIntegrateUnsat)
	CPPUNIT_TEST (testIntegrateAssertingBelowBT)
	CPPUNIT_TEST (testIntegrateConflictBelowBT)
	CPPUNIT_TEST (testFactsAreRemovedFromLearnt)
	CPPUNIT_TEST_SUITE (ClauseCreatorTest)
	CPPUNIT_TEST_SUITE_END ()
const Solver &	solver () const
Solver &	solver ()
Private Attributes
Literal	a
Literal	b
Literal	c
ClauseCreator	creator
SharedContext	ctx
Literal	d
Literal	e
Literal	f

Detailed Description

Definition at line 26 of file clause_creator_test.cpp.

Constructor & Destructor Documentation

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

Definition at line 74 of file clause_creator_test.cpp.

Member Function Documentation

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testEmptyClauseIsFalse ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testFactsAreAsserted ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testTopLevelSATClausesAreNotAdded ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testTopLevelFalseLitsAreRemoved ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testAddBinaryClause ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testAddTernaryClause ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testAddGenericClause ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorAssertsFirstLit ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorInitsWatches ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorNotifiesHeuristic ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorAddLitBug ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorSimplifyRemovesDuplicates ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorSimplifyFindsTauts ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorSimplifyMovesWatch ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreatorSimplifyBug ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreateNonAssertingLearntClause ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreateLearntClauseConflict ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreateNonAssertingLearntClauseAsserting ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testCreateBogusUnit ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testInitWatches ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateEmpty ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateUnit ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateUnitSAT ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateConflict ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateAssertingConflict ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateAssertingConflictBelowRoot ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateConflictBelowRoot ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSATBug1 ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSATBug2 ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSATBug3 ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSATBug4 ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateKnownOrderBug ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateNotConflictingBug ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSimplify ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateSAT ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateUnsat ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateAssertingBelowBT ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testIntegrateConflictBelowBT ) [private]

Clasp::Test::ClauseCreatorTest::CPPUNIT_TEST ( testFactsAreRemovedFromLearnt ) [private]

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

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

const Solver& Clasp::Test::ClauseCreatorTest::solver ( ) const [inline, private]

Definition at line 600 of file clause_creator_test.cpp.

Solver& Clasp::Test::ClauseCreatorTest::solver ( ) [inline, private]

Definition at line 601 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testAddBinaryClause ( ) [inline]

Definition at line 103 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testAddGenericClause ( ) [inline]

Definition at line 113 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testAddTernaryClause ( ) [inline]

Definition at line 108 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreateBogusUnit ( ) [inline]

Definition at line 296 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreateLearntClauseConflict ( ) [inline]

Definition at line 242 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreateNonAssertingLearntClause ( ) [inline]

Definition at line 221 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreateNonAssertingLearntClauseAsserting ( ) [inline]

Definition at line 270 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorAddLitBug ( ) [inline]

Definition at line 177 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorAssertsFirstLit ( ) [inline]

Definition at line 118 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorInitsWatches ( ) [inline]

Definition at line 132 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorNotifiesHeuristic ( ) [inline]

Definition at line 145 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorSimplifyBug ( ) [inline]

Definition at line 212 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorSimplifyFindsTauts ( ) [inline]

Definition at line 197 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorSimplifyMovesWatch ( ) [inline]

Definition at line 201 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testCreatorSimplifyRemovesDuplicates ( ) [inline]

Definition at line 189 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testEmptyClauseIsFalse ( ) [inline]

Definition at line 84 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testFactsAreAsserted ( ) [inline]

Definition at line 88 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testFactsAreRemovedFromLearnt ( ) [inline]

Definition at line 588 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testInitWatches ( ) [inline]

Definition at line 311 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateAssertingBelowBT ( ) [inline]

Definition at line 552 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateAssertingConflict ( ) [inline]

Definition at line 398 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateAssertingConflictBelowRoot ( ) [inline]

Definition at line 412 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateConflict ( ) [inline]

Definition at line 382 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateConflictBelowBT ( ) [inline]

Definition at line 571 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateConflictBelowRoot ( ) [inline]

Definition at line 428 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateEmpty ( ) [inline]

Definition at line 336 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateKnownOrderBug ( ) [inline]

Definition at line 491 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateNotConflictingBug ( ) [inline]

Definition at line 500 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSAT ( ) [inline]

Definition at line 525 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSATBug1 ( ) [inline]

Definition at line 442 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSATBug2 ( ) [inline]

Definition at line 453 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSATBug3 ( ) [inline]

Definition at line 465 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSATBug4 ( ) [inline]

Definition at line 481 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateSimplify ( ) [inline]

Definition at line 511 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateUnit ( ) [inline]

Definition at line 346 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateUnitSAT ( ) [inline]

Definition at line 372 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testIntegrateUnsat ( ) [inline]

Definition at line 540 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testTopLevelFalseLitsAreRemoved ( ) [inline]

Definition at line 97 of file clause_creator_test.cpp.

void Clasp::Test::ClauseCreatorTest::testTopLevelSATClausesAreNotAdded ( ) [inline]

Definition at line 92 of file clause_creator_test.cpp.

Member Data Documentation

Literal Clasp::Test::ClauseCreatorTest::a [private]

Definition at line 604 of file clause_creator_test.cpp.

Literal Clasp::Test::ClauseCreatorTest::b [private]

Definition at line 604 of file clause_creator_test.cpp.

Literal Clasp::Test::ClauseCreatorTest::c [private]

Definition at line 604 of file clause_creator_test.cpp.

ClauseCreator Clasp::Test::ClauseCreatorTest::creator [private]

Definition at line 603 of file clause_creator_test.cpp.

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

Definition at line 602 of file clause_creator_test.cpp.

Literal Clasp::Test::ClauseCreatorTest::d [private]

Definition at line 604 of file clause_creator_test.cpp.

Literal Clasp::Test::ClauseCreatorTest::e [private]

Definition at line 604 of file clause_creator_test.cpp.

Literal Clasp::Test::ClauseCreatorTest::f [private]

Definition at line 604 of file clause_creator_test.cpp.

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

clause_creator_test.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation