nx_smtlib_parse.nx
buildroot/runtime/nx_smtlib_parse.nx
about
nx_smtlib_parse.nx -- SMT-LIB v2 parser, propositional fragment.
Foundation for SMT-COMP entry (https://smt-comp.github.io/). SMT-LIB
is the canonical input format for SMT solvers (Z3, cvc5, Yices,
Bitwuzla). This MVP handles the QF_UF (Quantifier-Free Uninterpreted
Functions, Boolean-only) fragment -- enough to enter the easiest
SMT-COMP divisions.
Grammar handled:
script ::= command*
command ::= "(" "set-logic" symbol ")"
| "(" "declare-fun" symbol "()" "Bool" ")"
| "(" "declare-const" symbol "Bool" ")"
| "(" "assert" formula ")"
| "(" "check-sat" ")"
| "(" "exit" ")"
formula ::= symbol -- atom
| "true" | "false"
| "(" "not" formula ")"
| "(" "and" formula+ ")"
| "(" "or" formula+ ")"
| "(" "=>" formula formula ")"
| "(" "=" formula formula ")"
| "(" "xor" formula formula ")"
Output: a SatProblem (DIMACS literals) ready for nx_sat_solve.
Theories (LIA, LRA, BV, arrays, strings) deferred to later commits;
each requires a dedicated theory-solver primitive.
dependencies 7 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_result.nxnx_file_result.nxnx_sat_solver.nx
imported by: nx_smtlib_parse_test.nx
structs
| 54 | struct SmtParser |
consts
| 46 | const NX_SMT_TOK_LPAREN: nx_int = 1 |
| 47 | const NX_SMT_TOK_RPAREN: nx_int = 2 |
| 48 | const NX_SMT_TOK_SYM: nx_int = 3 |
| 49 | const NX_SMT_TOK_EOF: nx_int = 4 |
| 51 | const NX_SMT_MAX_SYM_LEN: nx_int = 64 |
| 52 | const NX_SMT_MAX_VARS: nx_int = 1024 |
| 62 | const NX_SMT_PARSER_BYTES: nx_int = 40 |
functions
| 64 | func nx_smt_parser_new(buf: *u8, n: nx_int) -> *SmtParser |
| 76 | func nx_smt_skip_ws(p: *SmtParser) called by 4: nx_smt_skip_wsnx_smt_next_toknx_smt_parse_formulanx_smt_handle_assert calls 1: nx_smt_skip_ws |
| 107 | func nx_smt_next_tok(p: *SmtParser, out_sym: *u8) -> nx_int |
| 135 | func nx_smt_var_id(p: *SmtParser, name: *u8) -> nx_int |
| 150 | func nx_smt_parse_formula(p: *SmtParser) -> nx_int; |
| 166 | func nx_smt_parse_formula(p: *SmtParser) -> nx_int |
| 233 | func nx_smt_handle_assert(p: *SmtParser) called by 1: nx_smtlib_parse calls 7: nx_smt_skip_wssys_mmapnx_smt_next_toknx_smt_var_idnx_sat_add_clausenx_str_eq+1 |
| 322 | func nx_smtlib_parse(buf: *u8, n: nx_int) -> *SatFormula called by 1: main calls 6: nx_smt_parser_newsys_mmapnx_smt_next_toknx_str_eqnx_smt_var_idnx_smt_handle_assert |