summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback