summaryrefslogtreecommitdiff
path: root/src/smt/boolean_terms.cpp
AgeCommit message (Expand)Author
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-15More simplification to internal implementation of tuples and records.ajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2015-12-15Breaking the include cycle between Record and Expr.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-10-16Throw error for recursively defined types involving Boolean.ajreynol
2015-01-22Do not drop patterns during boolean term rewriting. Narrow sygus search space...ajreynol
2014-12-03Floating point infrastructure.Martin Brain
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Corrected fix for missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-10-07Refactor quantifiers attributes.ajreynol
2014-07-12Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre f...Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-04-14Add initial support for co-datatypes.Andrew Reynolds
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-10Boolean terms conversion fix for datatypes, fixes a problem Andy discovered o...Morgan Deters
2014-04-03Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann...Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now wor...Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-08-08Parameterized, uninterpreted sorts need no Boolean-term conversionMorgan Deters
2013-07-11Fix for Boolean-term rewriting and LAMBDAsMorgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-07One more case for arrays of Boolean.Morgan Deters
2013-06-07Fix for bug 517.Morgan Deters
2013-05-17Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-29make Boolean term conversion partially non-recursive (resolves bug 501)Morgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-15Boolean terms rewriting for quantified variables of type Bool, when quantifie...Morgan Deters
2013-02-26Fix for quantifiers containing Boolean terms.Morgan Deters
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add faili...Morgan Deters
2012-12-01Some fixes for boolean arraysMorgan Deters
2012-11-29fix for andy: boolean terms stuff really shouldn't look at datatypes at all i...Morgan Deters
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback