projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2019-09-16
Andrew Reynolds
Fix spurious meta-info in regression (#3294)
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Remove equality inference option for quantifiers (...
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Move specific attributes out of term util (#3279)
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Sygus type info class (#3187)
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Fix HO model construction for functions having Boolean...
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Move virtual term substitution utilities to own file...
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Return RecoverableModalException when model is not...
commit
|
commitdiff
|
tree
2019-09-16
Aina Niemetz
Fix compiler warning in options.cpp. (#3284)
commit
|
commitdiff
|
tree
2019-09-16
Haniel Barbosa
Adding new scripts for CASC/TPTP (#3291)
commit
|
commitdiff
|
tree
2019-09-16
Andrew Reynolds
Initialize fields in sets inference manager (#3289)
commit
|
commitdiff
|
tree
2019-09-16
Aina Niemetz
parser: Improve error message for unrecognized input...
commit
|
commitdiff
|
tree
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
commit
|
commitdiff
|
tree
2019-09-13
Andrew Reynolds
Move higher-order matching predicate (#3280)
commit
|
commitdiff
|
tree
2019-09-13
Andrew Reynolds
Split, refactor and document the theory of sets (#3085)
commit
|
commitdiff
|
tree
2019-09-12
Andrew Reynolds
Rename UF with cardinality extension (#3241)
commit
|
commitdiff
|
tree
2019-09-12
Andrew Reynolds
Update to standard implementation of contains term...
commit
|
commitdiff
|
tree
2019-09-12
Andrew Reynolds
Fix default grammar construction for arrays when no...
commit
|
commitdiff
|
tree
2019-09-12
Andrew Reynolds
Encapsulate synth engine (#3271)
commit
|
commitdiff
|
tree
2019-09-12
Andrew Reynolds
Refactoring finite bounds in Quantifiers Engine (#3261)
commit
|
commitdiff
|
tree
2019-09-11
Ken Matsui
Fix not to output all warnings (#2778)
commit
|
commitdiff
|
tree
2019-09-11
Andrew Reynolds
Fix type assertion in getSynthSolutions (#3252)
commit
|
commitdiff
|
tree
2019-09-11
Andrew Reynolds
Infrastructure for instantiation rewriter (#3262)
commit
|
commitdiff
|
tree
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
commit
|
commitdiff
|
tree
2019-09-10
Andrew Reynolds
Fix issue related to enum in cegqi (#3267)
commit
|
commitdiff
|
tree
2019-09-09
Andrew Reynolds
Fix issue in cegqi related to enum (#3265)
commit
|
commitdiff
|
tree
2019-09-07
Andrew Reynolds
Remove portfolio (#3236)
commit
|
commitdiff
|
tree
2019-09-06
Mathias Preiner
Remove parsing/printing of meta-info command. (#3260)
commit
|
commitdiff
|
tree
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
commit
|
commitdiff
|
tree
2019-09-06
Andrew Reynolds
Make CEGQI term type to enum (#3256)
commit
|
commitdiff
|
tree
2019-09-06
Andrew Reynolds
Model API for domain elements (#3243)
commit
|
commitdiff
|
tree
2019-09-05
Andrew Reynolds
Explicitly pass current sygus solution to exclude ...
commit
|
commitdiff
|
tree
2019-09-05
Andrew Reynolds
Refactoring CEGQI interface (#3239)
commit
|
commitdiff
|
tree
2019-09-04
Andrew Reynolds
Towards incremental SyGuS in SMT engine (#3195)
commit
|
commitdiff
|
tree
2019-09-04
yoni206
More details in substitution function documentation...
commit
|
commitdiff
|
tree
2019-09-04
Andrew Reynolds
Move getCounterexampleLiteral out of term utilities...
commit
|
commitdiff
|
tree
2019-09-04
Mathias Preiner
Fix DAGification for printer. (#3233)
commit
|
commitdiff
|
tree
2019-09-04
Andrew Reynolds
Fixes related to destructing null (#3231)
commit
|
commitdiff
|
tree
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Fix out-of-bounds access in regexp inclusion test ...
commit
|
commitdiff
|
tree
2019-08-30
Andrew Reynolds
Undo unintential change to FindCxxTest (#3240)
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
commit
|
commitdiff
|
tree
2019-08-28
Andrew Reynolds
Removing comments related to issues (#3232)
commit
|
commitdiff
|
tree
2019-08-28
Andrew Reynolds
Fixes for get-abduct (#3229)
commit
|
commitdiff
|
tree
2019-08-26
Mathias Preiner
Make contrib/get-* more robust. (#3198)
commit
|
commitdiff
|
tree
2019-08-26
Andrew Reynolds
Remove unnecessary code from Cvc.g (#3213)
commit
|
commitdiff
|
tree
2019-08-24
Piotr Trojanek
fix misuse of iterator with a different container ...
commit
|
commitdiff
|
tree
2019-08-24
Piotr Trojanek
fix mismatch between "delete" and "new []" (#2795)
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Fixes for sygus regressions (#3219)
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Document transition inference utility (#3207)
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Exclude redundant lemmas when tracking inst lemmas...
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Fix argument in nonlinear extension. (#3216)
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Minor update to term util (#3208)
commit
|
commitdiff
|
tree
2019-08-23
Andrew Reynolds
Pass synthesis conjecture to sygus modules (#3212)
commit
|
commitdiff
|
tree
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
commit
|
commitdiff
|
tree
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
commit
|
commitdiff
|
tree
2019-08-19
Aina Niemetz
New C++ API: Add checks for Solver::checkValid and...
commit
|
commitdiff
|
tree
2019-08-18
Andrew Reynolds
Context-independent regular expression unfolding (...
commit
|
commitdiff
|
tree
2019-08-18
Andrew Reynolds
Cleaning make bound var in smt2 parser (#3192)
commit
|
commitdiff
|
tree
2019-08-17
Andrew Reynolds
Move quantifiers relevance module inside E-matching...
commit
|
commitdiff
|
tree
2019-08-17
Andrew Reynolds
Mark symbols introduced by named attributes as defined...
commit
|
commitdiff
|
tree
2019-08-15
Andrew Reynolds
Fix for when to apply single invocation techniques...
commit
|
commitdiff
|
tree
2019-08-15
Mathias Preiner
cmake: Use ExactVersion instead of SameMinorVersion...
commit
|
commitdiff
|
tree
2019-08-14
Mathias Preiner
Remove option --continued-execution. (#3189)
commit
|
commitdiff
|
tree
2019-08-14
Andrew Reynolds
Update to standard implementation of getting free...
commit
|
commitdiff
|
tree
2019-08-14
Andrew Reynolds
Call separate SMT engine for single invocation sygus...
commit
|
commitdiff
|
tree
2019-08-14
Mathias Preiner
cmake: Export CVC4 library interface. (#3179)
commit
|
commitdiff
|
tree
2019-08-14
Andres Noetzli
Enable Clang-Format for Java (#3064)
commit
|
commitdiff
|
tree
2019-08-14
Andrew Reynolds
Minor cleaning of sygus term database (#3159)
commit
|
commitdiff
|
tree
2019-08-14
Andrew Reynolds
Fix issue related to higher-order purification in term...
commit
|
commitdiff
|
tree
2019-08-14
Aina Niemetz
SmtEngine: Reorganize class according to guidelines...
commit
|
commitdiff
|
tree
2019-08-13
Aina Niemetz
New C++ API: Add checks and tests for Solver::simplify...
commit
|
commitdiff
|
tree
2019-08-13
Aina Niemetz
New C++ API: Fix test names of solver_black unit test...
commit
|
commitdiff
|
tree
2019-08-13
Aina Niemetz
New C++ API: Reorganize Solver code (move only). (...
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Track sygus variable to term relationship via attribut...
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Update option to disable symbolic definitions in string...
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Add string rewrite involving allchar stars (#3167)
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Properly implement logic info for separation logic...
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Implement check abduct feature (#3152)
commit
|
commitdiff
|
tree
2019-08-13
Andrew Reynolds
Introduce smt2 parsing utility ParseOp and refactor...
commit
|
commitdiff
|
tree
2019-08-12
Andrew Reynolds
Clean smt2 parsing of named attributes (#3172)
commit
|
commitdiff
|
tree
2019-08-12
Andrew Reynolds
Give rewrite engine pointer to conflict-based instanti...
commit
|
commitdiff
|
tree
2019-08-11
Aina Niemetz
New C++ API: Add documentation/guidelines for API guard...
commit
|
commitdiff
|
tree
2019-08-11
makaimann
New C++ API: Add templated getIndices method for OpTerm...
commit
|
commitdiff
|
tree
2019-08-10
Andrew Reynolds
Simplify how defined functions are tracked during parsi...
commit
|
commitdiff
|
tree
2019-08-10
Andrew Reynolds
Add option to only dump unsolved queries for --sygus...
commit
|
commitdiff
|
tree
2019-08-08
Andrew Reynolds
Reorganize includes for quantifiers engine (#3169)
commit
|
commitdiff
|
tree
2019-08-08
Andrew Reynolds
Add subdirectories to contrib for competition scripts...
commit
|
commitdiff
|
tree
2019-08-08
Mathias Preiner
Fix issues with Ninja build system and add configure...
commit
|
commitdiff
|
tree
2019-08-07
Aina Niemetz
New C++ API: Add checks and tests for push/pop. (#3121)
commit
|
commitdiff
|
tree
2019-08-07
Aina Niemetz
New C++ API: Introduce macros for try-catch blocks...
commit
|
commitdiff
|
tree
2019-08-06
Aina Niemetz
New C++ API: Fix branch prediction in CHECK macros...
commit
|
commitdiff
|
tree
2019-08-06
Andrew Reynolds
Properly parse qualified identifiers (#3111)
commit
|
commitdiff
|
tree
2019-08-06
Haniel Barbosa
Scripts for CASC-27 (#3163)
commit
|
commitdiff
|
tree
2019-08-06
Andrew Reynolds
Fix drat signature wrt side condition return types...
commit
|
commitdiff
|
tree
2019-08-05
Andrew Reynolds
Remove forward declarations in quantifiers engine ...
commit
|
commitdiff
|
tree
2019-08-04
Mathias Preiner
Fix regression script for incremental SMT-LIB v2 benchm...
commit
|
commitdiff
|
tree
2019-08-03
Andrew Reynolds
Fix printing issue related to nested quotes (#3154)
commit
|
commitdiff
|
tree
next