projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-06-04 Andrew ReynoldsEnable cegqi (with model values) for floating point... commit | commitdiff | tree
2018-06-04 Andres NoetzliRegressions: Support for requiring CVC4 features (... commit | commitdiff | tree
2018-06-02 Andrew Reynolds Fix assertion involving unassigned Boolean eqc in... commit | commitdiff | tree
2018-06-02 Andrew ReynoldsFix corner case of mixed int/real cegqi. (#2046) commit | commitdiff | tree
2018-06-02 Mathias PreinerFix BV-abstraction check to consider SKOLEM. (#2042) commit | commitdiff | tree
2018-06-02 Andrew ReynoldsFix preinitialization pass for finite model finding... commit | commitdiff | tree
2018-06-01 Andrew ReynoldsFix quantified bv variable elimination (#2039) commit | commitdiff | tree
2018-06-01 Andrew ReynoldsFix quantifiers conflict lemma handling (#2043) commit | commitdiff | tree
2018-06-01 Andrew ReynoldsApply preprocessing to counterexample lemmas in CEGQI... commit | commitdiff | tree
2018-06-01 Andrew Reynolds Use monomial sum utility to solve for quantifiers... commit | commitdiff | tree
2018-06-01 Andrew ReynoldsReduce before preregister. (#2025) commit | commitdiff | tree
2018-05-31 Mathias PreinerFix bv-abstraction check for AND with non bit-vector... commit | commitdiff | tree
2018-05-30 Aina NiemetzIgnore license key in set-info command. (#2021) commit | commitdiff | tree
2018-05-30 Andres NoetzliFix for issue #2002 (#2012) commit | commitdiff | tree
2018-05-30 Andrew ReynoldsFixes for quantifiers + incremental (#2009) commit | commitdiff | tree
2018-05-30 Andres Noetzli[SMT-COMP] Print non-(un)sat output to stderr (#2019) commit | commitdiff | tree
2018-05-30 Mathias PreinerNormalize negated bit-vector terms over equalities... commit | commitdiff | tree
2018-05-30 Mathias PreinerUse CaDiCaL for eager bit-blasting in QF_NIA and QF_UFB... commit | commitdiff | tree
2018-05-30 Andrew ReynoldsDraft run script for strings smt comp 2018. (#2016) commit | commitdiff | tree
2018-05-29 Andres Noetzli Make user's SMT2 version override file version (#2004) commit | commitdiff | tree
2018-05-29 Andrew ReynoldsDisable minisat elimination when nonlinear is enabled... commit | commitdiff | tree
2018-05-29 Andres NoetzliTrack input language in a single place (#2003) commit | commitdiff | tree
2018-05-28 Andrew ReynoldsBuiltin evaluation functions for sygus (#1991) commit | commitdiff | tree
2018-05-27 Andrew ReynoldsFix cegqi assertions for quantified non-linear cases... commit | commitdiff | tree
2018-05-27 Andres NoetzliFix no-cbqi-innermost option name in run script (#1994) commit | commitdiff | tree
2018-05-26 Mathias PreinerUpdate SymFPU. (#1992) commit | commitdiff | tree
2018-05-25 Andrew ReynoldsReenable repair const (#1983) commit | commitdiff | tree
2018-05-25 Andres NoetzliMiniSat: Be more careful about running proof code ... commit | commitdiff | tree
2018-05-25 Mathias PreinerAdd QF_BV configuration for SMTCOMP'18. (#1981) commit | commitdiff | tree
2018-05-25 Andrew ReynoldsFix various nl assertions. (#1980) commit | commitdiff | tree
2018-05-25 Andrew ReynoldsFix (#1979) commit | commitdiff | tree
2018-05-24 Andrew ReynoldsImprove simple constant symmetry breaking for sygus... commit | commitdiff | tree
2018-05-24 Andres NoetzliFix compiler warnings (#1959) commit | commitdiff | tree
2018-05-24 Andrew ReynoldsFix (#1975) commit | commitdiff | tree
2018-05-24 Andrew ReynoldsFixes for non-linear check model (#1974) commit | commitdiff | tree
2018-05-24 Andrew ReynoldsFix nl regression for unsat cores. (#1973) commit | commitdiff | tree
2018-05-24 Andrew ReynoldsRemove spurious assertion in nonlinear extension (... commit | commitdiff | tree
2018-05-23 Haniel BarbosaTowards better symbolic enumeration in SyGuS (#1971) commit | commitdiff | tree
2018-05-23 Andrew ReynoldsAdd notions of evaluated kinds in TheoryModel (#1947) commit | commitdiff | tree
2018-05-23 Andres NoetzliRemove ProofProxy (#1965) commit | commitdiff | tree
2018-05-23 Andrew ReynoldsGeneralize check-model in NonLinearExtension for quadra... commit | commitdiff | tree
2018-05-23 Andres NoetzliSet same options for proofs as for unsat cores (#1957) commit | commitdiff | tree
2018-05-23 Andrew ReynoldsRepair constants using symbolic constructors (#1960) commit | commitdiff | tree
2018-05-22 Andrew ReynoldsParse error for sygus grammar term with multiple let... commit | commitdiff | tree
2018-05-22 Andres NoetzliDisable symmetry breaker for unsat cores (#1958) commit | commitdiff | tree
2018-05-22 Andrew ReynoldsMake sygus infer find function definitions (#1951) commit | commitdiff | tree
2018-05-22 Andrew ReynoldsInfrastructure for strings strategies (#1883) commit | commitdiff | tree
2018-05-22 Mathias PreinerAdd SymFPU licensing information. (#1952) commit | commitdiff | tree
2018-05-21 Andrew ReynoldsImprovements in parsing and printing related to mixed... commit | commitdiff | tree
2018-05-21 Andrew ReynoldsInfrastructure to mark unused sygus strategies (#1950) commit | commitdiff | tree
2018-05-21 makaimannHandle IMPLIES in bool-to-bv and test it in regress0... commit | commitdiff | tree
2018-05-21 Andrew ReynoldsRefactor sygus eval unfold (#1946) commit | commitdiff | tree
2018-05-21 Andres NoetzliRemove Eclipse project files (#1928) commit | commitdiff | tree
2018-05-21 Andres NoetzliFix compiler warning in hashsmt example (#1927) commit | commitdiff | tree
2018-05-21 Haniel BarbosaAssign weight 1 for Boolean variables in SyGuS default... commit | commitdiff | tree
2018-05-21 Caleb DonovickFix file extension (#1919) commit | commitdiff | tree
2018-05-19 Haniel Barbosachanging default (#1944) commit | commitdiff | tree
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
next