search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Simulating a parse-only mode with Z3 for SMT-LIB v2 #59

Closed rbonichon closed 9 years ago

rbonichon commented 9 years ago

This is not a bug and more a want for explanation. If there is a better medium fot that kind of exchange (e-mail?), please feel free to indicate it.

I am running some benchmarks on various tools about SMT-LIB. One of the measuring stick is of course Z3. I am mostly interested as of now in the parsing time / AST construction.

Am I mistaken if I say that I can simulate/approximate a parse-only mode for Z3/SMT-LIB v2 by commenting line 2017 in src/parsers/smt2/smt2parser.cpp ? This is this line:

m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos);

I am trying to not trigger the SMT solving engine of Z3 and just have something close to simple AST construction.

wintersteiger commented 9 years ago

That change will disable check-sat commands in SMT2 input files (but not any other commands, or non-SMT2 input files). Alternatively, the API functions Z3_parse_smtlib2_string or Z3_parse_smtlib2_file could be useful too.

Closing this as resolved, please reopen if more questions come up.