projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)
[cvc5.git] / src / expr /
2021-02-12 Andrew Reynolds(proof-new) Option to not automatically consider symmet... tree | commitdiff
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841) tree | commitdiff
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... tree | commitdiff
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) tree | commitdiff
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) tree | commitdiff
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710) tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) tree | commitdiff
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof... tree | commitdiff
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) tree | commitdiff
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671) tree | commitdiff
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655) tree | commitdiff
2020-12-10 Gereon KremerRefactor KindMap (#5646) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) tree | commitdiff
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641) tree | commitdiff
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating... tree | commitdiff
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... tree | commitdiff
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own... tree | commitdiff
2020-12-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601) tree | commitdiff
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) tree | commitdiff
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... tree | commitdiff
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (... tree | commitdiff
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... tree | commitdiff
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-16 Andrew ReynoldsCleaning up scopes in preparation for symbol manager... tree | commitdiff
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic... tree | commitdiff
2020-11-12 Andrew ReynoldsMake symbol manager context dependent (#5424) tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsAdd simple substitution utility (#5397) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398) tree | commitdiff
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-03 Andrew ReynoldsAdd scope methods constructing types in API (#5393) tree | commitdiff
2020-11-02 Andrew ReynoldsAvoid dynamic allocation in symbol table implementation... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-29 Gereon KremerAdd NodeManager::mkOr() (#5360) tree | commitdiff
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... tree | commitdiff
2020-10-27 Andrew ReynoldsAdd missing methods involving datatype sorts to the... tree | commitdiff
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340) tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Updates to lazy proof chain (#5317) tree | commitdiff
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) tree | commitdiff
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Fix for CDProof::isSame (#5297) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262) tree | commitdiff
2020-10-19 Haniel Barbosa[proof-new] Improving cycle checking in lazycdproofchai... tree | commitdiff
2020-10-19 Andrew Reynolds(proof-new) Refactoring cyclic checks (#5291) tree | commitdiff
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat... tree | commitdiff
2020-10-18 Andrew Reynolds(proof-new) Implementation of trust substitution (... tree | commitdiff
2020-10-14 Andrew Reynolds(proof-new) Simplifications for proof rule checker... tree | commitdiff
2020-10-13 Andrew Reynolds(proof-new) New rules for Booleans (#5243) tree | commitdiff
2020-10-13 Andrew Reynolds(proof-new) Change merge policy for proof node updater... tree | commitdiff
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228) tree | commitdiff
2020-10-09 Andrew Reynolds(proof-new) Add lazy proof set utility (#5221) tree | commitdiff
2020-10-08 Andrew Reynolds(proof-new) Fixes and improvements for smt proof postpr... tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Allow null proofs from generators in LazyCD... tree | commitdiff
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205) tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ... tree | commitdiff
2020-09-30 Andrew Reynolds(proof-new) Add the term conversion sequence generator... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156) tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof node hash function (#5154) tree | commitdiff
2020-09-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151) tree | commitdiff
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... tree | commitdiff
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-21 Andrew Reynolds(proof-new) Add the arrays proof checker (#5047) tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Updates to proof node updater algorithm... tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Rewrites involving operators in term conver... tree | commitdiff
2020-09-17 Haniel Barbosa[proof-new] Have mkScope agnostic to True assumptions... tree | commitdiff
2020-09-16 Haniel Barbosa[proof-new] Adds Lazy CDProof chain data-structure... tree | commitdiff
2020-09-16 Haniel Barbosa[proof-new] Resolution rules and checkers (#5070) tree | commitdiff
2020-09-16 Haniel Barbosa[proof-new] A simple proof generator for buffered proof... tree | commitdiff
2020-09-11 Andrew Reynolds(proof-new) Handle mismatched assumptions in proof... tree | commitdiff
2020-09-11 Andrew Reynolds(proof-new) Use deep copy for final lemma step in proof... tree | commitdiff
2020-09-09 Andrew Reynolds(proof-new) Minor changes to proof node updater (#5011) tree | commitdiff
2020-09-03 Andrew Reynolds(proof-new) Improve debugging infrastructure for open... tree | commitdiff
2020-09-02 Gereon KremerRemove #line directives from generated files. (#5005) tree | commitdiff
2020-09-02 Andrew Reynolds(proof-new) Updates to builtin proof checker (#4962) tree | commitdiff
2020-09-02 Andrew Reynolds(proof-new) Add proof support in TheoryUF (#5002) tree | commitdiff
next