projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add getters to retrieve constants from api::Term (#5677)
[cvc5.git] / src /
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667) tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... tree | commitdiff
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655) 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-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ... tree | commitdiff
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast... 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 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) tree | commitdiff
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641) 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-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... tree | commitdiff
2020-12-09 yoni206update doc (#5619) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... 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-08 Mathias PreinerDisable algebraic BV subtheory by default and make... 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-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601) tree | commitdiff
2020-12-05 Everett MausChange generated options to be thread_local. (#5583) tree | commitdiff
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) tree | commitdiff
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) tree | commitdiff
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... tree | commitdiff
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... tree | commitdiff
2020-12-03 yoni206Models as (#5581) tree | commitdiff
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) tree | commitdiff
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530) tree | commitdiff
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-12-02 Aina NiemetzRemove use of this-> in FP literal. (#5565) tree | commitdiff
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... tree | commitdiff
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) 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 ReynoldsUse new let binding in AST printer (#5529) tree | commitdiff
2020-11-30 Aina Niemetzfloatingpoint: Use unique_ptr for FloatingPointLiteral... tree | commitdiff
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) 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 ReynoldsRemoving infrastructure related to SMT model (#5527) tree | commitdiff
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) 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 Andrew ReynoldsUse symbol manager for printing responses get-model... tree | commitdiff
2020-11-25 Andrew ReynoldsAllow printing of null node in let binder (#5523) 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 Reynolds(proof-new) Miscellaneous changes from proof-new (... tree | commitdiff
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... tree | commitdiff
2020-11-23 Gereon KremerAdd get-info :time. (#5485) 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-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500) 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 Andrew ReynoldsUpdates to API in preparation for using symbol manager... tree | commitdiff
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) tree | commitdiff
2020-11-20 Andrew ReynoldsFix use of declaration sequence command in cvc parser... 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 Niemetzfloatingpoint.h: Split in preparation to cleanly separa... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
next