Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-05-10 | Merge branch 'master' into mult_argsmult_args | Aina Niemetz | |
2018-05-10 | Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903) | Haniel Barbosa | |
2018-05-10 | Support multiple sets of command line args in regs | 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 | 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 | |
2018-05-03 | Link cegis unif with the enumeration manager (#1859) | Andrew Reynolds | |
2018-05-03 | Make CegisUnif default to Cegis when no unif used (#1836) | Haniel Barbosa | |
2018-05-02 | Fix cvc printer for nullary constructors (#1856) | Andrew Reynolds | |
2018-05-02 | Remove (dummy) SMT1 printer (#1854) | Andres Noetzli | |
2018-05-02 | Support HORN logic string (#1849) | Andrew Reynolds | |
2018-05-02 | Initial support for string standard in smt lib 2.6 (#1848) | Andrew Reynolds | |
2018-05-01 | Cegis unif enumerator manager (#1837) | Andrew Reynolds | |
2018-05-01 | Improve tangent planes for transcendental functions (#1832) | Andrew Reynolds | |
2018-04-30 | Refactor real2int (#1813) | Haniel Barbosa | |
This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. | |||
2018-04-30 | Remove dead code in bv-to-bool preprocessing pass (#1828) | Andres Noetzli | |
Fixes Coverity issue 1468436. As Coverity correctly detects, kind::BITVECTOR_XOR is dealt with in an if-statement before the switch statement on kind. This is because kind::XOR is binary while kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly indicates). | |||
2018-04-30 | Remove subsort symmetry breaking (#1807) | Andrew Reynolds | |
2018-04-30 | Fix 1156 (#1830) | Andrew Reynolds | |
2018-04-30 | Disable unsat-cores/proofs for slow regression (#1835) | Andres Noetzli | |