lib64cvc3_5-devel-2.4.1-1-omv2013.0.x86_64.rpm


Advertisement

Description

lib64cvc3_5-devel - Library and includes to use automatic SMT theorem proving

Distribution: OpenMandriva Cooker
Repository: OpenMandriva Contrib x86_64
Package name: lib64cvc3_5-devel
Package version: 2.4.1
Package release: 1-omv2013.0
Package architecture: x86_64
Package type: rpm
Installed size: 753.89 KB
Download size: 145.33 KB
Official Mirror: abf-downloads.openmandriva.org
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. CVC3 contains built-in support for theories for rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols. CVC3 also supports quantifiers. This is a development package for CVC3 shared library.

Alternatives

Provides

  • devel(libcvc3(64bit))
  • lib64cvc3-devel == 2.4.1-1
  • lib64cvc3_5-devel == 2.4.1-1:2013.0

    Download

    Install Howto

    1. Enable OpenMandriva Contrib repository on Install and Remove Software"
    2. Update packages list:
      # urpmi.update -a
    3. Install lib64cvc3_5-devel rpm package:
      # urpmi lib64cvc3_5-devel

    Files

    • /usr/include/cvc3/assumptions.h
    • /usr/include/cvc3/c_interface.h
    • /usr/include/cvc3/c_interface_defs.h
    • /usr/include/cvc3/cdflags.h
    • /usr/include/cvc3/cdlist.h
    • /usr/include/cvc3/cdmap.h
    • /usr/include/cvc3/cdmap_ordered.h
    • /usr/include/cvc3/cdo.h
    • /usr/include/cvc3/circuit.h
    • /usr/include/cvc3/clause.h
    • /usr/include/cvc3/cnf.h
    • /usr/include/cvc3/cnf_manager.h
    • /usr/include/cvc3/command_line_exception.h
    • /usr/include/cvc3/command_line_flags.h
    • /usr/include/cvc3/common_proof_rules.h
    • /usr/include/cvc3/compat_hash_map.h
    • /usr/include/cvc3/compat_hash_set.h
    • /usr/include/cvc3/context.h
    • /usr/include/cvc3/cvc_util.h
    • /usr/include/cvc3/debug.h
    • /usr/include/cvc3/dpllt.h
    • /usr/include/cvc3/dpllt_basic.h
    • /usr/include/cvc3/dpllt_minisat.h
    • /usr/include/cvc3/eval_exception.h
    • /usr/include/cvc3/exception.h
    • /usr/include/cvc3/expr.h
    • /usr/include/cvc3/expr_hash.h
    • /usr/include/cvc3/expr_manager.h
    • /usr/include/cvc3/expr_map.h
    • /usr/include/cvc3/expr_op.h
    • /usr/include/cvc3/expr_stream.h
    • /usr/include/cvc3/expr_transform.h
    • /usr/include/cvc3/expr_value.h
    • /usr/include/cvc3/fdstream.h
    • /usr/include/cvc3/formula_value.h
    • /usr/include/cvc3/hash_fun.h
    • /usr/include/cvc3/hash_map.h
    • /usr/include/cvc3/hash_set.h
    • /usr/include/cvc3/hash_table.h
    • /usr/include/cvc3/kinds.h
    • /usr/include/cvc3/lang.h
    • /usr/include/cvc3/memory_manager.h
    • /usr/include/cvc3/memory_manager_chunks.h
    • /usr/include/cvc3/memory_manager_context.h
    • /usr/include/cvc3/memory_manager_malloc.h
    • /usr/include/cvc3/notifylist.h
    • /usr/include/cvc3/os.h
    • /usr/include/cvc3/parser.h
    • /usr/include/cvc3/parser_exception.h
    • /usr/include/cvc3/pretty_printer.h
    • /usr/include/cvc3/proof.h
    • /usr/include/cvc3/queryresult.h
    • /usr/include/cvc3/rational.h
    • /usr/include/cvc3/sat_api.h
    • /usr/include/cvc3/search.h
    • /usr/include/cvc3/search_fast.h
    • /usr/include/cvc3/search_impl_base.h
    • /usr/include/cvc3/search_sat.h
    • /usr/include/cvc3/search_simple.h
    • /usr/include/cvc3/smartcdo.h
    • /usr/include/cvc3/smtlib_exception.h
    • /usr/include/cvc3/sound_exception.h
    • /usr/include/cvc3/statistics.h
    • /usr/include/cvc3/theorem.h
    • /usr/include/cvc3/theorem_manager.h
    • /usr/include/cvc3/theorem_producer.h
    • /usr/include/cvc3/theory.h
    • /usr/include/cvc3/theory_arith.h
    • /usr/include/cvc3/theory_arith3.h
    • /usr/include/cvc3/theory_arith_new.h
    • /usr/include/cvc3/theory_arith_old.h
    • /usr/include/cvc3/theory_array.h
    • /usr/include/cvc3/theory_bitvector.h
    • /usr/include/cvc3/theory_core.h
    • /usr/include/cvc3/theory_datatype.h
    • /usr/include/cvc3/theory_datatype_lazy.h
    • /usr/include/cvc3/theory_quant.h
    • /usr/include/cvc3/theory_records.h
    • /usr/include/cvc3/theory_simulate.h
    • /usr/include/cvc3/theory_uf.h
    • /usr/include/cvc3/translator.h
    • /usr/include/cvc3/type.h
    • /usr/include/cvc3/typecheck_exception.h
    • /usr/include/cvc3/variable.h
    • /usr/include/cvc3/vc.h
    • /usr/include/cvc3/vc_cmd.h
    • /usr/include/cvc3/vcl.h
    • /usr/lib64/libcvc3.so
    Advertisement
    Advertisement