summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
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-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-04Cegis unif register evaluation points (#1878)Andrew Reynolds
2018-05-03Move Lazy trie datastructure to its own file (#1871)Haniel Barbosa
2018-05-03Initialize cegis unif strategy (#1861)Andrew Reynolds
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)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
2018-05-01Cegis unif enumerator manager (#1837)Andrew Reynolds
2018-04-30Remove subsort symmetry breaking (#1807)Andrew Reynolds
2018-04-30Fix 1156 (#1830)Andrew Reynolds
2018-04-29Allow multiple functions in sygus unif approaches (#1831)Andrew Reynolds
2018-04-28Initial implementation of SygusUnifRL (#1829)Haniel Barbosa
2018-04-27Make construct solution behavior specific to SygusIO (#1827)Andrew Reynolds
2018-04-27New module for synthesizing functions in a data-driven SyGuS approach (#1819)Haniel Barbosa
2018-04-27Core improvements to extended rewriter (#1820)Andrew Reynolds
2018-04-26Fix subgoal generation context (#1816)Andrew Reynolds
2018-04-25Equality resolution in the extended rewriter (#1811)Andrew Reynolds
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-25Move candidate rewrite code to own file (#1804)Andrew Reynolds
2018-04-25Fix issue with multi-triggers that include variable triggers (#1810)Andrew Reynolds
2018-04-21Improve sygus sampling for strings (#1802)Andrew Reynolds
2018-04-20 Reenable filtering based on ordering in sygus sampler (#1784)Andrew Reynolds
2018-04-20Symmetry detection module (#1749)PaulMeng
2018-04-16Skolemize candidate rewrite rule checks (#1777)Andrew Reynolds
2018-04-15Fix mk type const (#1776)Andrew Reynolds
2018-04-14Another fix for sygus rr stats. (#1768)Andrew Reynolds
2018-04-13allowing --bool-to-bv without quantifiers (#1771)yoni206
2018-04-12Fix alpha equivalence for higher-order (#1769)Andrew Reynolds
2018-04-12Fixes for free variables in assertions (#1762)Andrew Reynolds
2018-04-10 Improve accuracy of stats for sygus sampler (#1755)Andrew Reynolds
2018-04-09Fix hasSubterm calls for higher-order (#1760)Andrew Reynolds
2018-04-09Fix higher-order term indexing. (#1754)Andrew Reynolds
2018-04-09Fix sygus substr static symmetry breaking (#1761)Andrew Reynolds
2018-04-08Allow predetermined first-order variables when constructing deep embedding. (...Andrew Reynolds
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-04-08Add quantifier name attribute. (#1756)Andrew Reynolds
2018-04-04Proper initialization and destruction of sygus unif (#1750)Andrew Reynolds
2018-04-04Fix for corner case of higher-order matching (#1708)Andrew Reynolds
2018-04-04Fix sygus infer (#1747)Andrew Reynolds
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
2018-04-03Make sygus unif I/O an subclass of sygus unif (#1741)Andrew Reynolds
2018-04-03Internal sygus type checking (#1734)Andrew Reynolds
2018-04-02Improvements to extended rewriter for Booleans and ITE (#1705)Andrew Reynolds
2018-04-02Make sygus unif utility use sygus unif strategies (#1732)Andrew Reynolds
2018-03-30Split strategy representation from SygusUnif (#1730)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback