summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Collapse)Author
2013-03-13post failed attempts at getting the incremental solver to worklianah
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-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
2012-12-12Merge pull request #2 from CVC4/1.0.xDejan Jovanović
1.0.x
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
* added printing for total bit-vector division kinds for debugging purposes
2012-12-10ported my bv-core branch from svn to gitLiana Hadarean
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches. (cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches.
2012-12-05Improved garbage collection for TheoryArith. The merges all of the code ↵Tim King
over from branches/arithmetic/converge except for the new code for simplex.
2012-12-01Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and ↵Tim King
Integer((long int)((1<<29)+1)) gave different values. This was confirmed on vm-int1.cims.nyu.edu. See http://www.ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.
2012-11-30Changes to SExpr to accept autoconversion from bool and const char*. Adding ↵Tim King
an example for combination.
2012-11-29fixes bug 438, incorporate subtypes into type unification when typechecking ↵Andrew Reynolds
parameterized datatypes
2012-11-27First chunk of boolean-terms support.Morgan Deters
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-26Improved implementation of Integer::length() with CLN enabled. Additional ↵Tim King
tests to sanity check both versions CLN and GMP versions of length.
2012-11-17* enable previously-failing (now succeeding) datatype example that uses recordsMorgan Deters
* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-17fix for language bindings (fixes debian build fail last night)Morgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ↵Morgan Deters
ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-15Fix for bug 447.Tim King
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, ↵Andrew Reynolds
refactoring code out of instantiators in preparation for quantifiers equality engine
2012-11-12changed BitVector::unsignedRem to match the behavior of the bit-blasted ↵Liana Hadarean
circuit for division by 0; temporary fix for bug440
2012-11-12* Fix language bindings: various issuesMorgan Deters
** remove a number of warnings in bindings generation ** give appropriate names for operator-overloading ** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code * Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to ↵Andrew Reynolds
be used yet), added new totality lemma option for uf strong solver
2012-11-10Beautifying integer_cln_imp.hTim King
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I ↵Morgan Deters
discovered (still outstanding). :-( * Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-22fix installation of certain header filesMorgan Deters
2012-10-11minor changes in wording for "cvc4 --version", and point to the COPYING file ↵Morgan Deters
for full info
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-11Fix wording on GPL in legal notices; also remove an unnecessary source ↵Morgan Deters
dependence. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-10Abstract values for SMT-LIB.Morgan Deters
Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. ↵Andrew Reynolds
cleaned up model code, TheoryModel::getValue is now const.
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
* fix minor issue with s-expr parsing in CVC and SMT grammars * other minor things (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09some documentation fixesMorgan Deters
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
(rather than SAT context) * Enable part of CVC3 system test (resolves bug 375) * Fix infinite recursion in beta reduction code (resolves bug 417) * Some model-building assertions have been added * Other minor changes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* Include a few bug testcases for resolved bugs.Morgan Deters
* Fix error message if you POP beyond the bottom user stack frame. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback