| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-23 | Adding a missing delete to smt2_compliance. | Tim King | |
| 2015-11-23 | Adding a missing delete to InstStrategyCegqi destructor. | Tim King | |
| 2015-11-23 | Isolating the dependencies on CVC4_ANTLR3_OLD_INPUT_STREAM. Also freeing ↵ | Tim King | |
| more memory for antlr input. | |||
| 2015-11-23 | Switching travis over to using the containers infrastructure. | Tim King | |
| 2015-11-23 | Freeing memory allocated for signal handling. | Tim King | |
| 2015-11-18 | Option for midpoints in cbqi. | ajreynol | |
| 2015-11-17 | Improve relevant domain computation for arithmetic, full saturation ↵ | ajreynol | |
| strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings. | |||
| 2015-11-12 | Updating the contrib/new-theory script and travis to use the new ↵ | Tim King | |
| Makefile.theories script. | |||
| 2015-11-12 | Updating the contrib/new-theory script and travis to use the new ↵ | Tim King | |
| Makefile.theories script. | |||
| 2015-11-12 | Minor fixes and improvements to purify quant, relational triggers. | ajreynol | |
| 2015-11-11 | Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation. | ajreynol | |
| 2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to ↵ | ajreynol | |
| cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions. | |||
| 2015-11-09 | Replacing an inefficient use of std::find(...) to use std::set's find() instead. | Tim King | |
| 2015-11-06 | Changing file permissions to add or remove executable tag as appropriate. | Tim King | |
| 2015-11-05 | Merging the google branch back into master. | Tim King | |
| 2015-11-05 | Fixes some initialization and desctruction problems in quantifiers. Also ↵ | Tim King | |
| restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts. | |||
| 2015-11-05 | This commit slightly generalizes the scripts for generating the _tags files. | Tim King | |
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol | |
| 2015-11-03 | Fixing typo. | Tim King | |
| 2015-11-03 | Adding a test to ensure the <build>/src/theory directory is available to the ↵ | Tim King | |
| scripts in src/Makefile.am. This should fix a bug in building the debian packages. | |||
| 2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol | |
| 2015-10-29 | Removes an extra dollar sign from src/options/mktagheaders. The extra dollar ↵ | Tim King | |
| sign came in as a copy paste from a Makefile. This was not proper bash. | |||
| 2015-10-27 | Adding the new mkdirs script to EXTRA_DIST. This should fix the failing ↵ | Tim King | |
| nightly distcheck. | |||
| 2015-10-26 | This commit fixes a bug related to a public header depending on a compiler ↵ | Tim King | |
| flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information. | |||
| 2015-10-26 | This commit removes using absolute paths in the generation of the .subdirs ↵ | Tim King | |
| file. This also rearranges generation of the file so that one .subdirs file is generated once per Makefile.am file. This keeps using relative paths clean. | |||
| 2015-10-26 | This commit moves the scripts for building the Debug_tags, Traces_tags, ↵ | Tim King | |
| Debug_tags.h and Trace_tags.h out of options/Makefile.am and into seperate scripts. This also enables these files always being created. | |||
| 2015-10-26 | This fixes a one definition rule violation for reduceDB_lt in Solver.cc in ↵ | Tim King | |
| minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *. | |||
| 2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol | |
| 2015-10-26 | Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ | ajreynol | |
| mixed Int/Real. Bug fixes. Updates to quantifiers rewriter. | |||
| 2015-10-24 | Revert "Default builds are now proof enabled." | Kshitij Bansal | |
| This reverts commit 4fd18dee3156a6dd1903b95662034d6e996ff88b. | |||
| 2015-10-24 | Fixes related to string contains. | ajreynol | |
| 2015-10-23 | This removes a bug for reading data that has been popped from the back of a ↵ | Tim King | |
| vector using a stale reference in the unconstrained simplifier. | |||
| 2015-10-23 | Specify that the default initialization must always be done for ↵ | Tim King | |
| CDOhash_map's data field. Without doing this, there exists a loop where uninitialized data can be read. This can happen if T is a type like bool. The trace goes: CDOhash_map::set(data) calls ContextObj::make_current(). Now (d_pScope->isCurrent()) is false. So ContextObj::make_current() calls ContextObj::update(). ContextObj::update() calls CDOhash_map::save(). CDOhash_map::save() calls return new(pCMM) CDOhash_map(*this) which calls the copy constructor which reads the data using d_data(other.d_data). | |||
| 2015-10-23 | Switching Options::current() to return a pointer. This helps avoid undefined ↵ | Tim King | |
| behavior due to dereferencing a null pointer in the future. | |||
| 2015-10-23 | Changes configure.ac so that the single recurisve invocation runs with a ↵ | Tim King | |
| relative path. This lets the @srcdir@ variable in configuration be a relative path. | |||
| 2015-10-23 | This patch slightly generalizes how the std::isfinite function in <cmath> is ↵ | Tim King | |
| referred. | |||
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for ↵ | ajreynol | |
| quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions. | |||
| 2015-10-21 | Minor refactoring in strings related to length. | ajreynol | |
| 2015-10-20 | Refactor strings, remove old cycle checks in normalize eqc. | ajreynol | |
| 2015-10-20 | Clean up explanations involving string length. Add regression. | ajreynol | |
| 2015-10-19 | Improve stratification of strings extended function reductions, add ↵ | ajreynol | |
| regressions. Eliminate preprocess for regexp. | |||
| 2015-10-19 | Improve regexp rewriter, simplify regexp preprocess, add basic trans closure ↵ | ajreynol | |
| for string contains, refactoring. | |||
| 2015-10-18 | Fix for no condense func values. | ajreynol | |
| 2015-10-16 | Add option to interleave enumerative instantiation with other strategies. | ajreynol | |
| 2015-10-16 | Throw error for recursively defined types involving Boolean. | ajreynol | |
| 2015-10-16 | Fix for codatatype constant rewrite, add regression. | ajreynol | |
| 2015-10-15 | Fix congruence check in strings, fixes bug 686. | ajreynol | |
| 2015-10-15 | Change semantics of str.substr to allow endpoint out of bounds, and return ↵ | ajreynol | |
| empty string for error conditions. Improve rewriter for str.substr. | |||
| 2015-10-15 | Decompose string contains, minor refactoring. | ajreynol | |
| 2015-10-13 | Merge pull request #77 from kbansal/macsegfault | Kshitij Bansal | |
| remove options infrastructure code which depended on undefined behavior | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback