Module Astral_internal

module AggresiveSimplifier : sig ... end
module Antiprenexing : sig ... end
module ArrayEncoding : sig ... end
module AstralLib : sig ... end
module BackendConfig : sig ... end
module BackendSelection : sig ... end
module BackendUtils : sig ... end
module Backend_preprocessor : sig ... end
module Backend_sig : sig ... end
module BaseLogic : sig ... end
module Bitvector : sig ... end
module BitvectorLocations : sig ... end
module BitvectorSets : sig ... end
module BitwuzlaNative : sig ... end
module Bitwuzla_backend : sig ... end
module Boolector_backend : sig ... end
module BuiltinBuilder : sig ... end
module CVC5_backend : sig ... end
module CVC5_native : sig ... end
module Colors : sig ... end
module Config : sig ... end
module ConfigReader : sig ... end
module Constant : sig ... end
module Context : sig ... end
module Counter : sig ... end
module DLS : sig ... end

Constructors

module Datatype : sig ... end
module DatatypeLocations : sig ... end
module Datatype_sig : sig ... end
module Debug : sig ... end
module Debug_sig : sig ... end
module DependencyGraph : sig ... end
module DirectSets : sig ... end
module DummyBackend : sig ... end
module Encoding_context_sig : sig ... end
module Engine : sig ... end
module EntailmentSimplifier : sig ... end
module EqualityRewritter : sig ... end
module Exceptions : sig ... end
module FileUtils : sig ... end
module FragmentChecker : sig ... end
module Freed : sig ... end
module Generic_smtlib : sig ... end

==== Translation ====

module GlobalSID : sig ... end
module HeapEncoding_sig : sig ... end
module HeapSort : sig ... end
module ID_sig : sig ... end
module Identifier : sig ... end
module IncrementalSolverBuilder : sig ... end
module IncrementalUnfolding : sig ... end
module InductiveDefinition : sig ... end
module Inlining : sig ... end
module Interval : sig ... end
module IntroduceIfThenElse : sig ... end
module Json_output : sig ... end
module LS : sig ... end

Constructors

module List_utils : sig ... end
module Lists : sig ... end

Singly-linked list parametrised by a sort S and field F.

module LocationBounds : sig ... end
module LocationBounds0 : sig ... end
module LocationBuilder : sig ... end
module LocationUtils : sig ... end
module Location_sig : sig ... end
module Logger : sig ... end
module LoggerState : sig ... end
module Logger_sig : sig ... end
module Logic_sig : sig ... end
module LowLevelSeplog : sig ... end
module MemoryModel : sig ... end
module MemoryModel0 : sig ... end
module ModelAdapter : sig ... end
module ModelChecker : sig ... end
module ModelParser : sig ... end
module NLS : sig ... end

Constructors

module NegationNormalisation : sig ... end
module Parser : sig ... end
module ParserContext : sig ... end
module ParserContext_type : sig ... end
module ParserException : sig ... end
module ParserUtils : sig ... end
module PathBound : sig ... end
module PreciseToImprecise : sig ... end
module PredicateAbstraction : sig ... end
module PredicatePreprocessing : sig ... end

Preprocessing

module Preprocessor : sig ... end
module PrintUtils : sig ... end
module Profiler : sig ... end
module QuantifierElimination : sig ... end
module QuantifierEncoding : sig ... end
module ReachabilityEncoding : sig ... end
module RemoveVariadic : sig ... end
module ReportUtils : sig ... end
module Result_syntax : sig ... end
module RuleAntiunification : sig ... end
module SID : sig ... end
module SID0 : sig ... end
module SID_checks : sig ... end
module SL : sig ... end
module SLID : sig ... end
module SL_builtins : sig ... end

This module groups constructors for builtin inductive predicates.

module SL_graph : sig ... end
module SL_graph0 : sig ... end
module SL_printer : sig ... end
module SL_quantifiers : sig ... end
module SMT : sig ... end
module SMTLIB_printer : sig ... end
module SMT_sig : sig ... end
module SetEncoding_sig : sig ... end
module Simplifier : sig ... end
module SingleQuerySolver : sig ... end
module SmallModels : sig ... end
module Smtlib_backend_builder : sig ... end
module Solver : sig ... end
module Solver_utils : sig ... end
module Sort : sig ... end
module SortBound : sig ... end
module StackHeapModel : sig ... end
module ThreeValuedLogic : sig ... end
module Topped_set : sig ... end
module Translation : sig ... end
module Translation_context : sig ... end
module Translation_sig : sig ... end
module UnfoldIDs : sig ... end
module UnicodeSymbols : sig ... end
module Variable : sig ... end
module Yices_backend : sig ... end
module Z3_backend : sig ... end
module Z3_external : sig ... end