summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2020-12-08Make term indices in the strings base solver aware of types (#5589)Andrew Reynolds
2020-12-08Proper implementation of expand definitions for sequences (#5616)Andrew Reynolds
2020-12-07Fix collect model values for sequences of sequences (#5579)Andrew Reynolds
2020-12-07[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)Haniel Barbosa
2020-12-07Add support for BV proofs with the simple bitblasting solver. (#5603)Mathias Preiner
2020-12-07Fix and reenable fact vs lemma optimization in datatypes (#5614)Andrew Reynolds
2020-12-07Add bitwise refinement mode for IAND (#5328)makaimann
2020-12-07Fix issue with free variables introduced by quantifier rewriter (#5602)Andrew Reynolds
2020-12-07Refactor initial phase of transcendental solver (#5599)Gereon Kremer
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-07 (proof-new) Split proof ensure closed checks to own file (#5522)Andrew Reynolds
2020-12-03Use mkAnd where the number of children may be less than two. (#5551)Gereon Kremer
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-12-01Remove assertion related to CEGQI dependency lemmas (#5559)Andrew Reynolds
2020-12-01Improve rewriting of str.<= (#4848)Andres Noetzli
2020-12-01Refactor transcendental solver (#5539)Gereon Kremer
2020-11-30More fixes for quantifier elimination (#5533)Andrew Reynolds
2020-11-30fp_converter: Properly separate out symbolic glue code. (#5501)Aina Niemetz
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
2020-11-30(proof-new) Proofs for regular expression elimination (#5361)Andrew Reynolds
2020-11-26Make CAD solver work for empty set of assertions (#5535)Gereon Kremer
2020-11-25Fully decouple SmtEngine and the Expr layer (#5532)Andrew Reynolds
2020-11-25Fix missed case of theory preprocessing (#5531)Andrew Reynolds
2020-11-25Disable fact vs lemma optimization in datatypes for now (#5521)Andrew Reynolds
2020-11-25Fix transcendental secant plane lemmas (#5525)Gereon Kremer
2020-11-24Refactor transcendental solver (#5514)Gereon Kremer
2020-11-23Fix regular expression consume for nested star (#5518)Andrew Reynolds
2020-11-23Change UF ho to ppRewrite instead of expand definition (#5499)Andrew Reynolds
2020-11-23Fix for sygusToBuiltinEval for non-ground composite terms (#5466)Andrew Reynolds
2020-11-22Fix quantifiers scope issue in strings preprocessor (#5491)Andrew Reynolds
2020-11-20Add posRewriteEqual to bags rewriter (#5498)mudathirmahgoub
2020-11-20Rename symfpu_literal.(h.in|cpp) -> floatingpoint_literal_symfpu.(h.in|cpp). ...Aina Niemetz
2020-11-20Fix remove term formula policy for terms beneath quantifiers (#5497)Andrew Reynolds
2020-11-20RoundingMode: Rename enum values to conform to code style guidelines. (#5494)Aina Niemetz
2020-11-20FloatingPoint: Separate out symFPU glue code. (#5492)Aina Niemetz
2020-11-20Fix #5493. (#5495)Aina Niemetz
2020-11-20Support nested quantifier elimination for get-qe command (#5490)Andrew Reynolds
2020-11-20Fix compiler warnings. (#5493)Aina Niemetz
2020-11-20(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)Gereon Kremer
2020-11-20Allow to pass ProofGenerator to arithmetic inference manager. (#5488)Gereon Kremer
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-11-19Add nested quantifier elimination module (#5422)Andrew Reynolds
2020-11-19Fix issues related to eliminating extended arithmetic operators (#5475)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-17FloatingPoint: Clean up and document header, format. (#5453)Aina Niemetz
2020-11-17Fix tangent plane lemmas (#5455)Gereon Kremer
2020-11-16Refactor tangent plane lemmas (#5449)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback