Age | Commit message (Expand) | Author |
2017-10-12 | Initial support for solving bit-vector inequalities (#1229) | Andrew Reynolds |
2017-10-12 | Sygus logics (#1226) | Andrew Reynolds |
2017-10-11 | Enable regressions for CBQI BV and fix inverse for LSHR. (#1234) | Aina Niemetz |
2017-10-11 | Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224) | Mathias Preiner |
2017-10-11 | Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ... | Andrew Reynolds |
2017-10-09 | CBQI BV: Add inverse for more operators. (#1213) | Aina Niemetz |
2017-10-03 | Add regression from #50 regarding "as" parsing in smt2 (#1188) | Andrew Reynolds |
2017-10-03 | Op overload parser (#1162) | Andrew Reynolds |
2017-10-01 | Refactor check function in last call effort of non-linear extension. (#1175) | Andrew Reynolds |
2017-09-30 | SyGuS streaming solution mode (#1131) | Andrew Reynolds |
2017-09-29 | Simplify representation of inversion Skolems for bv cegqi (#1164) | Andrew Reynolds |
2017-09-29 | Initial working version of BV word-level instantiation (#1158) | Andrew Reynolds |
2017-09-28 | Improve finite model finding for recursive predicates (#1150) | Andrew Reynolds |
2017-09-25 | Fix bug related to sort inference + subtypes. (#1125) | Andrew Reynolds |
2017-09-21 | Sygus inv templ refactor (#1110) | Andrew Reynolds |
2017-09-19 | Fix issue #1074, improve non-fatal error handling (#1075) | Andres Noetzli |
2017-09-18 | Fix issue #1105 involving string to int (#1112) | Andrew Reynolds |
2017-09-14 | Remove unhandled subtypes (#1098) | Andrew Reynolds |
2017-09-13 | Add isConst check for lambda expressions. (#1084) | Andrew Reynolds |
2017-09-10 | Ensure that expand definitions is called on all non-variable expressi… (#1070) | Andrew Reynolds |
2017-09-05 | Remove support for conversions between uint32/uint16 and string. (#1069) | Andrew Reynolds |
2017-08-31 | Answer unknown when uf-ss=no-minimal is combined with cardinality constraints... | Andrew Reynolds |
2017-08-30 | Fix model construction for parametric types (#1059) | Andrew Reynolds |
2017-08-14 | Build and test suite fixes for Windows (#186) | Mark Laws |
2017-08-08 | Use cache for datatypes cycle check, add regression. | ajreynol |
2017-08-04 | Set default language to smt lib 2.6 (including as a base language for sygus),... | ajreynol |
2017-07-29 | Add support for charat in native language, minor cleanup. | ajreynol |
2017-07-20 | Fix a few bugs related to sygus. | ajreynol |
2017-07-12 | Make type rules more strict for operators whose type rules involve subtypes. ... | ajreynol |
2017-07-10 | Add nl regression. | ajreynol |
2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring of... | ajreynol |
2017-07-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ... | ajreynol |
2017-07-05 | Fix for logic info, update regressions. Update casc tfa script. | ajreynol |
2017-07-05 | Non-linear supported in ALL logics. Minor fixes for set logic with sygus. | ajreynol |
2017-06-30 | Minor change to trigger selection, fixes related to subtypes (in macros, cbqi... | ajreynol |
2017-06-28 | Enable non-linear solve by default, update regressions. | ajreynol |
2017-06-22 | Fix assertion failure due to missing clause id (#180) | Andres Nötzli |
2017-06-21 | Properly handle subtypes in smt2 printer. | ajreynol |
2017-06-16 | Merge pull request #170 from CVC4/fix_2_6_parser3 | Clark Barrett |
2017-06-16 | Fix segfault by making unit conflict CDMaybe | Andres Nötzli |
2017-06-16 | Parse 'is', 'match' differently for non-DT input | Andres Noetzli |
2017-06-15 | Fix for bug 639. | Clark Barrett |
2017-06-15 | Add regression. | ajreynol |
2017-06-02 | Fix regression. | ajreynol |
2017-06-02 | Incorporate datatypes into smt comp script, add regression. | ajreynol |
2017-05-31 | Fix model construction for BV with cbqi. Minor change to defaults. | ajreynol |
2017-05-31 | Minor change to defaults, update smt comp script, minor changes to options in... | ajreynol |
2017-05-26 | Checking that equalities belong to the arithmetic theory in the solve() routine. | Tim King |
2017-05-15 | Cleanup handling of division (possible fix for bugs 803, 804, 805). | ajreynol |
2017-05-15 | Fix minor bug in sets rewriter | Andres Noetzli |