summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Collapse)Author
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-13Remove now-unused language bindings interface file.Morgan Deters
2013-07-13Fix language bindings and portfolio builds.Morgan Deters
2013-07-12Fix for curious GCC 4.8 translation with -O.Morgan Deters
2013-07-11Support 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-06Model output is now const; this related to bug 519Morgan Deters
2013-06-27Remove 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-27Remove 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-24Add files missing from last commitMorgan Deters
2013-06-24Support 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-24Add 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-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵Morgan Deters
to improper ITE removal in quantifier instantiations.
2013-04-26FCSimplex branch mergeTim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging 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-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-03-27some Java bindings fixes (fixes Debian build problems)Morgan Deters
2013-03-27Merge branch 'master' into bv-corelianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-25java input stream adapters workingMorgan Deters
2013-03-23Merge remote-tracking branch 'dddejan/c++11'Dejan Jovanović
Conflicts: src/smt/boolean_terms.cpp
2013-03-23changing string hash function to use the gnu namespaceDejan Jovanović
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-22compiles withDejan Jovanović
export CXXFLAGS='-std=gnu++0x' before configure fails all regressions in the parser
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-20Better reporting of detached git state in --version and --show-configMorgan Deters
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-19Remove PropositionalQuery class and all CUDD-related build stuff (and ↵Morgan Deters
references)
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-03-13post failed attempts at getting the incremental solver to worklianah
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for ↵Andrew Reynolds
boolean terms, improvement for pre skolemization
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-16Fix version identification for new git repository.Morgan Deters
2013-02-05dos2unix conversion for a number of files; this avoids spurious conflicts ↵Morgan Deters
when merging to master
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
2013-02-04Model 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-01merged master into branchlianah
2013-01-31Fix a small problem in clang builds due to namespaces and symbol lookupMorgan Deters
2013-01-28compiling implementation of new slicer finished; need to add debugging ↵lianah
information and debug.
2013-01-28Fixes 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-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2013-01-10fixed most bugs and added paranoid assertionslianah
2012-12-14Merging in patch from branch '1.0.x'.Tim King
2012-12-14Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.xTim King
2012-12-14Changing the rewriter to use Boute's Euclidean definition of division.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback