summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-11Merge branch '1.3.x'Morgan Deters
2014-03-11Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.Morgan Deters
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu...Andrew Reynolds
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2014-03-07Fix bug 554 (nominally).Morgan Deters
2014-03-07Fix strings-exp setting.Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback