Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2018-05-08 | Support for str.<= and str.< (#1882) | Andrew Reynolds | |
2018-05-08 | Fix order of preprocessing pass registration. (#1887) | Aina Niemetz | |
2018-05-08 | Classifying data in SygusUnifRL (#1886) | Haniel Barbosa | |
2018-05-08 | Infrastructure for CEGQI handled status (#1873) | Andrew Reynolds | |
2018-05-08 | only lazy trie changes (#1885) | Haniel Barbosa | |
2018-05-07 | Add support for str.code (#1821) | Andrew Reynolds | |
2018-05-05 | Fix handling of TO_REAL in cvc printer (#1876) | Andrew Reynolds | |
2018-05-04 | Remove special case for record selector printing. (#1875) | Andrew Reynolds | |
2018-05-04 | Cegis unif register evaluation points (#1878) | Andrew Reynolds | |
2018-05-04 | Make --output-lang consistent with --lang (#1877) | Andres Noetzli | |
2018-05-04 | Do not print tuples. (#1874) | Andrew Reynolds | |
2018-05-03 | Refactor bv-intro-pow2 preprocessing pass. (#1851) | Mathias Preiner | |
2018-05-03 | Fix printing of multiple datatypes (#1872) | Andres Noetzli | |
2018-05-03 | Move Lazy trie datastructure to its own file (#1871) | Haniel Barbosa | |
Preparation for further developing CegisUnif | |||
2018-05-03 | Initialize cegis unif strategy (#1861) | Andrew Reynolds | |
2018-05-03 | Document datatypes sygus (#1818) | Andrew Reynolds | |
2018-05-03 | Sets subtypes (#1095) | Andrew Reynolds | |
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression. | |||
2018-05-03 | Fix redundant internalPush calls. (#1865) | Mathias Preiner | |
The SMT2 parser by default passes a true expression to the CheckSatCommand, which results in checkSatisfiability (in SmtEngine) to always do an internal push. As a consequence, the work of each check-sat was reset even though no user level push/pop happened. | |||
2018-05-03 | Fix warnings in proof code (#1850) | Andres Noetzli | |
2018-05-03 | Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834) | Andrew Reynolds | |
2018-05-03 | Option to interleave tangent plane inferences (#1833) | Andrew Reynolds | |