projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-05-18 Andrew ReynoldsCache isInterpretedFinite (#1943) commit | commitdiff | tree
2018-05-18 Andrew ReynoldsCegis unif defaults to cegis when no unif (#1942) commit | commitdiff | tree
2018-05-18 Andrew ReynoldsUnified fairness scheme for cegis unif (#1941) commit | commitdiff | tree
2018-05-17 Andrew ReynoldsCatch type errors in sygus grammars for lambda (define... commit | commitdiff | tree
2018-05-17 Andrew ReynoldsFix debugPrint and add regress. (#1934) commit | commitdiff | tree
2018-05-17 Haniel BarbosaOption to force return values of Bool functions to... commit | commitdiff | tree
2018-05-17 Andrew ReynoldsCegis-specific infrastructure (#1933) commit | commitdiff | tree
2018-05-17 Andrew ReynoldsInternal propagation for refinement lemmas (#1932) commit | commitdiff | tree
2018-05-16 Andrew ReynoldsImprove the separation resolution scheme in cegis unif... commit | commitdiff | tree
2018-05-16 yoni206Refactor static learning preprocessing pass (#1857) commit | commitdiff | tree
2018-05-15 Andrew ReynoldsRefactoring get enumerator values in construct candidat... commit | commitdiff | tree
2018-05-15 Haniel Barbosaadding regressions (#1925) commit | commitdiff | tree
2018-05-15 Haniel BarbosaBuilding and refining solutions with dynamic condition... commit | commitdiff | tree
2018-05-15 Andrew ReynoldsFix free variables in cbqi preregister inst. (#1921) commit | commitdiff | tree
2018-05-15 Andrew ReynoldsFix annotations in regress2. (#1917) commit | commitdiff | tree
2018-05-15 Andrew ReynoldsMinor improvements to --nl-ext-purify (#1896) commit | commitdiff | tree
2018-05-15 Andrew Reynolds Incorporating dynamic condition enumeration into cegis... commit | commitdiff | tree
2018-05-14 MartinFloating point theory solver based on SymFPU (#1895) commit | commitdiff | tree
2018-05-14 Mathias PreinerAdd contrib/get-symfpu for downloading symfpu. (#1905) commit | commitdiff | tree
2018-05-14 Haniel BarbosaFix purification in SygusUnifRL (#1912) commit | commitdiff | tree
2018-05-14 Andrew ReynoldsAdd regressions, change defaults. (#1911) commit | commitdiff | tree
2018-05-14 Andrew ReynoldsFlag to check invariance of entire values in sygus... commit | commitdiff | tree
2018-05-14 Florian SchandaSmall change for more sensible line breaking in the... commit | commitdiff | tree
2018-05-11 Aina NiemetzRemove obsolete unit test for ackermannization. (#1906) commit | commitdiff | tree
2018-05-11 Aina NiemetzFix ackermannize preprocessing pass. (#1904) commit | commitdiff | tree
2018-05-11 Andres NoetzliSupport multiple sets of command line args in regs... commit | commitdiff | tree
2018-05-11 Haniel BarbosaAlso exclude ITEs from ITE conditions in SygusUnifStrat... commit | commitdiff | tree
2018-05-10 Andrew ReynoldsExclude Boolean connectives from ITE conditions in... commit | commitdiff | tree
2018-05-10 Andrew ReynoldsSygus repair constants (#1812) commit | commitdiff | tree
2018-05-10 Haniel BarbosaStatic learn redundant operators in CegisUnif (#1899) commit | commitdiff | tree
2018-05-10 Andrew ReynoldsAdd ITE to default Boolean sygus grammar (#1898) commit | commitdiff | tree
2018-05-10 Aina NiemetzRefactored BVAckermann preprocessing pass. (#1889) commit | commitdiff | tree
2018-05-10 Andrew ReynoldsFix priority of decisions for cegis unif (#1897) commit | commitdiff | tree
2018-05-09 Haniel BarbosaPiecing solutions together in CegisUnif (#1894) commit | commitdiff | tree
2018-05-09 yoni206Reorder class members in bv-to-bool and bool-to-bv... commit | commitdiff | tree
2018-05-09 Andrew ReynoldsBetter option names for PBE (#1891) commit | commitdiff | tree
2018-05-09 Andrew ReynoldsMake symmetry-breaker-exp into a preprocessing pass... commit | commitdiff | tree
2018-05-09 PaulMengAdd the symmetry breaker module (#1847) commit | commitdiff | tree
2018-05-08 Mathias PreinerRefactor bv-abstraction preprocessing pass. (#1860) commit | commitdiff | tree
2018-05-08 Andrew ReynoldsInfrastructure for approximations in model output ... commit | commitdiff | tree
2018-05-08 Andrew ReynoldsSupport for str.<= and str.< (#1882) commit | commitdiff | tree
2018-05-08 Aina NiemetzFix order of preprocessing pass registration. (#1887) commit | commitdiff | tree
2018-05-08 Haniel BarbosaClassifying data in SygusUnifRL (#1886) commit | commitdiff | tree
2018-05-08 Andrew ReynoldsInfrastructure for CEGQI handled status (#1873) commit | commitdiff | tree
2018-05-08 Haniel Barbosaonly lazy trie changes (#1885) commit | commitdiff | tree
2018-05-07 Andrew ReynoldsAdd support for str.code (#1821) commit | commitdiff | tree
2018-05-05 Andrew ReynoldsFix handling of TO_REAL in cvc printer (#1876) commit | commitdiff | tree
2018-05-05 Andrew ReynoldsRemove special case for record selector printing. ... commit | commitdiff | tree
2018-05-04 Andrew ReynoldsCegis unif register evaluation points (#1878) commit | commitdiff | tree
2018-05-04 Andres NoetzliMake --output-lang consistent with --lang (#1877) commit | commitdiff | tree
2018-05-04 Andrew ReynoldsDo not print tuples. (#1874) commit | commitdiff | tree
2018-05-04 Mathias PreinerRefactor bv-intro-pow2 preprocessing pass. (#1851) commit | commitdiff | tree
2018-05-04 Andres NoetzliFix printing of multiple datatypes (#1872) commit | commitdiff | tree
2018-05-04 Haniel BarbosaMove Lazy trie datastructure to its own file (#1871) commit | commitdiff | tree
2018-05-04 Andrew ReynoldsInitialize cegis unif strategy (#1861) commit | commitdiff | tree
2018-05-04 Andrew ReynoldsDocument datatypes sygus (#1818) commit | commitdiff | tree
2018-05-04 Andrew ReynoldsSets subtypes (#1095) commit | commitdiff | tree
2018-05-03 Mathias PreinerFix redundant internalPush calls. (#1865) commit | commitdiff | tree
2018-05-03 Andres NoetzliFix warnings in proof code (#1850) commit | commitdiff | tree
2018-05-03 Andrew ReynoldsInterleave quantifiers checks with ground theory checks... commit | commitdiff | tree
2018-05-03 Andrew ReynoldsOption to interleave tangent plane inferences (#1833) commit | commitdiff | tree
2018-05-03 Andrew ReynoldsLink cegis unif with the enumeration manager (#1859) commit | commitdiff | tree
2018-05-03 Haniel BarbosaMake CegisUnif default to Cegis when no unif used ... commit | commitdiff | tree
2018-05-03 Andrew ReynoldsFix cvc printer for nullary constructors (#1856) commit | commitdiff | tree
2018-05-03 Andres NoetzliRemove (dummy) SMT1 printer (#1854) commit | commitdiff | tree
2018-05-03 Andrew ReynoldsSupport HORN logic string (#1849) commit | commitdiff | tree
2018-05-03 Andrew ReynoldsInitial support for string standard in smt lib 2.6... commit | commitdiff | tree
2018-05-01 Andrew ReynoldsCegis unif enumerator manager (#1837) commit | commitdiff | tree
2018-05-01 Andrew ReynoldsImprove tangent planes for transcendental functions... commit | commitdiff | tree
2018-04-30 Haniel BarbosaRefactor real2int (#1813) commit | commitdiff | tree
2018-04-30 Andres NoetzliRemove dead code in bv-to-bool preprocessing pass ... commit | commitdiff | tree
2018-04-30 Andrew ReynoldsRemove subsort symmetry breaking (#1807) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsFix 1156 (#1830) commit | commitdiff | tree
2018-04-30 Andres NoetzliDisable unsat-cores/proofs for slow regression (#1835) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsAllow multiple functions in sygus unif approaches ... commit | commitdiff | tree
2018-04-30 Andrew ReynoldsMake factoring inference more aggressive (#1825) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsRefactor nonlinear check (#1814) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsImprovements to simple transcendental function check... commit | commitdiff | tree
2018-04-28 Haniel BarbosaInitial implementation of SygusUnifRL (#1829) commit | commitdiff | tree
2018-04-28 Andrew ReynoldsMake construct solution behavior specific to SygusIO... commit | commitdiff | tree
2018-04-27 Andrew ReynoldsPrint function for equality status. (#1826) commit | commitdiff | tree
2018-04-27 Andrew ReynoldsSimplify tangent plane direction (#1824) commit | commitdiff | tree
2018-04-27 Haniel BarbosaNew module for synthesizing functions in a data-driven... commit | commitdiff | tree
2018-04-27 Andrew ReynoldsCore improvements to extended rewriter (#1820) commit | commitdiff | tree
2018-04-26 Andrew ReynoldsFix subgoal generation context (#1816) commit | commitdiff | tree
2018-04-25 yoni206Refactor array-proofs and uf-proofs (#1655) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsEquality resolution in the extended rewriter (#1811) commit | commitdiff | tree
2018-04-25 yoni206Refactor bv-to-bool and bool-to-bv preprocessing passes... commit | commitdiff | tree
2018-04-25 Andrew ReynoldsMove candidate rewrite code to own file (#1804) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsAdd benchmark requiring subgoal generation with inducti... commit | commitdiff | tree
2018-04-25 Andrew ReynoldsRemove nl solve subs option. (#1803) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsFix issue with multi-triggers that include variable... commit | commitdiff | tree
2018-04-23 Andrew ReynoldsDraft smt comp 2018 for quantifiers and non-linear... commit | commitdiff | tree
2018-04-21 Andrew ReynoldsImprove sygus sampling for strings (#1802) commit | commitdiff | tree
2018-04-21 Andres NoetzliRemove unused cache.h (#1795) commit | commitdiff | tree
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv... commit | commitdiff | tree
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler... commit | commitdiff | tree
2018-04-20 Andrew ReynoldsDraft of casc j9 scripts (#1800) commit | commitdiff | tree
2018-04-20 yoni206Allow metadata lines in test files to have leading... commit | commitdiff | tree
2018-04-20 PaulMengSymmetry detection module (#1749) commit | commitdiff | tree
next