toDimacs method

String toDimacs({
  1. bool includeNames = true,
})

Convert a goal into a DIMACS formatted string.

The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

Implementation

String toDimacs({bool includeNames = true}) {
  return _c._z3
      .goal_to_dimacs_string(_goal, includeNames)
      .cast<Utf8>()
      .toDartString();
}