projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Modify the smt2 parser to use the Sygus grammar. (#4829)
[cvc5.git] / src / parser /
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... tree | commitdiff
2020-08-04 Andrew ReynoldsAdd API interface for specialized constructor term... tree | commitdiff
2020-08-03 Andrew ReynoldsUpdate datatypes in cvc parser to the new API (#4826) 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 Andrew ReynoldsDebug instantiations output (#4739) tree | commitdiff
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula... tree | commitdiff
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) tree | commitdiff
2020-07-10 Andrew ReynoldsFront end support for integer AND (#4717) tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) tree | commitdiff
2020-06-30 Ying ShengInterpolation step 1 (#4638) tree | commitdiff
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) tree | commitdiff
2020-06-23 Mathias PreinerAdd support for eqrange predicate (#4562) tree | commitdiff
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... tree | commitdiff
2020-06-06 Andres NoetzliKeep definitions when global-declarations enabled ... tree | commitdiff
2020-06-06 Andrew ReynoldsSmt2 parsing support for nested recursive datatypes... tree | commitdiff
2020-06-05 makaimannAdd a method for retrieving base of a constant array... tree | commitdiff
2020-06-04 Aina NiemetzNew C++ Api: First batch of API guards. (#4557) tree | commitdiff
2020-06-03 Andrew ReynoldsDo not apply unconstrained simplification when quantifi... tree | commitdiff
2020-06-02 Aina NiemetzNew C++ API: Keep reference to solver object in non... tree | commitdiff
2020-06-01 Andres NoetzliDo not parse ->/lambda unless --uf-ho enabled (#4544) tree | commitdiff
2020-05-22 Andrew ReynoldsUpdate string kind names in new API (#4509) tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-05-19 Andrew ReynoldsUpdate enum and option names for sygus languages (... tree | commitdiff
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... tree | commitdiff
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... tree | commitdiff
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) tree | commitdiff
2020-04-04 Aina NiemetzNew C++ API: Remove Op::getSort(). (#4208) tree | commitdiff
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) tree | commitdiff
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) tree | commitdiff
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) tree | commitdiff
2020-03-30 Andrew ReynoldsFix arguments to print callback (#4171) tree | commitdiff
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) tree | commitdiff
2020-03-28 Abdalrhman MohamedChange is-cons to (_ is cons) in Sygus benchmarks.... tree | commitdiff
2020-03-28 Abdalrhman MohamedStop printing datatype declaration for Sygus V1 grammar... tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
2020-03-22 Abdalrhman MohamedConvert V1 Sygus files to V2. (#4136) tree | commitdiff
2020-03-20 Andrew ReynoldsParse error for SyGuS version 1.0 vs 2.0 (#4057) tree | commitdiff
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... tree | commitdiff
2020-03-12 Andrew ReynoldsConvert most instances of dataypes in parsers to the... tree | commitdiff
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... tree | commitdiff
2020-03-09 Andrew ReynoldsClean up more uses of ExprManager in parsers (#3932) tree | commitdiff
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) tree | commitdiff
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) tree | commitdiff
2020-03-06 Andrew ReynoldsMake sygus datatype building independent of parser... tree | commitdiff
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
2020-02-27 Andrew ReynoldsRefactor operator applications in the parser (#3831) tree | commitdiff
2020-02-27 Haniel BarbosaChanging TPTP parser to accomodate new API (#3837) tree | commitdiff
2020-02-27 Andrew ReynoldsUpdate purifySygusGTerm to the new API (#3830) tree | commitdiff
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... tree | commitdiff
2020-02-27 Andrew ReynoldsMove fix for vacuous sygus types out of the parser... tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) tree | commitdiff
2020-02-26 Andrew ReynoldsRefactor type ascriptions in the parser (#3825) tree | commitdiff
2020-02-26 Andrew ReynoldsMinor improvement to ParseOp (#3808) tree | commitdiff
2020-02-26 Andrew ReynoldsMinor cleaning of smt2 parser (#3823) tree | commitdiff
2020-02-26 Andrew ReynoldsEmbed mkAssociative utilities within the API. (#3801) tree | commitdiff
2020-02-24 Andrew ReynoldsConvert parser input interface to api::Term (#3809) tree | commitdiff
2020-02-24 Abdalrhman MohamedFix bugs related to printing Sygus commands (#3804) tree | commitdiff
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-20 Andres NoetzliRemove parser from bindings (#3779) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-17 Haniel BarbosaUsing ParseOp in TPTP (#3764) tree | commitdiff
2020-02-17 Abdalrhman MohamedSupport dumping Sygus commands. (#3763) tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) tree | commitdiff
2020-01-07 Andrew ReynoldsFix unary minus parse check (#3594) tree | commitdiff
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) tree | commitdiff
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... tree | commitdiff
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) tree | commitdiff
2019-12-10 Haniel BarbosaFix ufho issues (#3551) tree | commitdiff
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) tree | commitdiff
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... tree | commitdiff
2019-11-30 Haniel Barbosaimproving parsing error messages related to HOL (#3510) tree | commitdiff
2019-11-29 Andrew ReynoldsCheck free variables in assertions when using SyGuS... tree | commitdiff
2019-11-25 Andrew ReynoldsBetter front-end type checking for SyGuS (#3496) tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-15 Andrew ReynoldsFix wrong kind in sygus version 1 parser (#3463) tree | commitdiff
2019-11-13 Andres NoetzliAllow (set-logic ...) after (reset) (#3457) tree | commitdiff
2019-11-04 Andrew ReynoldsAvoid non-well-founded sygus grammars (#3434) tree | commitdiff
2019-10-27 Andres NoetzliFix global-declarations support (#3403) tree | commitdiff
2019-10-11 Andrew ReynoldsCheck that logic is set when synth-fun command is encou... tree | commitdiff
2019-10-11 Aina NiemetzMake order of theories explicit in the source code... tree | commitdiff
2019-10-09 Andres NoetzliAvoid printing success for `--force-logic` (#3363) tree | commitdiff
2019-10-08 Andres Noetzli[CVC Parser] Add support for regular expressions (... tree | commitdiff
2019-10-08 Andres Noetzli[SMT2 Parser] Move code of `rewriterulesCommand` (... tree | commitdiff
2019-10-03 Andres Noetzli[SMT2 Parser] Move code of `sygusCommand` (#3335) tree | commitdiff
2019-09-30 Andrew ReynoldsAvoid cases of empty sygus grammars (#3301) tree | commitdiff
2019-09-28 Andrew ReynoldsSupport smt2 language "match" term (#3258) tree | commitdiff
2019-09-25 Andrew ReynoldsAdd isParameterized function to Expr (#3303) tree | commitdiff
2019-09-25 Mathias PreinerUse separate CMake project for CVC4 examples. (#3196) tree | commitdiff
2019-09-16 Aina Niemetzparser: Improve error message for unrecognized input... tree | commitdiff
2019-09-13 Andrew ReynoldsDisallow let in sygus grammars, check for free variable... tree | commitdiff
2019-09-06 Mathias PreinerRemove parsing/printing of meta-info command. (#3260) tree | commitdiff
next