summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2021-10-27Merge branch 'master' into issue7504issue7504Gereon Kremer
2021-10-27Require ITE branches to be first class types (#7508)Andres Noetzli
Fixes cvc5/cvc5-projects#316.
2021-10-27Fix care graph computation for higher-order (#7474)Andrew Reynolds
Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph. Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.
2021-10-27Fix model unsoundness for relation join (#7511)Andrew Reynolds
This fixes a model unsoundness issue in the theory solver for relations.
2021-10-27minor updateAndres Noetzli
2021-10-27Avoid non-terminating check with assumptions in strings rewriter (#7503)Andrew Reynolds
These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression. Instead, these rewrites are now moved to the extended rewriter.
2021-10-27[Regression Script] Fix use of undefined variablesAndres Noetzli
Fixes #7504.
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
Fixes #6766.
2021-10-27Make --version exit (#7506)Gereon Kremer
This PR adds the missing handler declaration for the --version option. Fixes #7505.
2021-10-26[proofs] Fix singleton check in MACRO_RES post-processing (#7498)Haniel Barbosa
Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way. Depends on #7497. Fixes cvc5/cvc5-projects#318
2021-10-26[proofs] Reset local var in SatProofManager since incremental exists (#7500)Haniel Barbosa
Fixes cvc5/cvc5-projects#317
2021-10-26Disable automatic symmetry in proofs of theory explanations (#7493)Andrew Reynolds
This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form. This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories. Fixes cvc5/cvc5-projects#311.
2021-10-26[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)Haniel Barbosa
Fixes cvc5/cvc5-projects#319
2021-10-26Add regressions for fixed issues (#7495)Andrew Reynolds
Fixes #4656. Fixes #5234. These do not occur on master.
2021-10-26Disable sygus-inst when incremental (#7485)Andrew Reynolds
Fixes #7385. Option --sygus-inst relies on the quantifier-free sygus extension of datatypes, which does not support incremental mode. Updating it to support incremental is a long term project. Until this is complete, --sygus-inst should not be run in incremental mode.
2021-10-25Add new method for enumerating unsat queries with SyGuS (#7459)Andrew Reynolds
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported). The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores. It does some minor refactoring of ExprMinerManager to support the new module.
2021-10-25Java and python unit tests for mkCardinalityConstraint (#7486)Andrew Reynolds
Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8.
2021-10-25Fix more missing uses of CDProof::isSame (#7491)Andrew Reynolds
Fixes cvc5/cvc5-projects#306.
2021-10-25Fix support for global declarations (#7480)Andrew Reynolds
Previously, we asserted global declarations as substitutions/formulas just before check-sat. This is not ideal since the current set of assertions can be preprocessed without having knowledge of definitions of defined functions. Moreover, this could lead to model unsoundness if it were the case that a defined symbol was solved during preprocessing. Fixes #7479. In that example, y was solved for true and then we failed to overwrite y with its definition (> x 0), hence dropping the definition. Now, y is defined as (> x 0) before we preprocess.
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-25Reenable proofs on some regressions (#7483)Andrew Reynolds
2021-10-25[Regression Script] Support older Python versions (#7482)Andres Noetzli
This removes two uses of f-strings, which are not supported by Python <3.6.
2021-10-24Add new eager conflict detection in strings for integer equivalence classes ↵Andrew Reynolds
(#7453) Required to address Zelkova bottlenecks. This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds. The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts. It also changes EqcInfo to store (str.len x) instead of x for length terms.
2021-10-22Add requires libpoly to regression (#7467)Andrew Reynolds
Required to avoid timeout in non-libpoly builds. FYI @dddejan .
2021-10-22Refactor java package name from cvc5 to io.github.cvc5.api (#7340)mudathirmahgoub
This PR refactors java package name from cvc5 to io.github.cvc5.api. It also refactor the names of cpp and java files.
2021-10-22[proof] Fixing CHAIN_RESOLUTION checker (#7465)Haniel Barbosa
Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain. Fixes cvc5/cvc5-projects#310
2021-10-22Fix out-of-sync pruning in CDCAC proofs (#7470)Gereon Kremer
This PR resolves a subtle issue with CDCAC proofs. The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals. This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered. Fixes cvc5/cvc5-projects#313.
2021-10-22Fix another double negation proof issue (#7468)Gereon Kremer
This PR fixes another subtle proof issue in the circuit propagator concerning negated ites. Fixes cvc5/cvc5-projects#309.
2021-10-22Add more abduction regressions (#7461)Andrew Reynolds
Fixes #5848. This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown. Also introduces subfolder regress/regress1/abduction.
2021-10-22Make CAD proofs user context dependent (#7466)Gereon Kremer
Given that arithmetic lemmas can survive the current (sat) context by being buffered in the inference manager, their proofs need to do as well. This PR changes the CAD proofs to be user context dependent. Fixes cvc5/cvc5-projects#315.
2021-10-22Making `IntBlaster` inherit from `EnvObj` (#7431)yoni206
This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications.
2021-10-22Do not use global proxy variable attribute for strings (#7460)Andrew Reynolds
Fixes #6180.
2021-10-22Add missing methods to Solver.java (#7299)mudathirmahgoub
A life of solver object was simple before summer. Then it got complicated with getDifficulty, optional proofs getProof, more assumptions addSygusAssume, and finally different options to choose from OptionInfo. This PR attempts to prepare solver objects for this new life.
2021-10-21Also fix case of negated ite (#7454)Gereon Kremer
This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.
2021-10-21Fix symmetric proof issue for ITE in circuit propagator (#7452)Gereon Kremer
This PR goes back to #7446 and implements a proper fix that handles both symmetrical cases.
2021-10-21[Regression Script] Fix printing of error diff (#7451)Andres Noetzli
2021-10-21[proofs] Fix open proof in SAT solver due to cycles (#7448)Haniel Barbosa
2021-10-21Add regression (#7447)Gereon Kremer
This PR fixes a proof for an xor term that failed to eliminate a double negation. Fixes cvc5/cvc5-projects#304
2021-10-21Fix incorrect proof from ITE in circuit propagator (#7446)Gereon Kremer
This PR fixes an incorrect proof in the circuit propagator related to back-propagation of an ite term. Fixes cvc5/cvc5-projects#305.
2021-10-21Refactor regressions script (#7249)Andres Noetzli
This makes the regression script more modular by refactoring all the different checks into separate classes, which makes it easier to add additional tests and to run only a subset of the tests.
2021-10-21Make cardinality constraint a nullary operator (#7333)Andrew Reynolds
This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously. It also removes an unimplemented kind CARDINALITY_VALUE. Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.
2021-10-21Enable and fix dump test (#7387)Andres Noetzli
Fixes #1649. The test was not enabled before and was still expecting CVC-style output.
2021-10-20Fix (#7437)Gereon Kremer
This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295. Fixes #7379.
2021-10-20Enable some previously failing regressions (#7434)Andrew Reynolds
2021-10-20api: Add Solver::mkSepEmp(). (#7432)Aina Niemetz
@alex-ozdemir
2021-10-20Add regressions for fixed issues (#7421)Andrew Reynolds
Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master.
2021-10-20Add `isNull` and `isUpdater` to `Sort` class of python API (#7423)yoni206
This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API.
2021-10-20Check for higher-order variables in TheoryUF::ppRewrite (#7408)Andrew Reynolds
Fixes #7000. That sequence of API calls now throws a logic exception.
2021-10-20Make SyGuS solver robust to non-closed enumerable sorts (#7417)Andrew Reynolds
This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts. It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method. It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding. This addresses several of the issues raised in #6605.
2021-10-20Check whether abduct option is enabled (#7418)Andrew Reynolds
This addresses one of the issues related to #6605.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback