two_sat_test.cc File Reference

#include <gtest/gtest.h>
#include <random>
#include <limits>
#include <Two_Sat.H>
#include <tpl_sgraph.H>
#include <tpl_agraph.H>

Include dependency graph for two_sat_test.cc:

Go to the source code of this file.

Functions
static bool	verify_assignment (const Array< bool > &assignment, const Array< std::pair< long, long > > &clauses)
	TEST (TwoSat, EmptyFormula)
	TEST (TwoSat, SingleClause)
	TEST (TwoSat, UnitClauseTrue)
	TEST (TwoSat, UnitClauseFalse)
	TEST (TwoSat, Contradiction)
	TEST (TwoSat, SimpleImplication)
	TEST (TwoSat, ImplicationChain)
	TEST (TwoSat, ImplicationChainContradiction)
	TEST (TwoSat, Equivalence)
	TEST (TwoSat, Xor)
	TEST (TwoSat, XorContradiction)
	TEST (TwoSat, SignedApi)
	TEST (TwoSat, SignedApiUnsat)
	TEST (TwoSat, AtMostOne)
	TEST (TwoSat, AtMostOneWithForced)
	TEST (TwoSat, AtMostOneConflict)
	TEST (TwoSat, AtMostOneEdgeCases)
	TEST (TwoSat, GraphColoring2Colors)
	TEST (TwoSat, GraphColoring2ColorsPath)
	TEST (TwoSat, AllClausesSame)
	TEST (TwoSat, BoundsChecking)
	TEST (TwoSat, StressBruteForce)
	TEST (TwoSat, WithListSDigraph)
	TEST (TwoSat, WithArrayDigraph)
	TEST (TwoSat, LargerSatisfiable)
	TEST (TwoSat, LargerUnsatisfiable)
	TEST (TwoSat, LiteralHelpers)

Function Documentation

TEST() [1/27]

TEST	(	TwoSat	,
		AllClausesSame
	)

Definition at line 330 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [2/27]

TEST	(	TwoSat	,
		AtMostOne
	)

Definition at line 230 of file two_sat_test.cc.

References Aleph::count(), and Aleph::divide_and_conquer_partition_dp().

TEST() [3/27]

TEST	(	TwoSat	,
		AtMostOneConflict
	)

Definition at line 263 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [4/27]

TEST	(	TwoSat	,
		AtMostOneEdgeCases
	)

Definition at line 275 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [5/27]

TEST	(	TwoSat	,
		AtMostOneWithForced
	)

Definition at line 247 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [6/27]

TEST	(	TwoSat	,
		BoundsChecking
	)

Definition at line 345 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [7/27]

TEST	(	TwoSat	,
		Contradiction
	)

Definition at line 111 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [8/27]

TEST	(	TwoSat	,
		EmptyFormula
	)

Definition at line 67 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [9/27]

TEST	(	TwoSat	,
		Equivalence
	)

Definition at line 162 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [10/27]

TEST	(	TwoSat	,
		GraphColoring2Colors
	)

Definition at line 300 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [11/27]

TEST	(	TwoSat	,
		GraphColoring2ColorsPath
	)

Definition at line 313 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [12/27]

TEST	(	TwoSat	,
		ImplicationChain
	)

Definition at line 135 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [13/27]

TEST	(	TwoSat	,
		ImplicationChainContradiction
	)

Definition at line 150 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [14/27]

TEST	(	TwoSat	,
		LargerSatisfiable
	)

Definition at line 460 of file two_sat_test.cc.

References Aleph::Array< T >::append(), Aleph::Array< T >::create(), Aleph::divide_and_conquer_partition_dp(), l1, l2, N, and rng.

TEST() [15/27]

TEST	(	TwoSat	,
		LargerUnsatisfiable
	)

Definition at line 505 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp(), and N.

TEST() [16/27]

TEST	(	TwoSat	,
		LiteralHelpers
	)

Definition at line 527 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [17/27]

TEST	(	TwoSat	,
		SignedApi
	)

Definition at line 201 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp(), and verify_assignment().

TEST() [18/27]

TEST	(	TwoSat	,
		SignedApiUnsat
	)

Definition at line 216 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [19/27]

TEST	(	TwoSat	,
		SimpleImplication
	)

Definition at line 122 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [20/27]

TEST	(	TwoSat	,
		SingleClause
	)

Definition at line 76 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [21/27]

TEST	(	TwoSat	,
		StressBruteForce
	)

Definition at line 365 of file two_sat_test.cc.

References Aleph::Array< T >::append(), Aleph::Array< T >::create(), Aleph::divide_and_conquer_partition_dp(), N, rng, and verify_assignment().

TEST() [22/27]

TEST	(	TwoSat	,
		UnitClauseFalse
	)

Definition at line 100 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [23/27]

TEST	(	TwoSat	,
		UnitClauseTrue
	)

Definition at line 89 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [24/27]

TEST	(	TwoSat	,
		WithArrayDigraph
	)

Definition at line 440 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp(), and verify_assignment().

TEST() [25/27]

TEST	(	TwoSat	,
		WithListSDigraph
	)

Definition at line 423 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp(), and verify_assignment().

TEST() [26/27]

TEST	(	TwoSat	,
		Xor
	)

Definition at line 175 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

TEST() [27/27]

TEST	(	TwoSat	,
		XorContradiction
	)

Definition at line 186 of file two_sat_test.cc.

References Aleph::divide_and_conquer_partition_dp().

verify_assignment()

static bool verify_assignment ( const Array< bool > &  assignment, const Array< std::pair< long, long > > &  clauses  )

static

Definition at line 46 of file two_sat_test.cc.

References Aleph::and, and Aleph::divide_and_conquer_partition_dp().

Referenced by TEST(), TEST(), TEST(), and TEST().