projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add new interfaces to term formula removal and theory preprocess (#5717)
[cvc5.git] / src / theory /
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... tree | commitdiff
2021-01-05 yoni206Adding str.len to triggers (#5746) 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 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 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-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684) 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-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-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) 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-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 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-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... 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-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-03 Gereon KremerUse mkAnd where the number of children may be less... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... tree | commitdiff
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) tree | commitdiff
2020-12-01 Gereon KremerRefactor transcendental solver (#5539) tree | commitdiff
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) tree | commitdiff
2020-11-30 Aina Niemetzfp_converter: Properly separate out symbolic glue code... 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 Gereon KremerMake CAD solver work for empty set of assertions (... tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-26 Andrew ReynoldsFix missed case of theory preprocessing (#5531) tree | commitdiff
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for... tree | commitdiff
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525) tree | commitdiff
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) tree | commitdiff
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) tree | commitdiff
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... tree | commitdiff
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite... tree | commitdiff
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... tree | commitdiff
2020-11-21 mudathirmahgoubAdd posRewriteEqual to bags rewriter (#5498) tree | commitdiff
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... tree | commitdiff
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... tree | commitdiff
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... tree | commitdiff
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492) tree | commitdiff
2020-11-20 Aina NiemetzFix #5493. (#5495) tree | commitdiff
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... tree | commitdiff
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) tree | commitdiff
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... tree | commitdiff
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... 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 ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) tree | commitdiff
2020-11-16 Gereon KremerRefactor tangent plane lemmas (#5449) tree | commitdiff
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) tree | commitdiff
next