cvc5.git
3 years agoAdd documentation on output tags (#7499)
Gereon Kremer [Wed, 27 Oct 2021 23:27:31 +0000 (16:27 -0700)]
Add documentation on output tags (#7499)

This PR adds documentation on how users can use -o. After some offline discussion, we decided it makes sense to generate them automatically in mkoptions.py and also include example outputs.

3 years ago[Regression Script] Fix use of undefined variables (#7510)
Andres Noetzli [Wed, 27 Oct 2021 23:15:56 +0000 (16:15 -0700)]
[Regression Script] Fix use of undefined variables (#7510)

Fixes #7504.

3 years agoFix patching for poly on windows (#7513)
Gereon Kremer [Wed, 27 Oct 2021 19:58:48 +0000 (12:58 -0700)]
Fix patching for poly on windows (#7513)

This PR is another step to fix our windows nightlies.
It moves the patch steps for libpoly in a separate script. Apparently, it is impossible to properly escape this stuff to work on all platforms and all cmake versions.

3 years agoRequire ITE branches to be first class types (#7508)
Andres Noetzli [Wed, 27 Oct 2021 19:46:24 +0000 (12:46 -0700)]
Require ITE branches to be first class types (#7508)

Fixes cvc5/cvc5-projects#316.

3 years agoFix care graph computation for higher-order (#7474)
Andrew Reynolds [Wed, 27 Oct 2021 18:40:18 +0000 (13:40 -0500)]
Fix care graph computation for higher-order (#7474)

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.

3 years agoFix model unsoundness for relation join (#7511)
Andrew Reynolds [Wed, 27 Oct 2021 18:02:52 +0000 (13:02 -0500)]
Fix model unsoundness for relation join  (#7511)

This fixes a model unsoundness issue in the theory solver for relations.

3 years agoPython api documentation for sorts (#7440)
yoni206 [Wed, 27 Oct 2021 17:41:24 +0000 (20:41 +0300)]
Python api documentation for sorts (#7440)

This PR adds documentation for the Sort python API.

3 years agoAvoid non-terminating check with assumptions in strings rewriter (#7503)
Andrew Reynolds [Wed, 27 Oct 2021 16:07:19 +0000 (11:07 -0500)]
Avoid non-terminating check with assumptions in strings rewriter (#7503)

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.

3 years agoDeterministic variables for RE elim (#7489)
Andrew Reynolds [Wed, 27 Oct 2021 15:27:30 +0000 (10:27 -0500)]
Deterministic variables for RE elim (#7489)

Fixes #6766.

3 years agoFix mac compile errors in sort.cpp (#7507)
mudathirmahgoub [Wed, 27 Oct 2021 10:05:43 +0000 (05:05 -0500)]
Fix mac compile errors in sort.cpp (#7507)

This fixes compile errors in Mac for the java api  where `jlong` means `long long`.

3 years agoMake --version exit (#7506)
Gereon Kremer [Wed, 27 Oct 2021 06:12:00 +0000 (23:12 -0700)]
Make --version exit (#7506)

This PR adds the missing handler declaration for the --version option.
Fixes #7505.

3 years agoFix libpoly build on windows (#7502)
Gereon Kremer [Wed, 27 Oct 2021 00:18:23 +0000 (17:18 -0700)]
Fix libpoly build on windows (#7502)

This PR should finally resolve the current issues with libpoly and windows cross compilation.

3 years ago[proofs] Fix singleton check in MACRO_RES post-processing (#7498)
Haniel Barbosa [Tue, 26 Oct 2021 20:59:31 +0000 (17:59 -0300)]
[proofs] Fix singleton check in MACRO_RES post-processing (#7498)

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

3 years ago[proofs] Modularize check for whether a clause is singleton (#7497)
Haniel Barbosa [Tue, 26 Oct 2021 20:46:46 +0000 (17:46 -0300)]
[proofs] Modularize check for whether a clause is singleton (#7497)

Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.

3 years ago[proofs] Reset local var in SatProofManager since incremental exists (#7500)
Haniel Barbosa [Tue, 26 Oct 2021 20:27:39 +0000 (17:27 -0300)]
[proofs] Reset local var in SatProofManager since incremental exists (#7500)

Fixes cvc5/cvc5-projects#317

3 years agoDisable automatic symmetry in proofs of theory explanations (#7493)
Andrew Reynolds [Tue, 26 Oct 2021 20:08:19 +0000 (15:08 -0500)]
Disable automatic symmetry in proofs of theory explanations (#7493)

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.

3 years ago[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)
Haniel Barbosa [Tue, 26 Oct 2021 19:42:14 +0000 (16:42 -0300)]
[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)

Fixes cvc5/cvc5-projects#319

3 years agoAdd regressions for fixed issues (#7495)
Andrew Reynolds [Tue, 26 Oct 2021 17:10:50 +0000 (12:10 -0500)]
Add regressions for fixed issues (#7495)

Fixes #4656. Fixes #5234. These do not occur on master.

3 years agoDisable sygus-inst when incremental (#7485)
Andrew Reynolds [Tue, 26 Oct 2021 16:24:31 +0000 (11:24 -0500)]
Disable sygus-inst when incremental (#7485)

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.

3 years ago[proofs] Alethe: Translate Block of clause pattern rule (#7406)
Lachnitt [Tue, 26 Oct 2021 14:14:01 +0000 (07:14 -0700)]
[proofs] Alethe: Translate Block of clause pattern rule (#7406)

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>
3 years ago[proofs] Alethe: Translate AND_INTRO rule (#7405)
Lachnitt [Tue, 26 Oct 2021 14:00:55 +0000 (07:00 -0700)]
[proofs] Alethe: Translate AND_INTRO rule (#7405)

Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years ago[proofs] Alethe: Translate AND_ELIM rule (#7404)
Lachnitt [Tue, 26 Oct 2021 13:40:07 +0000 (06:40 -0700)]
[proofs] Alethe: Translate AND_ELIM rule  (#7404)

Implementation of the translation of AND_ELIM rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years ago[proofs] Alethe: Translate CONTRA rule (#7403)
Lachnitt [Tue, 26 Oct 2021 13:21:26 +0000 (06:21 -0700)]
[proofs] Alethe: Translate CONTRA rule (#7403)

Implementation of the translation of CONTRA rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoUpload docs for tags to docs-releases (#7415)
Gereon Kremer [Tue, 26 Oct 2021 12:25:00 +0000 (05:25 -0700)]
Upload docs for tags to docs-releases (#7415)

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.

3 years agoFix frequent rebuild of options target (#7450)
Gereon Kremer [Tue, 26 Oct 2021 12:10:10 +0000 (05:10 -0700)]
Fix frequent rebuild of options target (#7450)

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.

3 years agoFix Configuration::isStaticBuild (#7456)
Gereon Kremer [Tue, 26 Oct 2021 11:58:53 +0000 (04:58 -0700)]
Fix Configuration::isStaticBuild (#7456)

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.

3 years ago[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
Lachnitt [Tue, 26 Oct 2021 11:46:26 +0000 (04:46 -0700)]
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)

Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years ago[proofs] Alethe: Translate MODUS_PONENS rule (#7401)
Lachnitt [Mon, 25 Oct 2021 22:24:04 +0000 (15:24 -0700)]
[proofs] Alethe: Translate MODUS_PONENS rule (#7401)

Implementation of the translation of MODUS_PONENS rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoAdd new method for enumerating unsat queries with SyGuS (#7459)
Andrew Reynolds [Mon, 25 Oct 2021 21:39:02 +0000 (16:39 -0500)]
Add new method for enumerating unsat queries with SyGuS (#7459)

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.

3 years ago[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)
Lachnitt [Mon, 25 Oct 2021 21:23:48 +0000 (14:23 -0700)]
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)

Implementation of the translation of EQ_RESOLVE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoFix spurious checks to closed proofs (#7484)
Andrew Reynolds [Mon, 25 Oct 2021 20:38:28 +0000 (15:38 -0500)]
Fix spurious checks to closed proofs (#7484)

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.

3 years agoJava and python unit tests for mkCardinalityConstraint (#7486)
Andrew Reynolds [Mon, 25 Oct 2021 20:23:31 +0000 (15:23 -0500)]
Java and python unit tests for mkCardinalityConstraint (#7486)

Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8.

3 years agoFix more missing uses of CDProof::isSame (#7491)
Andrew Reynolds [Mon, 25 Oct 2021 20:08:28 +0000 (15:08 -0500)]
Fix more missing uses of CDProof::isSame (#7491)

Fixes cvc5/cvc5-projects#306.

3 years agoFix support for global declarations (#7480)
Andrew Reynolds [Mon, 25 Oct 2021 18:23:39 +0000 (13:23 -0500)]
Fix support for global declarations (#7480)

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.

3 years agoRemove HOL/fmf bound messages in set defaults (#7487)
Andrew Reynolds [Mon, 25 Oct 2021 17:15:43 +0000 (12:15 -0500)]
Remove HOL/fmf bound messages in set defaults (#7487)

This block is misleading after the last commit.

3 years agoAdd inference for count map (#7264)
mudathirmahgoub [Mon, 25 Oct 2021 16:36:35 +0000 (11:36 -0500)]
Add inference for count map (#7264)

3 years agoReenable proofs on some regressions (#7483)
Andrew Reynolds [Mon, 25 Oct 2021 15:32:16 +0000 (10:32 -0500)]
Reenable proofs on some regressions (#7483)

3 years ago[proofs] Alethe: Translate SPLIT rule (#7399)
Lachnitt [Mon, 25 Oct 2021 13:26:40 +0000 (06:26 -0700)]
[proofs] Alethe: Translate SPLIT rule  (#7399)

Implementation of the translation of SPLIT rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years ago[Regression Script] Support older Python versions (#7482)
Andres Noetzli [Mon, 25 Oct 2021 11:59:53 +0000 (04:59 -0700)]
[Regression Script] Support older Python versions (#7482)

This removes two uses of f-strings, which are not supported by Python
<3.6.

3 years agoDelete redundant file option_Info.cpp (#7477)
mudathirmahgoub [Sun, 24 Oct 2021 20:59:26 +0000 (15:59 -0500)]
Delete redundant file option_Info.cpp (#7477)

3 years agoAdd new eager conflict detection in strings for integer equivalence classes (#7453)
Andrew Reynolds [Sun, 24 Oct 2021 18:31:56 +0000 (13:31 -0500)]
Add new eager conflict detection in strings for integer equivalence classes (#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.

3 years agoRemove spurious assertoin (#7458)
Andrew Reynolds [Sat, 23 Oct 2021 01:27:14 +0000 (20:27 -0500)]
Remove spurious assertoin (#7458)

Fixes #7439. That benchmark is now "unknown".

3 years agoAdd requires libpoly to regression (#7467)
Andrew Reynolds [Fri, 22 Oct 2021 23:28:09 +0000 (18:28 -0500)]
Add requires libpoly to regression (#7467)

Required to avoid timeout in non-libpoly builds.

FYI @dddejan .

3 years agoRefactor java package name from cvc5 to io.github.cvc5.api (#7340)
mudathirmahgoub [Fri, 22 Oct 2021 23:00:06 +0000 (18:00 -0500)]
Refactor java package name from cvc5 to io.github.cvc5.api (#7340)

This PR refactors java package name from cvc5 to io.github.cvc5.api.
It also refactor the names of cpp and java files.

3 years agoRemove options::X__name (#7414)
Gereon Kremer [Fri, 22 Oct 2021 22:32:33 +0000 (15:32 -0700)]
Remove options::X__name (#7414)

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.

3 years agoRemove stale pointer to proof node manager from skolemize utility (#7471)
Andrew Reynolds [Fri, 22 Oct 2021 22:21:02 +0000 (17:21 -0500)]
Remove stale pointer to proof node manager from skolemize utility (#7471)

Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).

3 years ago[proof] Fixing CHAIN_RESOLUTION checker (#7465)
Haniel Barbosa [Fri, 22 Oct 2021 22:08:27 +0000 (19:08 -0300)]
[proof] Fixing CHAIN_RESOLUTION checker (#7465)

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

3 years agoFix out-of-sync pruning in CDCAC proofs (#7470)
Gereon Kremer [Fri, 22 Oct 2021 21:49:50 +0000 (14:49 -0700)]
Fix out-of-sync pruning in CDCAC proofs (#7470)

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.

3 years agoFix another double negation proof issue (#7468)
Gereon Kremer [Fri, 22 Oct 2021 21:37:54 +0000 (14:37 -0700)]
Fix another double negation proof issue (#7468)

This PR fixes another subtle proof issue in the circuit propagator concerning negated ites.
Fixes cvc5/cvc5-projects#309.

3 years agoRemove `--uf-ho` option (#7463)
Andrew Reynolds [Fri, 22 Oct 2021 21:25:37 +0000 (16:25 -0500)]
Remove `--uf-ho` option (#7463)

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.

3 years agoFix symmetry issue in theory engine conflicts (#7469)
Andrew Reynolds [Fri, 22 Oct 2021 21:01:37 +0000 (16:01 -0500)]
Fix symmetry issue in theory engine conflicts (#7469)

Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.

3 years agoAdd more abduction regressions (#7461)
Andrew Reynolds [Fri, 22 Oct 2021 20:48:25 +0000 (15:48 -0500)]
Add more abduction regressions (#7461)

Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.

3 years ago[proofs] Alethe: Translate FACTORING rule (#7398)
Lachnitt [Fri, 22 Oct 2021 19:00:52 +0000 (12:00 -0700)]
[proofs] Alethe: Translate FACTORING rule (#7398)

Implementation of the translation of FACTORING rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years ago[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)
Lachnitt [Fri, 22 Oct 2021 18:38:47 +0000 (11:38 -0700)]
[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)

Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoMake CAD proofs user context dependent (#7466)
Gereon Kremer [Fri, 22 Oct 2021 18:08:33 +0000 (11:08 -0700)]
Make CAD proofs user context dependent (#7466)

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.

3 years agoRefactor theory inference manager constructor (#7457)
Andrew Reynolds [Fri, 22 Oct 2021 16:56:05 +0000 (11:56 -0500)]
Refactor theory inference manager constructor (#7457)

Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead.

Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV.

3 years agoMaking `IntBlaster` inherit from `EnvObj` (#7431)
yoni206 [Fri, 22 Oct 2021 14:56:39 +0000 (17:56 +0300)]
Making `IntBlaster` inherit from `EnvObj` (#7431)

This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications.

3 years agoDo not use global proxy variable attribute for strings (#7460)
Andrew Reynolds [Fri, 22 Oct 2021 14:39:26 +0000 (09:39 -0500)]
Do not use global proxy variable attribute for strings (#7460)

Fixes #6180.

3 years agoFix memory management of `ErrorInformation` (#7388)
Andres Noetzli [Fri, 22 Oct 2021 00:43:54 +0000 (17:43 -0700)]
Fix memory management of `ErrorInformation` (#7388)

Fixes
https://scan6.coverity.com/reports.htm#v37053/p11644/fileInstanceId=125548448&defectInstanceId=32441274&mergedDefectId=1453884.

3 years agoAdd missing methods to Solver.java (#7299)
mudathirmahgoub [Fri, 22 Oct 2021 00:22:00 +0000 (19:22 -0500)]
Add missing methods to Solver.java (#7299)

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.

3 years agoMake expression mining use configurable options and logic (#7426)
Andrew Reynolds [Fri, 22 Oct 2021 00:04:21 +0000 (19:04 -0500)]
Make expression mining use configurable options and logic (#7426)

Required for doing options-specific internal fuzzing using SyGuS.

3 years agodocs: Use light gray for background on the right. (#7438)
Aina Niemetz [Thu, 21 Oct 2021 21:37:05 +0000 (14:37 -0700)]
docs: Use light gray for background on the right. (#7438)

3 years agoAlso fix case of negated ite (#7454)
Gereon Kremer [Thu, 21 Oct 2021 21:07:08 +0000 (14:07 -0700)]
Also fix case of negated ite (#7454)

This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.

3 years agoFix symmetric proof issue for ITE in circuit propagator (#7452)
Gereon Kremer [Thu, 21 Oct 2021 19:10:26 +0000 (12:10 -0700)]
Fix symmetric proof issue for ITE in circuit propagator (#7452)

This PR goes back to #7446 and implements a proper fix that handles both symmetrical cases.

3 years agoSplit utilites from CEGIS core connective module (#7441)
Andrew Reynolds [Thu, 21 Oct 2021 18:48:56 +0000 (13:48 -0500)]
Split utilites from CEGIS core connective module (#7441)

Towards a new module for enumerating unsat queries via SyGuS.

3 years ago[Regression Script] Fix printing of error diff (#7451)
Andres Noetzli [Thu, 21 Oct 2021 18:13:52 +0000 (11:13 -0700)]
[Regression Script] Fix printing of error diff (#7451)

3 years ago[proofs] Fix open proof in SAT solver due to cycles (#7448)
Haniel Barbosa [Thu, 21 Oct 2021 17:14:24 +0000 (14:14 -0300)]
[proofs] Fix open proof in SAT solver due to cycles (#7448)

3 years agoAdd regression (#7447)
Gereon Kremer [Thu, 21 Oct 2021 16:48:47 +0000 (09:48 -0700)]
Add regression (#7447)

This PR fixes a proof for an xor term that failed to eliminate a double negation.

Fixes cvc5/cvc5-projects#304

3 years agoFix incorrect proof from ITE in circuit propagator (#7446)
Gereon Kremer [Thu, 21 Oct 2021 16:33:23 +0000 (09:33 -0700)]
Fix incorrect proof from ITE in circuit propagator (#7446)

This PR fixes an incorrect proof in the circuit propagator related to back-propagation of an ite term.
Fixes cvc5/cvc5-projects#305.

3 years agoRefactor regressions script (#7249)
Andres Noetzli [Thu, 21 Oct 2021 15:34:26 +0000 (08:34 -0700)]
Refactor regressions script (#7249)

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.

3 years agoMake cardinality constraint a nullary operator (#7333)
Andrew Reynolds [Thu, 21 Oct 2021 14:11:57 +0000 (09:11 -0500)]
Make cardinality constraint a nullary operator (#7333)

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.

3 years agoWorking on windows builds (#7381)
Gereon Kremer [Thu, 21 Oct 2021 12:31:59 +0000 (05:31 -0700)]
Working on windows builds (#7381)

This makes a push to fix our windows nightly builds. It does a couple of things:
- remove `CVC5_WINDOWS_BUILD` and check `CMAKE_SYSTEM_NAME` instead
- use `CMAKE_SHARED_LIBRARY_SUFFIX` instead of `so`
- properly set `IMPORTED_IMPLIB` on imported shared libraries
- fix the GMP build, where the header is different for shared and static builds
- fix the find&sed patching for libpoly
- add `CVC5_EXPORT` to nested types in the API
- remove `CVC5_EXPORT` from enums
- add `-Dcvc5_obj_EXPORTS` to actually enable exports
- Fix how template function `safe_print` is exported.

3 years agoAdd setup to generate graphs for cmake target dependencies (#7383)
Gereon Kremer [Thu, 21 Oct 2021 12:10:20 +0000 (05:10 -0700)]
Add setup to generate graphs for cmake target dependencies (#7383)

This adds the target `target-graphs` that generated graphs of cmake dependencies based on `cmake --graphviz`. It is a nice to tool to debug the cmake setup in some cases.

3 years agoEnable and fix dump test (#7387)
Andres Noetzli [Thu, 21 Oct 2021 01:31:52 +0000 (18:31 -0700)]
Enable and fix dump test (#7387)

Fixes #1649. The test was not enabled before and was still expecting
CVC-style output.

3 years agoFix (#7437)
Gereon Kremer [Thu, 21 Oct 2021 01:22:55 +0000 (18:22 -0700)]
Fix (#7437)

This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295.

Fixes #7379.

3 years agoEnable some previously failing regressions (#7434)
Andrew Reynolds [Wed, 20 Oct 2021 23:56:25 +0000 (18:56 -0500)]
Enable some previously failing regressions (#7434)

3 years agoFix docs upload (again) (#7435)
Gereon Kremer [Wed, 20 Oct 2021 23:45:48 +0000 (16:45 -0700)]
Fix docs upload (again) (#7435)

This is a follow-up to #7420. This time, I tested the modified code with every combination of values...

3 years agoapi: Add Solver::mkSepEmp(). (#7432)
Aina Niemetz [Wed, 20 Oct 2021 23:12:55 +0000 (16:12 -0700)]
api: Add Solver::mkSepEmp(). (#7432)

@alex-ozdemir

3 years agoapi: Improve documentation for special cases with nullary ops. (#7433)
Aina Niemetz [Wed, 20 Oct 2021 22:56:40 +0000 (15:56 -0700)]
api: Improve documentation for special cases with nullary ops. (#7433)

Fixes #7430.

3 years agoMove variadic trie utility to its own file (#7410)
Andrew Reynolds [Wed, 20 Oct 2021 22:39:12 +0000 (17:39 -0500)]
Move variadic trie utility to its own file (#7410)

Work towards a new internal fuzzing technique.

The new fuzzing technique leverages elements of the IJCAR 2020 paper on abduction, this moves https://github.com/cvc5/cvc5/blob/master/src/theory/quantifiers/sygus/cegis_core_connective.h#L44 to its own file. A followup PR will break this and further utility methods out of this file.

3 years agoAdd regressions for fixed issues (#7421)
Andrew Reynolds [Wed, 20 Oct 2021 22:28:52 +0000 (17:28 -0500)]
Add regressions for fixed issues (#7421)

Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master.

3 years agoAdd `isNull` and `isUpdater` to `Sort` class of python API (#7423)
yoni206 [Wed, 20 Oct 2021 22:18:33 +0000 (01:18 +0300)]
Add `isNull` and `isUpdater` to `Sort` class of python API  (#7423)

This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API.

3 years agoThrow exception if checking model with separation logic heap (#7422)
Andrew Reynolds [Wed, 20 Oct 2021 22:09:07 +0000 (17:09 -0500)]
Throw exception if checking model with separation logic heap (#7422)

Fixes #5515.

It is currently not possible to check-model with separation logic. Checking models requires either additional bookkeeping (heap per formula position) or otherwise is expensive to check.

This makes us give a recoverable exception.

3 years agoCheck for higher-order variables in TheoryUF::ppRewrite (#7408)
Andrew Reynolds [Wed, 20 Oct 2021 22:01:01 +0000 (17:01 -0500)]
Check for higher-order variables in TheoryUF::ppRewrite (#7408)

Fixes #7000. That sequence of API calls now throws a logic exception.

3 years agoFix inadvertent failure of workflow step (#7420)
Gereon Kremer [Wed, 20 Oct 2021 21:42:16 +0000 (14:42 -0700)]
Fix inadvertent failure of workflow step (#7420)

This fixes an issue introduced with #7352: jobs fail immediately if any command has a non-zero exit code. The way we obtained the exit code of the `diff` command was incompatible with this policy, which is why we currently never upload any docs to `docs-ci`.

3 years agoEliminate last static calls to rewriter from smt layer (#7355)
Andrew Reynolds [Wed, 20 Oct 2021 21:07:09 +0000 (16:07 -0500)]
Eliminate last static calls to rewriter from smt layer (#7355)

3 years agoMake SyGuS solver robust to non-closed enumerable sorts (#7417)
Andrew Reynolds [Wed, 20 Oct 2021 20:47:06 +0000 (15:47 -0500)]
Make SyGuS solver robust to non-closed enumerable sorts (#7417)

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.

3 years agoDo not construct instantiation for checking propagating instantiations spurious ...
Andrew Reynolds [Wed, 20 Oct 2021 20:34:33 +0000 (15:34 -0500)]
Do not construct instantiation for checking propagating instantiations spurious (#7390)

This makes the check for when an instantiation is "propagating" faster by not constructing the substitution + rewriting of the entire formula, and instead threading the substitution through the entailment check utility's evaluateTerm utility.

On a handful of challenge Facebook benchmarks, we go 35 seconds -> 18 seconds with this change.

This also eliminates the argument exp to the evaluateTerm method, which is no longer used, and eliminates hasSubs from several methods, which is redundant.

3 years agoCheck whether abduct option is enabled (#7418)
Andrew Reynolds [Wed, 20 Oct 2021 19:48:11 +0000 (14:48 -0500)]
Check whether abduct option is enabled (#7418)

This addresses one of the issues related to #6605.

3 years agoapi: Rename get(BV|FP)*Size functions for consistency. (#7428)
Aina Niemetz [Wed, 20 Oct 2021 19:14:59 +0000 (12:14 -0700)]
api: Rename get(BV|FP)*Size functions for consistency. (#7428)

3 years ago[proofs] Alethe: Documentation on Translation (#7394)
Lachnitt [Wed, 20 Oct 2021 18:50:38 +0000 (11:50 -0700)]
[proofs] Alethe: Documentation on Translation (#7394)

Provides background on the translation into the Alethe calculus that is common to all rules.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
3 years agoAdd LFSC signature for n-ary programs (#7360)
Andrew Reynolds [Wed, 20 Oct 2021 17:27:33 +0000 (12:27 -0500)]
Add LFSC signature for n-ary programs (#7360)

This is the last utility signature. Theory signatures will be added afterwards.

3 years agoUse codatatype bound variables for codatatype values (#7425)
Andrew Reynolds [Wed, 20 Oct 2021 16:49:53 +0000 (11:49 -0500)]
Use codatatype bound variables for codatatype values (#7425)

Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts.

3 years agoReimplement support for relational triggers (#7063)
Andrew Reynolds [Wed, 20 Oct 2021 16:14:50 +0000 (11:14 -0500)]
Reimplement support for relational triggers (#7063)

This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.

This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.

This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.

3 years agoDo not make assumption about model for Boolean variables in FMF (#7407)
Andrew Reynolds [Wed, 20 Oct 2021 14:34:10 +0000 (09:34 -0500)]
Do not make assumption about model for Boolean variables in FMF (#7407)

Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.

Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.

3 years agoCorrectly parse uninterpreted constant values in get-value (#7393)
Andrew Reynolds [Wed, 20 Oct 2021 11:57:44 +0000 (06:57 -0500)]
Correctly parse uninterpreted constant values in get-value (#7393)

SMT-LIB indicates that abstract values can appear in terms as arguments to `get-value`.  This is not currently the case, as pointed out by #6908.

This updates our parser so that bindings are added to the symbol table for all uninterpreted constants in the model whenever we parse a `get-value` term.

Fixes #6908.

3 years agoAvoid escaping `double-quotes` twice. (#7409)
Abdalrhman Mohamed [Wed, 20 Oct 2021 01:11:53 +0000 (20:11 -0500)]
Avoid escaping `double-quotes` twice. (#7409)

With -o raw-benchmark, The command:

(echo """")
was printed as

(echo """""""")
because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once.

3 years agoMake proofs of rewrites robust to use in internal subsolvers (#7411)
Andrew Reynolds [Wed, 20 Oct 2021 00:35:14 +0000 (19:35 -0500)]
Make proofs of rewrites robust to use in internal subsolvers (#7411)

We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance.

This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique.

3 years agoAdd basic regular expression type enumerator (#7416)
Andrew Reynolds [Wed, 20 Oct 2021 00:24:32 +0000 (19:24 -0500)]
Add basic regular expression type enumerator (#7416)

The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.

It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.

3 years agoFix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)
Andrew Reynolds [Tue, 19 Oct 2021 23:53:56 +0000 (18:53 -0500)]
Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)

Fixes a proof checking failure during post-processing.

Fixes a rare case where the RHS of equality resolve step requires a symmetry step.