summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2013-01-23Adding miplibtrick option.Tim King
2013-01-23Adding substitution size cap.Tim King
2013-01-23fix to workaround ANTLR 3.2 issue with initializationMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23add user patterns to the Smt1 parser; update NEWS fileMorgan Deters
2013-01-22Merge branch '1.0.x'Morgan Deters
2013-01-22fix for theory preprocessing cache on clang, perhaps others.Morgan Deters
2013-01-22Merge branch '1.0.x'Morgan Deters
2013-01-22update ANTLR URLs (antlr.org -> antlr3.org)Morgan Deters
2013-01-19Merge branch '1.0.x'Morgan Deters
2013-01-19Fix an options-processing bug on some platforms (e.g., MacOS).Morgan Deters
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ↵Morgan Deters
bracketing
2012-12-21Merge branch '1.0.x'Dejan Jovanović
2012-12-21adding copy constructor for the datatype enumeratorDejan Jovanović
fixes bug 484
2012-12-18Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-15Fix printing of EXISTS in CVC language printerMorgan Deters
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-11Merge branch '1.0.x', getting fix for bug 480Morgan Deters
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-11Merge branch '1.0.x' (getting fix for bug 479)Morgan Deters
2012-12-11Ignore unknown term annotations (giving a warning). Resolves bug 479.Morgan Deters
2012-12-11adding cache for preprocessing datatypes terms to fix bug 475, fix for ↵Andrew Reynolds
handling user attributes in quantifiers (was broken) (cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)
2012-12-11adding cache for preprocessing datatypes terms to fix bug 475, fix for ↵Andrew Reynolds
handling user attributes in quantifiers (was broken)
2012-12-07Fix to portfolio buildsMorgan Deters
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)
2012-12-07Fix performance issue in a DFS search (bug 474)Kshitij Bansal
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)
2012-12-06Fix to portfolio buildsMorgan Deters
2012-12-06Fix performance issue in a DFS search (bug 474)Kshitij Bansal
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-06Fix for fuzzer-found model bugClark Barrett
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
2012-12-06* tuple and record support in compatibility libraryMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
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-05Cleanup of arithmetic, and some new utility functions for the coming ↵Tim King
fcsimplex code.
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵Tim King
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
2012-12-04* Add support for --decision=justification + incremental (bug 437)Kshitij Bansal
- Fix a destruction order issue this triggered in DE (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-03Fix for fuzzer-found model bugClark Barrett
2012-12-01fix to TNode assertion (which is too strict, given lax ordering requirements ↵Morgan Deters
on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others
2012-12-01Throw a logic exception if user makes an assertion using a STORE_ALLClark Barrett
2012-12-01remove instantiator frameworkMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01fix memory corruption issue in debug builds that led to unhelpful outputMorgan Deters
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵Morgan Deters
failing regression for bug 472
2012-12-01drastic simplification of quantifiers code regarding equality queries, ↵Andrew Reynolds
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
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-12-01Some fixes for boolean arraysMorgan Deters
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01fix #line annotation warningMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback