| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
|
|
|
|
|
|
`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring
|
|
This commit adds a floating-point sampler inspired by PyMPF [0]. It also
creates a new Sampler class that can be used for creating random values
of different sorts (currently BV and FP values).
[0] https://github.com/florianschanda/PyMPF
|
|
|
|
|
|
|
|
As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions
in floatingpoint.h, which was problematic when installing the header
files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and
simply including the header files in another project would be missing
that definition. This commit moves floatingpoint.h to a template file
floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at
configure-time when generating floatingpoint.h (this is the same
solution that integer.h and rational.h use). I have tested the fix with
the examples provided in #2013 and they work.
|
|
* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.
* Enable the bit-vector theory when setting the logic, not in expandDefinition.
This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.
* Use symfpu to implement the literal floating-point objects.
* Add kinds for bit-blasted components.
* Print the new kinds.
* Typing rules for the new kinds.
* Constant folding for the component kinds.
* Add support for components to the theory solver.
* Add explicit equivalences between classification functions and equalities.
* Use symfpu to do symbolic conversions of floating-point operations.
* Implement conversions via (over-)approximation and refinement.
* Correct a copy and paste error in the generation of uninterpretted functions for conversions.
|
|
|
|
|
|
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
|
|
|
|
This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
|
|
|
|
|
|
assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)
|
|
|
|
|
|
throwing exceptions. This is called from destructors and therefore it is inappropraiate to throw exceptions. This solution is temporary until Assert() is deprecated in favor of an aborting version. (#1539)
|
|
|
|
Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.
|
|
|
|
|
|
Removing more miscellaneous throw specifiers.
|
|
* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.
|
|
The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0.
|
|
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
|
|
|
|
This adds functions on Integers to compute modular addition, multiplication and inverse.
This is required for the Gaussian Elimination preprocessing pass for BV.
|
|
* Initialize TimerStat::d_start.
* 0 initializing d_data.
|
|
Returns a copy of d_value to enable public access of GMP and CLN data.
|
|
* Work on rewriter for string contains.
* Add rewrites that mix str.to.int and str.contains. Documentation, add regression.
* Minor
* Minor
* Address review, add a few TODOs. Improve some non-digit -> not is number.
* Fix
* Simplify.
* Clang format, minor fixing of comments.
|
|
CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.
|
|
* Argument for strings class to specify whether to process escape sequences.
* Change default value on string constructor.
* Make CVC4::String::toString symmetric to the constructor for CVC4::String, document.
* Clang format.
|
|
CVC4 was computing hashes for pairs of objects by simply XORing the
hashes of the two objects. This commit implements a better way of
combining hashes based on the FNV-1a hash algorithm. The algorithm is
public domain.
|
