Function z3_sys::Z3_goal_to_dimacs_string [−][src]
pub unsafe extern "C" fn Z3_goal_to_dimacs_string(
c: Z3_context,
g: Z3_goal
) -> Z3_string
Expand description
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 the if caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.