projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Fixes for SyGuS + regular expressions (#3313)
[cvc5.git]
/
src
/
2019-08-26
Andrew Reynolds
Remove unnecessary code from Cvc.g (#3213)
tree
|
commitdiff
2019-08-24
Piotr Trojanek
fix misuse of iterator with a different container ...
tree
|
commitdiff
2019-08-24
Piotr Trojanek
fix mismatch between "delete" and "new []" (#2795)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Fixes for sygus regressions (#3219)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Document transition inference utility (#3207)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Exclude redundant lemmas when tracking inst lemmas...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Fix argument in nonlinear extension. (#3216)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Minor update to term util (#3208)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Pass synthesis conjecture to sygus modules (#3212)
tree
|
commitdiff
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
tree
|
commitdiff
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
tree
|
commitdiff
2019-08-19
Aina Niemetz
New C++ API: Add checks for Solver::checkValid and...
tree
|
commitdiff
2019-08-18
Andrew Reynolds
Context-independent regular expression unfolding (...
tree
|
commitdiff
2019-08-18
Andrew Reynolds
Cleaning make bound var in smt2 parser (#3192)
tree
|
commitdiff
2019-08-17
Andrew Reynolds
Move quantifiers relevance module inside E-matching...
tree
|
commitdiff
2019-08-17
Andrew Reynolds
Mark symbols introduced by named attributes as defined...
tree
|
commitdiff
2019-08-15
Andrew Reynolds
Fix for when to apply single invocation techniques...
tree
|
commitdiff
2019-08-14
Mathias Preiner
Remove option --continued-execution. (#3189)
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Update to standard implementation of getting free...
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Call separate SMT engine for single invocation sygus...
tree
|
commitdiff
2019-08-14
Mathias Preiner
cmake: Export CVC4 library interface. (#3179)
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Minor cleaning of sygus term database (#3159)
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Fix issue related to higher-order purification in term...
tree
|
commitdiff
2019-08-14
Aina Niemetz
SmtEngine: Reorganize class according to guidelines...
tree
|
commitdiff
2019-08-13
Aina Niemetz
New C++ API: Add checks and tests for Solver::simplify...
tree
|
commitdiff
2019-08-13
Aina Niemetz
New C++ API: Reorganize Solver code (move only). (...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Track sygus variable to term relationship via attribut...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Update option to disable symbolic definitions in string...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Add string rewrite involving allchar stars (#3167)
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Properly implement logic info for separation logic...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Implement check abduct feature (#3152)
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Introduce smt2 parsing utility ParseOp and refactor...
tree
|
commitdiff
2019-08-12
Andrew Reynolds
Clean smt2 parsing of named attributes (#3172)
tree
|
commitdiff
2019-08-12
Andrew Reynolds
Give rewrite engine pointer to conflict-based instanti...
tree
|
commitdiff
2019-08-11
Aina Niemetz
New C++ API: Add documentation/guidelines for API guard...
tree
|
commitdiff
2019-08-11
makaimann
New C++ API: Add templated getIndices method for OpTerm...
tree
|
commitdiff
2019-08-10
Andrew Reynolds
Simplify how defined functions are tracked during parsi...
tree
|
commitdiff
2019-08-10
Andrew Reynolds
Add option to only dump unsolved queries for --sygus...
tree
|
commitdiff
2019-08-08
Andrew Reynolds
Reorganize includes for quantifiers engine (#3169)
tree
|
commitdiff
2019-08-08
Mathias Preiner
Fix issues with Ninja build system and add configure...
tree
|
commitdiff
2019-08-07
Aina Niemetz
New C++ API: Add checks and tests for push/pop. (#3121)
tree
|
commitdiff
2019-08-07
Aina Niemetz
New C++ API: Introduce macros for try-catch blocks...
tree
|
commitdiff
2019-08-06
Aina Niemetz
New C++ API: Fix branch prediction in CHECK macros...
tree
|
commitdiff
2019-08-06
Andrew Reynolds
Properly parse qualified identifiers (#3111)
tree
|
commitdiff
2019-08-05
Andrew Reynolds
Remove forward declarations in quantifiers engine ...
tree
|
commitdiff
2019-08-03
Andrew Reynolds
Fix printing issue related to nested quotes (#3154)
tree
|
commitdiff
2019-08-03
Haniel Barbosa
Collapse @ chains in SMT2 printer (#3140)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Flip the polarity of the argument of get-abduct (#3153)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Move basic sygus enumerator to its own file (#3149)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Remove simplification specialized for sygus si solution...
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Support default sygus grammar for strings (#3148)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Throw option exception when track inst lemmas is not...
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Fix solution filtering for streaming abducts (#3143)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Fix BVGauss unit tests. (#3142)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Enable sygus logic when produce-abducts is true (#3144)
tree
|
commitdiff
2019-08-01
Mathias Preiner
Fix memory leak in rewriter (debug mode). (#3141)
tree
|
commitdiff
2019-08-01
Andrew Reynolds
Move some generic utilities out of quantifiers (#3139)
tree
|
commitdiff
2019-08-01
Andrew Reynolds
Regular expression intersection modes (#3134)
tree
|
commitdiff
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
tree
|
commitdiff
2019-07-31
Andrew Reynolds
Add some missing cases in evaluator (#3133)
tree
|
commitdiff
2019-07-31
Andrew Reynolds
Eager conflict detection in strings based on constant...
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Track solver execution mode (#3132)
tree
|
commitdiff
2019-07-30
Haniel Barbosa
Code to activate hoelim preprocessing pass (#3129)
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Minor improvement for rewriter for str.replace (#3124)
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Handle RE intersections modulo equality (#3120)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Fix match trie for polymorphic operators (#3125)
tree
|
commitdiff
2019-07-29
yoni206
Refactoring of bit-vector elimination rules (#3105)
tree
|
commitdiff
2019-07-27
Andrew Reynolds
Minor improvement to term canonizer (#3123)
tree
|
commitdiff
2019-07-26
Andrew Reynolds
Input user grammar in sygus abduct (#3119)
tree
|
commitdiff
2019-07-25
Andrew Reynolds
Split infer info data structure in strings (#3107)
tree
|
commitdiff
2019-07-24
Andrew Reynolds
Minor refactoring of regexp operation (#3116)
tree
|
commitdiff
2019-07-24
Andrew Reynolds
Fix null node when using no-strings-lazy-pp (#3114)
tree
|
commitdiff
2019-07-24
Andrew Reynolds
Move string util functions (#3115)
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix sygus datatype parsing in sygus v1 format (#3113)
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix help messages (#3096)
tree
|
commitdiff
2019-07-23
yoni206
Get operators in node (#3094)
tree
|
commitdiff
2019-07-22
Andres Noetzli
Avoid move constructor of std::fstream for GCC < 5...
tree
|
commitdiff
2019-07-19
yoni206
SyGuS grammar refactor (#3100)
tree
|
commitdiff
2019-07-19
Andrew Reynolds
Fixes for sygus with datatypes (#3103)
tree
|
commitdiff
2019-07-19
Andrew Reynolds
Fix case of unfolding negative membership in reg exp...
tree
|
commitdiff
2019-07-18
Andrew V. Jones
Removing forward-declaration of undefined function...
tree
|
commitdiff
2019-07-18
Andrew Reynolds
Basic rewrites for tolower/toupper (#3095)
tree
|
commitdiff
2019-07-17
Andrew Reynolds
Minor clean in strings. (#3093)
tree
|
commitdiff
2019-07-16
Andrew Reynolds
Add support for str.tolower and str.toupper (#3092)
tree
|
commitdiff
2019-07-15
Andrew Reynolds
Add string rewrite to distribute character stars over...
tree
|
commitdiff
2019-07-08
Andrew Reynolds
Towards refactoring relations (#3078)
tree
|
commitdiff
2019-07-06
Andrew Reynolds
Refactor strings to use an inference manager object...
tree
|
commitdiff
2019-07-02
Andrew Reynolds
Use unique_ptr for UF modules (#3080)
tree
|
commitdiff
2019-07-02
Alex Ozdemir
Optimize DRAT optimization: clause matching (#3074)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Refactoring of relevance vector in quantifiers (#3070)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Support sygus version 2 format (#3066)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Split higher-order UF solver (#2890)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Add higher-order elimination preprocessing pass (#2865)
tree
|
commitdiff
2019-06-28
makaimann
Make mkOpTerm const (#3072)
tree
|
commitdiff
2019-06-27
Andrew Reynolds
Variable elimination rewrite for quantified strings...
tree
|
commitdiff
next