summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2014-06-25Turn strings-exp off by default (for the release)Morgan Deters
2014-06-23Fatal error if --unconstrained-simp and --produce-models used together (befor...Morgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19New translator features: expand define-funs and combine assertions.Morgan Deters
2014-06-19Fix for new CASC features, fixes Java builds.Morgan Deters
2014-06-19For casc : print models of functions rewritten by sort inference.ajreynol
2014-06-14Evil bitvector preprocessing pass for simplifying powers of two.lianah
2014-06-13Fix handling of ALIA.ajreynol
2014-06-11Some clean-up, post bv-merge.Morgan Deters
2014-06-10Merging Tim's pseudoboolean work from his fmcad14 branch.Tim King
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-06-09Disallow copy/assignment of SmtEngine.Morgan Deters
2014-06-06Sets translate, and other short fixesKshitij Bansal
2014-06-04SmtEngine::checkModel() now checks that model values are of the correct type ...Morgan Deters
2014-05-28Add option to avoid dumping partial models/proofs.Andrew Reynolds
2014-05-27Some fixes to GC order in Java.Morgan Deters
2014-05-26Separating an implicit inclusion of smt_engine.h from theory.h.Tim King
2014-05-15Minor fixes. Add SMTCOMP 2014 script.Andrew Reynolds
2014-05-14Finish --dump-instantiations option. Update scripts.Andrew Reynolds
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-05-10Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m...Andrew Reynolds
2014-05-09Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC...Andrew Reynolds
2014-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat...Andrew Reynolds
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback