projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add tuple projection operator (#5904)
[cvc5.git] / src / parser / smt2 / smt2.cpp
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) blob | commitdiff | raw
2021-02-08 Andrew ReynoldsRemove support for inst closure (#5874) blob | commitdiff | raw | diff to current
2021-01-21 Andrew ReynoldsAdd div, mod, abs in non-strict parsing mode (#5793) blob | commitdiff | raw | diff to current
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear... blob | commitdiff | raw | diff to current
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) blob | commitdiff | raw | diff to current
2020-12-16 Andrew ReynoldsUse uint64 utility when parsing tuple selectors in... 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-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-09 Andrew ReynoldsAdd symbol manager (#5380) blob | commitdiff | raw | diff to current
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) 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-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336) blob | commitdiff | raw | diff to current
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... blob | commitdiff | raw | diff to current
2020-10-07 Aina NiemetzNew C++ API: Rename Term::isConst() to Term::isValue... blob | commitdiff | raw | diff to current
2020-10-06 mudathirmahgoubAdd operators bag.from_set, bag.to_set to the theory... blob | commitdiff | raw | diff to current
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) 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-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) blob | commitdiff | raw | diff to current
2020-09-02 Andres Noetzli[API] Fix Python Examples (#4943) 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-28 yoni206Supporting seq.nth (#4723) blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) blob | commitdiff | raw | diff to current
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) blob | commitdiff | raw | diff to current
2020-07-10 Andrew ReynoldsFront end support for integer AND (#4717) blob | commitdiff | raw | diff to current
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... blob | commitdiff | raw | diff to current
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) blob | commitdiff | raw | diff to current
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) blob | commitdiff | raw | diff to current
2020-06-23 Mathias PreinerAdd support for eqrange predicate (#4562) blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... 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-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
2020-05-22 Andrew ReynoldsUpdate string kind names in new API (#4509) blob | commitdiff | raw | diff to current
2020-05-19 Andrew ReynoldsUpdate enum and option names for sygus languages (... blob | commitdiff | raw | diff to current
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... blob | commitdiff | raw | diff to current
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... blob | commitdiff | raw | diff to current
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) blob | commitdiff | raw | diff to current
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) blob | commitdiff | raw | diff to current
2020-03-30 Andrew ReynoldsFix arguments to print callback (#4171) blob | commitdiff | raw | diff to current
2020-03-28 Abdalrhman MohamedChange is-cons to (_ is cons) in Sygus benchmarks.... blob | commitdiff | raw | diff to current
2020-03-22 Abdalrhman MohamedConvert V1 Sygus files to V2. (#4136) blob | commitdiff | raw | diff to current
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsConvert most instances of dataypes in parsers to the... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... blob | commitdiff | raw | diff to current
2020-03-09 Andrew ReynoldsClean up more uses of ExprManager in parsers (#3932) blob | commitdiff | raw | diff to current
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) blob | commitdiff | raw | diff to current
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... blob | commitdiff | raw | diff to current
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) blob | commitdiff | raw | diff to current
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsRefactor operator applications in the parser (#3831) blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsUpdate purifySygusGTerm to the new API (#3830) blob | commitdiff | raw | diff to current
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsRefactor type ascriptions in the parser (#3825) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsMinor cleaning of smt2 parser (#3823) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsEmbed mkAssociative utilities within the API. (#3801) blob | commitdiff | raw | diff to current
2020-02-24 Abdalrhman MohamedFix bugs related to printing Sygus commands (#3804) blob | commitdiff | raw | diff to current
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) blob | commitdiff | raw | diff to current
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) blob | commitdiff | raw | diff to current
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) blob | commitdiff | raw | diff to current
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) blob | commitdiff | raw | diff to current
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... blob | commitdiff | raw | diff to current
2019-12-10 Haniel BarbosaFix ufho issues (#3551) blob | commitdiff | raw | diff to current
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) blob | commitdiff | raw | diff to current
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... blob | commitdiff | raw | diff to current
2019-11-25 Andrew ReynoldsBetter front-end type checking for SyGuS (#3496) blob | commitdiff | raw | diff to current
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) blob | commitdiff | raw | diff to current
2019-11-15 Andrew ReynoldsFix wrong kind in sygus version 1 parser (#3463) blob | commitdiff | raw | diff to current
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) blob | commitdiff | raw | diff to current
2019-10-11 Andrew ReynoldsCheck that logic is set when synth-fun command is encou... blob | commitdiff | raw | diff to current
2019-10-11 Aina NiemetzMake order of theories explicit in the source code... blob | commitdiff | raw | diff to current
2019-10-09 Andres NoetzliAvoid printing success for `--force-logic` (#3363) blob | commitdiff | raw | diff to current
2019-10-08 Andres Noetzli[SMT2 Parser] Move code of `rewriterulesCommand` (... blob | commitdiff | raw | diff to current
2019-10-03 Andres Noetzli[SMT2 Parser] Move code of `sygusCommand` (#3335) blob | commitdiff | raw | diff to current
2019-09-25 Andrew ReynoldsAdd isParameterized function to Expr (#3303) blob | commitdiff | raw | diff to current
2019-09-13 Andrew ReynoldsDisallow let in sygus grammars, check for free variable... blob | commitdiff | raw | diff to current
2019-09-06 Mathias PreinerRemove SMT1 parser. (#3228) blob | commitdiff | raw | diff to current
2019-08-17 Andrew ReynoldsMark symbols introduced by named attributes as defined... blob | commitdiff | raw | diff to current
2019-08-13 Andrew ReynoldsIntroduce smt2 parsing utility ParseOp and refactor... blob | commitdiff | raw | diff to current
2019-08-12 Andrew ReynoldsClean smt2 parsing of named attributes (#3172) blob | commitdiff | raw | diff to current
2019-08-10 Andrew ReynoldsSimplify how defined functions are tracked during parsi... blob | commitdiff | raw | diff to current
2019-08-06 Andrew ReynoldsProperly parse qualified identifiers (#3111) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) blob | commitdiff | raw | diff to current
2019-07-23 Andrew ReynoldsFix sygus datatype parsing in sygus v1 format (#3113) blob | commitdiff | raw | diff to current
2019-07-16 Andrew ReynoldsAdd support for str.tolower and str.toupper (#3092) blob | commitdiff | raw | diff to current
2019-07-01 Andrew ReynoldsSupport sygus version 2 format (#3066) blob | commitdiff | raw | diff to current
2019-06-21 Andres NoetzliFix and simplify handling of --force-logic (#3062) blob | commitdiff | raw | diff to current
2019-06-12 Andres NoetzliRefactor parser to define fewer tokens for symbols... blob | commitdiff | raw | diff to current
2019-05-06 Andres NoetzliAdd support for re.all (#2980) blob | commitdiff | raw | diff to current
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) blob | commitdiff | raw | diff to current
next