projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... commit | commitdiff | tree
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all... commit | commitdiff | tree
2021-02-11 Haniel Barbosa[proof-new] Adding a proof-producing ensure literal... commit | commitdiff | tree
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) commit | commitdiff | tree
2021-02-11 Andrew ReynoldsFix spurious assertion failure in regexp normalization... commit | commitdiff | tree
2021-02-11 Andrew ReynoldsSimplify interface for preprocessor (#5890) commit | commitdiff | tree
2021-02-10 Andrew ReynoldsRefactor term registration visitors (#5875) commit | commitdiff | tree
2021-02-10 Andrew ReynoldsFix open proof for factoring lemma (#5885) commit | commitdiff | tree
2021-02-10 Andrew ReynoldsSimplify method for inferring proxy lemmas in strings... commit | commitdiff | tree
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) commit | commitdiff | tree
2021-02-10 Andrew ReynoldsOptimize get skolems method (#5876) commit | commitdiff | tree
2021-02-10 Andrew ReynoldsDo not traverse quantifiers in term formula removal... commit | commitdiff | tree
2021-02-09 Mathias Preinercmake: Make Python3 default and improve toml error... commit | commitdiff | tree
2021-02-09 Andrew ReynoldsEliminating dependencies from inst utils (#5882) commit | commitdiff | tree
2021-02-09 Andrew ReynoldsMake term database optionally SAT-context-dependent... commit | commitdiff | tree
2021-02-09 Aina Niemetzgoogle test: expr: Migrate node_manager_black. (#5857) commit | commitdiff | tree
2021-02-09 Aina Niemetzgoogle test: main: Migrate interactive_shell_black... commit | commitdiff | tree
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_cardinality_black.... commit | commitdiff | tree
2021-02-09 Aina Niemetzgoogle test: expr: Migrate node_self_iterator_black... commit | commitdiff | tree
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) commit | commitdiff | tree
2021-02-09 Aina Niemetzgoogle test: expr: Migrate type_node_white. (#5872) commit | commitdiff | tree
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management... commit | commitdiff | tree
2021-02-08 Andrew ReynoldsFix disequality between seq.unit terms (#5880) commit | commitdiff | tree
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_white. (#5869) commit | commitdiff | tree
2021-02-08 Haniel BarbosaFix dumping of assertions for monolithic preprocessing... commit | commitdiff | tree
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874) commit | commitdiff | tree
2021-02-08 Aina NiemetzUse consistent names for fixtures in unit tests. (... commit | commitdiff | tree
2021-02-08 Aina Niemetzgoogle test: expr: Migrate node_traversal_black. (... commit | commitdiff | tree
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio... commit | commitdiff | tree
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check... commit | commitdiff | tree
2021-02-05 Aina Niemetzgoogle test: expr: Migrate symbol_table_black. (#5870) commit | commitdiff | tree
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
next