smt_solvers_interface

prob_prolog/src/smt_solvers_interface/smt_solvers_interface.pl

Modules

  • ProB_Preferences_maxx.pl
  • TestPrefs.pl
  • alloy2b
  • alloy2b_benchmarks
  • ample_sets
  • any.pl
  • assert_profiler
  • ast_cleanup_for_smt
  • ast_inspector
  • ast_optimizer_for_smt
  • ast_to_difference_logic
  • atelierb_provers_interface
  • atom.pl
  • avl_custom
  • avl_tools
  • avl_tree.pl
  • avl_ugraphs
  • avlp
  • b2sat
  • b2setlog
  • b_arithmetic_expressions.pl
  • b_ast_cleanup
  • b_ast_cleanup_rewrite_rules
  • b_cogen
  • b_compiler
  • b_enumerate
  • b_enumeration_order_analysis
  • b_expression_sharing
  • b_global_sets
  • b_intelligent_trace_replay
  • b_interpreter
  • b_interpreter_components
  • b_interpreter_eventb
  • b_machine_identifier_normalization
  • b_operation_cache
  • b_operation_guards
  • b_read_write_info
  • b_show_history
  • b_simplifier
  • b_state_model_check
  • b_synthesis
  • b_to_cnf
  • b_trace_checking
  • banditfuzz
  • basic_unit_tests
  • before_after_predicates
  • benchmark.pl
  • benchmark_analyser.pl
  • between.pl
  • bf_env
  • bliss_interface
  • block_checker.pl
  • bmachine
  • bmachine_construction
  • bmachine_static_checks
  • bmachine_structure
  • bmc
  • bool_pred
  • bool_pred_test.pl
  • boolean.pl
  • bsyntaxtree
  • bsyntaxtree_quantifiers
  • bvisual
  • bvisual_any_maxsolver
  • cbc_ba
  • cbc_path_solver
  • cbc_refinement_checks
  • cdclt_pred_to_sat
  • cdclt_preprocessing
  • cdclt_sat_solver
  • cdclt_settings
  • cdclt_solver
  • cdclt_stats
  • ce_replay
  • chr_set_membership
  • closures
  • clpfd_interface
  • clpfd_lists
  • clpfd_off_interface
  • clpfd_tables
  • code2vec
  • code2vec_tests
  • codespeed_versions
  • compile_time_flags
  • consistencycheck
  • constraints
  • counter
  • coverage_statistics
  • coverage_term_expander.pl
  • coverage_tools
  • coverage_tools_annotations
  • csp_basic
  • csp_sequences
  • csp_sets
  • csp_tuples
  • ctigar
  • ctl
  • custom_explicit_sets
  • cvc4interface
  • debug
  • debugging_calls
  • debugging_calls_te.pl
  • delay
  • dependence
  • dev.pl
  • difference_logic_solver
  • disprover
  • disprover_test_runner
  • disprover_test_runner_cli.pl
  • domain
  • domain_test.pl
  • dot_graphs_static_analysis
  • eclipse_interface
  • enable_graph
  • enabling_analysis
  • enabling_predicates
  • error_manager
  • eval_interface
  • eval_let_store
  • eval_strings
  • eventhandling
  • example.pl
  • experiment.pl
  • external_function_declarations
  • external_functions
  • external_functions_reals
  • external_functions_svg
  • fastio_inspector.pl
  • fd_utils_clpfd
  • fdr_csp_generator
  • fibonacci_heap
  • find_whens.pl
  • fixed_value.pl
  • float.pl
  • fuzzer
  • fuzzer_runner.pl
  • fuzzfile
  • fuzzing
  • gensym
  • grammar
  • graph_iso_nauty
  • graphical_state_viewer_images
  • graphiso
  • graphiso_test
  • ground_truth
  • gui_tcltk.pl
  • hashing
  • haskell_csp
  • haskell_csp_analyzer
  • heuristic_grouping.pl
  • hit_profiler
  • ic3
  • inf_arith
  • input_syntax_tree
  • integer.pl
  • interval_calc
  • json_parser
  • junit_tests
  • kernel_card_arithmetic
  • kernel_cardinality_attr
  • kernel_dif
  • kernel_equality
  • kernel_freetypes
  • kernel_frozen_info
  • kernel_lists
  • kernel_mappings
  • kernel_mappings_dispatch
  • kernel_non_empty_attr
  • kernel_objects
  • kernel_ordering
  • kernel_propagation
  • kernel_reals
  • kernel_records
  • kernel_strings
  • kernel_sym_break_order
  • kernel_tools
  • kernel_waitflags
  • kernel_z
  • kinduction
  • kodkod
  • kodkod2
  • kodkod_annotator
  • kodkod_integer_recalc
  • kodkod_printer
  • kodkod_process
  • kodkod_rewrite
  • kodkod_test
  • kodkod_tools
  • kodkod_translate
  • kodkod_typing
  • latex_processor
  • library_setup
  • list.pl
  • location_vars_to_program
  • logger
  • logging
  • ltl
  • ltl2ba
  • ltl_fairness
  • ltl_propositions
  • ltl_safety
  • ltl_tools
  • ltl_translate
  • ltl_verification
  • ltlc
  • ltsmin
  • ltsmin_c_interface
  • ltsmin_trace
  • master
  • maxsolver
  • mcdc_coverage
  • member_of.pl
  • memoization
  • meta_interface
  • mic_generation
  • model_checker
  • model_translation
  • module_information
  • msg_interop
  • mutate_expressions
  • mutation.pl
  • mutation_prob_ast_int_expr.pl
  • mutation_prob_ast_pred.pl
  • mutation_prob_ast_seq_expr.pl
  • mutation_prob_ast_set_expr.pl
  • mutations
  • myheap
  • number.pl
  • operation_data_generator
  • optimizing_solver
  • ordsetsp
  • parsercall
  • partition_detection
  • pathes
  • pathes_extensions_db
  • pathes_lib
  • performance_messages
  • pge_algo
  • plspec
  • plspec_core
  • plspec_logger
  • plspec_test
  • pltables
  • pltables_export
  • pltables_export_csv
  • pltables_export_html
  • pltables_export_latex
  • pltables_export_tools
  • pltables_export_xml
  • plunit_test_runner
  • pragmas
  • predicate_abstraction
  • predicate_analysis
  • predicate_data_generator
  • predicate_debugger
  • predicate_evaluator
  • predicate_handling
  • pref_definitions
  • preferences
  • preprofiler
  • preserve_behaviour_test.pl
  • prettyprinter
  • prob2_interface
  • prob_ast_any.pl
  • prob_ast_boolean.pl
  • prob_ast_couple.pl
  • prob_ast_eval_int_expr.pl
  • prob_ast_eval_pred.pl
  • prob_ast_eval_seq_expr.pl
  • prob_ast_eval_set_expr.pl
  • prob_ast_expr.pl
  • prob_ast_identifier.pl
  • prob_ast_int_expr.pl
  • prob_ast_integer.pl
  • prob_ast_minimize_int_expr.pl
  • prob_ast_minimize_pred.pl
  • prob_ast_minimize_seq_expr.pl
  • prob_ast_minimize_set_expr.pl
  • prob_ast_pred.pl
  • prob_ast_record.pl
  • prob_ast_sat.pl
  • prob_ast_seq.pl
  • prob_ast_seq_expr.pl
  • prob_ast_set.pl
  • prob_ast_set_expr.pl
  • prob_ast_string.pl
  • prob_cli
  • prob_cov.pl
  • prob_cov_runner.pl
  • prob_profiling_cli.pl
  • prob_rule_compiler
  • prob_socketserver
  • prob_startup
  • prob_state_predicates
  • prob_tcltk.pl
  • prob_type.pl
  • prob_value_any.pl
  • prob_value_boolean.pl
  • prob_value_integer.pl
  • prob_value_record.pl
  • prob_value_seq.pl
  • prob_value_set.pl
  • prob_value_string.pl
  • probhash
  • probsocket_proxy.pl
  • profiler
  • profiler_gui
  • profiler_te
  • prologTasks
  • prothon
  • proz
  • ptest.pl
  • quantifier_instantiation
  • random_permutations
  • rational.pl
  • record_detection
  • reduce_graph_state_space
  • refinement_checker
  • regexp
  • rewrite_rules_db
  • runtime_profiler
  • safety_mc
  • sap
  • sat_symmetry_breaking
  • satsolver
  • schemaexpansion
  • schemavars
  • self_check
  • self_check_off.pl
  • seq_rewriter
  • set_rewriter
  • smt_common_predicates
  • smt_solver_benchmarks
  • smt_solvers_interface
  • smt_symmetry_breaking
  • smtlib2_cli
  • smtlib2_environment
  • smtlib2_interpreter
  • smtlib2_parser
  • smtlib2_parser_tests
  • smtlib2_translation
  • snippets.pl
  • softfloat
  • solver_dispatcher
  • solver_handling
  • solver_interface
  • solvercalls
  • source_profiler
  • specfile
  • state_as_dot_graph
  • state_custom_dot_graph
  • state_graph_canon
  • state_packing
  • state_permuter
  • state_space
  • state_space_dijkstra
  • state_space_exploration_modes
  • state_space_explorer
  • state_space_open_nodes
  • state_space_open_nodes_c
  • state_space_reduction
  • static_analysis
  • static_enabling_analysis
  • static_ordering
  • store
  • subexpressions
  • succeed_max
  • symmetry_marker
  • symmetry_reduction
  • synthesis_tests
  • synthesis_util
  • system_call
  • table_tools
  • tcltk_interface
  • tcltk_tree_inspector
  • test
  • test2
  • test_fibonacci_heap
  • test_nodestore.pl
  • test_paths
  • test_regexp
  • test_regexp_unicode
  • test_runner
  • test_runner_cov.pl
  • test_typechecker
  • testcases
  • testdining
  • testltlc
  • tests.pl
  • testsignal.pl
  • timer
  • tools
  • tools_commands
  • tools_fastread
  • tools_files
  • tools_io
  • tools_lists
  • tools_matching
  • tools_meta
  • tools_portability
  • tools_positions
  • tools_printing
  • tools_strings
  • tools_timeout
  • trace_generator
  • translate
  • translate_keywords
  • tree.pl
  • typechecker
  • typing_tools
  • uml_generator
  • unbound_spec_test.pl
  • unsat_core_generalization
  • unsat_cores
  • user_interrupts
  • user_signal
  • validator
  • validator_test
  • value_persistance
  • variable.pl
  • version
  • visb_visualiser
  • visualize_graph
  • weakest_preconditions
  • well_def_analyser
  • well_def_hyps
  • well_def_prover
  • well_def_tools
  • welldef
  • whash_send
  • worker
  • xml2b
  • xml_prob
  • xtl_interface
  • z3interface
  • z_tools
  • z_typechecker
  • zenvironment
  • zmq
  • zmq_rpc
  • zparameters
  • ztransformations
  • Predicates of smt_solvers_interface

  • add_clause/4
  • add_literal/3
  • add_state_to_bindings/3
  • add_translation_for_solver/9
  • backjump_on_symbol/1
  • binary_operator/1
  • bind_in_prob_state/2
  • check_sat/7
  • check_sat_aux/7
  • cleanup_core_for_backjumping/2
  • clear_state/0
  • combine_satisfiable_component_results/3
  • constraint_uses_unfixed_deferred_set/2
  • contains_introduced_identifiers/2
  • contains_solver_name_with_prefix/2
  • contains_unsupported_aux/4
  • contains_unsupported_type_or_expression/3
  • contains_unsupported_type_or_expression/4
  • convert_to_cnf_model/3
  • create_bounded_smt_identifier/5
  • create_bounded_smt_state/5
  • create_enum_element_smt_state/3
  • create_exprs_for_rec_value_fields/7
  • create_let_state/7
  • create_smt_identifier/5
  • create_smt_state/5
  • create_term_size_pairs/2
  • create_virtual_enum_elms/3
  • create_virtual_enum_elms/4
  • filter_unsupported_types_or_expressions/5
  • gen_leading_zeros/4
  • get_couple_types_comp_args/2
  • get_couple_types_comp_args/4
  • get_full_pred/9
  • get_model_or_return_result/8
  • get_smt_time_out/2
  • init_smt_supported_interpreter/0
  • is_bool/2
  • is_external_function_identifier/1
  • is_ground_real/1
  • known_solver_exception/2
  • lookup/4
  • lookup_literal/3
  • mk_deferred_set_identifiers/4
  • mk_deferred_set_identifiers2/3
  • mk_expr/6
  • mk_expr_aux/7
  • mk_expr_maplist/6
  • mk_expr_skip/6
  • mk_sort/3
  • mk_value/7
  • mk_value_aux/7
  • mk_value_maplist/7
  • number_to_atom/2
  • pairwise_disjoint/5
  • pairwise_disjoint/6
  • pairwise_disjoint_mk_expr/6
  • pairwise_union/4
  • prepare_enumerated_sets_with_elms/2
  • prepare_unfixed_deferred_sets_with_virtual_elms/3
  • prob_pred_literal/1
  • remove_solvers_with_prefix/3
  • remove_useless_bindings/3
  • reset_smt_supported_interpreter/0
  • sat_skeleton_is_contradictory/2
  • setup_deferred_sets/4
  • setup_enumerated_set/4
  • setup_sets/3
  • smt_add_cnf/2
  • smt_add_cnf/3
  • smt_add_extra_clause_cnf/2
  • smt_add_predicate/5
  • smt_add_predicate_aux/3
  • smt_add_predicate_to_solver/5
  • smt_reset_cnf/1
  • smt_solve_cnf/2
  • smt_solve_pre_cleaned_predicate/6
  • smt_solve_predicate/4
  • smt_solve_predicate/5
  • smt_solve_predicate6/6
  • smt_solve_predicate_aux/6
  • smt_solve_predicate_free/3
  • smt_solve_predicate_in_state/5
  • solve_components_with_z3/7
  • sort_components_descending_term_size/2
  • store_core_for_backjumping/1
  • translate_binding/2
  • translate_literal/4
  • translate_smt_model_to_b_values_with_timeout/5
  • translate_solver_name/3
  • treat_exception/3
  • unary_operator/1
  • unsupported_expr/4
  • unsupported_type/3
  • unsupported_value_type/1
  • validate_selected_solvers/2
  • validate_selected_z3_solvers/1
  • Module Information

    Module Information


    Dynamic Predicates:           backjumping_symbols/1           solve_in_state/0           stored_solver_cnf_reference/1           stored_literal_avl_map/1

    1541 Lines

    97 Predicates

    10 Exports

    60 Imports

    Imports Exports

    Name:     term_size/2

    Module:     terms


    Name:     list_to_set/2

    Module:     sets


    Name:     same_length/2

    Module:     lists


    Name:     maplist/2

    Module:     lists


    Name:     maplist/3

    Module:     lists


    Name:     maplist/4

    Module:     lists


    Name:     append/2

    Module:     lists


    Name:     exclude/3

    Module:     lists


    Name:     include/3

    Module:     lists


    Name:     select/3

    Module:     lists


    Name:     nth0/3

    Module:     lists


    Name:     some/2

    Module:     lists


    Name:     is_list/1

    Module:     lists


    Name:    get_time_out_with_factor/2

    Module:    tools_timeout


    Name:    get_state_for_b_formula/3

    Module:    specfile


    Name:    debug_mode/1

    Module:    debug


    Name:    debug_level_active_for/1

    Module:    debug


    Name:    debug_format/3

    Module:    debug


    Name:    b_get_machine_set/1

    Module:    bmachine


    Name:    infer_value_type/2

    Module:    kernel_objects


    Name:    equal_object/2

    Module:    kernel_objects


    Name:    map_over_typed_bexpr/3

    Module:    bsyntaxtree


    Name:    safe_create_texpr/4

    Module:    bsyntaxtree


    Name:    find_typed_identifier_uses/2

    Module:    bsyntaxtree


    Name:    find_typed_identifier_uses/3

    Module:    bsyntaxtree


    Name:    get_texpr_type/2

    Module:    bsyntaxtree


    Name:    get_texpr_expr/2

    Module:    bsyntaxtree


    Name:    get_texpr_id/2

    Module:    bsyntaxtree


    Name:    predicate_components_in_scope/3

    Module:    bsyntaxtree


    Name:    conjunction_to_list/2

    Module:    bsyntaxtree


    Name:    conjunct_predicates/2

    Module:    bsyntaxtree


    Name:    disjunction_to_list/2

    Module:    bsyntaxtree


    Name:    syntaxtraversion/6

    Module:    bsyntaxtree


    Name:    add_error_fail/3

    Module:    error_manager


    Name:    add_message/2

    Module:    error_manager


    Name:    add_message/3

    Module:    error_manager


    Name:    add_message/4

    Module:    error_manager


    Name:    add_error/3

    Module:    error_manager


    Name:    add_internal_error/2

    Module:    error_manager


    Name:    add_warning/3

    Module:    error_manager


    Name:    start_ms_timer/1

    Module:    tools


    Name:    stop_ms_timer_with_debug_msg/2

    Module:    tools


    Name:    split_atom/3

    Module:    tools


    Name:    atom_prefix/2

    Module:    tools_strings


    Name:    translate_bexpression/2

    Module:    translate


    Name:    get_preference/2

    Module:    preferences


    Name:    b_test_boolean_expression_cs/5

    Module:    b_interpreter


    Name:    safe_time_out/3

    Module:    tools_meta


    Name:    b_global_deferred_set/1

    Module:    b_global_sets


    Name:    unfixed_deferred_set/1

    Module:    b_global_sets


    Name:    b_get_global_enumerated_sets/1

    Module:    b_global_sets


    Name:    is_b_global_constant/3

    Module:    b_global_sets


    Name:    get_user_defined_scope/4

    Module:    b_global_sets


    Name:    list_contains_unfixed_deferred_set_id/1

    Module:    b_global_sets


    Name:    expand_custom_set_to_list_now/2

    Module:    custom_explicit_sets


    Name:    register_event_listener/3

    Module:    eventhandling


    Name:    is_external_function_name/1

    Module:    external_functions


    Name:    module_info/2

    Module:    module_information


    Name:     list_to_avl/2

    Module:     avl


    Name:     avl_fetch/3

    Module:     avl


    Name:    smt_solve_predicate/4


    Name:    smt_solve_predicate/5


    Name:    smt_solve_predicate_free/3


    Name:    smt_add_predicate/5


    Name:    smt_solve_predicate_in_state/5


    Name:    reset_smt_supported_interpreter/0


    Name:    smt_add_cnf/3


    Name:    smt_add_extra_clause_cnf/2


    Name:    smt_solve_cnf/2


    Name:    smt_reset_cnf/1



    Predicates

    Predicates:

  • add_clause/4
  • add_literal/3
  • add_state_to_bindings/3
  • add_translation_for_solver/9
  • backjump_on_symbol/1
  • binary_operator/1
  • bind_in_prob_state/2
  • check_sat/7
  • check_sat_aux/7
  • cleanup_core_for_backjumping/2
  • clear_state/0
  • combine_satisfiable_component_results/3
  • constraint_uses_unfixed_deferred_set/2
  • contains_introduced_identifiers/2
  • contains_solver_name_with_prefix/2
  • contains_unsupported_aux/4
  • contains_unsupported_type_or_expression/3
  • contains_unsupported_type_or_expression/4
  • convert_to_cnf_model/3
  • create_bounded_smt_identifier/5
  • create_bounded_smt_state/5
  • create_enum_element_smt_state/3
  • create_exprs_for_rec_value_fields/7
  • create_let_state/7
  • create_smt_identifier/5
  • create_smt_state/5
  • create_term_size_pairs/2
  • create_virtual_enum_elms/3
  • create_virtual_enum_elms/4
  • filter_unsupported_types_or_expressions/5
  • gen_leading_zeros/4
  • get_couple_types_comp_args/2
  • get_couple_types_comp_args/4
  • get_full_pred/9
  • get_model_or_return_result/8
  • get_smt_time_out/2
  • init_smt_supported_interpreter/0
  • is_bool/2
  • is_external_function_identifier/1
  • is_ground_real/1
  • known_solver_exception/2
  • lookup/4
  • lookup_literal/3
  • mk_deferred_set_identifiers/4
  • mk_deferred_set_identifiers2/3
  • mk_expr/6
  • mk_expr_aux/7
  • mk_expr_maplist/6
  • mk_expr_skip/6
  • mk_sort/3
  • mk_value/7
  • mk_value_aux/7
  • mk_value_maplist/7
  • number_to_atom/2
  • pairwise_disjoint/5
  • pairwise_disjoint/6
  • pairwise_disjoint_mk_expr/6
  • pairwise_union/4
  • prepare_enumerated_sets_with_elms/2
  • prepare_unfixed_deferred_sets_with_virtual_elms/3
  • prob_pred_literal/1
  • remove_solvers_with_prefix/3
  • remove_useless_bindings/3
  • reset_smt_supported_interpreter/0
  • sat_skeleton_is_contradictory/2
  • setup_deferred_sets/4
  • setup_enumerated_set/4
  • setup_sets/3
  • smt_add_cnf/2
  • smt_add_cnf/3
  • smt_add_extra_clause_cnf/2
  • smt_add_predicate/5
  • smt_add_predicate_aux/3
  • smt_add_predicate_to_solver/5
  • smt_reset_cnf/1
  • smt_solve_cnf/2
  • smt_solve_pre_cleaned_predicate/6
  • smt_solve_predicate/4
  • smt_solve_predicate/5
  • smt_solve_predicate6/6
  • smt_solve_predicate_aux/6
  • smt_solve_predicate_free/3
  • smt_solve_predicate_in_state/5
  • solve_components_with_z3/7
  • sort_components_descending_term_size/2
  • store_core_for_backjumping/1
  • translate_binding/2
  • translate_literal/4
  • translate_smt_model_to_b_values_with_timeout/5
  • translate_solver_name/3
  • treat_exception/3
  • unary_operator/1
  • unsupported_expr/4
  • unsupported_type/3
  • unsupported_value_type/1
  • validate_selected_solvers/2
  • validate_selected_z3_solvers/1


  • add_clause/4

    add_clause/4



    add_literal/3

    add_literal/3



    add_state_to_bindings/3

    add_state_to_bindings/3



    add_translation_for_solver/9

    add_translation_for_solver/9



    backjump_on_symbol/1

    backjump_on_symbol/1



    binary_operator/1

    binary_operator/1



    bind_in_prob_state/2

    bind_in_prob_state/2



    check_sat/7

    check_sat/7

    Description:
    check_sat(+SelectedSolvers, +Solver, +UsesDefSet, +Translations, -Result, -SolvedTranslation).



    check_sat_aux/7

    check_sat_aux/7



    cleanup_core_for_backjumping/2

    cleanup_core_for_backjumping/2



    clear_state/0

    clear_state/0



    combine_satisfiable_component_results/3

    combine_satisfiable_component_results/3



    constraint_uses_unfixed_deferred_set/2

    constraint_uses_unfixed_deferred_set/2



    contains_introduced_identifiers/2

    contains_introduced_identifiers/2



    contains_solver_name_with_prefix/2

    contains_solver_name_with_prefix/2



    contains_unsupported_aux/4

    contains_unsupported_aux/4



    contains_unsupported_type_or_expression/3

    contains_unsupported_type_or_expression/3



    contains_unsupported_type_or_expression/4

    contains_unsupported_type_or_expression/4



    convert_to_cnf_model/3

    convert_to_cnf_model/3



    create_bounded_smt_identifier/5

    create_bounded_smt_identifier/5



    create_bounded_smt_state/5

    create_bounded_smt_state/5



    create_enum_element_smt_state/3

    create_enum_element_smt_state/3



    create_exprs_for_rec_value_fields/7

    create_exprs_for_rec_value_fields/7

    Description:
    create_exprs_for_rec_value_fields(+FieldTypes, +Fields, +TranslationType, +Solver, +LS, +GS, -FieldExprs).



    create_let_state/7

    create_let_state/7



    create_smt_identifier/5

    create_smt_identifier/5



    create_smt_state/5

    create_smt_state/5



    create_term_size_pairs/2

    create_term_size_pairs/2



    create_virtual_enum_elms/3

    create_virtual_enum_elms/3

    Description:
    create_virtual_enum_elms(+DefaultSetSize, +DefSet, -DefElms).



    create_virtual_enum_elms/4

    create_virtual_enum_elms/4



    filter_unsupported_types_or_expressions/5

    filter_unsupported_types_or_expressions/5



    gen_leading_zeros/4

    gen_leading_zeros/4



    get_couple_types_comp_args/2

    get_couple_types_comp_args/2



    get_couple_types_comp_args/4

    get_couple_types_comp_args/4



    get_full_pred/9

    get_full_pred/9

    Description:
    get_full_pred(+TranslationType, +Solver, +Pred, +ProBState, -FullPred, -FullProBState, -Filtered, -SkippedVars, -UnsupportedLPs).



    get_model_or_return_result/8

    get_model_or_return_result/8



    get_smt_time_out/2

    get_smt_time_out/2



    init_smt_supported_interpreter/0

    init_smt_supported_interpreter/0



    is_bool/2

    is_bool/2



    is_external_function_identifier/1

    is_external_function_identifier/1



    is_ground_real/1

    is_ground_real/1



    known_solver_exception/2

    known_solver_exception/2



    lookup/4

    lookup/4



    lookup_literal/3

    lookup_literal/3



    mk_deferred_set_identifiers/4

    mk_deferred_set_identifiers/4



    mk_deferred_set_identifiers2/3

    mk_deferred_set_identifiers2/3



    mk_expr/6

    mk_expr/6



    mk_expr_aux/7

    mk_expr_aux/7



    mk_expr_maplist/6

    mk_expr_maplist/6



    mk_expr_skip/6

    mk_expr_skip/6



    mk_sort/3

    mk_sort/3



    mk_value/7

    mk_value/7



    mk_value_aux/7

    mk_value_aux/7



    mk_value_maplist/7

    mk_value_maplist/7



    number_to_atom/2

    number_to_atom/2



    pairwise_disjoint/5

    pairwise_disjoint/5



    pairwise_disjoint/6

    pairwise_disjoint/6



    pairwise_disjoint_mk_expr/6

    pairwise_disjoint_mk_expr/6



    pairwise_union/4

    pairwise_union/4



    prepare_enumerated_sets_with_elms/2

    prepare_enumerated_sets_with_elms/2



    prepare_unfixed_deferred_sets_with_virtual_elms/3

    prepare_unfixed_deferred_sets_with_virtual_elms/3



    prob_pred_literal/1

    prob_pred_literal/1



    remove_solvers_with_prefix/3

    remove_solvers_with_prefix/3

    Description:
    remove_solvers_with_prefix(+Prefix, +SelectedSolvers, -NewSelectedSolvers).



    remove_useless_bindings/3

    remove_useless_bindings/3



    reset_smt_supported_interpreter/0

    reset_smt_supported_interpreter/0



    sat_skeleton_is_contradictory/2

    sat_skeleton_is_contradictory/2

    Description:
    sat_skeleton_is_contradictory(+Pred, +Solver).



    setup_deferred_sets/4

    setup_deferred_sets/4



    setup_enumerated_set/4

    setup_enumerated_set/4



    setup_sets/3

    setup_sets/3



    smt_add_cnf/2

    smt_add_cnf/2



    smt_add_cnf/3

    smt_add_cnf/3



    smt_add_extra_clause_cnf/2

    smt_add_extra_clause_cnf/2



    smt_add_predicate/5

    smt_add_predicate/5

    Block: smt_add_predicate(-,?,?,?,?)



    smt_add_predicate_aux/3

    smt_add_predicate_aux/3



    smt_add_predicate_to_solver/5

    smt_add_predicate_to_solver/5



    smt_reset_cnf/1

    smt_reset_cnf/1



    smt_solve_cnf/2

    smt_solve_cnf/2



    smt_solve_pre_cleaned_predicate/6

    smt_solve_pre_cleaned_predicate/6

    Description:
    smt_solve_pre_cleaned_predicate(+SelectedSolvers, +Solver, +CPred, +ProBState, -Result).



    smt_solve_predicate/4

    smt_solve_predicate/4

    Description:
    smt_solve_predicate(+SolverName, +Pred, +State, -Result).



    smt_solve_predicate/5

    smt_solve_predicate/5

    Description:
    smt_solve_predicate(+Solver, +OptionList, +Pred, +State, -Result).



    smt_solve_predicate6/6

    smt_solve_predicate6/6

    Description:
    smt_solve_predicate6(+SelectedSolvers, +Solver, +Options, +Pred, +State, -Result).



    smt_solve_predicate_aux/6

    smt_solve_predicate_aux/6

    Description:
    smt_solve_predicate_aux(+SelectedSolvers, +Solver, +OptionsList, +CPred, +ProBState, -Result).



    smt_solve_predicate_free/3

    smt_solve_predicate_free/3



    smt_solve_predicate_in_state/5

    smt_solve_predicate_in_state/5



    solve_components_with_z3/7

    solve_components_with_z3/7

    Description:
    solve_components_with_z3(+Components, +AvailableSolvers, +Options, +State, +ResultAcc, +UnknownOccurred, -Result).



    sort_components_descending_term_size/2

    sort_components_descending_term_size/2



    store_core_for_backjumping/1

    store_core_for_backjumping/1



    translate_binding/2

    translate_binding/2



    translate_literal/4

    translate_literal/4



    translate_smt_model_to_b_values_with_timeout/5

    translate_smt_model_to_b_values_with_timeout/5



    translate_solver_name/3

    translate_solver_name/3



    treat_exception/3

    treat_exception/3



    unary_operator/1

    unary_operator/1



    unsupported_expr/4

    unsupported_expr/4

    Description:
    change in Z3: lambda inside recursive functions was declared unsupported until proper support is provided (see https://github.com/Z3Prover/z3/issues/5813)
    see mk_op_iteration_func_decl in /extensions/z3interface/src/cpp/main.cpp



    unsupported_type/3

    unsupported_type/3



    unsupported_value_type/1

    unsupported_value_type/1



    validate_selected_solvers/2

    validate_selected_solvers/2



    validate_selected_z3_solvers/1

    validate_selected_z3_solvers/1



    Determinacy Checker

    Determinacy Checker:

    ! Existence error in argument 1 of absolute_file_name/3
    ! file probsrc(tools_timeout) does not exist
    ! goal: absolute_file_name(probsrc(tools_timeout),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/smt_solvers_interface/smt_solvers_interface.pl')])