summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-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-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-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-03New model code, mostly workinClark Barrett
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03--wait-to-join / --no-wait-to-join optionKshitij Bansal
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
2012-10-02workaround for a nasty CLN bugMorgan Deters
2012-10-01"Fix" (disable) portfolio when using quantifiersKshitij Bansal
2012-10-01make sure to mark LogicInfo as CVC4_PUBLICMorgan Deters
2012-10-01fix for dejan: term ITEs now dumped correctlyMorgan Deters
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-30minor changes to arithmetic assertions involving nonlinearity and models (rel...Morgan Deters
2012-09-30minor fixes to pickler (hopefully fixes Debian build from last night)Morgan Deters
2012-09-29Calling the setIncompleteness() flag on all full checks once a non-linear ter...Tim King
2012-09-29Fix a few segfaults in driver.Morgan Deters
2012-09-29draft RELEASE-NOTES file, and minor release stuffMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback