Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-08-25 | Added missing includes (algorithm). | Aina Niemetz | |
Algorithm was previously removed from src/util/regexp.h which broke compilation on some platforms. | |||
2017-08-24 | Test Java API on CI | Pat Hawks | |
2017-08-24 | Add include to fix build | Andres Noetzli | |
2017-08-24 | Merge pull request #191 from timothy-king/cleanup-regexp | Andrew Reynolds | |
Cleaning up the CVC4::String class. | |||
2017-08-23 | Fix typos | Andres Noetzli | |
2017-08-23 | Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051) | Tim King | |
2017-08-21 | Cleanup: use Assert rather than C assert. (#1052) | Aina Niemetz | |
2017-08-21 | Updated NYU -> Stanford | Clark Barrett | |
2017-08-21 | Change Bugzilla urls to Github issues. | Mathias Preiner | |
2017-08-17 | Remove unused SubrangeBound(s) classes (#221) | Andres Noetzli | |
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. | |||
2017-08-17 | Add mbqi interleave option, change option fs-inst to fs-interleave. | ajreynol | |
2017-08-14 | Minimize includes in expr.h: remove dups, iostream (#219) | Andres Noetzli | |
2017-08-14 | Move function definitions from metakind.h to cpp (#218) | Andres Noetzli | |
2017-08-14 | Move function definitions from kind.h to kind.cpp (#217) | Andres Noetzli | |
2017-08-14 | Move function defns from smt_engine_scope.h to cpp (#216) | Andres Noetzli | |
Additionally, this commit removes unnecessary includes, adds includes to smt_engine.h in files that require it and removes s_smtEngine_current from smt_engine_scope.h. | |||
2017-08-14 | Use antlr-3.4 directory if already present in CVC4 root directory (#213) | Mathias Preiner | |
* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4. | |||
2017-08-14 | Merge pull request #214 from CVC4/fix_warn_nonlinear | Aina Niemetz | |
Fix compiler warnings in theory/arith/nonlinear_extension.cpp | |||
2017-08-14 | Build and test suite fixes for Windows (#186) | Mark Laws | |
- Build fixes for Windows - Make proof checking tempfile handling portable - Test suite fixes for Windows | |||
2017-08-11 | Fix compiler warnings in theory/arith/nonlinear_extension.cpp | Aina Niemetz | |
2017-08-11 | Maintain frontier for tangent planes. | ajreynol | |
2017-08-10 | Fix line numbers in options_template | Andres Noetzli | |
2017-08-09 | Fix compiler warning in src/context/context.h. | Mathias Preiner | |
2017-08-09 | Fix help message for disable-unit-testing in configure.ac (don't -> do not) | Aina Niemetz | |
Previous help message broke syntax highlighting in vim. | |||
2017-08-09 | Remove AigBitblaster implementation if ABC is not compiled (#212) | Mathias Preiner | |
* Guard use of AigBitblaster with CVC4_USE_ABC. This removes the Unreachable() implementation of AigBitblaster in case CVC4 is not compiled with ABC support. | |||
2017-08-09 | Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp | Aina Niemetz | |
2017-08-09 | Fix compiler warning in sat_proof_implementation | Andres Noetzli | |
2017-08-08 | Use cache for datatypes cycle check, add regression. | ajreynol | |
2017-08-08 | Merge pull request #211 from CVC4/fix_warn_sygus | Andrew Reynolds | |
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp | |||
2017-08-07 | Optionally split regression tests into test groups (#207) | Andres Noetzli | |
To prevent timing out on Travis, this commit adds the option to split the regression tests into groups and run each group in a separate job. The group of a test is determined by computing a checksum of its name. | |||
2017-08-07 | Fix compiler warning in theory/quantifiers/term_database_sygus.cpp | Aina Niemetz | |
2017-08-07 | Change sygus output for failed reconstruction case. | ajreynol | |
2017-08-07 | Make quantifier elimination more robust to preprocessing. | ajreynol | |
2017-08-04 | Reorganized bitvector.h | Aina Niemetz | |
2017-08-04 | Fix comments | Aina Niemetz | |
2017-08-04 | Fix typos in comments | Aina Niemetz | |
2017-08-04 | Set default language to smt lib 2.6 (including as a base language for ↵ | ajreynol | |
sygus), update regressions. | |||
2017-08-02 | Disable debug symbols for production builds. | Mathias Preiner | |
2017-07-31 | Minor improvement for enumerative instantiation. | ajreynol | |
2017-07-30 | Fix memory leak in symbol table (#209) | Andres Noetzli | |
Commit 4cab39bd4f166716cd3d357a175c346afb838137 moved d_exprMap, d_typeMap, and d_functions into SymbolTable::Implementation but did not move the deletion of those objects from SymbolTable to the SymbolTable::Implementation desconstructor, resulting in a memory leak. This commit fixes the issue. | |||
2017-07-29 | Change remaining hash_set -> unordered_set (#208) | Andres Noetzli | |
The nightly competition build has been failing due to a remaining use of hash_set in approx_simplex.cpp. This commit changes the remaining uses of hash_set to unordered_set. The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC required changing the configure.ac for LFSC to require C++11 support to make sure that it can be compiled independently from the rest of CVC4 (some of our Travis tests do that as well). To have the macros for these additional checks available, the commit adds a symlink to the files in config that contain the macros). I did not find a way to add macros from a parent's folder that did not break `make distcheck | |||
2017-07-29 | Add support for charat in native language, minor cleanup. | ajreynol | |
2017-07-28 | Fix cache issues for cyclic string equations. | ajreynol | |
2017-07-26 | -Og for non-opt build, parallel pcvc4 check (#206) | Andres Noetzli | |
-Og enables optimizations that do not interfere with debugging. This is the new default for debug builds if the compiler supports the flag. This commit also enables parallel checking for the portfolio build on Travis. | |||
2017-07-26 | Use TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in ↵ | Mathias Preiner | |
configure.ac. (#200) CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file. | |||
2017-07-23 | Disabling compiling unit tests with coverity scan for now. | Tim King | |
2017-07-22 | Deprecating the unused convenience_node_builders.h (#203) | Tim King | |
2017-07-22 | Consolidating the opaque pointers in SymbolTable. (#204) | Tim King | |
* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header. * Removing the guard for SymbolTable for the move constructor. | |||
2017-07-20 | Merge branch 'master' into cleanup-regexp | Tim King | |
2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
* 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. | |||
2017-07-20 | Fix a few bugs related to sygus. | ajreynol | |