cvc5.git
3 years agoEnable CI for Junit tests (#7436)
mudathirmahgoub [Wed, 3 Nov 2021 21:32:10 +0000 (16:32 -0500)]
Enable CI for Junit tests (#7436)

This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.

3 years agoFix debug trace for miplib (#7563)
Andrew Reynolds [Wed, 3 Nov 2021 21:12:37 +0000 (16:12 -0500)]
Fix debug trace for miplib (#7563)

A debug trace on miplib referred to a possibly out of bounds child.

3 years agoRefactor skolem construction (#7561)
Andrew Reynolds [Wed, 3 Nov 2021 17:43:02 +0000 (12:43 -0500)]
Refactor skolem construction (#7561)

This makes all methods for constructing skolems local to SkolemManager.

It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.

This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.

3 years agoFormalize more string skolems (#7554)
Andrew Reynolds [Wed, 3 Nov 2021 16:12:18 +0000 (11:12 -0500)]
Formalize more string skolems (#7554)

This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.

Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.

3 years agoFix preregistration for floating point theory (#7558)
Andrew Reynolds [Wed, 3 Nov 2021 10:27:20 +0000 (05:27 -0500)]
Fix preregistration for floating point theory (#7558)

Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.

Fixes cvc5/cvc5-projects#329.

3 years agobv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)
Mathias Preiner [Tue, 2 Nov 2021 22:01:01 +0000 (15:01 -0700)]
bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)

When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates.

Fixes the nightly failure.

3 years agoMove `fmf.card` printing code. (#7559)
Abdalrhman Mohamed [Tue, 2 Nov 2021 21:45:44 +0000 (16:45 -0500)]
Move `fmf.card` printing code. (#7559)

The code for printing fmf.card does not run in its current location. This PR moves the code to a different switch statement to ensure that it runs.

3 years agoAdd printing methods for some commands. (#7557)
Abdalrhman Mohamed [Tue, 2 Nov 2021 20:14:19 +0000 (15:14 -0500)]
Add printing methods for some commands. (#7557)

This PR is a step towards enabling -o raw-benchmark. It adds printing methods for some of the new commands and fixes some other miscellaneous issues.

3 years agoImprove syntax for fmf cardinality constraints (#7556)
Andrew Reynolds [Tue, 2 Nov 2021 19:58:13 +0000 (14:58 -0500)]
Improve syntax for fmf cardinality constraints (#7556)

This is an experimental extension of smt2.

3 years agoAdd LFSC signature for quantifiers (#7540)
Andrew Reynolds [Tue, 2 Nov 2021 13:16:29 +0000 (08:16 -0500)]
Add LFSC signature for quantifiers (#7540)

Also includes a fix for the Boolean signature. After the strings PR and this one, the initial LFSC signature is complete.

3 years agoFix setDefaults() for proofs with bitblast-internal. (#7552)
Mathias Preiner [Tue, 2 Nov 2021 01:26:26 +0000 (18:26 -0700)]
Fix setDefaults() for proofs with bitblast-internal. (#7552)

3 years agobv: Remove remaining Rewriter::rewrite calls. (#7545)
Mathias Preiner [Tue, 2 Nov 2021 01:00:12 +0000 (18:00 -0700)]
bv: Remove remaining Rewriter::rewrite calls. (#7545)

3 years agoMake quant elimination robust to presence of other quantified formulas (#7551)
Andrew Reynolds [Tue, 2 Nov 2021 00:17:38 +0000 (19:17 -0500)]
Make quant elimination robust to presence of other quantified formulas (#7551)

Fixes #4813

3 years agoEliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)
Andrew Reynolds [Mon, 1 Nov 2021 23:34:41 +0000 (18:34 -0500)]
Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)

There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter.

3 years agoWeaken assertion in CEGQI (#7548)
Andrew Reynolds [Mon, 1 Nov 2021 23:04:16 +0000 (18:04 -0500)]
Weaken assertion in CEGQI (#7548)

The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.

Fixes #7537.

3 years agoAdd explicit option enum value __MAX_VALUE (#7547)
Gereon Kremer [Mon, 1 Nov 2021 22:28:54 +0000 (15:28 -0700)]
Add explicit option enum value __MAX_VALUE (#7547)

This PR fixes a subtle issue with the dict ordering changing across different python versions.
To store the flags of -o, we store a bitset with the index being the enum value cast to size_t. To specify the bitset size, we simply used the last enum value (in the toml file). This, however, assumes that the order within dictionaries is stable: toml simply puts all modes in a python dict.
This PR avoids this issue by introducing an explicit __MAX_VALUE enum value. Note that this also avoids the need to update the bitset definition when new output tags are added.

3 years agobv: Remove layered solver. (#7455)
Mathias Preiner [Mon, 1 Nov 2021 20:59:47 +0000 (13:59 -0700)]
bv: Remove layered solver. (#7455)

This commit removes the old bit-vector solver code.

3 years agoapi: Fix documentation for kind IAND. (#7536)
Aina Niemetz [Mon, 1 Nov 2021 20:25:32 +0000 (13:25 -0700)]
api: Fix documentation for kind IAND. (#7536)

3 years agoFix a couple of issues with uploading docs for releases (#7543)
Gereon Kremer [Mon, 1 Nov 2021 20:09:41 +0000 (13:09 -0700)]
Fix a couple of issues with uploading docs for releases (#7543)

This PR fixes multiple issues with uploading docs for releases: the regular upload moved the generated docs, so the release upload would not find the docs; the check whether we have a release was incorrect; we probably want $NAME instead of docs-$NAME here.

3 years agoClean up CLN includes (#7544)
Gereon Kremer [Mon, 1 Nov 2021 19:51:44 +0000 (12:51 -0700)]
Clean up CLN includes (#7544)

This PR pushes a couple of includes for the CLN integers from the header into the source files.

3 years agoAdd fuzzing target for murxla (#7490)
Gereon Kremer [Mon, 1 Nov 2021 18:37:22 +0000 (11:37 -0700)]
Add fuzzing target for murxla (#7490)

This PR aims to make it easier for cvc5 developers to fuzz the current cvc5 working copy with murxla.
It adds a new external project Murxla-EP that builds murxla, linking (only) against cvc5. It depends (indirectly) on the make install target, which is called with a custom install prefix for this purpose.
As the murxla repository is not public yet, automatically downloading it does not work, but instead we need the user to clone it manually for now.
The user should simply execute make fuzz-murxla and follow the instructions.

3 years agoFix upwards closure for relations (#7515)
Andrew Reynolds [Mon, 1 Nov 2021 14:44:13 +0000 (09:44 -0500)]
Fix upwards closure for relations (#7515)

This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms).

It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join.

It disables a regression that times out after these fixes, and does further cleanup.

3 years agoReplace more static options accesses (#7531)
Gereon Kremer [Mon, 1 Nov 2021 12:08:09 +0000 (05:08 -0700)]
Replace more static options accesses (#7531)

This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.

3 years agoRefactor DidYouMean (#7535)
Gereon Kremer [Mon, 1 Nov 2021 10:52:55 +0000 (03:52 -0700)]
Refactor DidYouMean (#7535)

This refactors the `DidYouMean` class, which is used to make helpful suggestions for misspelled tags and options. It uses `std::vector` instead of `std::set`, moves it from `options` to `util` (so that we can keep using it in both libcvc5 and the driver) and generally modernizes the code a bit. Also, it replaces the stand-alone and never executed test by a regular unit test.

3 years agoapi: Add guard against querying value from term with free vars. (#7529)
Mathias Preiner [Sun, 31 Oct 2021 19:47:28 +0000 (12:47 -0700)]
api: Add guard against querying value from term with free vars. (#7529)

3 years agoFix soundess issue for bags with negative multiplicity (#7539)
mudathirmahgoub [Sun, 31 Oct 2021 14:07:36 +0000 (09:07 -0500)]
Fix soundess issue for bags with negative multiplicity (#7539)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
One error was with the rewrite rule (bag.count x (bag x c) = c which did not account for cases when c is negative.
This conflicts with fact that all multiplicities are non-negative.
Another error was that the difference_remove inference rule didn't consider the negative case for (count e B)

(= (count e (difference_remove A B)) (ite (=  (count e B) 0) (count e A) 0))) ; not enough
(= (count e (difference_remove A B)) (ite (<= (count e B) 0) (count e A) 0))) ; the right rule

3 years agoRemove assertSkeleton for bag elements during model building (#7538)
mudathirmahgoub [Sun, 31 Oct 2021 13:50:38 +0000 (08:50 -0500)]
Remove  assertSkeleton for bag elements during model building   (#7538)

This PR fixes a bug found by cvc5 fuzzy sygus.

3 years agoFix proof of nl lemma for a corner case (#7530)
Gereon Kremer [Fri, 29 Oct 2021 22:37:39 +0000 (15:37 -0700)]
Fix proof of nl lemma for a corner case (#7530)

This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.

3 years agoStart post-release for 0.0.3
Mathias Preiner [Fri, 29 Oct 2021 22:25:01 +0000 (15:25 -0700)]
Start post-release for 0.0.3

3 years agoBump version to 0.0.3
Mathias Preiner [Fri, 29 Oct 2021 22:25:01 +0000 (15:25 -0700)]
Bump version to 0.0.3

3 years agoRemove options::X__numValues (#7419)
Gereon Kremer [Fri, 29 Oct 2021 19:05:05 +0000 (12:05 -0700)]
Remove options::X__numValues (#7419)

This PR removes yet another special purpose options detail that is only used in a single place: X__numValues currently holds the number of modes for an option, that is the number of elements of the respective enums. It is solely used to obtain the size of the std::bitset used to store the flags passed to the -o option. However, it can easily be replaced using the last mode.

This PR also improves a bit on options-related documentation.

3 years agoMinor cleanup of proof messages (#7494)
Andrew Reynolds [Fri, 29 Oct 2021 18:33:30 +0000 (13:33 -0500)]
Minor cleanup of proof messages (#7494)

Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.

3 years agoFix model construction for higher order involving irrelevant function terms (#7526)
Andrew Reynolds [Fri, 29 Oct 2021 17:50:59 +0000 (12:50 -0500)]
Fix model construction for higher order involving irrelevant function terms (#7526)

This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.

3 years agoAdd PfRule ARITH_POLY_NORM (#7501)
Andrew Reynolds [Fri, 29 Oct 2021 16:36:26 +0000 (11:36 -0500)]
Add PfRule ARITH_POLY_NORM (#7501)

This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.

3 years agoImprovements for LFSC proof conversion (#7524)
Andrew Reynolds [Fri, 29 Oct 2021 13:32:06 +0000 (08:32 -0500)]
Improvements for LFSC proof conversion (#7524)

Includes miscellaneous improvements and fixes to the LFSC proof conversion from proof-new in preparation for CI on master.

3 years agoRemove static access to options in decision folder (#7527)
Gereon Kremer [Fri, 29 Oct 2021 00:28:29 +0000 (17:28 -0700)]
Remove static access to options in decision folder (#7527)

This PR replaces static accesses to options (options::foo()) by using the options object provided via the environment.

3 years agoFix proof for xor in circuit propagator (#7525)
Gereon Kremer [Thu, 28 Oct 2021 22:03:07 +0000 (15:03 -0700)]
Fix proof for xor in circuit propagator (#7525)

This PR fixes another double negation issue in the circuit propagator.
Fixes cvc5/cvc5-projects#332.

3 years agoCombine `--static` and `--static-binary` (#7520)
Gereon Kremer [Thu, 28 Oct 2021 19:30:13 +0000 (12:30 -0700)]
Combine `--static` and `--static-binary` (#7520)

This PR combines the two configure flags --static and --static-binary into a single --static. Consequently, the two corresponding cmake variables are combined as well. The two variables have been implying each other for some time now and were only used to build not-completely-static binaries for MacOS, which is now done automatically anyway.

3 years ago[proofs] Fix assertion in EqProof conversion (#7522)
Haniel Barbosa [Thu, 28 Oct 2021 18:59:43 +0000 (15:59 -0300)]
[proofs] Fix assertion in EqProof conversion  (#7522)

Also improves a few traces.

Fixes cvc5/cvc5-projects#330

3 years agoAdd support for checking if a `-Wno` flag exists before using it (#7514)
Andrew V. Jones [Thu, 28 Oct 2021 18:06:38 +0000 (19:06 +0100)]
Add support for checking if a `-Wno` flag exists before using it (#7514)

This PR resolves that issue by checking that a -W<error-class> flag exists before trying to use the -Wno-<error-class> flag.

3 years agoAdd a `define-fun` command for each `:named` term. (#7308)
Abdalrhman Mohamed [Thu, 28 Oct 2021 17:04:06 +0000 (12:04 -0500)]
Add a `define-fun` command for each `:named` term. (#7308)

This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.

3 years agoProperly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)
Andrew Reynolds [Thu, 28 Oct 2021 15:45:19 +0000 (10:45 -0500)]
Properly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)

Fixes one of the issues raised in cvc5/cvc5-projects#331, the other involves missing skolem definitions for str.replace_all_re @4tXJ7f .

This properly guards cases of proof reconstruction for STRINGS_EXTF_EQ_REW where an intermediate step in the proof checker inferring something stronger than what it is asked to prove. In particular, substitution+rewriting is more powerful than congruence+rewriting:
s=x => (str.<= t s) ----> (= r "") since (str.<= t "") ----> (= r "")
but additionally:
(str.<= t s) * { s -> x } ----> true, which is possible if s occurs as a subterm of t.

The proof reconstruction for STRINGS_EXTF_EQ_REW is not precise as there are several other aspects that are not covered. After this PR, we properly guard and fail to reconstruct if the above issue arises, so the assertion failure will not throw.

3 years agoLFSC signature for linear arithmetic (#7445)
Andrew Reynolds [Thu, 28 Oct 2021 15:31:29 +0000 (10:31 -0500)]
LFSC signature for linear arithmetic (#7445)

3 years agoLFSC signature for CNF (#7444)
Andrew Reynolds [Thu, 28 Oct 2021 15:12:34 +0000 (10:12 -0500)]
LFSC signature for CNF (#7444)

3 years agoLFSC signature for Booleans (#7443)
Andrew Reynolds [Thu, 28 Oct 2021 14:53:49 +0000 (09:53 -0500)]
LFSC signature for Booleans (#7443)

3 years agoLFSC signature for equality (#7442)
Andrew Reynolds [Thu, 28 Oct 2021 14:39:07 +0000 (09:39 -0500)]
LFSC signature for equality (#7442)

3 years agoFix `(set-info <sexpr>)` parsing and printing bugs. (#7427)
Abdalrhman Mohamed [Thu, 28 Oct 2021 11:26:49 +0000 (06:26 -0500)]
Fix `(set-info <sexpr>)` parsing and printing bugs. (#7427)

Given
```smt2
(set-info :source (0 1 True False x ""))
```
`cvc5` currently prints the command below with `-o raw-benchmark`
```smt2
(set-info : |(0 1 True False x )|)
```
This PR ensures that `cvc5` correctly prints the command by
- Parsing and storing keywords eagerly before parsing their values.
- Removing pre-processing steps done to symbols and string literals.

3 years agoRemove separate cpp docs for UnknownExplanation (#7516)
Gereon Kremer [Thu, 28 Oct 2021 10:07:59 +0000 (03:07 -0700)]
Remove separate cpp docs for UnknownExplanation (#7516)

This removes the separate documentation for the `UnknownExplanation` enum, as it is already included in the documentation of the `Result` class.

3 years agoBuild shared and static in CI (#7472)
Gereon Kremer [Thu, 28 Oct 2021 01:08:13 +0000 (18:08 -0700)]
Build shared and static in CI (#7472)

This PR changes our strategy to deal with shared vs. static builds in CI jobs.
All jobs now build cvc5 both shared and static by default. The builds happen in different build directories (build-shared and build-static), and we configure ccache such that these two build directories share a common cache.

3 years agoAdd missing API checks to getValue (#7475)
Andrew Reynolds [Wed, 27 Oct 2021 23:52:44 +0000 (18:52 -0500)]
Add missing API checks to getValue (#7475)

Fixes cvc5/cvc5-projects#307.

3 years agoAdd comments for arith type rules. (#7488)
Gereon Kremer [Wed, 27 Oct 2021 23:40:31 +0000 (16:40 -0700)]
Add comments for arith type rules. (#7488)

Add comments for the arithmetic type rules.

Fixes cvc5/cvc5-projects#273.

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.