Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |||
2015-10-13 | remove options infrastructure code which depended on undefined behavior | Kshitij Bansal | |
appears to be source of crashes on mac | |||
2015-10-12 | Merge pull request #76 from CVC4/proofs | Kshitij Bansal | |
Proofs | |||
2015-10-11 | fix regression tests, support fallback mode for proofs | Kshitij Bansal | |
2015-10-11 | Default builds are now proof enabled. | Liana Hadarean | |
2015-10-11 | Fix strings preprocessing + incremental, fixes bug 682. Add initial ↵ | ajreynol | |
infrastructure for str.contains inferences. | |||
2015-10-09 | Temporary reverting commit 477e72b (proofs as default build) until we fix ↵ | Liana Hadarean | |
nightly builds. | |||
2015-10-08 | Minor improvements to strings. Refactor rewriter. Enable fairness for ↵ | ajreynol | |
multiple sorts in UF finite model finding by default. | |||
2015-10-07 | Default builds are now proof enabled. | Liana Hadarean | |
2015-10-07 | Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648) | Liana Hadarean | |
2015-10-07 | Minor improvements, add endpoint eq inference to strings. | ajreynol | |
2015-10-06 | More improvements to strings rewriter for regexps, contains, indexof, ↵ | ajreynol | |
replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len. | |||
2015-10-02 | Fixes related to explanations for cycles, sym inferences. Minor fixes and ↵ | ajreynol | |
improvements. | |||
2015-10-02 | Improvements to rewriter for regexp, contains, indexof. Improvements and ↵ | ajreynol | |
fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions. | |||
2015-10-01 | Evaluate extended operators on partially concrete arguments. More aggressive ↵ | ajreynol | |
rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms. |