projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula... commit | commitdiff | tree
2020-12-21 Andrew ReynoldsFix issue with selector triggers (#5689) commit | commitdiff | tree
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... commit | commitdiff | tree
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) commit | commitdiff | tree
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704) commit | commitdiff | tree
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... commit | commitdiff | tree
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) commit | commitdiff | tree
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699) commit | commitdiff | tree
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof... commit | commitdiff | tree
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696) commit | commitdiff | tree
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... commit | commitdiff | tree
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695) commit | commitdiff | tree
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) commit | commitdiff | tree
2020-12-17 Haniel Barbosa[proof-new] Only use old proof code for unsat cores... commit | commitdiff | tree
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) commit | commitdiff | tree
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684) commit | commitdiff | tree
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) commit | commitdiff | tree
2020-12-16 mudathirmahgoubRenamed InferInfo::getAntecedant to InferInfo::getAntec... commit | commitdiff | tree
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) commit | commitdiff | tree
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... commit | commitdiff | tree
2020-12-16 Andrew ReynoldsUse uint64 utility when parsing tuple selectors in... commit | commitdiff | tree
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680) commit | commitdiff | tree
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678) commit | commitdiff | tree
2020-12-15 Andrew ReynoldsProper expand definitions for sets (#5676) commit | commitdiff | tree
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... commit | commitdiff | tree
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671) commit | commitdiff | tree
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) commit | commitdiff | tree
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (... commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing... commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667) commit | commitdiff | tree
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) commit | commitdiff | tree
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... commit | commitdiff | tree
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655) commit | commitdiff | tree
2020-12-14 Andrew ReynoldsFix and improve evaluator (#5563) commit | commitdiff | tree
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... commit | commitdiff | tree
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ... commit | commitdiff | tree
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654) commit | commitdiff | tree
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast... commit | commitdiff | tree
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) commit | commitdiff | tree
2020-12-10 Gereon KremerRefactor KindMap (#5646) commit | commitdiff | tree
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (... commit | commitdiff | tree
2020-12-10 Andrew ReynoldsRefactor regressions (#5639) commit | commitdiff | tree
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634) commit | commitdiff | tree
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) commit | commitdiff | tree
2020-12-09 Aina NiemetzFix compiler warnings. (#5644) commit | commitdiff | tree
2020-12-09 Andrew Reynolds(proof-new) Make theory preprocessor proofs self contai... commit | commitdiff | tree
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) commit | commitdiff | tree
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641) commit | commitdiff | tree
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632) commit | commitdiff | tree
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633) commit | commitdiff | tree
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630) commit | commitdiff | tree
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622) commit | commitdiff | tree
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627) commit | commitdiff | tree
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... commit | commitdiff | tree
2020-12-09 yoni206update doc (#5619) commit | commitdiff | tree
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592) commit | commitdiff | tree
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587) commit | commitdiff | tree
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) commit | commitdiff | tree
2020-12-08 Abdalrhman... Fix a bug with synth-fun printer (#5512) commit | commitdiff | tree
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... commit | commitdiff | tree
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... commit | commitdiff | tree
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating... commit | commitdiff | tree
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... commit | commitdiff | tree
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make... commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... commit | commitdiff | tree
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... commit | commitdiff | tree
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... commit | commitdiff | tree
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own... commit | commitdiff | tree
2020-12-07 Gereon KremerAdd regression from #4927 (#5556) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601) commit | commitdiff | tree
2020-12-05 Everett MausChange generated options to be thread_local. (#5583) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: expr: Migrate attribute_black. (#5598) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdo_black. (#5586) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_white. (#5585) commit | commitdiff | tree
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: api: Migrate sort_black. (#5594) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_black. (#5584) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdlist_black. (#5582) commit | commitdiff | tree
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) commit | commitdiff | tree
2020-12-04 Mathias Preinerupdate-copyright: Preserve file permissions. (#5597) commit | commitdiff | tree
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: api: Migrate solver_black. (#5570) commit | commitdiff | tree
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... commit | commitdiff | tree
2020-12-03 yoni206Models as (#5581) commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: Add fixture for context tests. (#5590) commit | commitdiff | tree
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) commit | commitdiff | tree
2020-12-03 Gereon KremerMake run_regression.py executable. (#5588) commit | commitdiff | tree
2020-12-03 Aina NiemetzUpdate copyright headers. commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: base: Migrate map_util_black. (#5580) commit | commitdiff | tree
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... commit | commitdiff | tree
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) commit | commitdiff | tree
next