projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2020-03-10 Andrew ReynoldsEnsure standard miniscoping is applied before aggressiv... commit | commitdiff | tree
2020-03-09 Andrew ReynoldsEliminate spurious assertion (#3976) commit | commitdiff | tree
2020-03-09 Aina NiemetzDecisionEngine: Use unique_ptr for enabled strategies... commit | commitdiff | tree
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972) commit | commitdiff | tree
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) commit | commitdiff | tree
2020-03-09 Andres NoetzliIncrease stack size for Windows builds to 100 MB (... commit | commitdiff | tree
2020-03-09 Andrew ReynoldsClean up more uses of ExprManager in parsers (#3932) commit | commitdiff | tree
2020-03-09 Andrew ReynoldsConvert more uses of strings to words (#3921) commit | commitdiff | tree
2020-03-09 Andres NoetzliFix quoting of options on Travis (#3981) commit | commitdiff | tree
2020-03-09 Andrew ReynoldsFixes for bounds on transcendental functions (#3832) commit | commitdiff | tree
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945) commit | commitdiff | tree
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... commit | commitdiff | tree
2020-03-06 Andrew ReynoldsMinor refactor for theory of sets (#3924) commit | commitdiff | tree
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) commit | commitdiff | tree
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) commit | commitdiff | tree
2020-03-06 Andres NoetzliIgnore model check warning in regression test (#3926) commit | commitdiff | tree
2020-03-06 Andrew ReynoldsMake sygus datatype building independent of parser... commit | commitdiff | tree
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... commit | commitdiff | tree
2020-03-06 Andres NoetzliMake output of regression script more readable (#3911) commit | commitdiff | tree
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) commit | commitdiff | tree
2020-03-05 Alex OzdemirAdd a new arith constraint proof rule: IntTightenAP... commit | commitdiff | tree
2020-03-05 Alex OzdemirRevert "Add a new arith constraint proof rule: IntTight... commit | commitdiff | tree
next