projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
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 Mohamed
Modify the smt2 parser to use the Sygus grammar. (...
tree
|
commitdiff
2020-08-04
Andrew Reynolds
Add API interface for specialized constructor term...
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Update datatypes in cvc parser to the new API (#4826)
tree
|
commitdiff
2020-07-28
yoni206
Supporting seq.nth (#4723)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
tree
|
commitdiff
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
tree
|
commitdiff
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
tree
|
commitdiff
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
tree
|
commitdiff
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-19
Andres Noetzli
Add logic check for define-fun(s)-rec (#4577)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-06
Andres Noetzli
Keep definitions when global-declarations enabled ...
tree
|
commitdiff
2020-06-06
Andrew Reynolds
Smt2 parsing support for nested recursive datatypes...
tree
|
commitdiff
2020-06-05
makaimann
Add a method for retrieving base of a constant array...
tree
|
commitdiff
2020-06-04
Aina Niemetz
New C++ Api: First batch of API guards. (#4557)
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifi...
tree
|
commitdiff
2020-06-02
Aina Niemetz
New C++ API: Keep reference to solver object in non...
tree
|
commitdiff
2020-06-01
Andres Noetzli
Do not parse ->/lambda unless --uf-ho enabled (#4544)
tree
|
commitdiff
2020-05-22
Andrew Reynolds
Update string kind names in new API (#4509)
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-05-19
Andrew Reynolds
Update enum and option names for sygus languages (...
tree
|
commitdiff
2020-04-28
Andrew Reynolds
Support the SMT-LIB Unicode string standard by default...
tree
|
commitdiff
2020-04-13
Andrew Reynolds
Fix SyGuS define-fun printing from benchmarks coming...
tree
|
commitdiff
2020-04-08
mudathirmahgoub
Added CHOOSE operator for sets (#4211)
tree
|
commitdiff
2020-04-04
Aina Niemetz
New C++ API: Remove Op::getSort(). (#4208)
tree
|
commitdiff
2020-04-01
Andrew Reynolds
Support char smt-lib syntax (#4188)
tree
|
commitdiff
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
tree
|
commitdiff
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
tree
|
commitdiff
2020-03-30
Andrew Reynolds
Fix arguments to print callback (#4171)
tree
|
commitdiff
2020-03-30
mudathirmahgoub
Frontend support for the choice operator (#4175)
tree
|
commitdiff
2020-03-28
Abdalrhman Mohamed
Change is-cons to (_ is cons) in Sygus benchmarks....
tree
|
commitdiff
2020-03-28
Abdalrhman Mohamed
Stop printing datatype declaration for Sygus V1 grammar...
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-22
Abdalrhman Mohamed
Convert V1 Sygus files to V2. (#4136)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Parse error for SyGuS version 1.0 vs 2.0 (#4057)
tree
|
commitdiff
2020-03-19
Andres Noetzli
Only allow bv2nat/int2bv with BV and integer logic...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Convert most instances of dataypes in parsers to the...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix non-parametrized operators in subgoal generation...
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Clean up more uses of ExprManager in parsers (#3932)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Simplify DatatypeDeclarationCommand command (#3928)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Remove tester name from APIs (#3929)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Make sygus datatype building independent of parser...
tree
|
commitdiff
2020-03-05
Andrew Reynolds
Migrate a majority of the functionality in parsers...
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Refactor operator applications in the parser (#3831)
tree
|
commitdiff
2020-02-27
Haniel Barbosa
Changing TPTP parser to accomodate new API (#3837)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Update purifySygusGTerm to the new API (#3830)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression differe...
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Move fix for vacuous sygus types out of the parser...
tree
|
commitdiff
2020-02-26
Andrew Reynolds
More fixes for printing sygus commands (#3812)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Refactor type ascriptions in the parser (#3825)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Minor improvement to ParseOp (#3808)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Minor cleaning of smt2 parser (#3823)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Embed mkAssociative utilities within the API. (#3801)
tree
|
commitdiff
2020-02-24
Andrew Reynolds
Convert parser input interface to api::Term (#3809)
tree
|
commitdiff
2020-02-24
Abdalrhman Mohamed
Fix bugs related to printing Sygus commands (#3804)
tree
|
commitdiff
2020-02-21
Andrew Reynolds
Simple changes towards unicode string standard (#3791)
tree
|
commitdiff
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
tree
|
commitdiff
2020-02-20
Andres Noetzli
Remove parser from bindings (#3779)
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-02-17
Haniel Barbosa
Using ParseOp in TPTP (#3764)
tree
|
commitdiff
2020-02-17
Abdalrhman Mohamed
Support dumping Sygus commands. (#3763)
tree
|
commitdiff
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
tree
|
commitdiff
2020-02-14
Andrew Reynolds
Update sygus v1 parser to use ParseOp utility (#3756)
tree
|
commitdiff
2020-01-07
Andrew Reynolds
Fix unary minus parse check (#3594)
tree
|
commitdiff
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
tree
|
commitdiff
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array consta...
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
tree
|
commitdiff
2019-12-10
Haniel Barbosa
Fix ufho issues (#3551)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
tree
|
commitdiff
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
tree
|
commitdiff
2019-11-30
Haniel Barbosa
improving parsing error messages related to HOL (#3510)
tree
|
commitdiff
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
tree
|
commitdiff
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-15
Andrew Reynolds
Fix wrong kind in sygus version 1 parser (#3463)
tree
|
commitdiff
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
tree
|
commitdiff
2019-10-27
Andres Noetzli
Fix global-declarations support (#3403)
tree
|
commitdiff
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
tree
|
commitdiff
2019-10-11
Aina Niemetz
Make order of theories explicit in the source code...
tree
|
commitdiff
2019-10-09
Andres Noetzli
Avoid 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 Reynolds
Avoid cases of empty sygus grammars (#3301)
tree
|
commitdiff
2019-09-28
Andrew Reynolds
Support smt2 language "match" term (#3258)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Add isParameterized function to Expr (#3303)
tree
|
commitdiff
2019-09-25
Mathias Preiner
Use separate CMake project for CVC4 examples. (#3196)
tree
|
commitdiff
2019-09-16
Aina Niemetz
parser: Improve error message for unrecognized input...
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove parsing/printing of meta-info command. (#3260)
tree
|
commitdiff
next