summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-12-02Remove dagification visitor (#5574)Andrew Reynolds
2020-12-02Add associative utilities to node manager (#5530)Andrew Reynolds
2020-12-02Use new let binding for cvc printer (#5561)Andrew Reynolds
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-12-01Remove use of this-> in FP literal. (#5565)Aina Niemetz
2020-12-01Remove assertion related to CEGQI dependency lemmas (#5559)Andrew Reynolds
2020-12-01Fix issues related to model declarations (#5560)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-30Use new let binding in AST printer (#5529)Andrew Reynolds
2020-11-30floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503)Aina Niemetz
2020-11-30Eliminate uses of SExpr from the parser. (#5496)Abdalrhman Mohamed
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-26Removing infrastructure related to SMT model (#5527)Andrew Reynolds
2020-11-26Move expand definitions to its own file (#5528)Andrew Reynolds
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-25Use symbol manager for printing responses get-model (#5516)Andrew Reynolds
2020-11-24Allow printing of null node in let binder (#5523)Andrew Reynolds
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-23(proof-new) Miscellaneous changes from proof-new (#5445)Andrew Reynolds
2020-11-23Add declare model symbol methods to SymbolManager and Model (#5480)Andrew Reynolds
2020-11-23Add get-info :time. (#5485)Gereon Kremer
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-20Rename floatingpoint.h.in -> floatingpoin.h. (#5500)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-20Updates to API in preparation for using symbol manager for model (#5481)Andrew Reynolds
2020-11-20Fix compiler warnings. (#5493)Aina Niemetz
2020-11-20Fix use of declaration sequence command in cvc parser (#5479)Andrew Reynolds
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-19floatingpoint.h: Split in preparation to cleanly separate symFPU glue code. (...Aina Niemetz
2020-11-19Use new let binding utility in smt2 printer (#5472)Andrew Reynolds
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback