dlinear::BoundImplicator Class Reference

Use theory reasoning to add relations between literals using some simple theory inferences. More...

#include <BoundImplicator.h>

Classes
struct	Constraint
	Constraint. More...

Public Member Functions
	BoundImplicator (const Config &config, std::function< void(const Formula &)> assert, const PredicateAbstractor &predicate_abstractor)
	Construct a BoundImplicator.
void	Propagate ()
	Use theory reasoning to propagate some simple theory inferences.

Private Member Functions
template<int NVariables>
void	AddAssertion (const Formula &assertion)
	Add an assertion to the constraints_ map.
void	PropagateAssertions ()
	Propagate the sorted constraints by adding them to the context by calling the assert_ function.

Private Attributes
const Config &	config_
	Configuration.
const std::function< void(const Formula &)>	assert_
	Assertion function. It adds assertions to the context.
const PredicateAbstractor &	predicate_abstractor_
	Predicate abstractor.
std::map< Variable, SortedVector< Constraint > >	constraints_
	Map of constraints for each variable.

Detailed Description

Use theory reasoning to add relations between literals using some simple theory inferences.

It will help the SAT solver to prune trivially unsatisfiable branches, improving the chances of finding a feasible solution faster.

Precondition

All the assertions in the predicate_abstractor are flattered.

Definition at line 37 of file BoundImplicator.h.

Constructor & Destructor Documentation

BoundImplicator()

dlinear::BoundImplicator::BoundImplicator	(	const Config &	config,
		std::function< void(const Formula &)>	assert,
		const PredicateAbstractor &	predicate_abstractor )

Construct a BoundImplicator.

Parameters

config	configuration
assert	assertion function. It adds assertions to the context
predicate_abstractor	predicate abstractor containing the assertions

Definition at line 14 of file BoundImplicator.cpp.

Member Function Documentation

AddAssertion()

template<int NVariables>

void dlinear::BoundImplicator::AddAssertion ( const Formula & assertion )

private

Add an assertion to the constraints_ map.

Based on the number of free variables in the assertion, it will call the appropriate AddAssertion method.

Template Parameters

NVariables

number of free variables in the assertion

Parameters

assertion

assertion to add

---

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

• dlinear/solver/BoundImplicator.h
• dlinear/solver/BoundImplicator.cpp