package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

Dune Dependency

alt-ergo.ocamlpro.com Readme LicenseRef-OCamlPro-Non-Commercial-Purpose-License-Version-1 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

O

OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.0.tar.gz

sha256=7f1906900272125315833b9f0a6abc3c5af7b836d604fdb10a98a9079c1b99f9

md5=d99bfaf748f7c640222e59677e6afd7c

doc/src/alt-ergo-lib/ite.ml.html

Source file `ite.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
(******************************************************************************)
(*                                                                            *)
(*     Alt-Ergo: The SMT Solver For Software Verification                     *)
(*     Copyright (C) 2013-2018 --- OCamlPro SAS                               *)
(*                                                                            *)
(*     This file is distributed under the terms of the license indicated      *)
(*     in the file 'License.OCamlPro'. If 'License.OCamlPro' is not           *)
(*     present, please contact us to clarify licensing.                       *)
(*                                                                            *)
(******************************************************************************)

type 'a abstract = unit

module type ALIEN = sig
  include Sig.X
  val embed : r abstract -> r
  val extract : r -> (r abstract) option
end

module Shostak (X : ALIEN) = struct

  type t = X.r abstract
  type r = X.r

  let name           = "Ite"
  let is_mine_symb _ _ = false
  let fully_interpreted _ = assert false
  let type_info _    = assert false
  let color _        = assert false
  let print _ _      = assert false
  let embed _        = assert false
  let is_mine _      = assert false
  let compare _ _    = assert false
  let equal _ _      = assert false
  let hash _         = assert false
  let leaves _       = assert false
  let subst _ _ _    = assert false
  let make _         = assert false
  let term_extract _ = None, false
  let abstract_selectors _ _ = assert false
  let solve _ _ = assert false
  let assign_value _ _ _ = assert false
  let choose_adequate_model _ _ _ = assert false
end