projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-02-05 Andrew ReynoldsMinor cleaning of quantifiers engine (#5858) commit | commitdiff | tree
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_manager_white. (#5864) commit | commitdiff | tree
2021-02-05 Aina NiemetzRemove obsolete include from node_black unit test.... commit | commitdiff | tree
2021-02-05 Aina Niemetzgoogle test: expr: Migrate node_builder_black. (#5855) commit | commitdiff | tree
2021-02-05 Andrew ReynoldsMiscellaneous cleaning in theory engine (#5854) commit | commitdiff | tree
2021-02-04 yoni206Adding an option to optimize polite combination for... commit | commitdiff | tree
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829) commit | commitdiff | tree
2021-02-04 yoni206Clarifying documentation of `--static-binary` (#5844) commit | commitdiff | tree
2021-02-04 Andrew ReynoldsEliminate equality query dependence on quantifiers... commit | commitdiff | tree
2021-02-04 Haniel Barbosa[proof-new] Catch trivial cycles in SAT proof generatio... commit | commitdiff | tree
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) commit | commitdiff | tree
2021-02-03 Haniel Barbosa[proof-new] Fix MACRO_RESOLUTION expansion for singleto... commit | commitdiff | tree
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841) commit | commitdiff | tree
2021-02-02 Andrew Reynolds(proof-new) Refactor theory preprocessing (#5835) commit | commitdiff | tree
2021-02-02 Andrew ReynoldsRemove quantifiers regression from decision folder... commit | commitdiff | tree
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) commit | commitdiff | tree
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846) commit | commitdiff | tree
2021-02-02 Haniel Barbosa[proof-new] Fix bug in expansion of MACRO_RESOLUTION... commit | commitdiff | tree
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827) commit | commitdiff | tree
2021-02-01 Andrew ReynoldsSimplify alpha equivalence module (#5839) commit | commitdiff | tree
2021-02-01 Abdalrhman... Avoid calling the printers while converting sexpr to... commit | commitdiff | tree
2021-02-01 mudathirmahgoubFix BagsRewriter::rewriteUnionDisjoint (#5840) commit | commitdiff | tree
2021-01-30 Andrew ReynoldsFix unguarded call to get representative (#5838) commit | commitdiff | tree
2021-01-29 Haniel Barbosa[proof-new] Connecting new unsat cores (#5834) commit | commitdiff | tree
2021-01-29 mudathirmahgoubAdd bag inferences for operators: intersection, duplica... commit | commitdiff | tree
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... commit | commitdiff | tree
2021-01-28 Andrew ReynoldsReorganize calls to quantifiers engine from SmtEngine... commit | commitdiff | tree
2021-01-28 mudathirmahgoubRemove regex header from cvc4cpp.cpp (#5826) commit | commitdiff | tree
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) commit | commitdiff | tree
2021-01-28 Andrew ReynoldsUse standard equality engine information in quantifiers... commit | commitdiff | tree
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) commit | commitdiff | tree
2021-01-27 Andrew ReynoldsAdd option for whether to filter candidate rewrite... commit | commitdiff | tree
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) commit | commitdiff | tree
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... commit | commitdiff | tree
2021-01-27 Alex OzdemirThread proofs through arith channels & similar (#5818) commit | commitdiff | tree
2021-01-27 Andrew ReynoldsUse term canonizer utility locally in quantifiers ... commit | commitdiff | tree
2021-01-27 Andrew ReynoldsUse standard conflict mechanism in quantifiers state... commit | commitdiff | tree
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821) commit | commitdiff | tree
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) commit | commitdiff | tree
2021-01-26 Andrew ReynoldsRefactor quantifiers engine initialization (#5813) commit | commitdiff | tree
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) commit | commitdiff | tree
2021-01-26 Alex OzdemirAdd proofs to TheoryArithPrivate::propagate (#5812) commit | commitdiff | tree
2021-01-25 mudathirmahgoubRefactor bags::SolverState (#5783) commit | commitdiff | tree
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocesse... commit | commitdiff | tree
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) commit | commitdiff | tree
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) commit | commitdiff | tree
2021-01-25 mudathirmahgoubrename InferInfo::d_newSkolem to InferInfo::d_skolems... commit | commitdiff | tree
2021-01-24 Andrew Reynolds Initial cleaning of e-matching instantiation strategy... commit | commitdiff | tree
2021-01-24 Andrew ReynoldsInitial cleaning of triggers (#5795) commit | commitdiff | tree
2021-01-24 Andrew ReynoldsInitial cleaning of inst match generator (#5794) commit | commitdiff | tree
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) commit | commitdiff | tree
2021-01-24 Andrew ReynoldsAdd interface for getting preprocessed term (#5798) commit | commitdiff | tree
2021-01-22 Haniel Barbosa[proof-new] Expanding MACRO_RESOLUTION in post-processi... commit | commitdiff | tree
2021-01-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793) commit | commitdiff | tree
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792) commit | commitdiff | tree
2021-01-20 Andrew ReynoldsRefactoring the single invocation solver (#5706) commit | commitdiff | tree
2021-01-20 Andrew ReynoldsFix type issues with relevant domain computation (... commit | commitdiff | tree
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger... commit | commitdiff | tree
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop... commit | commitdiff | tree
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear... commit | commitdiff | tree
2021-01-20 Andrew ReynoldsUse arbitrary ground term assignment for sorts where... commit | commitdiff | tree
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) commit | commitdiff | tree
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... commit | commitdiff | tree
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) commit | commitdiff | tree
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775) commit | commitdiff | tree
2021-01-13 Ying ShengAdd unit test for api getInterpolant() -- issue #5593... commit | commitdiff | tree
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) commit | commitdiff | tree
2021-01-12 Aina Niemetzgoogle test: expr: Migrate node_black. (#5764) commit | commitdiff | tree
2021-01-12 Aina Niemetzgoogle test: Use ASSERT_* instead of EXPECT_*. (#5765) commit | commitdiff | tree
2021-01-12 yoni206Foreign theory rewrite option (#5763) commit | commitdiff | tree
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) commit | commitdiff | tree
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... commit | commitdiff | tree
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760) commit | commitdiff | tree
2021-01-09 yoni206Strings arith checks preprocessing pass: step 2 (#5750) commit | commitdiff | tree
2021-01-09 mudathirmahgoubFix issue 5513 (#5757) commit | commitdiff | tree
2021-01-08 mudathirmahgoubRename getAntecedent to getPremises (#5754) commit | commitdiff | tree
2021-01-08 Haniel Barbosa[proof-new] Implementing getProof in the API and SMT... commit | commitdiff | tree
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) commit | commitdiff | tree
2021-01-08 yoni206bv-to-int: avoid binarizing nodes twice (#5749) commit | commitdiff | tree
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... commit | commitdiff | tree
2021-01-07 Haniel BarbosaRemove dependency on expression layer in TPTP parser... commit | commitdiff | tree
2021-01-07 Haniel BarbosaFix warning in TPTP parser (#5752) commit | commitdiff | tree
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747) commit | commitdiff | tree
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... commit | commitdiff | tree
2021-01-05 yoni206Adding str.len to triggers (#5746) commit | commitdiff | tree
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... commit | commitdiff | tree
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... commit | commitdiff | tree
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY... commit | commitdiff | tree
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708) commit | commitdiff | tree
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) commit | commitdiff | tree
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... commit | commitdiff | tree
2020-12-23 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714) commit | commitdiff | tree
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707) commit | commitdiff | tree
2020-12-23 Andrew ReynoldsMinor simplification to Theory::theoryOf (#5719) commit | commitdiff | tree
2020-12-22 yoni206Delete duplicated code (#5718) commit | commitdiff | tree
2020-12-22 Andrew ReynoldsMove slow regression to regress3 (#5715) commit | commitdiff | tree
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... commit | commitdiff | tree
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) commit | commitdiff | tree
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) commit | commitdiff | tree
2020-12-21 Haniel BarbosaHave unsat core regression agnostic to number of assert... commit | commitdiff | tree
next