cvc3 2.2-13.1 source package in Ubuntu
Changelog
cvc3 (2.2-13.1) unstable; urgency=low * NMU. Change dependencies libgmp3-dev --> libgmp-dev. -- Ubuntu Archive Auto-Sync <email address hidden> Sat, 30 Apr 2011 12:42:01 +0000
Upload details
- Uploaded by:
- Ubuntu Archive Auto-Sync
- Uploaded to:
- Oneiric
- Original maintainer:
- Chris Conway
- Architectures:
- any
- Section:
- math
- Urgency:
- Low Urgency
See full publishing history Publishing
| Series | Published | Component | Section | |
|---|---|---|---|---|
| Precise | release | universe | math |
Downloads
| File | Size | SHA-256 Checksum |
|---|---|---|
| cvc3_2.2.orig.tar.gz | 1.0 MiB | 5182c8bd7b90f4ee8b35d4f731c8fa42e4bc8d00471a99a8c9aec7bc4b1381b7 |
| cvc3_2.2-13.1.diff.gz | 64.6 KiB | 3e69ca88a5e78a8d46731c47652bb1d5298656bc6c61ded3aa959bcf6e5ac504 |
| cvc3_2.2-13.1.dsc | 1.1 KiB | 3aed973011596264a6bdc92c629d3380c3641ae524c6fa613eb2b37f2b1b4bac |
Available diffs
- diff from 2.2-13 to 2.2-13.1 (8.8 KiB)
Binary packages built by this source
- cvc3: No summary available for cvc3 in ubuntu quantal.
No description available for cvc3 in ubuntu quantal.
- cvc3-el: No summary available for cvc3-el in ubuntu oneiric.
No description available for cvc3-el in ubuntu oneiric.
- libcvc3-2: No summary available for libcvc3-2 in ubuntu oneiric.
No description available for libcvc3-2 in ubuntu oneiric.
- libcvc3-2-dev: No summary available for libcvc3-2-dev in ubuntu quantal.
No description available for libcvc3-2-dev in ubuntu quantal.
- libcvc3-2-java: Java bindings for CVC3 (bytecode library)
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 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package provides architecture-independent files of the Java
bindings for CVC3
- libcvc3-2-jni: No summary available for libcvc3-2-jni in ubuntu quantal.
No description available for libcvc3-2-jni in ubuntu quantal.
