summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-05-18Cache isInterpretedFinite (#1943)Andrew Reynolds
2018-05-18Cegis unif defaults to cegis when no unif (#1942)Andrew Reynolds
2018-05-18Unified fairness scheme for cegis unif (#1941)Andrew Reynolds
2018-05-17Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937)Andrew Reynolds
2018-05-17Fix debugPrint and add regress. (#1934)Andrew Reynolds
2018-05-17Option to force return values of Bool functions to be constant in CegisUnif ↵Haniel Barbosa
(#1930)
2018-05-17Cegis-specific infrastructure (#1933)Andrew Reynolds
2018-05-17Internal propagation for refinement lemmas (#1932)Andrew Reynolds
2018-05-16Improve the separation resolution scheme in cegis unif (#1931)Andrew Reynolds
2018-05-15Refactor static learning preprocessing pass (#1857)yoni206
2018-05-15Refactoring get enumerator values in construct candidate for cegis unif (#1926)Andrew Reynolds
2018-05-15Building and refining solutions with dynamic condition generation in ↵Haniel Barbosa
CegisUnif (#1920)
2018-05-15Fix free variables in cbqi preregister inst. (#1921)Andrew Reynolds
2018-05-14Minor improvements to --nl-ext-purify (#1896)Andrew Reynolds
2018-05-14 Incorporating dynamic condition enumeration into cegis unif (#1916)Andrew Reynolds
2018-05-15Floating 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-14Fix purification in SygusUnifRL (#1912)Haniel Barbosa
2018-05-14Add regressions, change defaults. (#1911)Andrew Reynolds
2018-05-14Flag to check invariance of entire values in sygus explain (#1908)Andrew Reynolds
2018-05-14Small change for more sensible line breaking in the output of get-model. (#1910)Florian Schanda
2018-05-11Fix 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-10Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)Haniel Barbosa
2018-05-10Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)Andrew Reynolds
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-10Static learn redundant operators in CegisUnif (#1899)Haniel Barbosa
2018-05-10Add ITE to default Boolean sygus grammar (#1898)Andrew Reynolds
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2018-05-10Fix priority of decisions for cegis unif (#1897)Andrew Reynolds
2018-05-09Piecing solutions together in CegisUnif (#1894)Haniel Barbosa
2018-05-09Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)yoni206
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-05-09Make symmetry-breaker-exp into a preprocessing pass (#1890)Andrew Reynolds
2018-05-09Add the symmetry breaker module (#1847)PaulMeng
2018-05-08Refactor bv-abstraction preprocessing pass. (#1860)Mathias Preiner
2018-05-08Infrastructure for approximations in model output (#1884)Andrew Reynolds
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-08Fix order of preprocessing pass registration. (#1887)Aina Niemetz
2018-05-08Classifying data in SygusUnifRL (#1886)Haniel Barbosa
2018-05-08Infrastructure for CEGQI handled status (#1873)Andrew Reynolds
2018-05-08only lazy trie changes (#1885)Haniel Barbosa
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-05Fix handling of TO_REAL in cvc printer (#1876)Andrew Reynolds
2018-05-04Remove special case for record selector printing. (#1875)Andrew Reynolds
2018-05-04Cegis unif register evaluation points (#1878)Andrew Reynolds
2018-05-04Make --output-lang consistent with --lang (#1877)Andres Noetzli
2018-05-04Do not print tuples. (#1874)Andrew Reynolds
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-05-03Fix printing of multiple datatypes (#1872)Andres Noetzli
2018-05-03Move Lazy trie datastructure to its own file (#1871)Haniel Barbosa
Preparation for further developing CegisUnif
2018-05-03Initialize cegis unif strategy (#1861)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback