summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-27Python api documentation for sorts (#7440)yoni206
This PR adds documentation for the Sort python API.
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-27Deterministic variables for RE elim (#7489)Andrew Reynolds
Fixes #6766.
2021-10-27Fix mac compile errors in sort.cpp (#7507)mudathirmahgoub
This fixes compile errors in Mac for the java api where `jlong` means `long long`.
2021-10-27Make --version exit (#7506)Gereon Kremer
This PR adds the missing handler declaration for the --version option. Fixes #7505.
2021-10-27Fix libpoly build on windows (#7502)Gereon Kremer
This PR should finally resolve the current issues with libpoly and windows cross compilation.
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] Modularize check for whether a clause is singleton (#7497)Haniel Barbosa
Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.
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-26[proofs] Alethe: Translate Block of clause pattern rule (#7406)Lachnitt
Implementation of the translation of a number of rules that follow the clause pattern into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate AND_INTRO rule (#7405)Lachnitt
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate AND_ELIM rule (#7404)Lachnitt
Implementation of the translation of AND_ELIM rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26[proofs] Alethe: Translate CONTRA rule (#7403)Lachnitt
Implementation of the translation of CONTRA rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-26Upload docs for tags to docs-releases (#7415)Gereon Kremer
This automatically uploads the generated docs to a new repository docs-releases (which should eventually become docs). In contrast to docs-ci, we only store docs for releases there.
2021-10-26Fix frequent rebuild of options target (#7450)Gereon Kremer
The mkoptions.py script only updates its output files if their content would actually change. This avoid a full rebuild on every run, and makes sure that only parts that actually change are rebuild. Unfortunately this interacts badly with how cmake/make/... do inter-target dependency tracking. This PR adds a stamp file options.stamp that is always updated by mkoptions.py and used by cmake as main output.
2021-10-26Fix Configuration::isStaticBuild (#7456)Gereon Kremer
This PR fixes a minor issue in Configuration::isStaticBuild() which would always return true. Note that CVC5_STATIC_BUILD is always defined via #cmakedefine01 in cvc5config.h.
2021-10-26[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)Lachnitt
Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-25[proofs] Alethe: Translate MODUS_PONENS rule (#7401)Lachnitt
Implementation of the translation of MODUS_PONENS rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
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-25[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)Lachnitt
Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-25Fix spurious checks to closed proofs (#7484)Andrew Reynolds
This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver. This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.
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-25Remove HOL/fmf bound messages in set defaults (#7487)Andrew Reynolds
This block is misleading after the last commit.
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-25Reenable proofs on some regressions (#7483)Andrew Reynolds
2021-10-25[proofs] Alethe: Translate SPLIT rule (#7399)Lachnitt
Implementation of the translation of SPLIT rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
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-24Delete redundant file option_Info.cpp (#7477)mudathirmahgoub
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-23Remove spurious assertoin (#7458)Andrew Reynolds
Fixes #7439. That benchmark is now "unknown".
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-22Remove options::X__name (#7414)Gereon Kremer
This PR removes the static strings options::module::X__name that hold the primary long option name. We used them to figure out which option an handler function was called on for certain handler functions. This was always a weird way, and the past refactorings have eliminated all these cases. This also removes the need to the two arguments option and flag to all option handlers.
2021-10-22Remove stale pointer to proof node manager from skolemize utility (#7471)Andrew Reynolds
Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).
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-22Remove `--uf-ho` option (#7463)Andrew Reynolds
This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder. It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.
2021-10-22Fix symmetry issue in theory engine conflicts (#7469)Andrew Reynolds
Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.
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-22[proofs] Alethe: Translate FACTORING rule (#7398)Lachnitt
Implementation of the translation of FACTORING rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-10-22[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)Lachnitt
Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback