projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Simplify parser (#8592)
[cvc5.git] / src / parser / smt2 / Smt2.g
2022-04-08 Andres NoetzliSimplify parser (#8592) blob | commitdiff | raw
2022-04-08 Andrew ReynoldsDo not allow unresolved sorts in smt2 (#8587) blob | commitdiff | raw | diff to current
2022-04-08 Andrew ReynoldsProperly parse numerals as real when integers are disab... blob | commitdiff | raw | diff to current
2022-04-05 Mathias PreinerUpdate copyright headers for release 1.0 (#8539) blob | commitdiff | raw | diff to current
2022-04-04 Andrew ReynoldsRename getInstantiatedConstructorTerm to getInstantiate... blob | commitdiff | raw | diff to current
2022-04-01 Andres Noetzli[API] Add mode argument for `Solver::blockModel()`... blob | commitdiff | raw | diff to current
2022-04-01 Mathias Preinerapi: Swap arguments of declareSygusVar. (#8499) blob | commitdiff | raw | diff to current
2022-03-31 Andrew ReynoldsHandled quoted symbols in indexed operators (#8491) blob | commitdiff | raw | diff to current
2022-03-31 Aina NiemetzSort, TypeNode: Rename functions related to datatypes... blob | commitdiff | raw | diff to current
2022-03-30 Andrew ReynoldsChange tuple tokens and update datatypes theory ref... blob | commitdiff | raw | diff to current
2022-03-29 Mathias PreinerIntroduce internal namespace and remove api namespace... blob | commitdiff | raw | diff to current
2022-03-29 Andrew ReynoldsMake ensureTermSort private (#8436) blob | commitdiff | raw | diff to current
2022-03-28 Mathias PreinerRename get-interpol to get-interpolant. (#8424) blob | commitdiff | raw | diff to current
2022-03-25 Mathias Preinerapi: Unify mkOp variants. (#8369) blob | commitdiff | raw | diff to current
2022-03-25 Andres Noetzli[Parser] Fix resolution of indexed symbols (#8383) blob | commitdiff | raw | diff to current
2022-03-25 Aina Niemetzapi: Rename kind NULL_EXPR to NULL_TERM. (#8402) blob | commitdiff | raw | diff to current
2022-03-25 Andrew ReynoldsProperly guard commands in the SyGuS API (#8390) blob | commitdiff | raw | diff to current
2022-03-24 Andrew ReynoldsFix a couple of parse error messages for sygus (#8381) blob | commitdiff | raw | diff to current
2022-03-22 Andres Noetzli[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334) blob | commitdiff | raw | diff to current
2022-03-22 Mathias Preinerapi: Unify mkTerm variants. (#8357) blob | commitdiff | raw | diff to current
2022-03-17 Gereon KremerReplace `Debug` by `Trace` (#7793) blob | commitdiff | raw | diff to current
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099) blob | commitdiff | raw | diff to current
2022-03-02 Andrew ReynoldsEliminate CDHashMap::insertAtContextLevelZero (#8173) blob | commitdiff | raw | diff to current
2022-02-28 Andrew ReynoldsTrack names for witness terms in model (#8184) blob | commitdiff | raw | diff to current
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) blob | commitdiff | raw | diff to current
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) blob | commitdiff | raw | diff to current
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... blob | commitdiff | raw | diff to current
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... blob | commitdiff | raw | diff to current
2021-12-10 Abdalrhman MohamedMute `define-fun` command generated for named terms... blob | commitdiff | raw | diff to current
2021-12-07 Andrew ReynoldsAllow sygus in incremental mode (#7756) blob | commitdiff | raw | diff to current
2021-12-01 Andrew ReynoldsRemove spurious assertion in parser (#7713) blob | commitdiff | raw | diff to current
2021-12-01 Andrew ReynoldsDefine sort undeclared (#7714) blob | commitdiff | raw | diff to current
2021-11-22 Gereon KremerRefactor IO stream manipulators (#7555) blob | commitdiff | raw | diff to current
2021-11-15 Aina Niemetzapi: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) blob | commitdiff | raw | diff to current
2021-11-09 Gereon KremerRemove antlr_tracing.h (#7608) blob | commitdiff | raw | diff to current
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... blob | commitdiff | raw | diff to current
2021-11-02 Andrew ReynoldsImprove syntax for fmf cardinality constraints (#7556) blob | commitdiff | raw | diff to current
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... blob | commitdiff | raw | diff to current
2021-10-28 Abdalrhman MohamedFix `(set-info <sexpr>)` parsing and printing bugs... blob | commitdiff | raw | diff to current
2021-10-20 Andrew ReynoldsCorrectly parse uninterpreted constant values in get... blob | commitdiff | raw | diff to current
2021-10-20 Abdalrhman MohamedAvoid escaping `double-quotes` twice. (#7409) blob | commitdiff | raw | diff to current
2021-10-14 Andrew ReynoldsImprove parser for tuple select (#7364) blob | commitdiff | raw | diff to current
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) blob | commitdiff | raw | diff to current
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... blob | commitdiff | raw | diff to current
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... blob | commitdiff | raw | diff to current
2021-09-29 Andrew ReynoldsUpdate the syntax for tuples in smt2 (#7265) blob | commitdiff | raw | diff to current
2021-09-22 Andrew ReynoldsMinimal fixing version for tuple update parsing (#7228) blob | commitdiff | raw | diff to current
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) blob | commitdiff | raw | diff to current
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081) blob | commitdiff | raw | diff to current
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998) blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... blob | commitdiff | raw | diff to current
2021-08-03 Andrew ReynoldsRemove "inUnsatCore" flag throughout (#6964) blob | commitdiff | raw | diff to current
2021-05-20 Gereon KremerAdd more getters for api::Term (#6496) blob | commitdiff | raw | diff to current
2021-05-19 Andres NoetzliImprove handling of `:named` attributes (#6549) blob | commitdiff | raw | diff to current
2021-05-08 Andrew ReynoldsAdd support for datatype update (#6449) blob | commitdiff | raw | diff to current
2021-04-20 Andrew ReynoldsAdd instantiation pool feature to the API (#6358) blob | commitdiff | raw | diff to current
2021-04-19 Gereon KremerRemove linking against gmp and cln in tests and parser... blob | commitdiff | raw | diff to current
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsInitial support for parametric datatypes in sygus ... blob | commitdiff | raw | diff to current
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) blob | commitdiff | raw | diff to current
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) blob | commitdiff | raw | diff to current
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) blob | commitdiff | raw | diff to current
2020-11-30 Abdalrhman MohamedEliminate uses of SExpr from the parser. (#5496) blob | commitdiff | raw | diff to current
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) blob | commitdiff | raw | diff to current
2020-11-16 Andrew ReynoldsCleaning up scopes in preparation for symbol manager... blob | commitdiff | raw | diff to current
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434) blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... blob | commitdiff | raw | diff to current
2020-11-02 Andrew ReynoldsMiscellaneous cleaning of parser (#5369) blob | commitdiff | raw | diff to current
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) blob | commitdiff | raw | diff to current
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... blob | commitdiff | raw | diff to current
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) blob | commitdiff | raw | diff to current
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-10 Andrew ReynoldsParser error for wrong number of datatypes (#5049) blob | commitdiff | raw | diff to current
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... blob | commitdiff | raw | diff to current
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739) blob | commitdiff | raw | diff to current
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula... blob | commitdiff | raw | diff to current
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) blob | commitdiff | raw | diff to current
2020-06-30 Ying ShengInterpolation step 1 (#4638) blob | commitdiff | raw | diff to current
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) blob | commitdiff | raw | diff to current
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-06-06 Andres NoetzliKeep definitions when global-declarations enabled ... blob | commitdiff | raw | diff to current
2020-06-06 Andrew ReynoldsSmt2 parsing support for nested recursive datatypes... blob | commitdiff | raw | diff to current
2020-06-05 makaimannAdd a method for retrieving base of a constant array... blob | commitdiff | raw | diff to current
2020-06-04 Aina NiemetzNew C++ Api: First batch of API guards. (#4557) blob | commitdiff | raw | diff to current
2020-06-03 Andrew ReynoldsDo not apply unconstrained simplification when quantifi... blob | commitdiff | raw | diff to current
2020-06-02 Aina NiemetzNew C++ API: Keep reference to solver object in non... blob | commitdiff | raw | diff to current
2020-06-01 Andres NoetzliDo not parse ->/lambda unless --uf-ho enabled (#4544) blob | commitdiff | raw | diff to current
next