projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Only allow bv2nat/int2bv with BV and integer logic (#4118)
[cvc5.git]
/
test
/
regress
/
regress0
/
2020-03-19
Andres Noetzli
Only allow bv2nat/int2bv with BV and integer logic...
tree
|
commitdiff
2020-03-19
Andrew Reynolds
Fix issue with multiple infinities in CEGQI for LIRA...
tree
|
commitdiff
2020-03-16
Andres Noetzli
Create master equality engine at context level 0 (...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Do not allow quantifiers over real variables in real...
tree
|
commitdiff
2020-03-12
Aina Niemetz
New C++ API: Remove support for (reset). (#4037)
tree
|
commitdiff
2020-03-11
Andres Noetzli
reset-assertions: Update TheoryEngine's PropEngine...
tree
|
commitdiff
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix sort inference for top-level Boolean variables...
tree
|
commitdiff
2020-03-10
Aina Niemetz
Fix issue with reset-assertions. (#3988)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
tree
|
commitdiff
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
tree
|
commitdiff
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
tree
|
commitdiff
2020-03-08
Ying Sheng
Explicit end marker for models printed in the CVC langu...
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Remove tester name from APIs (#3929)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Support default sygus grammar construction for sets...
tree
|
commitdiff
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
tree
|
commitdiff
2020-03-05
Andrew Reynolds
Fix issues with real to int (#3918)
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Throw warning instead of error for non-constant values...
tree
|
commitdiff
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Fix assertion related to assignability in the model...
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Replace conditional rewrite pass in quantifiers with...
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Fix large models for strings (#3835)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression differe...
tree
|
commitdiff
2020-02-26
Andrew Reynolds
More fixes for printing sygus commands (#3812)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
tree
|
commitdiff
2020-02-25
yoni206
bv_to_int preprocessing pass
tree
|
commitdiff
2020-02-24
Andres Noetzli
Make lambda rewriter more robust (#3806)
tree
|
commitdiff
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
tree
|
commitdiff
2020-02-21
Andrew Reynolds
Simple changes towards unicode string standard (#3791)
tree
|
commitdiff
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
tree
|
commitdiff
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
tree
|
commitdiff
2020-02-08
Andres Noetzli
Make "unknown" non-critical for unsat cores check ...
tree
|
commitdiff
2020-02-07
Andrew Reynolds
Refactor check-model handling in SmtEngine (#3723)
tree
|
commitdiff
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
tree
|
commitdiff
2020-02-04
Alex Ozdemir
Regression tests for arithmetic proofs. (#3701)
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Minor fixes to regressions (#3702)
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasib...
tree
|
commitdiff
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
tree
|
commitdiff
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
tree
|
commitdiff
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
tree
|
commitdiff
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus defau...
tree
|
commitdiff
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
tree
|
commitdiff
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
tree
|
commitdiff
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
tree
|
commitdiff
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
tree
|
commitdiff
2019-12-17
Andrew Reynolds
Fix spurious parse error for rational real array consta...
tree
|
commitdiff
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Add support for set comprehension (#3312)
tree
|
commitdiff
2019-12-10
Haniel Barbosa
Fix ufho issues (#3551)
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
Andrew Reynolds
Fix the subtyping relation for functions (#3494)
tree
|
commitdiff
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
tree
|
commitdiff
2019-12-02
Andrew Reynolds
Ensure quantifiers options are set with --no-strings...
tree
|
commitdiff
2019-11-30
Andres Noetzli
Competition build: Skip parsing error regression (...
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-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
tree
|
commitdiff
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
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
Andres Noetzli
Fix global-declarations support (#3403)
tree
|
commitdiff
2019-10-15
Andres Noetzli
Fix regression (#3393)
tree
|
commitdiff
2019-10-14
Andres Noetzli
Disable regression test for competition build (#3388)
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-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
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-03
yoni206
Disable proofs for unsupported logics (#3327)
tree
|
commitdiff
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
tree
|
commitdiff
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
tree
|
commitdiff
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
tree
|
commitdiff
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
tree
|
commitdiff
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Properly implement logic info for separation logic...
tree
|
commitdiff
2019-08-06
Andrew Reynolds
Properly parse qualified identifiers (#3111)
tree
|
commitdiff
2019-08-04
Mathias Preiner
Fix regression script for incremental SMT-LIB v2 benchm...
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-08-02
Andrew Reynolds
Enable sygus logic when produce-abducts is true (#3144)
tree
|
commitdiff
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
tree
|
commitdiff
2019-07-30
Andrew Reynolds
Minor improvement for rewriter for str.replace (#3124)
tree
|
commitdiff
2019-07-30
Haniel Barbosa
Remove hard coded option for TPTP regressions in run_re...
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix sygus datatype parsing in sygus v1 format (#3113)
tree
|
commitdiff
2019-07-18
Andrew Reynolds
Basic rewrites for tolower/toupper (#3095)
tree
|
commitdiff
2019-07-16
Andrew Reynolds
Add support for str.tolower and str.toupper (#3092)
tree
|
commitdiff
2019-06-21
Andres Noetzli
Fix and simplify handling of --force-logic (#3062)
tree
|
commitdiff
2019-06-12
Andres Noetzli
Refactor parser to define fewer tokens for symbols...
tree
|
commitdiff
next