Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters | |
2013-07-13 | Remove now-unused language bindings interface file. | Morgan Deters | |
2013-07-13 | Fix language bindings and portfolio builds. | Morgan Deters | |
2013-07-12 | Fix for curious GCC 4.8 translation with -O. | Morgan Deters | |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters | |
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases. | |||
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters | |
2013-06-27 | Remove output.h from public space, to avoid clashes with symbols defined in ↵ | Morgan Deters | |
users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. | |||
2013-06-27 | Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they ↵ | Morgan Deters | |
don't escape to user space Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. | |||
2013-06-24 | Add files missing from last commit | Morgan Deters | |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵ | Morgan Deters | |
allows linearization of div,mod,/ by a constant. | |||
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option ↵ | Andrew Reynolds | |
for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine | |||
2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵ | Morgan Deters | |
to improper ITE removal in quantifier instantiations. | |||
2013-04-26 | FCSimplex branch merge | Tim King | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2013-04-01 | Merging some cleanup work: | Morgan Deters | |
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed | |||
2013-04-01 | Fix for iff terms over equalities between the same term and differing constants. | Tim King | |
2013-03-27 | some Java bindings fixes (fixes Debian build problems) | Morgan Deters | |
2013-03-27 | Merge branch 'master' into bv-core | lianah | |
2013-03-26 | added model generation for bv subtheories and bv-inequality solver option | lianah | |
2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters | |
2013-03-25 | java input stream adapters working | Morgan Deters | |
2013-03-23 | Merge remote-tracking branch 'dddejan/c++11' | Dejan Jovanović | |
Conflicts: src/smt/boolean_terms.cpp | |||
2013-03-23 | changing string hash function to use the gnu namespace | Dejan Jovanović | |
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem | |||
2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters | |
2013-03-22 | compiles with | Dejan Jovanović | |
export CXXFLAGS='-std=gnu++0x' before configure fails all regressions in the parser | |||
2013-03-21 | Merge branch 'master' into bv-core | lianah | |
2013-03-20 | Better reporting of detached git state in --version and --show-config | Morgan Deters | |
2013-03-19 | merged master with dejan's constant evaluating equality engine | Liana Hadarean | |
2013-03-19 | Remove PropositionalQuery class and all CUDD-related build stuff (and ↵ | Morgan Deters | |
references) | |||
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-03-13 | post failed attempts at getting the incremental solver to work | lianah | |
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for ↵ | Andrew Reynolds | |
boolean terms, improvement for pre skolemization | |||
2013-02-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-16 | Fix version identification for new git repository. | Morgan Deters | |
2013-02-05 | dos2unix conversion for a number of files; this avoids spurious conflicts ↵ | Morgan Deters | |
when merging to master | |||
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters | |
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed ↵ | Andrew Reynolds | |
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted. | |||
2013-02-01 | merged master into branch | lianah | |
2013-01-31 | Fix a small problem in clang builds due to namespaces and symbol lookup | Morgan Deters | |
2013-01-28 | compiling implementation of new slicer finished; need to add debugging ↵ | lianah | |
information and debug. | |||
2013-01-28 | Fixes for Win32 (closes bugs 488 and 489) | Morgan Deters | |
* timer statistics now supported (closes bug 488) * use of --mmap doesn't crash anymore (closes bug 489) | |||
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters | |
2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters | |
2013-01-10 | fixed most bugs and added paranoid assertions | lianah | |
2012-12-14 | Merging in patch from branch '1.0.x'. | Tim King | |
2012-12-14 | Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x | Tim King | |
2012-12-14 | Changing the rewriter to use Boute's Euclidean definition of division. | Tim King | |