C++ API for parsing DIMACS files

[rainoftime]

Z3 has a frontend for DIMACS CNF files. But unlike SMT-LIB2, we cannot use C++ API to parse a DIMACS file, construct an expression object, and add the expression to a solver. Is there any plan for supporting this? Maybe some extensions of DIMACS like Pseudo Boolean(PB) constraints and QBF are also worthwhile to be added.

I noticed that a similar issue was addressed before https://github.com/Z3Prover/z3/issues/1042

[NikolajBjorner]

Since parsing DIMACS and WCNF isn't onerous I would prefer to not expose API features for this. Below is a simple cnf to smt2 conversion script. It can be changed to directly add assertions to a solver.

Z3 isn't a better solver on QBF benchmarks that have been exposed to QBF solvers, at least I hope not, because otherwise the state of QBF would be unimpressive :-).

import sys

def parse_decl(line, ous):
    decls = line.split()
    nvars = int(decls[2])
    for i in range(nvars):
        ous.write("(declare-const p%d Bool)\n" % (i + 1))    

def parse_clause(line, ous):
    literals = line.split()   
    assert (literals[-1] == '0')
    ous.write("(assert (or ")
    for p in literals:
        if p == '0':
           break
        if p[0] == '-':
           ous.write("(not p")
           ous.write(p[1:])
           ous.write(") ")
        else:
           ous.write("p")
           ous.write(p)
           ous.write(" ")
    ous.write("))\n")

def parse_file(file):
    ins = open(file)
    ous = open("%s.smt2" % file, 'w')
    ous.write("(set-logic QF_FD)\n")
    line = ins.readline()
    parse_decl(line, ous)
    line = ins.readline()
    while line:
        parse_clause(line, ous)
        line = ins.readline()
    ous.write("(check-sat)")
    ins.close()
    ous.close()

[rainoftime]

Since many automated reasoning algorithms and tools((PB, QBF, SAT#, etc..) can be built on top of Minisat by extending it or just using its C APIs. Personally, I think exposing C/C++ APIs for interacting with z3's SAT engine(z3/src/sat) would help a lot.

[NikolajBjorner]

Added to an unstable dev branch, which has a dedicated Z3_solver_from_file method.