projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Do not insist on bound values being constant in arithmetic instantiation (#3643)
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithmetic...
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
commit
|
commitdiff
|
tree
2020-01-26
Alex Ozdemir
Axioms for affine function bounds. Tests. (#3632)
...yoni206 <yoni206@users.noreply.
github
.com>
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal representati...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
...43099566+ahmed-irfan@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus default...
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types and side conditions for affine bounds (#3631)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Affine Axioms (#3630)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types & side-conditions for linear and affine fns ...
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Axioms (and side conditions) for tightening bounds...
...yoni206 <yoni206@users.noreply.
github
.com>
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2020-01-18
Alex Ozdemir
LIRA proof: Arithmetic predicates & reification thereof...
commit
|
commitdiff
|
tree
2020-01-17
Alex Ozdemir
LIRA sig: int, real terms, and conversions (#3610)
commit
|
commitdiff
|
tree
2020-01-17
Andrew Reynolds
Use axioms when checking goal entailment for abduction...
commit
|
commitdiff
|
tree
2020-01-15
Aina Niemetz
New C++ API: Add nullary constructor for Result. (...
commit
|
commitdiff
|
tree
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
commit
|
commitdiff
|
tree
2020-01-14
Andres Noetzli
Disable unsat cores for regression that times out ...
commit
|
commitdiff
|
tree
2020-01-13
Andres Noetzli
Support arbitrary unsigned integer attributes (#3591)
commit
|
commitdiff
|
tree
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
commit
|
commitdiff
|
tree
2020-01-10
Mathias Preiner
Fix enum names in AIG bitblaster. (#3599)
commit
|
commitdiff
|
tree
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
commit
|
commitdiff
|
tree
2020-01-10
Andres Noetzli
Optimize str.substr reduction (#3595)
commit
|
commitdiff
|
tree
2020-01-08
Andrew Reynolds
Fix backtracking issue in sygus fast enumerator (#3593)
commit
|
commitdiff
|
tree
2020-01-08
mudathirmahgoub
Universe set cardinality for finite types with finite...
commit
|
commitdiff
|
tree
2020-01-07
Andrew Reynolds
Fix unary minus parse check (#3594)
commit
|
commitdiff
|
tree
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
commit
|
commitdiff
|
tree
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
...yoni206 <yoni206@users.noreply.
github
.com>
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2019-12-19
Mathias Preiner
Fix typo in smt_options.toml. (#3579)
commit
|
commitdiff
|
tree
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
commit
|
commitdiff
|
tree
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
commit
|
commitdiff
|
tree
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
commit
|
commitdiff
|
tree
2019-12-16
Andrew Reynolds
Revert evaluate as node. (#3574)
commit
|
commitdiff
|
tree
2019-12-13
Andrew Reynolds
Eliminate Expr-level calls in TypeNode (#3562)
commit
|
commitdiff
|
tree
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Use the node-level datatypes API (#3556)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Fixes for regressions (#3557)
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Fix CEGIS refinement for recursive functions evaluation...
commit
|
commitdiff
|
tree
2019-12-12
Andrew Reynolds
Activate node-level datatype API (#3540)
commit
|
commitdiff
|
tree
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
commit
|
commitdiff
|
tree
2019-12-11
Andrew Reynolds
Support symbolic unfolding in UNIF+PI (#3553)
commit
|
commitdiff
|
tree
2019-12-10
Andrew Reynolds
Incorporate rewriting on demand in the evaluator (...
commit
|
commitdiff
|
tree
2019-12-10
Andrew Reynolds
Allow unsat cores with sygus inference (#3550)
commit
|
commitdiff
|
tree
2019-12-09
Andrew Reynolds
Disable sygus inference when combined with incremental...
commit
|
commitdiff
|
tree
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
commit
|
commitdiff
|
tree
2019-12-07
Andres Noetzli
Use str.subtr in str.to.int/int.to.str reduction (...
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Throw exception instead of warning for approximate...
commit
|
commitdiff
|
tree
2019-12-06
Andres Noetzli
Add lemma for str.to.int/int.to.str (#3541)
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
commit
|
commitdiff
|
tree
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
commit
|
commitdiff
|
tree
2019-12-06
Alex Ozdemir
[proof] Eliminate side-condition from ER signature...
...yoni206 <yoni206@users.noreply.
github
.com>
commit
|
commitdiff
|
tree
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
commit
|
commitdiff
|
tree
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fix (#3530)
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fixes for SyGuS PBE + templated string concatenations...
commit
|
commitdiff
|
tree
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multiple...
commit
|
commitdiff
|
tree
2019-12-04
Andres Noetzli
Fix corner case in model construction of strings (...
commit
|
commitdiff
|
tree
2019-12-03
Andrew Reynolds
Improve flexibility of lemma output in non-linear solver...
commit
|
commitdiff
|
tree
2019-12-03
Aina Niemetz
Fix clang-format file for brace wrapping with case...
commit
|
commitdiff
|
tree
2019-12-03
makaimann
Minor refactor: rename opterm_black to op_black (#3521)
commit
|
commitdiff
|
tree
2019-12-02
makaimann
OpTerm Refactor: Allow retrieving OpTerm used to create...
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitting...
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
commit
|
commitdiff
|
tree
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
commit
|
commitdiff
|
tree
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
commit
|
commitdiff
|
tree
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
commit
|
commitdiff
|
tree
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
commit
|
commitdiff
|
tree
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
commit
|
commitdiff
|
tree
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
commit
|
commitdiff
|
tree
2019-11-22
Andrew Reynolds
Minor refactoring of compute model value for nl (#3489)
commit
|
commitdiff
|
tree
2019-11-21
Haniel Barbosa
hard limit for rec-fun eval (#3485)
commit
|
commitdiff
|
tree
2019-11-21
Andrew Reynolds
Evaluation unfolding for symbolic SyGuS constructors...
commit
|
commitdiff
|
tree
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
commit
|
commitdiff
|
tree
2019-11-18
Andrew Reynolds
Use standard sygus interface for abduction and rewrite...
commit
|
commitdiff
|
tree
2019-11-18
Andrew Reynolds
Improve interface for sygus datatype, fix utilities...
commit
|
commitdiff
|
tree
2019-11-18
Andrew Reynolds
Updates to the unit tests, api, and examples for datatypes...
commit
|
commitdiff
|
tree
2019-11-17
Andres Noetzli
Add support for ThreadSanitizer instrumentation (#3467)
commit
|
commitdiff
|
tree
2019-11-16
Andrew Reynolds
Use standard interface for sygus default grammar constructio...
commit
|
commitdiff
|
tree
2019-11-15
Andrew Reynolds
Introduce SyGuS datatype API (#3465)
commit
|
commitdiff
|
tree
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
commit
|
commitdiff
|
tree
2019-11-13
Andrew Reynolds
Distinguish unknown status for model printing (#3454)
commit
|
commitdiff
|
tree
2019-11-13
Andrew Reynolds
Refactor non-linear extension for model-based refinement...
commit
|
commitdiff
|
tree
2019-11-11
Andrew Reynolds
Add missing utilities for Node-level Datatype API ...
commit
|
commitdiff
|
tree
2019-11-11
Andrew Reynolds
Eliminate remaining references to type/expr in datatype...
commit
|
commitdiff
|
tree
2019-11-08
Mathias Preiner
cmake: Disable C++ GNU extensions. (#3446)
commit
|
commitdiff
|
tree
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
commit
|
commitdiff
|
tree
2019-11-05
Andrew Reynolds
Separate model object in non-linear extension (#3426)
commit
|
commitdiff
|
tree
2019-11-05
Andrew Reynolds
Refactor type matcher utility (#3439)
commit
|
commitdiff
|
tree
2019-11-04
Andrew Reynolds
Make check synth solution robust to auxiliary assertions...
commit
|
commitdiff
|
tree
2019-11-04
Andrew Reynolds
Fix ho extensionality in collect model info (#3435)
commit
|
commitdiff
|
tree
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
commit
|
commitdiff
|
tree
2019-11-04
Andrew Reynolds
Make getSynthSolution return a Bool (#3306)
commit
|
commitdiff
|
tree
2019-11-04
Andrew Reynolds
Eliminate deprecated utility function from sygus (...
commit
|
commitdiff
|
tree
2019-11-01
Andrew Reynolds
Fix non-termination in datatype type enumerator (#3369)
commit
|
commitdiff
|
tree
2019-11-01
Andres Noetzli
Fix and refactor TheoryStrings::checkFlatForms() (...
commit
|
commitdiff
|
tree
2019-11-01
Andrew Reynolds
Eagerly beta reduce during sygus to builtin term conversion...
commit
|
commitdiff
|
tree
2019-11-01
Andrew Reynolds
Rename datatypes sygus solver (#3417)
commit
|
commitdiff
|
tree
next