projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Disable sygus inference when combined with incremental and proofs (#3539)
[cvc5.git]
/
src
/
2019-12-09
Andrew Reynolds
Disable sygus inference when combined with incremental...
tree
|
commitdiff
2019-12-09
Andrew Reynolds
Fix case of uninterpreted constant instantiation in...
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Simplify rewrite for character matching (#3545)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Use str.subtr in str.to.int/int.to.str reduction (...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Throw exception instead of warning for approximate...
tree
|
commitdiff
2019-12-06
Andres Noetzli
Add lemma for str.to.int/int.to.str (#3541)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Optimize the rewriter for DT_SYGUS_EVAL (#3529)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
tree
|
commitdiff
2019-12-06
Alex Ozdemir
[proof] Eliminate side-condition from ER signature...
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Introduce the Node-level Datatypes API (#3462)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
tree
|
commitdiff
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
tree
|
commitdiff
2019-12-05
makaimann
Add mkOp for a single Kind (#3522)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
tree
|
commitdiff
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
tree
|
commitdiff
2019-12-04
Andrew Reynolds
Fixes for SyGuS PBE + templated string concatenations...
tree
|
commitdiff
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multipl...
tree
|
commitdiff
2019-12-04
Andres Noetzli
Fix corner case in model construction of strings (...
tree
|
commitdiff
2019-12-03
Andrew Reynolds
Improve flexibility of lemma output in non-linear solve...
tree
|
commitdiff
2019-12-03
Andres Noetzli
Rewrite `str.contains` used for character matching...
tree
|
commitdiff
2019-12-03
makaimann
Add isNullHelper to avoid calling API function isNull...
tree
|
commitdiff
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
tree
|
commitdiff
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitt...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
tree
|
commitdiff
2019-12-01
Andres Noetzli
Prevent ref count from reaching zero in BV instantiator...
tree
|
commitdiff
2019-11-30
Haniel Barbosa
improving parsing error messages related to HOL (#3510)
tree
|
commitdiff
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
tree
|
commitdiff
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
tree
|
commitdiff
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
tree
|
commitdiff
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
tree
|
commitdiff
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
tree
|
commitdiff
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
tree
|
commitdiff
2019-11-22
Andrew Reynolds
Minor refactoring of compute model value for nl (#3489)
tree
|
commitdiff
2019-11-21
Haniel Barbosa
hard limit for rec-fun eval (#3485)
tree
|
commitdiff
2019-11-21
Andrew Reynolds
Evaluation unfolding for symbolic SyGuS constructors...
tree
|
commitdiff
2019-11-20
Haniel Barbosa
Lazy evaluation via rec-funs of ITE expressions (...
tree
|
commitdiff
2019-11-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
tree
|
commitdiff
2019-11-19
Alex Ozdemir
Add a few comments to ProofManager (#3477)
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-18
Andrew Reynolds
Use standard sygus interface for abduction and rewrite...
tree
|
commitdiff
2019-11-18
Andrew Reynolds
Improve interface for sygus datatype, fix utilities...
tree
|
commitdiff
2019-11-18
Andrew Reynolds
Updates to the unit tests, api, and examples for dataty...
tree
|
commitdiff
2019-11-17
Andres Noetzli
Add support for ThreadSanitizer instrumentation (#3467)
tree
|
commitdiff
2019-11-16
Andrew Reynolds
Use standard interface for sygus default grammar constr...
tree
|
commitdiff
2019-11-15
Andrew Reynolds
Introduce SyGuS datatype API (#3465)
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-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
next