projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) commit | commitdiff | tree
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsDisable slow regression (#4157) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsAdd stats for string reductions, lemmas and conflicts... commit | commitdiff | tree
2020-03-26 Andrew ReynoldsGeneralize more string-specific functions (#4152) commit | commitdiff | tree
2020-03-26 Andrew ReynoldsCare graphs based on polymorphic operators in strings... commit | commitdiff | tree
2020-03-25 Andres NoetzliSupport async-signal-safe printing of inferences (... commit | commitdiff | tree
2020-03-25 Ahmed Irfanbv2int : linear mult opt (#4142) commit | commitdiff | tree
2020-03-25 Andrew Reynolds Generalize more uses of string-specific functions... commit | commitdiff | tree
2020-03-24 yoni206Int2BV fail on demand (#4079) commit | commitdiff | tree
2020-03-24 Andrew ReynoldsRestrict partial triggers to standard quantified formul... commit | commitdiff | tree
2020-03-24 Andrew ReynoldsRestrict cases of sygus grammar reduction based on... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsInfer when sygus operators are equivalent to builtin... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) commit | commitdiff | tree
2020-03-23 Andrew ReynoldsThrow exception for non-well-founded unimplemented... commit | commitdiff | tree
2020-03-23 Andrew ReynoldsChange transcendental function app slave list to unorde... commit | commitdiff | tree
2020-03-23 Andres NoetzliCollect statistics about normal form inferences (#4127) commit | commitdiff | tree
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher... commit | commitdiff | tree
2020-03-22 Abdalrhman... Convert V1 Sygus files to V2. (#4136) commit | commitdiff | tree
2020-03-21 Andres NoetzliSimplify heuristic in `processNEqc` (#4129) commit | commitdiff | tree
2020-03-21 Andres NoetzliDon't run bv_nat parse test with competition build... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsGeneralize mkConcat for types (#4123) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsFix sort comparison within assertion in cegis (#4113) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsSplit string-specific operators from TheoryStringsRewri... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsDo not assign higher-order representative if function... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsHandle failures for sygus QE preprocess (#4072) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsParse error for SyGuS version 1.0 vs 2.0 (#4057) commit | commitdiff | tree
2020-03-20 Andrew ReynoldsMake handling of illegal internal representatives in... commit | commitdiff | tree
2020-03-20 Andrew ReynoldsRefactor enumerator for strings (#4014) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsFix regression output related to sygus+bv-div-zero... commit | commitdiff | tree
2020-03-19 yoni206Bv2int fail on demand commit | commitdiff | tree
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... commit | commitdiff | tree
2020-03-19 Andrew ReynoldsSyGuS must use total bitvector division (#4119) commit | commitdiff | tree
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... commit | commitdiff | tree
2020-03-19 Andrew ReynoldsRemove spurious assertion (#4117) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsExplicitly handle isFinite for rounding modes (#4115) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsAlways enable cbqi literal dependency (#4116) commit | commitdiff | tree
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... commit | commitdiff | tree
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) commit | commitdiff | tree
2020-03-17 Aina NiemetzSmtEngine: Convert members owned by SmtEngine to unique... commit | commitdiff | tree
2020-03-16 Alex OzdemirRemove AlwaysAssert(false) for hole. commit | commitdiff | tree
2020-03-16 Alex Ozdemirclang-format commit | commitdiff | tree
2020-03-16 Alex OzdemirFix simplicity check in prop commit | commitdiff | tree
2020-03-16 Alex OzdemirFix antecedent loop. Whoops commit | commitdiff | tree
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes commit | commitdiff | tree
2020-03-16 Alex OzdemirExpand the definition of a "simple" farkas proof. commit | commitdiff | tree
2020-03-16 Aina NiemetzDecisionEngine: Use single unique pointer for ITE strat... commit | commitdiff | tree
2020-03-16 Aina NiemetzIssue 4077: Add unit test to reproduce issue. (#4107) commit | commitdiff | tree
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... commit | commitdiff | tree
2020-03-16 Andrew ReynoldsHandle cases in --sygus-rr where evaluation is not... commit | commitdiff | tree
2020-03-13 Andrew ReynoldsRemoving a few deprecated options (#4052) commit | commitdiff | tree
2020-03-13 Andrew ReynoldsRemove regress for real to int (#4071) commit | commitdiff | tree
2020-03-13 Andrew ReynoldsGeneralize type rules for strings to sequences (#3987) commit | commitdiff | tree
2020-03-13 Andrew ReynoldsFix case of non-constant value for sygus sampling ... commit | commitdiff | tree
2020-03-12 Andrew ReynoldsAdd options for nec regression (#4056) commit | commitdiff | tree
2020-03-12 Andrew ReynoldsConvert most instances of dataypes in parsers to the... commit | commitdiff | tree
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... commit | commitdiff | tree
2020-03-12 Andrew ReynoldsRemove local theory extension option (#4048) commit | commitdiff | tree
2020-03-12 Andrew ReynoldsDo not make models for quantified function variables... commit | commitdiff | tree
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) commit | commitdiff | tree
2020-03-12 Andrew ReynoldsEnsure legal candidate equalities when using relational... commit | commitdiff | tree
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) commit | commitdiff | tree
2020-03-12 Aina NiemetzHide options for and related to the BV abstraction... commit | commitdiff | tree
2020-03-12 Andrew ReynoldsSimplifications to the Datatypes API (#4040) commit | commitdiff | tree
2020-03-12 makaimannAdd automatic Cython binding installation (#3933) commit | commitdiff | tree
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... commit | commitdiff | tree
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) commit | commitdiff | tree
2020-03-11 Andrew ReynoldsAdd missing datatype functions to new API (#3930) commit | commitdiff | tree
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) commit | commitdiff | tree
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... commit | commitdiff | tree
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) commit | commitdiff | tree
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... commit | commitdiff | tree
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... commit | commitdiff | tree
2020-03-11 Andrew ReynoldsFix (#4017) commit | commitdiff | tree
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (... commit | commitdiff | tree
2020-03-11 Andres NoetzliIntroduce tables in the rewriter (#3742) commit | commitdiff | tree
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) commit | commitdiff | tree
2020-03-11 Aina Niemetzbv-gauss-elim: Fix handling of inconsistent case. ... commit | commitdiff | tree
2020-03-11 Andrew ReynoldsFix real to int for parameterized kinds (#4016) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsFix options for regression: --sort-inference is incompa... commit | commitdiff | tree
2020-03-10 Andrew ReynoldsFix sort inference for top-level Boolean variables... commit | commitdiff | tree
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsLogic exception instead of assertion failure for instan... commit | commitdiff | tree
2020-03-10 Mathias PreinerUpdate bug report template commit | commitdiff | tree
2020-03-10 Andrew ReynoldsRemove assertion in resolution bound inferences (#3980) commit | commitdiff | tree
2020-03-10 Aina NiemetzUse fixed-width types in test/unit/context/contest_mm_b... commit | commitdiff | tree
2020-03-10 Aina NiemetzFix -Wshadow warning in test/unit/context/context_mm_bl... commit | commitdiff | tree
2020-03-10 Andrew ReynoldsConsolidate options that disable produceModels (#3973) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsFix assertion failure in sort inference for Boolean... commit | commitdiff | tree
2020-03-10 Aina NiemetzFix -Wshadow warnings in sygus_grammar_cons.cpp. (... commit | commitdiff | tree
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM... commit | commitdiff | tree
2020-03-10 Andrew Reynolds Fix real as int for incremental (#3979) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsDo not traverse quantifiers in nl ext purify (#3982) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsOnly register sygus terms to unfold if option is set... commit | commitdiff | tree
2020-03-10 Alex OzdemirDocument bv-to-bool recursion (#3848) commit | commitdiff | tree
2020-03-10 makaimannEnhancement: make the bool-to-bv pass more robust and... commit | commitdiff | tree
2020-03-10 Andrew ReynoldsRename sygus option name (#3977) commit | commitdiff | tree
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975) commit | commitdiff | tree
next