formalsec / ocaml-cvc5 Goto Github PK

Makes the code consistent

Getting:

File "bin/dune", line 11, characters 7-12:
11 |  (name main2)
            ^^^^^
/usr/bin/ld: /home/filipe/.local/share/opam/wasp/lib/cvc5/libcvc5.a(cadical.cpp.o): in function `cvc5::internal::prop::CadicalSolver::getProofSketch()':
cadical.cpp:(.text+0x56e): undefined reference to `CaDiCaL::Solver::flush_proof_trace(bool)'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking (exit code 1)

On ubuntu server:

Description:    Ubuntu 23.10
Release:        23.10
Codename:       mantic

Need to investigate further

We will follow CVC5 versioning to provide bindings for each specific version of the prover

opam's sandboxing doesn't allow network requests, so we can't rely on the --auto-download flag for cvc5's build

Instead, we need to build each dependency separately through dune

Some license

Once this repository is public we could add some github actions to verify that it builds and passes tests on pull requests and such

Something like: https://github.com/formalsec/encoding/blob/main/.github/workflows/build.yml

When dealing with a bigger number of formulas a fatal error/seg fault occurs.

For instance, in example incremental.ml (https://github.com/formalsec/ocaml-cvc5/blob/main/examples/incremental.ml), if the number of loop iterations is set to a higher number (e.g. 5000 iterations) we get the error:

Fatal error: exception Invalid_argument("Invalid term in 'children' at index 0, expected a term associated with the term manager of this solver") or simply a segmentation fault.