cvc5.git
2018-05-10 Andrew ReynoldsExclude Boolean connectives from ITE conditions in...
2018-05-10 Andrew ReynoldsSygus repair constants (#1812)
2018-05-10 Haniel BarbosaStatic learn redundant operators in CegisUnif (#1899)
2018-05-10 Andrew ReynoldsAdd ITE to default Boolean sygus grammar (#1898)
2018-05-10 Aina NiemetzRefactored BVAckermann preprocessing pass. (#1889)
2018-05-10 Andrew ReynoldsFix priority of decisions for cegis unif (#1897)
2018-05-09 Haniel BarbosaPiecing solutions together in CegisUnif (#1894)
2018-05-09 yoni206Reorder class members in bv-to-bool and bool-to-bv...
2018-05-09 Andrew ReynoldsBetter option names for PBE (#1891)
2018-05-09 Andrew ReynoldsMake symmetry-breaker-exp into a preprocessing pass...
2018-05-09 PaulMengAdd the symmetry breaker module (#1847)
2018-05-08 Mathias PreinerRefactor bv-abstraction preprocessing pass. (#1860)
2018-05-08 Andrew ReynoldsInfrastructure for approximations in model output ...
2018-05-08 Andrew ReynoldsSupport for str.<= and str.< (#1882)
2018-05-08 Aina NiemetzFix order of preprocessing pass registration. (#1887)
2018-05-08 Haniel BarbosaClassifying data in SygusUnifRL (#1886)
2018-05-08 Andrew ReynoldsInfrastructure for CEGQI handled status (#1873)
2018-05-08 Haniel Barbosaonly lazy trie changes (#1885)
2018-05-07 Andrew ReynoldsAdd support for str.code (#1821)
2018-05-05 Andrew ReynoldsFix handling of TO_REAL in cvc printer (#1876)
2018-05-05 Andrew ReynoldsRemove special case for record selector printing. ...
2018-05-04 Andrew ReynoldsCegis unif register evaluation points (#1878)
2018-05-04 Andres NoetzliMake --output-lang consistent with --lang (#1877)
2018-05-04 Andrew ReynoldsDo not print tuples. (#1874)
2018-05-04 Mathias PreinerRefactor bv-intro-pow2 preprocessing pass. (#1851)
2018-05-04 Andres NoetzliFix printing of multiple datatypes (#1872)
2018-05-04 Haniel BarbosaMove Lazy trie datastructure to its own file (#1871)
2018-05-04 Andrew ReynoldsInitialize cegis unif strategy (#1861)
2018-05-04 Andrew ReynoldsDocument datatypes sygus (#1818)
2018-05-04 Andrew ReynoldsSets subtypes (#1095)
2018-05-03 Mathias PreinerFix redundant internalPush calls. (#1865)
2018-05-03 Andres NoetzliFix warnings in proof code (#1850)
2018-05-03 Andrew ReynoldsInterleave quantifiers checks with ground theory checks...
2018-05-03 Andrew ReynoldsOption to interleave tangent plane inferences (#1833)
2018-05-03 Andrew ReynoldsLink cegis unif with the enumeration manager (#1859)
2018-05-03 Haniel BarbosaMake CegisUnif default to Cegis when no unif used ...
2018-05-03 Andrew ReynoldsFix cvc printer for nullary constructors (#1856)
2018-05-03 Andres NoetzliRemove (dummy) SMT1 printer (#1854)
2018-05-03 Andrew ReynoldsSupport HORN logic string (#1849)
2018-05-03 Andrew ReynoldsInitial support for string standard in smt lib 2.6...
2018-05-01 Andrew ReynoldsCegis unif enumerator manager (#1837)
2018-05-01 Andrew ReynoldsImprove tangent planes for transcendental functions...
2018-04-30 Haniel BarbosaRefactor real2int (#1813)
2018-04-30 Andres NoetzliRemove dead code in bv-to-bool preprocessing pass ...
2018-04-30 Andrew ReynoldsRemove subsort symmetry breaking (#1807)
2018-04-30 Andrew ReynoldsFix 1156 (#1830)
2018-04-30 Andres NoetzliDisable unsat-cores/proofs for slow regression (#1835)
2018-04-30 Andrew ReynoldsAllow multiple functions in sygus unif approaches ...
2018-04-30 Andrew ReynoldsMake factoring inference more aggressive (#1825)
2018-04-30 Andrew ReynoldsRefactor nonlinear check (#1814)
2018-04-30 Andrew ReynoldsImprovements to simple transcendental function check...
2018-04-28 Haniel BarbosaInitial implementation of SygusUnifRL (#1829)
2018-04-28 Andrew ReynoldsMake construct solution behavior specific to SygusIO...
2018-04-27 Andrew ReynoldsPrint function for equality status. (#1826)
2018-04-27 Andrew ReynoldsSimplify tangent plane direction (#1824)
2018-04-27 Haniel BarbosaNew module for synthesizing functions in a data-driven...
2018-04-27 Andrew ReynoldsCore improvements to extended rewriter (#1820)
2018-04-26 Andrew ReynoldsFix subgoal generation context (#1816)
2018-04-25 yoni206Refactor array-proofs and uf-proofs (#1655)
2018-04-25 Andrew ReynoldsEquality resolution in the extended rewriter (#1811)
2018-04-25 yoni206Refactor bv-to-bool and bool-to-bv preprocessing passes...
2018-04-25 Andrew ReynoldsMove candidate rewrite code to own file (#1804)
2018-04-25 Andrew ReynoldsAdd benchmark requiring subgoal generation with inducti...
2018-04-25 Andrew ReynoldsRemove nl solve subs option. (#1803)
2018-04-25 Andrew ReynoldsFix issue with multi-triggers that include variable...
2018-04-23 Andrew ReynoldsDraft smt comp 2018 for quantifiers and non-linear...
2018-04-21 Andrew ReynoldsImprove sygus sampling for strings (#1802)
2018-04-21 Andres NoetzliRemove unused cache.h (#1795)
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler...
2018-04-20 Andrew ReynoldsDraft of casc j9 scripts (#1800)
2018-04-20 yoni206Allow metadata lines in test files to have leading...
2018-04-20 PaulMengSymmetry detection module (#1749)
2018-04-20 Andres NoetzliRestrict test summary to first-level subfolders (#1797)
2018-04-19 yoni206Adding config/tap-driver.sh to .gitignore (#1792)
2018-04-19 Andres NoetzliRefactor pbRewrites preprocessing pass (#1767)
2018-04-19 Andres NoetzliRemove tap-driver.sh (#1791)
2018-04-17 Andres NoetzliAdd timeout (option) to regression script (#1786)
2018-04-17 Andres NoetzliDisable slow regression test (#1787)
2018-04-16 Andres NoetzliDisable check proofs/unsat cores for two regs (#1785)
2018-04-16 Andrew ReynoldsMake 256 the default cardinality for strings (#1783)
2018-04-16 Andres NoetzliRemoveTermFormulas: Remove ContainsTermITEVisitor ...
2018-04-16 Andrew ReynoldsSkolemize candidate rewrite rule checks (#1777)
2018-04-16 Andrew ReynoldsMake strings fmf apply to all but internally generated...
2018-04-15 Andrew ReynoldsFix type error with regexp (#1778)
2018-04-15 Andrew ReynoldsFix mk type const (#1776)
2018-04-14 Andrew ReynoldsAnother fix for sygus rr stats. (#1768)
2018-04-14 Andres Noetzli[Reg] Make status/unsat-core detection more robust...
2018-04-14 Andres NoetzliFix get-unsat-core detection in regression script ...
2018-04-14 yoni206allowing --bool-to-bv without quantifiers (#1771)
2018-04-14 Andres NoetzliFix use-after-free in eager bitblaster (#1772)
2018-04-14 Andrew ReynoldsDisable split for negative contains. (#1774)
2018-04-13 Andres NoetzliFix issue in regression script when proofs enabled...
2018-04-13 Andrew ReynoldsFix alpha equivalence for higher-order (#1769)
2018-04-12 Andrew ReynoldsFixes for free variables in assertions (#1762)
2018-04-11 Aina NiemetzRefactored BVGauss preprocessing pass. (#1766)
2018-04-11 Andrew ReynoldsProperly implement function extensionality based on...
2018-04-10 Andrew Reynolds Improve accuracy of stats for sygus sampler (#1755)
2018-04-10 Andres NoetzliRemove unused arith options (#1758)
2018-04-10 Andrew ReynoldsFix hasSubterm calls for higher-order (#1760)
next