summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-10-26better parametric datatype arity checking; fixes bug 433Morgan Deters
2012-10-26Fixed a failing datatype regression with check-modelsClark Barrett
2012-10-26fixed bug in datatypes decision procedure enforcing rewriting of incorrectly ...Andrew Reynolds
2012-10-26More bug fixes and more checks for modelsClark Barrett
2012-10-25more minor fixes to build systemACSYS
2012-10-24fixed assertion failures in efficient e-matchingAndrew Reynolds
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
2012-10-24Updated the ArithStaticLearner to be user context dependent.Tim King
2012-10-24Fix for systems that do not have the MAP_FILE macro defined.Tim King
2012-10-24fix for bug 429 Dejan Jovanović
2012-10-24efficient e-matching now specific to rewrite rulesAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
2012-10-23fixed problem with datatypes giving incorrect explanations, now corrected and...Andrew Reynolds
2012-10-23More debugging info, small changes to model builderClark Barrett
2012-10-23Added reads that were missing in collectModelInfoClark Barrett
2012-10-23fixed TheoryBV collectModel info to check for shared terms; this seems to fix...Liana Hadarean
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-22fix parser generation in distributed tarballs (should fix bug #427)Morgan Deters
2012-10-22one more incorrect #line fixedMorgan Deters
2012-10-22fix installation of certain header filesMorgan Deters
2012-10-19Fix for model building with shared terms for arithmetic.Tim King
2012-10-19Fix problem with incremental with portfolio. Fixes bug 420.Kshitij Bansal
2012-10-19BV theory model fixLiana Hadarean
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
2012-10-17first working version of new inst-gen-style quantifier instantiation techniqu...Andrew Reynolds
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-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ć
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback