projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2019-10-14
Andrew Reynolds
Apply sygus repair constant techniques restricted to...
commit
|
commitdiff
|
tree
2019-10-14
Andrew Reynolds
Ensure lemmas from sygus repair const are guarded ...
commit
|
commitdiff
|
tree
2019-10-14
Andrew Reynolds
Minor refactor in strings rewriter (#3387)
commit
|
commitdiff
|
tree
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
commit
|
commitdiff
|
tree
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
commit
|
commitdiff
|
tree
2019-10-11
Andres Noetzli
Add support for UBSan instrumentation (#3382)
commit
|
commitdiff
|
tree
2019-10-11
Aina Niemetz
Make order of theories explicit in the source code...
commit
|
commitdiff
|
tree
2019-10-10
Andrew Reynolds
Warning instead of assertion for failing propagating...
commit
|
commitdiff
|
tree
2019-10-10
Mathias Preiner
test: Add TS_UTILS_EXPECT_ABORT macro for unit tests...
commit
|
commitdiff
|
tree
2019-10-09
Aina Niemetz
NodeValue: Use 'using' instead of 'typedef'. (#3374)
commit
|
commitdiff
|
tree
2019-10-09
Aina Niemetz
NodeValue: Use fixed width return type for getRefCount...
commit
|
commitdiff
|
tree
2019-10-09
Aina Niemetz
Reorder NodeValue class according to our code style...
commit
|
commitdiff
|
tree
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
commit
|
commitdiff
|
tree
2019-10-09
Mathias Preiner
cmake: Fix include of CVC4JavaTargets.cmake. (#3373)
commit
|
commitdiff
|
tree
2019-10-09
Aina Niemetz
New C++ API: Term: Add missing checks for null. (#3364)
commit
|
commitdiff
|
tree
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
commit
|
commitdiff
|
tree
2019-10-08
Andrew Reynolds
Fix method for getting arithmetic function definition...
commit
|
commitdiff
|
tree
2019-10-08
Piotr Trojanek
prefer prefix ++ operator for iterators
commit
|
commitdiff
|
tree
2019-10-08
Piotr Trojanek
pass parameters by reference where it affects performance
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
commit
|
commitdiff
|
tree
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
commit
|
commitdiff
|
tree
2019-10-08
Aina Niemetz
Build system: Add build type for incremental competitio...
commit
|
commitdiff
|
tree
2019-10-08
Aina Niemetz
New C++ API: Add Term::getId(). (#3360)
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
[SMT2 Parser] Move code of `rewriterulesCommand` (...
commit
|
commitdiff
|
tree
2019-10-06
Andrew Reynolds
Fix typo in regression (#3359)
commit
|
commitdiff
|
tree
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
commit
|
commitdiff
|
tree
2019-10-04
Andrew Reynolds
Avoid duplicate lemmas in datatypes (#3310)
commit
|
commitdiff
|
tree
2019-10-03
yoni206
Disable proofs for unsupported logics (#3327)
commit
|
commitdiff
|
tree
2019-10-03
Aina Niemetz
Travis: Reenable building and running of examples....
commit
|
commitdiff
|
tree
2019-10-03
Andres Noetzli
Add missing type definitions to CDHashMap iterator...
commit
|
commitdiff
|
tree
2019-10-03
Andres Noetzli
[SMT2 Parser] Move code of `sygusCommand` (#3335)
commit
|
commitdiff
|
tree
2019-10-03
Aina Niemetz
Fix compiler warning. (#3348)
commit
|
commitdiff
|
tree
2019-10-02
Andres Noetzli
[SMT-COMP] Remove --unconstrained-simp for incremental...
commit
|
commitdiff
|
tree
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
commit
|
commitdiff
|
tree
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
commit
|
commitdiff
|
tree
2019-09-30
Andrew Reynolds
Add help for sygus 2.0 (#3318)
commit
|
commitdiff
|
tree
2019-09-30
Andrew Reynolds
Avoid cases of empty sygus grammars (#3301)
commit
|
commitdiff
|
tree
2019-09-29
Andrew Reynolds
Fail single invocation techniques when utility inferenc...
commit
|
commitdiff
|
tree
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
commit
|
commitdiff
|
tree
2019-09-28
Andrew Reynolds
Support smt2 language "match" term (#3258)
commit
|
commitdiff
|
tree
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
commit
|
commitdiff
|
tree
2019-09-27
Andres Noetzli
Make substitution index context-independent (#2474)
commit
|
commitdiff
|
tree
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
commit
|
commitdiff
|
tree
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
commit
|
commitdiff
|
tree
2019-09-25
Andrew Reynolds
Add isParameterized function to Expr (#3303)
commit
|
commitdiff
|
tree
2019-09-25
Mathias Preiner
Use separate CMake project for CVC4 examples. (#3196)
commit
|
commitdiff
|
tree
2019-09-25
Mathias Preiner
Add Windows cross-compiling instructions to INSTALL...
commit
|
commitdiff
|
tree
2019-09-25
Andrew Reynolds
Fix printing of instantiation patterns (#3305)
commit
|
commitdiff
|
tree
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
commit
|
commitdiff
|
tree
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
commit
|
commitdiff
|
tree
2019-09-19
makaimann
Add support for creating constant arrays to the new...
commit
|
commitdiff
|
tree
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
commit
|
commitdiff
|
tree
2019-09-18
Andres Noetzli
Add run script for next SMT-COMP (#3298)
commit
|
commitdiff
|
tree
2019-09-18
Andrew Reynolds
Minor cleaning (#3295)
commit
|
commitdiff
|
tree
2019-09-17
Andrew Reynolds
Encapsulate relevant domain (#3293)
commit
|
commitdiff
|
tree
2019-09-17
Andrew Reynolds
Avoid computing cardinality when constructing models...
commit
|
commitdiff
|
tree
2019-09-17
Andrew Reynolds
Remove parameterized check (#3290)
commit
|
commitdiff
|
tree
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
next