summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-10Merge branch 'master' into mult_argsmult_argsAina Niemetz
2018-05-10Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)Haniel Barbosa
2018-05-10Support multiple sets of command line args in regsAndres 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-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
2018-05-02Fix cvc printer for nullary constructors (#1856)Andrew Reynolds
2018-05-02Remove (dummy) SMT1 printer (#1854)Andres Noetzli
2018-05-02Support HORN logic string (#1849)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-05-01Cegis unif enumerator manager (#1837)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-30Refactor 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-30Remove 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-30Remove subsort symmetry breaking (#1807)Andrew Reynolds
2018-04-30Fix 1156 (#1830)Andrew Reynolds
2018-04-30Disable unsat-cores/proofs for slow regression (#1835)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback