Class Paramita::Testing::SatSolverDummy¶

Inherits the following classes: Paramita::SatSolver

Public Static Attributes inherited from Paramita::SatSolver¶

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::SatSolver"`

Public Static Attributes inherited from Paramita::NonIncrSatSolver¶

See Paramita::NonIncrSatSolver

Type	Name
constexpr const char *const	m_interface_id = `/* multi line expression */`

Public Static Attributes inherited from Paramita::ClauseContainer¶

See Paramita::ClauseContainer

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::ClauseContainer"`

Public Static Attributes inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
constexpr const char *const	m_interface_id = `"Paramita::Plugin"`

Public Functions¶

Type	Name
virtual	add_clause (const Clause & clause) override Add a single clause.
virtual std::uint64_t	max_var () override const Get the largest variable used by the container.
virtual std::vector< Literal >	model () override const Get the model (solution) after solving.
virtual	set_minimum_var (std::uint64_t var) override Sets the maximum variable known to the container to at least this one.
virtual std::optional< bool >	solve (const std::vector< Literal > & assumptions, const SolvingBudget & budget) override Solve the underlying formula under the given assumptions.

Public Functions inherited from Paramita::SatSolver¶

See Paramita::SatSolver

Type	Name
	SatSolver () = default
	SatSolver (const SatSolver &) = delete
	SatSolver (SatSolver &&) = delete
virtual	add_observed_var (int var) Marks a variable as observed by the external propagator.
virtual SatSolver *	clone () override Clones the incremental SAT solver.
virtual	connect_external_propagator (std::shared_ptr< Paramita::Propagator > propagator) Connects an external `Propagator` to the solver.
virtual	connect_learner (std::shared_ptr< Paramita::Learner > learner) Connects a `Learner` to the solver.
virtual	disconnect_external_propagator () Disconnects the currently connected external propagator.
virtual	disconnect_learner () Disconnects the currently connected learner.
virtual	force_backtrack (int new_level) Forces the solver to backtrack.
virtual bool	is_decision (int lit) Checks whether a literal is assigned as a decision.
SatSolver &	operator= (const SatSolver & container) = delete
SatSolver &	operator= (SatSolver &&) = delete
virtual	remove_observed_var (int var) Stops observing a variable.
virtual	reset_observed_vars () Removes all observed variables.
	~SatSolver () override

Public Functions inherited from Paramita::NonIncrSatSolver¶

See Paramita::NonIncrSatSolver

Type	Name
	NonIncrSatSolver () = default
	NonIncrSatSolver (const NonIncrSatSolver &) = delete Deleted copy constructor (pure interface).
	NonIncrSatSolver (NonIncrSatSolver &&) = delete Deleted move constructor (pure interface).
virtual	assume (Literal lit) Add an assumption for the next `solve` or`propagate` call.
virtual NonIncrSatSolver *	clone () override Clones the SAT solver.
virtual std::vector< Literal >	core () Retrieve the unsatisfiable core.
virtual bool	failed (Literal lit) Check if a literal belongs to the unsatisfiable core.
virtual	freeze (Literal lit) Freeze a variable.
virtual std::optional< bool >	get_phase (Literal lit) Returns the default phase for a decision variable.
virtual	interrupt () Interrupts the resolution process.
virtual std::optional< bool >	is_fixed (Literal lit) Detect if a variable is implied at root level.
virtual bool	is_frozen (Literal lit) Checks if a variable is frozen.
virtual	melt (Literal lit) Melts a variable.
virtual std::vector< Literal >	model () const = 0 Get the model (solution) after solving.
virtual int	num_active_vars () Counts how many variables are active.
virtual long	num_conflicts () Get the number of conflicts encountered.
NonIncrSatSolver &	operator= (const NonIncrSatSolver & container) = delete Deleted copy assignment (pure interface).
NonIncrSatSolver &	operator= (NonIncrSatSolver &&) = delete Deleted move assignment (pure interface).
virtual	phase (Literal lit) Set the default phase for a decision variable during branching.
virtual std::pair< bool, std::vector< Literal > >	propagate (const std::vector< Literal > & assumptions) Propagate the given assumptions.
virtual	simplify (unsigned int num_rounds) Simplify the formula.
virtual std::optional< bool >	solve (const std::vector< Literal > & assumptions, const SolvingBudget & budget) = 0 Solve the underlying formula under the given assumptions.
virtual	unphase (Literal lit) Removes the default phase for a decision variable.
virtual std::optional< bool >	val_lit (Literal lit) Get the truth value for a literal.
	~NonIncrSatSolver () override

Public Functions inherited from Paramita::ClauseContainer¶

See Paramita::ClauseContainer

Type	Name
	ClauseContainer () = default Constructor that initializes an empty container.
	ClauseContainer (const ClauseContainer &) = delete Deleted copy constructor (pure interface).
	ClauseContainer (ClauseContainer &&) = delete Deleted move constructor (pure interface).
virtual	add_clause (const Clause & clause) = 0 Add a single clause.
virtual	add_clauses (const std::vector< Clause > & clauses) Add multiple clauses to the container.
virtual	add_lit (Literal lit) Add a clause literal by literal.
virtual ClauseContainer *	clone () Clones the current CNF Container.
virtual std::uint64_t	max_var () const = 0 Get the largest variable used by the container.
virtual int	num_clauses () const Get the number of clauses hold currently by the container.
ClauseContainer &	operator= (const ClauseContainer & container) = delete Deleted copy assignment (pure interface).
ClauseContainer &	operator= (ClauseContainer &&) = delete Deleted move assignment (pure interface).
virtual	set_minimum_var (std::uint64_t var) = 0 Sets the maximum variable known to the container to at least this one.
	~ClauseContainer () override Virtual destructor for the container.

Public Functions inherited from Paramita::Plugin¶

See Paramita::Plugin

Type	Name
	Plugin () = default
	Plugin (const Plugin &) = delete Deleted constructor (pure interface).
	Plugin (Plugin &&) = delete Deleted constructor (pure interface).
virtual ParameterType	get (const std::string & name) Get the parameter's value.
virtual ParameterSpace	get_parameter_space () Get the parameter space for this class.
Plugin &	operator= (const Plugin & container) = delete Deleted constructor (pure interface).
Plugin &	operator= (Plugin &&) = delete Deleted constructor (pure interface).
virtual	set (const std::string & name, const ParameterType & value) Set a parameter.
virtual	~Plugin () = default

Public Functions Documentation¶

function add_clause¶

Add a single clause.

inline virtual Paramita::Testing::SatSolverDummy::add_clause (
    const Clause & clause
) override

The clause is represented as a sequence of literals. Each literal is represented as an integer, where its absolut value is the identifier of a variable. A positive integer represents the variable and a negative integer its negation.

Parameters:

clause The clause to be added to the container.

Implements Paramita::ClauseContainer::add_clause

function max_var¶

Get the largest variable used by the container.

inline virtual std::uint64_t Paramita::Testing::SatSolverDummy::max_var () override const

The largest variable is determined by its identifier.

Note:

Note that this does not mean that the container has clauses containing literals for all the variables between 1 and CnfContainerinterface::max_var, there may be gaps.

Warning:

If the container creates variables internally, this method MUST also consider those variables, even if the user did not add them directly. This ensures that the user cannot generate variable clashes when adding new clauses to the container.

Postcondition:

The return value is equal or larger to the absolute value for any literal passed to add_clause, add_clauses, or add_lit.

Returns:

The (positive) integer representing the largest variable.

Implements Paramita::ClauseContainer::max_var

function model¶

Get the model (solution) after solving.

inline virtual std::vector< Literal > Paramita::Testing::SatSolverDummy::model () override const

Returns:

The vector where the solution will be stored. Each element of the vector is a literal that was set to true.

Precondition:

The method solve was called.

Precondition:

A solution was found by solve.

Warning:

Undefined behaviour if solve returned std::nothing.

Exception:

NotSolvedException if solve was not called before.
UnsatisfiableException if solve found the instance to be unsatisfiable.

Implements Paramita::NonIncrSatSolver::model

function set_minimum_var¶

Sets the maximum variable known to the container to at least this one.

inline virtual Paramita::Testing::SatSolverDummy::set_minimum_var (
    std::uint64_t var
) override

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the ClauseContainer::max_var method to determine the next free variable, this method ensures that existing variables cannot be reused.

Postcondition:

The value returned by max_var must be larger or equal than the one provided.

Postcondition:

The value returned by max_var cannot be reduced by this call.

Parameters:

var The variable to be registered to the container.

Implements Paramita::ClauseContainer::set_minimum_var

function solve¶

Solve the underlying formula under the given assumptions.

inline virtual std::optional< bool > Paramita::Testing::SatSolverDummy::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) override

If interrupted, the solver is responsible from clearing the interruption.

See also: interrupt

Parameters:

assumptions A vector with literals that will be fixed during this solve call.
budget Solving limits for this call.

Precondition:

The method solve was not called previously OR no the formula has not been modified since the last solve call.

Postcondition:

The solving budget is reset to unlimited.

Returns:

An option with a boolean representing the satisfiability status of the formula under the specified assumptions, or std::nullopt if it could not be determined.

Implements Paramita::NonIncrSatSolver::solve