projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Distinguish unknown status for model printing (#3454)
[cvc5.git]
/
src
/
2019-11-13
Andrew Reynolds
Distinguish unknown status for model printing (#3454)
tree
|
commitdiff
2019-11-13
Andrew Reynolds
Refactor non-linear extension for model-based refinemen...
tree
|
commitdiff
2019-11-11
Andrew Reynolds
Add missing utilities for Node-level Datatype API ...
tree
|
commitdiff
2019-11-11
Andres Noetzli
Fix mkConst<RoundingMode>() for Python bindings (#3447)
tree
|
commitdiff
2019-11-11
Andrew Reynolds
Eliminate remaining references to type/expr in datatype...
tree
|
commitdiff
2019-11-10
Andrew Reynolds
Fix bugs related to sygus higher-order + recursive...
tree
|
commitdiff
2019-11-09
Andrew Reynolds
Fixes in relations related to datatypes not passed...
tree
|
commitdiff
2019-11-08
Mathias Preiner
cmake: Disable C++ GNU extensions. (#3446)
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Move more string utility functions (#3398)
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Migrate more datatype methods to the Node level (#3443)
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
tree
|
commitdiff
2019-11-06
Andres Noetzli
Remove casts to subclasses of Type in API (#3420)
tree
|
commitdiff
2019-11-05
Andrew Reynolds
Separate model object in non-linear extension (#3426)
tree
|
commitdiff
2019-11-05
Andrew Reynolds
Refactor type matcher utility (#3439)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Make check synth solution robust to auxiliary assertion...
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Fix ho extensionality in collect model info (#3435)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Make getSynthSolution return a Bool (#3306)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Eliminate deprecated utility function from sygus (...
tree
|
commitdiff
2019-11-01
Andrew Reynolds
Fix non-termination in datatype type enumerator (#3369)
tree
|
commitdiff
2019-11-01
Andres Noetzli
Fix and refactor TheoryStrings::checkFlatForms() (...
tree
|
commitdiff
2019-11-01
Andrew Reynolds
Eagerly beta reduce during sygus to builtin term conver...
tree
|
commitdiff
2019-11-01
Andrew Reynolds
Rename datatypes sygus solver (#3417)
tree
|
commitdiff
2019-10-31
Mathias Preiner
Fix Unimplemented() macros missed in #3366. (#3424)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-30
Andrew Reynolds
Split some generic utilities from the non-linear extens...
tree
|
commitdiff
2019-10-28
Andrew Reynolds
Fix for non-linear models (#3410)
tree
|
commitdiff
2019-10-28
Andres Noetzli
Fix integer division rewrite (#3415)
tree
|
commitdiff
2019-10-27
Andrew Reynolds
Fix collect model info for higher-order (#3409)
tree
|
commitdiff
2019-10-27
Andres Noetzli
Fix global-declarations support (#3403)
tree
|
commitdiff
2019-10-23
Andrew Reynolds
Fixes for SyGuS + regular expressions (#3313)
tree
|
commitdiff
2019-10-23
Andrew Reynolds
Refactoring skolems for sets (#3381)
tree
|
commitdiff
2019-10-22
Aina Niemetz
NodeValue: Eliminate redundant NBITS macros. (#3400)
tree
|
commitdiff
2019-10-20
Andrew V. Jones
Cleaning-up the declaration of wrapped functions/method...
tree
|
commitdiff
2019-10-18
makaimann
Update overflow check to handle negative numbers (...
tree
|
commitdiff
2019-10-17
Andrew Reynolds
Move datatype utility functions to own file (#3397)
tree
|
commitdiff
2019-10-16
Andrew Reynolds
Solver state for theory of strings (#3181)
tree
|
commitdiff
2019-10-15
Andres Noetzli
Fix line numbers in templates (#3391)
tree
|
commitdiff
2019-10-15
Andres Noetzli
Fix OOB access (#3383)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Support UF in default sygus grammars (#3319)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Apply sygus repair constant techniques restricted to...
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Ensure lemmas from sygus repair const are guarded ...
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Minor refactor in strings rewriter (#3387)
tree
|
commitdiff
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
tree
|
commitdiff
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
tree
|
commitdiff
2019-10-11
Andres Noetzli
Add support for UBSan instrumentation (#3382)
tree
|
commitdiff
2019-10-11
Aina Niemetz
Make order of theories explicit in the source code...
tree
|
commitdiff
2019-10-10
Andrew Reynolds
Warning instead of assertion for failing propagating...
tree
|
commitdiff
2019-10-09
Aina Niemetz
NodeValue: Use 'using' instead of 'typedef'. (#3374)
tree
|
commitdiff
2019-10-09
Aina Niemetz
NodeValue: Use fixed width return type for getRefCount...
tree
|
commitdiff
2019-10-09
Aina Niemetz
Reorder NodeValue class according to our code style...
tree
|
commitdiff
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
tree
|
commitdiff
2019-10-09
Aina Niemetz
New C++ API: Term: Add missing checks for null. (#3364)
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Fix method for getting arithmetic function definition...
tree
|
commitdiff
2019-10-08
Piotr Trojanek
prefer prefix ++ operator for iterators
tree
|
commitdiff
2019-10-08
Piotr Trojanek
pass parameters by reference where it affects performance
tree
|
commitdiff
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
tree
|
commitdiff
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
tree
|
commitdiff
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
tree
|
commitdiff
2019-10-08
Aina Niemetz
New C++ API: Add Term::getId(). (#3360)
tree
|
commitdiff
2019-10-08
Andres Noetzli
[SMT2 Parser] Move code of `rewriterulesCommand` (...
tree
|
commitdiff
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
tree
|
commitdiff
2019-10-04
Andrew Reynolds
Avoid duplicate lemmas in datatypes (#3310)
tree
|
commitdiff
2019-10-03
yoni206
Disable proofs for unsupported logics (#3327)
tree
|
commitdiff
2019-10-03
Andres Noetzli
Add missing type definitions to CDHashMap iterator...
tree
|
commitdiff
2019-10-03
Andres Noetzli
[SMT2 Parser] Move code of `sygusCommand` (#3335)
tree
|
commitdiff
2019-10-03
Aina Niemetz
Fix compiler warning. (#3348)
tree
|
commitdiff
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
tree
|
commitdiff
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
tree
|
commitdiff
2019-09-30
Andrew Reynolds
Add help for sygus 2.0 (#3318)
tree
|
commitdiff
2019-09-30
Andrew Reynolds
Avoid cases of empty sygus grammars (#3301)
tree
|
commitdiff
2019-09-29
Andrew Reynolds
Fail single invocation techniques when utility inferenc...
tree
|
commitdiff
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
tree
|
commitdiff
2019-09-28
Andrew Reynolds
Support smt2 language "match" term (#3258)
tree
|
commitdiff
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
tree
|
commitdiff
2019-09-27
Andres Noetzli
Make substitution index context-independent (#2474)
tree
|
commitdiff
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
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-25
Andrew Reynolds
Fix printing of instantiation patterns (#3305)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
tree
|
commitdiff
2019-09-19
makaimann
Add support for creating constant arrays to the new...
tree
|
commitdiff
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
tree
|
commitdiff
2019-09-18
Andrew Reynolds
Minor cleaning (#3295)
tree
|
commitdiff
2019-09-17
Andrew Reynolds
Encapsulate relevant domain (#3293)
tree
|
commitdiff
2019-09-17
Andrew Reynolds
Avoid computing cardinality when constructing models...
tree
|
commitdiff
2019-09-17
Andrew Reynolds
Remove parameterized check (#3290)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Remove equality inference option for quantifiers (...
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Move specific attributes out of term util (#3279)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Sygus type info class (#3187)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Fix HO model construction for functions having Boolean...
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Move virtual term substitution utilities to own file...
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Return RecoverableModalException when model is not...
tree
|
commitdiff
2019-09-16
Aina Niemetz
Fix compiler warning in options.cpp. (#3284)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Initialize fields in sets inference manager (#3289)
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
next