Namespace containing dimacs io utilities. More...
Functions | |
| Literal | from_dimacs (int val) noexcept |
| int | to_dimacs (Literal l) noexcept |
| auto | read_from_dimacs (std::istream &in) -> std::pair< std::vector< std::vector< Literal > >, std::size_t > |
| template<std::ranges::range R> | |
| std::string | to_dimacs (const R &clauses) |
| template<concepts::typed_range< Literal > L> | |
| std::string | to_dimacs (const L &literals) |
Detailed Description
Namespace containing dimacs io utilities.
Function Documentation
◆ from_dimacs()
|
noexcept |
Converts an integer to a sat::Literal
- Parameters
-
val literal value. The value +5 for example corresponds to the positive literal of the variable with ID 5, whereas -5 corresponds to the negative literal
- Returns
- converted Literal
◆ read_from_dimacs()
| auto sat::inout::read_from_dimacs | ( | std::istream & | in | ) | -> std::pair< std::vector< std::vector< Literal > >, std::size_t > |
Reads a SAT problem from a stream
- Parameters
-
in input stream to read from
- Returns
- std::pair containing (all clauses of the problem, the number of variables in the problem)
◆ to_dimacs() [1/3]
template<concepts::typed_range< Literal > L>
| std::string sat::inout::to_dimacs | ( | const L & | literals | ) |
Converts a range of literals to dimacs format
- Template Parameters
-
L Literal range type
- Parameters
-
literals the literals to convert
- Returns
- dimacs string
◆ to_dimacs() [2/3]
template<std::ranges::range R>
| std::string sat::inout::to_dimacs | ( | const R & | clauses | ) |
Converts a range of clauses to dimacs format
- Template Parameters
-
R clause range type
- Parameters
-
clauses A range of clauses
- Returns
- dimacs string
References sat::Variable::get(), and sat::var().
Here is the call graph for this function:
◆ to_dimacs() [3/3]
|
noexcept |
Converts a sat::Literal to a dimacs literal
- Parameters
-
l Literal to convert
- Returns
- 1 based integer representing the literal in dimacs format
