projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-12-02 Aina NiemetzRemove use of this-> in FP literal. (#5565) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: Infrastructure and first api test. (#5548) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) commit | commitdiff | tree
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) commit | commitdiff | tree
2020-12-01 Gereon KremerRefactor transcendental solver (#5539) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regressions from #5099 (#5557) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regression for #4335. (#5554) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555) commit | commitdiff | tree
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) commit | commitdiff | tree
2020-12-01 yoni206fix metadata for a test (#5546) commit | commitdiff | tree
2020-11-30 Aina Niemetzfp_converter: Properly separate out symbolic glue code... commit | commitdiff | tree
2020-11-30 Andrew ReynoldsUse new let binding in AST printer (#5529) commit | commitdiff | tree
2020-11-30 Aina Niemetzfloatingpoint: Use unique_ptr for FloatingPointLiteral... commit | commitdiff | tree
2020-11-30 Abdalrhman... Eliminate uses of SExpr from the parser. (#5496) commit | commitdiff | tree
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) commit | commitdiff | tree
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... commit | commitdiff | tree
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... commit | commitdiff | tree
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsFix missed case of theory preprocessing (#5531) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for... commit | commitdiff | tree
2020-11-25 Andrew ReynoldsAdd regressions for closed issues (#5526) commit | commitdiff | tree
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525) commit | commitdiff | tree
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... commit | commitdiff | tree
2020-11-25 Andrew ReynoldsAllow printing of null node in let binder (#5523) commit | commitdiff | tree
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite... commit | commitdiff | tree
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (... commit | commitdiff | tree
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... commit | commitdiff | tree
2020-11-23 Gereon KremerAdd get-info :time. (#5485) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... commit | commitdiff | tree
2020-11-21 mudathirmahgoubAdd posRewriteEqual to bags rewriter (#5498) commit | commitdiff | tree
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... commit | commitdiff | tree
2020-11-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... commit | commitdiff | tree
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... commit | commitdiff | tree
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492) commit | commitdiff | tree
2020-11-20 Aina NiemetzFix #5493. (#5495) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... commit | commitdiff | tree
2020-11-20 Andrew ReynoldsUpdates to API in preparation for using symbol manager... commit | commitdiff | tree
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsFix use of declaration sequence command in cvc parser... commit | commitdiff | tree
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... commit | commitdiff | tree
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... commit | commitdiff | tree
2020-11-19 Aina Niemetzfloatingpoint.h: Split in preparation to cleanly separa... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) commit | commitdiff | tree
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) commit | commitdiff | tree
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) commit | commitdiff | tree
2020-11-18 Mathias PreinerAdd -> operator overload for cd* iterators. (#5464) commit | commitdiff | tree
2020-11-18 Andrew ReynoldsDisable slow nl regression (#5467) commit | commitdiff | tree
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) commit | commitdiff | tree
2020-11-18 Andrew ReynoldsMinor cleanup of SmtEngine (#5450) commit | commitdiff | tree
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... commit | commitdiff | tree
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) commit | commitdiff | tree
2020-11-18 Andrew ReynoldsFix asan issues related to solver and symbol manager... commit | commitdiff | tree
2020-11-18 Aina NiemetzFloatingPoint: Use uint32_t instead of unsigned. (... commit | commitdiff | tree
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... commit | commitdiff | tree
2020-11-18 Mathias Preinerci: Simplify Python dependency installs for Linux and... commit | commitdiff | tree
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) commit | commitdiff | tree
2020-11-16 Gereon KremerRefactor tangent plane lemmas (#5449) commit | commitdiff | tree
2020-11-16 Andrew ReynoldsCleaning up scopes in preparation for symbol manager... commit | commitdiff | tree
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) commit | commitdiff | tree
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) commit | commitdiff | tree
2020-11-14 Andrew Reynolds(proof-new) Proofs for non-clausal simplification ... commit | commitdiff | tree
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) commit | commitdiff | tree
2020-11-13 yoni206Model declarations printing options (#5432) commit | commitdiff | tree
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434) commit | commitdiff | tree
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... commit | commitdiff | tree
2020-11-12 Andrew ReynoldsSimplify sygus solver and sygus stream (#5389) commit | commitdiff | tree
2020-11-12 Andrew ReynoldsFix printing of define named function (#5425) commit | commitdiff | tree
2020-11-12 yoni206Models standard (#5415) commit | commitdiff | tree
2020-11-12 Andrew Reynolds(proof-new) Separate explanation stages in proof equali... commit | commitdiff | tree
2020-11-12 Andrew ReynoldsFix redundant refinement lemma in sygus solver (#5399) commit | commitdiff | tree
2020-11-12 Andrew Reynolds(proof-new) Proofs for skolemization (#5339) commit | commitdiff | tree
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... commit | commitdiff | tree
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic... commit | commitdiff | tree
2020-11-12 Andrew Reynolds(proof-new) Add datatypes inference to proof constructo... commit | commitdiff | tree
2020-11-12 Andrew ReynoldsMake symbol manager context dependent (#5424) commit | commitdiff | tree
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) commit | commitdiff | tree
2020-11-11 Andrew ReynoldsRewrite witness terms at prerewrite (#5419) commit | commitdiff | tree
2020-11-11 Andrew ReynoldsAdd simple substitution utility (#5397) commit | commitdiff | tree
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) commit | commitdiff | tree
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... commit | commitdiff | tree
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... commit | commitdiff | tree
2020-11-10 Alex OzdemirPin LFSC version (#5412) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398) commit | commitdiff | tree
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... commit | commitdiff | tree
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) commit | commitdiff | tree
2020-11-09 Gereon KremerProperly clear interrupt for solve() as well. (#5403) commit | commitdiff | tree
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) commit | commitdiff | tree
next