Skip to content

CDCL(OCAC) static Linux x86-64 binary (v1.0.4)

Latest

Choose a tag to compare

@fuqi-jia fuqi-jia released this 27 Jun 19:06

Statically-linked Linux x86-64 build of CDCL(OCAC) — the complete OMT(NRA) solver (cvc5 1.0.4 fork). ldd reports not a dynamic executable, so no libraries are needed: just download, chmod +x, and run.

Usage

./cvc5-ocac-static-linux-x86_64 input.smt2

with (set-logic OMT_QF_NRA) and (minimize ...) / (maximize ...). Returns exact optima, including algebraic numbers (e.g. the optimum of max x s.t. x^2<=2 is reported as the real algebraic number for sqrt(2)).

Built from main (commit with the libpoly lp_variable_t->poly::Variable build fix) via ./configure.sh --auto-download --poly --cocoa --static --static-binary.