| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-01-04 | Fix finiteness check for bounded fmf (#3589) | Andrew Reynolds | |
| Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced. This fixes #3587. | |||
| 2019-12-30 | [proof] ITE translation fix (#3484) | Alex Ozdemir | |
| * Bugfix: convert ifte arms to formulas for printing We have two kinds of ITEs in our LFSC proofs: * ite: for sort-typed expressions * ifte: for formulas Say that we have a Bool-sorted ITE. We had machinery for emitting an `ifte` for it, but this machinery didn't actually convert the arms of the ITE into formulas... Facepalm. Fixed now. * Test the lifting of ITEs from arithmetic. This test verifies that booleans ITEs are correctly lifted to formula ITEs in LRA proofs. It used to fail, but now passes. * clang-format * Typos. * Add test to CMake * Set --check-proofs in test * Address Yoni * Expand printsAsBool documentation * Assert ITE typing soundness * Assert a subtype relation for ITEs, not equality * Update src/proof/arith_proof.h Thanks Yoni! Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: yoni206 <yoni206@users.noreply.github.com> | |||
| 2019-12-23 | Initial support for string reverse (#3581) | Andrew Reynolds | |
| Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`). Also improves support in a few places for tolower/toupper. | |||
| 2019-12-18 | Increment Taylor degree for tangent and secant plane inferences for ↵ | Andrew Reynolds | |
| transcendentals (#3577) | |||
| 2019-12-18 | Avoid calling rewriter from type checker (#3548) | Andres Noetzli | |
| Fixes #3536. The type checker for the chain operator was calling the rewriter. However, the floating-point rewriter was expecting `TheoryFp::expandDefinition()` to be applied before rewriting. If the chain operator had subterms that were supposed to be removed by `TheoryFp::expandDefinition()`, the FP rewriter was throwing an exception. This commit fixes the issue by not calling the full rewriter in the type checker but by just expanding the chain operator. This is a bit less efficient than before because the rewriter does not cache the result of expanding the chain operator anymore but assuming that there are no long chains, the performance impact should be negligible. It also seemed like a reasonable assumption that the rewriter can expect to run after `expandDefinition()` because otherwise the rewriter has to expand definitions, which may be too restrictive. | |||
| 2019-12-17 | Fix spurious parse error for rational real array constants (#3554) | Andrew Reynolds | |
| Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value. This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant. | |||
| 2019-12-16 | Support ackermannization on uninterpreted sorts in BV (#3372) | Ying Sheng | |
| Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1. | |||
| 2019-12-13 | Add support for set comprehension (#3312) | Andrew Reynolds | |
| 2019-12-13 | Disable check-synth-sol in regression with recursive functions (#3560) | Andrew Reynolds | |
| 2019-12-12 | Make CEGIS sampling robust to non-vanilla CEGIS (#3559) | Andrew Reynolds | |
| 2019-12-12 | Fix Unif+PI algorithm with symbolic unfolding (#3558) | Haniel Barbosa | |
| 2019-12-12 | Fixes for regressions (#3557) | Andrew Reynolds | |
| 2019-12-11 | Fix CEGIS refinement for recursive functions evaluation (#3555) | Andrew Reynolds | |
| 2019-12-11 | Do not substitute beneath arithmetic terms in the non-linear solver (#3324) | Andrew Reynolds | |
| 2019-12-10 | Fix ufho issues (#3551) | Haniel Barbosa | |
| 2019-12-10 | Allow unsat cores with sygus inference (#3550) | Andrew Reynolds | |
| 2019-12-09 | Fix case of uninterpreted constant instantiation in FMF (#3543) | Andrew Reynolds | |
| Fixes #3537. This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound). | |||
| 2019-12-08 | [Regressions] Require proof support for abduction (#3546) | Andres Noetzli | |
| 2019-12-06 | New algorithm for interpolation and abduction based on unsat cores (#3255) | Andrew Reynolds | |
| 2019-12-05 | Make nonlinear solver intercept model assignments from the linear arithmetic ↵ | Andrew Reynolds | |
| solver (#3525) | |||
| 2019-12-05 | Refactor mode options for Unif+PI (#3531) | Andrew Reynolds | |
| 2019-12-05 | Bi-directional unrolling of R* regular expressions (#3532) | Andres Noetzli | |
| 2019-12-04 | Fix the subtyping relation for functions (#3494) | Andrew Reynolds | |
| 2019-12-04 | New grammar construction modes for SyGuS (#3486) | Andrew Reynolds | |
| 2019-12-04 | Fix (#3530) | Andrew Reynolds | |
| 2019-12-04 | Fix single invocation solution construction for multiple function case (#3516) | Andrew Reynolds | |
| 2019-12-02 | [SMT2 Printer] Quote symbols starting with digit (#3517) | Andres Noetzli | |
| 2019-12-02 | Update ownership policy for dynamic quantifiers splitting (#3493) | Andrew Reynolds | |
| 2019-12-02 | Fix case of higher-order + sygus inference (#3509) | Andrew Reynolds | |
| 2019-12-01 | Ensure quantifiers options are set with --no-strings-lazy-pp (#3515) | Andrew Reynolds | |
| 2019-11-29 | Competition build: Skip parsing error regression (#3511) | Andres Noetzli | |
| 2019-11-29 | Fix fast SyGuS enumeration for interpreted constants (#3501) | Andrew Reynolds | |
| 2019-11-27 | Fix sygus inference for choice functions introduced at preprocess (#3500) | Andrew Reynolds | |
| 2019-11-27 | Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502) | Haniel Barbosa | |
| 2019-11-27 | Fix indexof range lemma (#3499) | Andrew Reynolds | |
| 2019-11-25 | Better front-end type checking for SyGuS (#3496) | Andrew Reynolds | |
| 2019-11-22 | fixing stupid typo (#3488) | Haniel Barbosa | |
| 2019-11-21 | hard limit for rec-fun eval (#3485) | Haniel Barbosa | |
| 2019-11-20 | Lazy evaluation via rec-funs of ITE expressions (#3482) | Haniel Barbosa | |
| 2019-11-18 | Fix reduction of `sqrt` (#3478) | Andres Noetzli | |
| 2019-11-15 | Fix wrong kind in sygus version 1 parser (#3463) | Andrew Reynolds | |
| 2019-11-13 | Allow (set-logic ...) after (reset) (#3457) | Andres Noetzli | |
| Fixes #3353. #3062 introduced a flag that tracks whether we have seen a `(set-logic ...)` command to improve the handling of `--force-logic`. However, the flag was not set to `false` when `(reset)` was called. This commit fixes the issue. | |||
| 2019-11-10 | Fix bugs related to sygus higher-order + recursive functions (#3448) | Andrew Reynolds | |
| 2019-11-06 | [Regressions] Remove leading whitespace in output (#3444) | Andres Noetzli | |
| 2019-11-06 | Support for SyGuS PBE + recursive functions (#3433) | Andrew Reynolds | |
| 2019-11-04 | [Regressions] Support for running w/ default args (#3436) | Andres Noetzli | |
| 2019-11-04 | Avoid non-well-founded sygus grammars (#3434) | Andrew Reynolds | |
| 2019-11-04 | Make getSynthSolution return a Bool (#3306) | Andrew Reynolds | |
| 2019-11-01 | Fix non-termination in datatype type enumerator (#3369) | Andrew Reynolds | |
| 2019-10-28 | Fix for non-linear models (#3410) | Andrew Reynolds | |
| * Towards fix for non-linear models * Format * Fix * More * Improve * Format * More | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback