projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Make eq chain an aggressive rewrite in extended rewriter (#3679)
[cvc5.git]
/
test
/
regress
/
CMakeLists.txt
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewrite...
blob
|
commitdiff
|
raw
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invoc...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithme...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal represe...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus defau...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-14
Andrew Reynolds
Generalize example-based sym breaking to conjectures...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andrew Reynolds
Fix side condition check in sygus core connective ...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-10
Andrew Reynolds
Track trivial cases in transition inference (#3598)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-08
Andrew Reynolds
Fix backtracking issue in sygus fast enumerator (#3593)
blob
|
commitdiff
|
raw
|
diff to current
2020-01-08
mudathirmahgoub
Universe set cardinality for finite types with finite...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
blob
|
commitdiff
|
raw
|
diff to current
2020-01-04
Andrew Reynolds
Fix finiteness check for bounded fmf (#3589)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-18
Andrew Reynolds
Increment Taylor degree for tangent and secant plane...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array consta...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Haniel Barbosa
Fix Unif+PI algorithm with symbolic unfolding (#3558)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Fixes for regressions (#3557)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-12
Andrew Reynolds
Fix CEGIS refinement for recursive functions evaluation...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-11
Andrew Reynolds
Do not substitute beneath arithmetic terms in the non...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-09
Andrew Reynolds
Fix case of uninterpreted constant instantiation in...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andrew Reynolds
Make nonlinear solver intercept model assignments from...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-05
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-04
Andrew Reynolds
Fix single invocation solution construction for multipl...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Update ownership policy for dynamic quantifiers splitt...
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Fix case of higher-order + sygus inference (#3509)
blob
|
commitdiff
|
raw
|
diff to current
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-30
Andrew Reynolds
Fix fast SyGuS enumeration for interpreted constants...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Andrew Reynolds
Fix sygus inference for choice functions introduced...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-21
Haniel Barbosa
hard limit for rec-fun eval (#3485)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-20
Haniel Barbosa
Lazy evaluation via rec-funs of ITE expressions (...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-15
Andrew Reynolds
Fix wrong kind in sygus version 1 parser (#3463)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-10
Andrew Reynolds
Fix bugs related to sygus higher-order + recursive...
blob
|
commitdiff
|
raw
|
diff to current
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
blob
|
commitdiff
|
raw
|
diff to current
2019-11-01
Andrew Reynolds
Fix non-termination in datatype type enumerator (#3369)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-28
Andrew Reynolds
Fix for non-linear models (#3410)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-28
Andres Noetzli
Fix integer division rewrite (#3415)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-27
Andres Noetzli
Fix global-declarations support (#3403)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-23
Andrew Reynolds
Fixes for SyGuS + regular expressions (#3313)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-14
Andrew Reynolds
Remove benchmark (#3389)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-14
Andrew Reynolds
Support UF in default sygus grammars (#3319)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-14
Andrew Reynolds
Apply sygus repair constant techniques restricted to...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-14
Andrew Reynolds
Ensure lemmas from sygus repair const are guarded ...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-13
Andrew Reynolds
Eliminate negative constant coefficients in div/mod...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andrew Reynolds
Fix method for getting arithmetic function definition...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
blob
|
commitdiff
|
raw
|
diff to current
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-03
yoni206
Disable proofs for unsupported logics (#3327)
blob
|
commitdiff
|
raw
|
diff to current
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-30
Andrew Reynolds
Avoid cases of empty sygus grammars (#3301)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-29
Andrew Reynolds
Fail single invocation techniques when utility inferenc...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Add isParameterized function to Expr (#3303)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
blob
|
commitdiff
|
raw
|
diff to current
2019-09-17
Andrew Reynolds
Avoid computing cardinality when constructing models...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-16
Andrew Reynolds
Fix HO model construction for functions having Boolean...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Fix default grammar construction for arrays when no...
blob
|
commitdiff
|
raw
|
diff to current
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Exclude redundant lemmas when tracking inst lemmas...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-20
Andrew Reynolds
Fixes for sygus inference on quantifier free problems...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-18
Andrew Reynolds
Context-independent regular expression unfolding (...
blob
|
commitdiff
|
raw
|
diff to current
2019-08-14
Andrew Reynolds
Update to standard implementation of getting free...
blob
|
commitdiff
|
raw
|
diff to current
next