summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2014-04-14Add initial support for co-datatypes.Andrew Reynolds
2014-04-10Fix the build; --check-proof works for UF but not for the new UFC logic.Morgan Deters
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-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-09fix get-info error-behaviorKshitij Bansal
2014-04-04For security, add --no-filesystem-access option, which disables SMT-LIB scrip...Morgan Deters
2014-04-03Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann...Morgan Deters
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
2014-03-20cleanupKshitij Bansal
2014-03-19Refactor the theory specific parts of definition expansion into the theory so...Martin Brain
2014-03-19Set dumping options from (set-option..) and API more directly.Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback