summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Collapse)Author
2020-01-29Fix isLeq function in String utility (#3659)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen ↵Andrew Reynolds
(#3641)
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function ↵Andrew Reynolds
apps (#3605)
2020-01-14Disable unsat cores for regression that times out (#3607)Andres Noetzli
Regression `regress2/strings/issue3203.smt2` is currently timing out depending on the version of the libraries loaded (see #3606 for more info). This commit temporarily disables the regression to get the nightlies to pass again.
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
* rewrote set cardinality for finite-types * small changes and format
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2020-01-04Fix 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-23Initial 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-18Increment Taylor degree for tangent and secant plane inferences for ↵Andrew Reynolds
transcendentals (#3577)
2019-12-18Avoid 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-17Fix 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-16Support 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-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-13Disable check-synth-sol in regression with recursive functions (#3560)Andrew Reynolds
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Fixes for regressions (#3557)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
2019-12-10Allow unsat cores with sygus inference (#3550)Andrew Reynolds
2019-12-09Fix 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-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ↵Andrew Reynolds
solver (#3525)
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-04Fix the subtyping relation for functions (#3494)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fix (#3530)Andrew Reynolds
2019-12-04Fix 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-02Fix case of higher-order + sygus inference (#3509)Andrew Reynolds
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-11-29Competition build: Skip parsing error regression (#3511)Andres Noetzli
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback