summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
2020-11-18Add -> operator overload for cd* iterators. (#5464)Mathias Preiner
2020-11-18Disable slow nl regression (#5467)Andrew Reynolds
2020-11-18Add let binding utility (#5444)Andrew Reynolds
2020-11-18Minor cleanup of SmtEngine (#5450)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
2020-11-18Fix asan issues related to solver and symbol manager (#5457)Andrew Reynolds
2020-11-17FloatingPoint: Use uint32_t instead of unsigned. (#5459)Aina Niemetz
2020-11-17FloatingPoint: Clean up and document header, format. (#5453)Aina Niemetz
2020-11-17ci: Simplify Python dependency installs for Linux and macOS. (#5458)Mathias Preiner
2020-11-17Fix tangent plane lemmas (#5455)Gereon Kremer
2020-11-16Refactor tangent plane lemmas (#5449)Gereon Kremer
2020-11-16Cleaning up scopes in preparation for symbol manager (#5442)Andrew Reynolds
2020-11-16Improve accuracy of resource limitation (#4763)Gereon Kremer
2020-11-14Fix double conflict in extended string solver (#5435)Andrew Reynolds
2020-11-14(proof-new) Proofs for non-clausal simplification (#5409)Andrew Reynolds
2020-11-13(proof-new) Enable proofs for datatypes (#5436)Andrew Reynolds
2020-11-13Model declarations printing options (#5432)yoni206
2020-11-13Add more features to symbol manager (#5434)Andrew Reynolds
2020-11-12Make regular expression difference left associative (#5430)Andrew Reynolds
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
2020-11-12Fix printing of define named function (#5425)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback