summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2014-03-04Guard java-specific swig code with SWIGJAVA.Thomas Hunger
2014-02-28a new regular expression engine for solving both positive and negative member...Tianyi Liang
2014-02-21portfolio: fix export of emptysetKshitij Bansal
2014-02-20Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q...Andrew Reynolds
2014-02-18switch to total function str.to.int: maps invalid and non-digit strings to 0Tianyi Liang
2014-02-17bring back the commits which is lost accidentally.Tianyi Liang
2014-02-17add str2intTianyi Liang
2014-02-17Fix for strings-exp: enable quantifiersMorgan Deters
2014-02-17Fix strings preprocessing for justification heuristicMorgan Deters
2014-02-17type conversionTianyi Liang
2014-02-13fix expanding defTianyi Liang
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-22Some minor fixes to SmtEngine strings settings.Morgan Deters
2014-01-22add warning for using strings in ALL_SUPPORTEDTianyi Liang
2014-01-22Smarter options, but still have a bugTianyi Liang
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for in...Andrew Reynolds
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-10Whitespace.Morgan Deters
2013-12-10Remove "NodeValue width" outputMorgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now wor...Morgan Deters
2013-12-04Partial kind branch merge, including new --rewrite-apply-to-const feature.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-02Another fix to Java destruction order issues. Thanks to Zheng Manchun for th...Morgan Deters
2013-11-29Fix proofs build.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-27Incremental is now on by default when using from API, off for command-line dr...Morgan Deters
2013-11-26Fix Java destruction order issue; thanks to Zheng Manchun for reporting this ...Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-28Turn off model-based arrays (causing crashes in portfolio)Clark Barrett
2013-10-09fixed options::proof() segfaultlianah
2013-10-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-09More improvements to datatypes, eager selector collapsing, improved collect m...Andrew Reynolds
2013-10-08added currying for uf proofs; still needs debugginglianah
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric dataty...Andrew Reynolds
2013-10-03Added support for converting unsorted problems to multi-sorted problems via s...Andrew Reynolds
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-27Some fixes to recent strings commits.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback