summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2018-05-27Fix cegqi assertions for quantified non-linear cases. (#1999)Andrew Reynolds
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1979)Andrew Reynolds
2018-05-24Improve simple constant symmetry breaking for sygus (#1977)Andrew Reynolds
2018-05-24Fix compiler warnings (#1959)Andres Noetzli
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Towards better symbolic enumeration in SyGuS (#1971)Haniel Barbosa
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Infrastructure for strings strategies (#1883)Andrew Reynolds
2018-05-21Infrastructure to mark unused sygus strategies (#1950)Andrew Reynolds
2018-05-21Refactor sygus eval unfold (#1946)Andrew Reynolds
2018-05-21Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)Haniel Barbosa
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-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-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-14Flag to check invariance of entire values in sygus explain (#1908)Andrew Reynolds
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-09Better option names for PBE (#1891)Andrew Reynolds
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-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-04Cegis unif register evaluation points (#1878)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback