summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-15Fix free variables in cbqi preregister inst. (#1921)Andrew Reynolds
2018-05-14Fix annotations in regress2. (#1917)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-14Add contrib/get-symfpu for downloading symfpu. (#1905)Mathias Preiner
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-11Remove obsolete unit test for ackermannization. (#1906)Aina Niemetz
With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.
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-10Support 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-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
2018-05-03Document datatypes sygus (#1818)Andrew Reynolds
2018-05-03Sets 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-03Fix 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-03Fix warnings in proof code (#1850)Andres Noetzli
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)Andrew Reynolds
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-03Link cegis unif with the enumeration manager (#1859)Andrew Reynolds
2018-05-03Make CegisUnif default to Cegis when no unif used (#1836)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback