Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds Term.{is_fp, get_fp} #30

Merged
merged 2 commits into from
Aug 21, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Make types not mutually recursive
  • Loading branch information
filipeom committed Aug 21, 2024
commit fb146d4546781e23ec6423567a03cb4424b22b1f
52 changes: 26 additions & 26 deletions cvc5_external.ml
Original file line number Diff line number Diff line change
@@ -23,57 +23,57 @@

type ptr

and result = ptr
type result = ptr

and synth_result = ptr
type synth_result = ptr

and sort = ptr
type sort = ptr

and term = ptr
type term = ptr

and op = ptr
type op = ptr

and datatype = ptr
type datatype = ptr

and datatype_constructor_decl = ptr
type datatype_constructor_decl = ptr

and datatype_decl = ptr
type datatype_decl = ptr

and datatype_selector = ptr
type datatype_selector = ptr

and datatype_constructor = ptr
type datatype_constructor = ptr

and grammar = ptr
type grammar = ptr

and solver = ptr
type solver = ptr

and term_manager = ptr
type term_manager = ptr

and option_info = ptr
type option_info = ptr

and proof = ptr
type proof = ptr

and proof_rule = ptr
type proof_rule = ptr

and statistics = ptr
type statistics = ptr

and unknown_explanation = ptr
type unknown_explanation = ptr

and sort_kind = ptr
type sort_kind = ptr

and kind = ptr
type kind = ptr

and rounding_mode = ptr
type rounding_mode = ptr

and proof_format = ptr
type proof_format = ptr

and proof_component = ptr
type proof_component = ptr

and learned_lit_type = ptr
type learned_lit_type = ptr

and block_model_mode = ptr
type block_model_mode = ptr

and find_synth_target = ptr
type find_synth_target = ptr

external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat"