projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[Unit Tests] Add missing include (#6990)
[cvc5.git] / src / printer /
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... tree | commitdiff
2021-08-04 Gereon KremerRefactor managed streams (#6934) tree | commitdiff
2021-07-30 Andrew ReynoldsSimplify smt2 printer (#6954) tree | commitdiff
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914) tree | commitdiff
2021-07-14 Andrew ReynoldsFix models for sequences of infinite element type ... tree | commitdiff
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827) tree | commitdiff
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) tree | commitdiff
2021-06-26 yoni206pow2 -- final changes (#6800) tree | commitdiff
2021-06-09 Andrew ReynoldsFixes related to printing tuples, define-fun commands... tree | commitdiff
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) tree | commitdiff
2021-06-02 Andrew ReynoldsFixes for printing define-fun-rec (#6673) tree | commitdiff
2021-05-27 Andres NoetzliFix `str.replace_re` and `str.replace_re_all` (#6615) tree | commitdiff
2021-05-27 Aina NiemetzFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD... tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth respons... tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-18 Andrew ReynoldsFix smt2 printing (#6558) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-08 Andrew ReynoldsAdd support for datatype update (#6449) tree | commitdiff
2021-05-07 Haniel BarbosaProperly printing INST_PATTERN_LIST by itself (#6507) tree | commitdiff
2021-04-27 Andrew ReynoldsAdd internal support for datatype update (#6450) tree | commitdiff
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) tree | commitdiff
2021-04-20 Andrew ReynoldsAdd instantiation pool feature to the API (#6358) tree | commitdiff
2021-04-20 Aina NiemetzRemove support for CVC3 language. (#6369) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-30 Andrew ReynoldsFix printing for double patterns (#6235) tree | commitdiff
2021-03-30 Andrew ReynoldsMake SEXPR simply typed (#6160) tree | commitdiff
2021-03-25 Aina NiemetzFP: Refactor FloatingPointLiteral in preparation for... tree | commitdiff
2021-03-18 Abdalrhman MohamedEliminate more uses of SExpr. (#6149) tree | commitdiff
2021-03-15 Andrew ReynoldsLetify quantifier bodies independently (#6112) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) tree | commitdiff
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-26 Andrew ReynoldsMinor improvement and fix to smt2 printer (#6009) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC... tree | commitdiff
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management... tree | commitdiff
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) tree | commitdiff
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-03 yoni206Models as (#5581) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) tree | commitdiff
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) tree | commitdiff
2020-11-30 Andrew ReynoldsUse new let binding in AST printer (#5529) 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-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-13 yoni206Model declarations printing options (#5432) tree | commitdiff
2020-11-12 yoni206Models standard (#5415) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-10-20 Abdalrhman MohamedRemove some Commands from the API. (#5268) tree | commitdiff
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277) tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-11 Andrew ReynoldsAdd witness to cvc printer. (#5057) tree | commitdiff
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) tree | commitdiff
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) tree | commitdiff
2020-09-04 Abdalrhman MohamedUse Result::Sat instead of BenchmarkStatus in printers... tree | commitdiff
2020-09-02 Abdalrhman MohamedIntroduce an internal version of Commands. (#4988) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-18 Abdalrhman MohamedRefactor functions that print commands (Part 2) (#4905) tree | commitdiff
2020-08-12 Abdalrhman MohamedRefactor functions that print commands (Part 1) (#4869) tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) tree | commitdiff
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... tree | commitdiff
2020-07-28 yoni206Supporting seq.nth (#4723) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-14 Andres NoetzliUse TypeNode/Node in ArrayStoreAll (#4728) tree | commitdiff
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) tree | commitdiff
2020-07-13 Andres NoetzliRemove ExprSequence (#4724) tree | commitdiff
next