projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2020-03-05 Andres NoetzliAdd a new arith constraint proof rule: IntTightenAP... commit | commitdiff | tree
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... commit | commitdiff | tree
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... commit | commitdiff | tree
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... commit | commitdiff | tree
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... commit | commitdiff | tree
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) commit | commitdiff | tree
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) commit | commitdiff | tree
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... commit | commitdiff | tree
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers... commit | commitdiff | tree
2020-03-03 Andres NoetzliFix `TheorySetsPrive::eqNotifyPostMerge()` (#3901) commit | commitdiff | tree
2020-03-03 Mathias PreinerFix variable shadowing bug in sets. (#3898) commit | commitdiff | tree
2020-03-02 Andrew Reynolds Split collect model info by types in strings (#3847) commit | commitdiff | tree
2020-02-29 Andrew ReynoldsConvert more uses of string to word (#3834) commit | commitdiff | tree
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... commit | commitdiff | tree
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) commit | commitdiff | tree
2020-02-29 Aina NiemetzpropEngine: Reorder class declaration according to... commit | commitdiff | tree
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model... commit | commitdiff | tree
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... commit | commitdiff | tree
2020-02-28 Andrew ReynoldsUse enum for quantifiers rewrite steps (#3840) commit | commitdiff | tree
2020-02-27 Andrew ReynoldsRefactor operator applications in the parser (#3831) commit | commitdiff | tree
2020-02-27 Haniel BarbosaChanging TPTP parser to accomodate new API (#3837) commit | commitdiff | tree
2020-02-27 Andrew ReynoldsUpdate purifySygusGTerm to the new API (#3830) commit | commitdiff | tree
2020-02-27 Andrew ReynoldsFix large models for strings (#3835) commit | commitdiff | tree
next