| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-21 | Add SymFPU licensing information. (#1952) | Mathias Preiner | |
| 2018-05-21 | Improvements in parsing and printing related to mixed int/real (#1879) | Andrew Reynolds | |
| This eliminates some hacks for dealing with Int/Real. - Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA. - Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant. - Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852. - Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml). | |||
| 2018-05-21 | Infrastructure to mark unused sygus strategies (#1950) | Andrew Reynolds | |
| 2018-05-21 | Handle IMPLIES in bool-to-bv and test it in regress0 (#1929) | makaimann | |
| 2018-05-21 | Refactor sygus eval unfold (#1946) | Andrew Reynolds | |
| 2018-05-21 | Remove Eclipse project files (#1928) | Andres Noetzli | |
| No one of the core devs is currently using Eclipse, so the Eclipse project files are essentially useless since they are not guaranteed to be up-to-date. | |||
| 2018-05-21 | Fix compiler warning in hashsmt example (#1927) | Andres Noetzli | |
| Previously, we were using delete for an array allocated on the heap, which caused a warning. @dddejan fixed this and other issues in PR #1909 but after @ajreynol fixed the other issues in a separate PR and to not waste @dddejan's time, I am submitting this fix separately (note: the fix is slightly different in that it changes the array to a vector, making a delete[] unnecessary). | |||
| 2018-05-21 | Assign weight 1 for Boolean variables in SyGuS default grammars (#1948) | Haniel Barbosa | |
| 2018-05-21 | Fix file extension (#1919) | Caleb Donovick | |
| * Fix file extension * Update Makefile | |||
| 2018-05-18 | changing default (#1944) | Haniel Barbosa | |
| 2018-05-18 | Cache isInterpretedFinite (#1943) | Andrew Reynolds | |
| 2018-05-18 | Cegis unif defaults to cegis when no unif (#1942) | Andrew Reynolds | |
| 2018-05-18 | Unified fairness scheme for cegis unif (#1941) | Andrew Reynolds | |
| 2018-05-17 | Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937) | Andrew Reynolds | |
| 2018-05-17 | Fix debugPrint and add regress. (#1934) | Andrew Reynolds | |
| 2018-05-17 | Option to force return values of Bool functions to be constant in CegisUnif ↵ | Haniel Barbosa | |
| (#1930) | |||
| 2018-05-17 | Cegis-specific infrastructure (#1933) | Andrew Reynolds | |
| 2018-05-17 | Internal propagation for refinement lemmas (#1932) | Andrew Reynolds | |
| 2018-05-16 | Improve the separation resolution scheme in cegis unif (#1931) | Andrew Reynolds | |
| 2018-05-15 | Refactor static learning preprocessing pass (#1857) | yoni206 | |
| 2018-05-15 | Refactoring get enumerator values in construct candidate for cegis unif (#1926) | Andrew Reynolds | |
| 2018-05-15 | adding regressions (#1925) | Haniel Barbosa | |
| 2018-05-15 | Building and refining solutions with dynamic condition generation in ↵ | Haniel Barbosa | |
| CegisUnif (#1920) | |||
| 2018-05-15 | Fix free variables in cbqi preregister inst. (#1921) | Andrew Reynolds | |
| 2018-05-14 | Fix annotations in regress2. (#1917) | Andrew Reynolds | |
| 2018-05-14 | Minor improvements to --nl-ext-purify (#1896) | Andrew Reynolds | |
| 2018-05-14 | Incorporating dynamic condition enumeration into cegis unif (#1916) | Andrew Reynolds | |
| 2018-05-15 | Floating point theory solver based on SymFPU (#1895) | Martin | |
| * Add some symfpu accessor functions to reduce the size of the literal 'back-end'. * Enable the bit-vector theory when setting the logic, not in expandDefinition. This is needed because it is possible to add variables of float or rounding mode sort but not use any theory specific functions or predicates and thus not enable the bit-vector theory. * Use symfpu to implement the literal floating-point objects. * Add kinds for bit-blasted components. * Print the new kinds. * Typing rules for the new kinds. * Constant folding for the component kinds. * Add support for components to the theory solver. * Add explicit equivalences between classification functions and equalities. * Use symfpu to do symbolic conversions of floating-point operations. * Implement conversions via (over-)approximation and refinement. * Correct a copy and paste error in the generation of uninterpretted functions for conversions. | |||
| 2018-05-14 | Add contrib/get-symfpu for downloading symfpu. (#1905) | Mathias Preiner | |
| 2018-05-14 | Fix purification in SygusUnifRL (#1912) | Haniel Barbosa | |
| 2018-05-14 | Add regressions, change defaults. (#1911) | Andrew Reynolds | |
| 2018-05-14 | Flag to check invariance of entire values in sygus explain (#1908) | Andrew Reynolds | |
| 2018-05-14 | Small change for more sensible line breaking in the output of get-model. (#1910) | Florian Schanda | |
| 2018-05-11 | Remove obsolete unit test for ackermannization. (#1906) | Aina Niemetz | |
| With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete. | |||
| 2018-05-11 | Fix ackermannize preprocessing pass. (#1904) | Aina Niemetz | |
| Ackermannization did not consider cases where UF are Boolean. Model generation is still not supported, but now guarded against when bit-vectors are combined with arrays and/or uninterpreted functions and --bitblast=eager. | |||
| 2018-05-10 | Support multiple sets of command line args in regs (#1902) | Andres Noetzli | |
| This commit adds support for multiple sets of command line arguments for regressions. Each use of a `COMMAND-LINE` directive is interpreted as a separate set of command line arguments. | |||
| 2018-05-10 | Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903) | Haniel Barbosa | |
| 2018-05-10 | Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900) | Andrew Reynolds | |
| 2018-05-10 | Sygus repair constants (#1812) | Andrew Reynolds | |
| 2018-05-10 | Static learn redundant operators in CegisUnif (#1899) | Haniel Barbosa | |
| 2018-05-10 | Add ITE to default Boolean sygus grammar (#1898) | Andrew Reynolds | |
| 2018-05-10 | Refactored BVAckermann preprocessing pass. (#1889) | Aina Niemetz | |
| 2018-05-10 | Fix priority of decisions for cegis unif (#1897) | Andrew Reynolds | |
| 2018-05-09 | Piecing solutions together in CegisUnif (#1894) | Haniel Barbosa | |
| 2018-05-09 | Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893) | yoni206 | |
| 2018-05-09 | Better option names for PBE (#1891) | Andrew Reynolds | |
| 2018-05-09 | Make symmetry-breaker-exp into a preprocessing pass (#1890) | Andrew Reynolds | |
| 2018-05-09 | Add the symmetry breaker module (#1847) | PaulMeng | |
| 2018-05-08 | Refactor bv-abstraction preprocessing pass. (#1860) | Mathias Preiner | |
| 2018-05-08 | Infrastructure for approximations in model output (#1884) | Andrew Reynolds | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback