projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove a few miscellaneous references to the expr layer (#5661)
[cvc5.git] / src /
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY... tree | commitdiff
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708) tree | commitdiff
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) tree | commitdiff
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... tree | commitdiff
2020-12-23 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714) tree | commitdiff
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707) tree | commitdiff
2020-12-23 Andrew ReynoldsMinor simplification to Theory::theoryOf (#5719) tree | commitdiff
2020-12-22 yoni206Delete duplicated code (#5718) tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) tree | commitdiff
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710) tree | commitdiff
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin... tree | commitdiff
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula... tree | commitdiff
2020-12-21 Andrew ReynoldsFix issue with selector triggers (#5689) tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... tree | commitdiff
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687) tree | commitdiff
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704) tree | commitdiff
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) tree | commitdiff
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699) tree | commitdiff
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof... tree | commitdiff
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696) tree | commitdiff
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695) tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) tree | commitdiff
2020-12-17 Haniel Barbosa[proof-new] Only use old proof code for unsat cores... tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) tree | commitdiff
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684) tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) tree | commitdiff
2020-12-16 mudathirmahgoubRenamed InferInfo::getAntecedant to InferInfo::getAntec... tree | commitdiff
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) tree | commitdiff
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro... tree | commitdiff
2020-12-16 Andrew ReynoldsUse uint64 utility when parsing tuple selectors in... tree | commitdiff
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680) tree | commitdiff
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678) tree | commitdiff
2020-12-15 Andrew ReynoldsProper expand definitions for sets (#5676) tree | commitdiff
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... tree | commitdiff
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671) tree | commitdiff
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) tree | commitdiff
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667) tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... tree | commitdiff
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655) tree | commitdiff
2020-12-14 Andrew ReynoldsFix and improve evaluator (#5563) tree | commitdiff
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... tree | commitdiff
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ... tree | commitdiff
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast... tree | commitdiff
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) 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 NiemetzFix compiler warnings. (#5644) tree | commitdiff
2020-12-09 Andrew Reynolds(proof-new) Make theory preprocessor proofs self contai... 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-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622) tree | commitdiff
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... tree | commitdiff
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627) tree | commitdiff
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... tree | commitdiff
2020-12-09 yoni206update doc (#5619) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... tree | commitdiff
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... tree | commitdiff
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... tree | commitdiff
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... 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-08 Mathias PreinerDisable algebraic BV subtheory by default and make... tree | commitdiff
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... tree | commitdiff
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... 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-05 Everett MausChange generated options to be thread_local. (#5583) tree | commitdiff
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) tree | commitdiff
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) tree | commitdiff
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... tree | commitdiff
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... tree | commitdiff
2020-12-03 yoni206Models as (#5581) 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 Aina NiemetzFix RoundingMode mapping in API. (#5578) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) tree | commitdiff
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530) tree | commitdiff
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-12-02 Aina NiemetzRemove use of this-> in FP literal. (#5565) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... tree | commitdiff
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) tree | commitdiff
next