summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
2012-10-14fix #line number warnings (sorry!)Morgan Deters
2012-10-12Added assertions and tracing code for collectModelInfo phaseClark Barrett
2012-10-12Latest changes to model codeClark Barrett
2012-10-11Fix bug 421, again, and add a second, independent test case for the sameMorgan Deters
2012-10-11minor changes in wording for "cvc4 --version", and point to the COPYING file ...Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-11Fix wording on GPL in legal notices; also remove an unnecessary source depend...Morgan Deters
2012-10-11compliance noteMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-10-10cleanup up some static data members in the quantifiers codeAndrew Reynolds
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-09typoKshitij Bansal
2012-10-09bugfix: isQuantified, bugfix: flushKshitij Bansal
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. c...Andrew Reynolds
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
2012-10-09fixed bv rewriter to evaluate bvurem over constantsLiana Hadarean
2012-10-09More fixes to model codeClark Barrett
2012-10-09made datatypes rewrite incorrect selectors to ground term. this feature can ...Andrew Reynolds
2012-10-09usability: remove --no-interactive from --smtlib optionMorgan Deters
2012-10-09fix for bug 415Dejan Jovanović
2012-10-09* Add assertion in TheoryModel code to ensure we don't get inconsistentMorgan Deters
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4...Morgan Deters
2012-10-09some documentation fixesMorgan Deters
2012-10-09adding mergePredicates method to the equality engine to be able toDejan Jovanović
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-08added reduced bv model failing test caseLiana Hadarean
2012-10-08Fixed problem in assertEqualityEngine: predicates that are not false are noClark Barrett
2012-10-08small fix for compat JNI library installationMorgan Deters
2012-10-08fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't a...Morgan Deters
2012-10-06turn off cudd by default in configure scriptMorgan Deters
2012-10-06* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASSMorgan Deters
2012-10-06* Clean up some options documentationMorgan Deters
2012-10-06* Some documentation about building compatibility and language bindingsMorgan Deters
2012-10-06* Include a few bug testcases for resolved bugs.Morgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
2012-10-05fix \fileMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04disable model-generation by default in cvc3 compatibility layer. should fix ...Morgan Deters
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-04IllegalArgumentException in java needs to be named "CVC4IllegalArgumentExcept...Morgan Deters
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
2012-10-03implemented collectModelInfo for TheoryBVLiana Hadarean
2012-10-03updates to contrib scripts to match docsMorgan Deters
2012-10-03better documentation, allow examples to be installed, etcMorgan Deters
2012-10-03New model code, mostly workinClark Barrett
2012-10-03new README and INSTALL filesMorgan Deters
2012-10-03added support for interrupting TheoryBVLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback