| Age | Commit message (Collapse) | Author |
|---|
|
|
|
* 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.
|
|
Older versions of GMP in combination with newer versions of GCC and
C++11 cause errors [0]. This commit adds the necessary includes of
<cstddef>.
[0] https://gcc.gnu.org/gcc-4.9/porting_to.html
|
|
This was introduced by changing the implementation of "isNumber" in this commit:
a94318b
This fixes issue #1105.
|
|
- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output
|
|
Commit 62b673a6b8444c14c169a984dd6e3fc8f685851e remove most of the
record/tuple infrastructure but did not remove the classes RecordSelect and
TupleSelect which lead to issues with Java bindings (the references to the
corresponding mkConst implementations could not be resolved). This commit
removes the remaining traces of those classes.
|
|
Cleaning up the CVC4::String class.
|
|
|
|
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
|
|
|
|
|
|
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
|
|
|
|
|
|
|
When CVC4 gets interrupted, we use async-signal safe printing functions
to print statistics. Unfortunately, the code for that was invoking copy
constructors, which is problematic due to memory allocation; for example
with statistics such as ReferenceStat<std::string>. This commit adds a
getDataRef() method for statistics that returns a const reference to the
object being printed such that the copy constructor is not called. Note:
modifying getData() was unfortunately not an option because in the case
of TimerStat, we can't return a reference to an object on the stack. We
could remove the const modifier on getData() and use d_data to store the
information but then we would have to remove it on
safeFlushInformation() and potentially other methods as well, which
seems like a worse solution.
|
|
|
|
|
|
This commit fixes two issues reported by Coverity:
- Fixes the check whether the buffer is full in safe_print_hex
- Removes dead code in safe_print for floating-point values
Additionally, it fixes an issue reported by Andy where the names of the
statistics were printed as "<unsupported>" due to calling the const char*
version instead of the std::string version of safe_print.
Finally, this fixes an issue where --segv-spin would not print the program name
because it was a const char*. The program name is now stored as a string.
NOTE: As a side effect, the last part also fixes Coverity issue 1362944, which
has been in CVC4 for a long time.
|
|
As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).
Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics
|
|
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
|
