cvc5.git
3 years agoMake `--solve-int-as-bv=X` robust to rewriting (#6722)
Andres Noetzli [Wed, 9 Jun 2021 20:31:45 +0000 (13:31 -0700)]
Make `--solve-int-as-bv=X` robust to rewriting (#6722)

After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.

3 years agoUpdate CVC4 URLs/macros (#6666)
Andres Noetzli [Wed, 9 Jun 2021 20:14:38 +0000 (13:14 -0700)]
Update CVC4 URLs/macros (#6666)

3 years agoReorder ITE rewrites (#6723)
Andres Noetzli [Wed, 9 Jun 2021 19:53:31 +0000 (12:53 -0700)]
Reorder ITE rewrites (#6723)

Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.

3 years agoMake squasing more robust (#6713)
Gereon Kremer [Wed, 9 Jun 2021 19:25:04 +0000 (21:25 +0200)]
Make squasing more robust (#6713)

This PR makes squashing olds commits in the docs-cleanup CI job more robust: it makes sure that the squash commit has a proper commit date and that we gracefully handle if there is nothing to squash.

3 years agoIntegrate learned literal manager into preprocessing pass context (#6718)
Andrew Reynolds [Wed, 9 Jun 2021 18:52:13 +0000 (13:52 -0500)]
Integrate learned literal manager into preprocessing pass context (#6718)

Towards "learned rewrite" preprocessing pass / improvements to Int <-> BV.

3 years agoFixes related to printing tuples, define-fun commands in smt2 (#6679)
Andrew Reynolds [Wed, 9 Jun 2021 17:50:31 +0000 (12:50 -0500)]
Fixes related to printing tuples, define-fun commands in smt2 (#6679)

This PR fixes some initial issues with printing datatypes in smt2.

It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.

3 years agoPush complex check inside GetInstantiationsCommand (#6715)
Gereon Kremer [Wed, 9 Jun 2021 17:15:30 +0000 (19:15 +0200)]
Push complex check inside GetInstantiationsCommand (#6715)

This PR pushes a rather complex check from the CommandExecutor inside the GetInstantiationsCommand.
The aim is to only use the instFormatMode option in the library (command.cpp) but not the main driver (command_executor.cpp).

3 years agoUpdate options for SMT-COMP (#6704)
Andres Noetzli [Wed, 9 Jun 2021 16:40:10 +0000 (09:40 -0700)]
Update options for SMT-COMP (#6704)

This commit removes obsolete options for BV and strings logics, and
updates QF_NIA to spend more time on our best configuration.

Co-authored-by: Gereon Kremer nafur42@gmail.com
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
3 years ago[Optimization] support for push/pop (#6706)
Ouyancheng [Wed, 9 Jun 2021 15:53:16 +0000 (08:53 -0700)]
[Optimization] support for push/pop (#6706)

Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.

3 years agoRemoving spurious HO checks (#6707)
Haniel Barbosa [Wed, 9 Jun 2021 14:34:22 +0000 (11:34 -0300)]
Removing spurious HO checks (#6707)

3 years agoRequire statistics for regression (#6714)
Gereon Kremer [Wed, 9 Jun 2021 14:03:04 +0000 (16:03 +0200)]
Require statistics for regression (#6714)

This PR makes a new regression explicitly require statistics.

3 years agodocs: Migrate separation logic theory reference. (#6702)
Aina Niemetz [Wed, 9 Jun 2021 07:20:14 +0000 (00:20 -0700)]
docs: Migrate separation logic theory reference. (#6702)

This migrates page https://cvc4.github.io/separation-logic.

3 years agodocs: Fix `Kind` description (#6712)
Andres Noetzli [Wed, 9 Jun 2021 07:09:26 +0000 (00:09 -0700)]
docs: Fix `Kind` description (#6712)

This commit changes the Kind description not to include C/C++
preprocessor statements and updates the kind of bit-vector addtion.
It also marks some of the information as internal to exclude it from the
public documentation.

3 years agoFix for 2 dimensional dependent bounded quantifiers (#6710)
Andrew Reynolds [Tue, 8 Jun 2021 23:47:40 +0000 (18:47 -0500)]
Fix for 2 dimensional dependent bounded quantifiers (#6710)

This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.

Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.

3 years agoAdd learned literal manager utility (#6709)
Andrew Reynolds [Tue, 8 Jun 2021 21:50:41 +0000 (16:50 -0500)]
Add learned literal manager utility (#6709)

This is a simple class to maintain a list of literals that we have learned that may be useful during preprocessing.

This is work towards a "learned rewrite" preprocessing pass / better support for Int/BV translations during preprocessing.

3 years agoFix statistics option handler (#6703)
Gereon Kremer [Tue, 8 Jun 2021 15:21:45 +0000 (17:21 +0200)]
Fix statistics option handler (#6703)

This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.

3 years agoMake env hold a pointer to the original options to properly initialize subsolvers...
Gereon Kremer [Tue, 8 Jun 2021 13:43:13 +0000 (15:43 +0200)]
Make env hold a pointer to the original options to properly initialize subsolvers (#6705)

This PR extends the Env class to hold a pointer to the original options that are owned by the api::Solver. These original options will be used to properly initialize subsolvers as using the current options leads to subtle issues as setDefaults is not (in general) idempotent.

3 years agoRemove `binary_name` option (#6693)
Gereon Kremer [Tue, 8 Jun 2021 07:05:35 +0000 (09:05 +0200)]
Remove `binary_name` option (#6693)

The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().

3 years agoChange output of getRealValue to a fraction. (#6692)
Alex Ozdemir [Tue, 8 Jun 2021 06:42:59 +0000 (23:42 -0700)]
Change output of getRealValue to a fraction. (#6692)

Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.

We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.

Also, document some (potential) weirdness with calling mkReal on floating-point values.

3 years agoMake TheoryUF compatible with central equality engine (#6695)
Andrew Reynolds [Tue, 8 Jun 2021 06:29:10 +0000 (01:29 -0500)]
Make TheoryUF compatible with central equality engine (#6695)

Work towards central equality engine.

This does some minor reorganization to TheoryUF, related to UF+cardinality constraints that makes it compatible with central equality engine. In particular, preNotifyFact is removed in favor of adding conflicts after cardinality constraints are added to the equality engine. This ensures that the central equality engine can explain conflicts that involve cardinality constraints (which will no longer be the responsibility of UF when --ee-mode=central).

3 years agoFix str.update reduction (#6696)
Andrew Reynolds [Tue, 8 Jun 2021 06:11:28 +0000 (01:11 -0500)]
Fix str.update reduction (#6696)

Fixes the 2nd benchmark from #6653.

3 years ago(proof-new) Fix missing connection in trust substitution proofs (#6685)
Andrew Reynolds [Mon, 7 Jun 2021 17:44:20 +0000 (12:44 -0500)]
(proof-new) Fix missing connection in trust substitution proofs (#6685)

This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.

Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.

3 years agoRemove `Options::wasSetByUser()` (#6682)
Gereon Kremer [Mon, 7 Jun 2021 17:00:10 +0000 (19:00 +0200)]
Remove `Options::wasSetByUser()` (#6682)

This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.

3 years ago(proof-new) Lazy proof chain debug names (#6680)
Andrew Reynolds [Mon, 7 Jun 2021 14:09:59 +0000 (09:09 -0500)]
(proof-new) Lazy proof chain debug names (#6680)

3 years agoSupport public option modules (#6691)
Gereon Kremer [Sun, 6 Jun 2021 11:09:40 +0000 (13:09 +0200)]
Support public option modules (#6691)

This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).

3 years agoRemove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)
Andres Noetzli [Sat, 5 Jun 2021 03:22:57 +0000 (20:22 -0700)]
Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)

Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.

3 years agoMiscellaneous changes from central ee branch (#6687)
Andrew Reynolds [Fri, 4 Jun 2021 21:05:43 +0000 (16:05 -0500)]
Miscellaneous changes from central ee branch (#6687)

Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.

3 years agopow2: header file for pow2 solver (#6676)
yoni206 [Fri, 4 Jun 2021 17:01:45 +0000 (10:01 -0700)]
pow2: header file for pow2 solver (#6676)

This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests.

3 years agobv: Enable bitblast solver by default. (#6660)
Mathias Preiner [Fri, 4 Jun 2021 13:30:35 +0000 (06:30 -0700)]
bv: Enable bitblast solver by default. (#6660)

This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.

3 years agoAdd missing dereference (#6684)
Gereon Kremer [Fri, 4 Jun 2021 13:17:57 +0000 (15:17 +0200)]
Add missing dereference (#6684)

3 years agoFix handling of start index in `str.indexof_re` (#6674)
Andres Noetzli [Fri, 4 Jun 2021 00:41:40 +0000 (17:41 -0700)]
Fix handling of start index in `str.indexof_re` (#6674)

Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.

3 years agoSome cleanup in `mkoptions.py` (#6667)
Gereon Kremer [Fri, 4 Jun 2021 00:14:27 +0000 (02:14 +0200)]
Some cleanup in `mkoptions.py` (#6667)

This PR does some general cleanup in the mkoptions.py script: removal of obsolete code and some fixes to the comments.

3 years agodocs: Migrate datatypes theory reference. (#6662)
Aina Niemetz [Fri, 4 Jun 2021 00:07:05 +0000 (17:07 -0700)]
docs: Migrate datatypes theory reference. (#6662)

This migrates https://cvc4.github.io/datatypes.

3 years agoAdding unit tests for the datatypes python API (#6658)
yoni206 [Thu, 3 Jun 2021 23:57:29 +0000 (16:57 -0700)]
Adding unit tests for the datatypes python API (#6658)

This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API.
This is the last part of the python api unit tests for datatypes.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
3 years agoSimplify automatic set-logic in smt2 parser (#6678)
Andrew Reynolds [Thu, 3 Jun 2021 22:49:32 +0000 (17:49 -0500)]
Simplify automatic set-logic in smt2 parser (#6678)

This simplifies the smt2 parser so that automatically setting the logic is done directly instead of being buffered as a command.

This prevents spurious errors for features that require (A) checking the logic is set and (B) fully intialize the underlying SMT engine.  `declare-pool` is an example of an smt2 command where the user will get an error (instead of a warning) when set-logic is not used due to setting the logic, after fully initing SMT engine and then executing the buffered set-logic command.

Note this should also make dump=raw-benchmark more accurate (no set-logic is included when dumping benchmarks with no set-logic command).

3 years ago[GitHub Actions] Make caching of dependencies depend on image version (#6677)
Andres Noetzli [Thu, 3 Jun 2021 22:26:52 +0000 (15:26 -0700)]
[GitHub Actions] Make caching of dependencies depend on image version (#6677)

Our Clang builds started to fail to link when the environment changed. This commit changes our CI to only use cached dependencies if the build environment has not changed.

3 years agoRenaming pow2 to p2 in regression tests (#6675)
yoni206 [Thu, 3 Jun 2021 14:39:55 +0000 (07:39 -0700)]
Renaming pow2 to p2 in regression tests (#6675)

We plan to add a unary pow2 operator to cvc5, that is obtained from the binary operator pow by fixing the first argument to 2.
An initial working branch is here: https://github.com/yoni206/cvc5/tree/pow2

This PR does the first step, which is to rename some uninterpreted symbols in regression tests from pow2 to p2, to avoid clashing with the new operator.

3 years agoRemove references to `bv-div-zero-const` in docs (#6672)
Andres Noetzli [Wed, 2 Jun 2021 21:37:48 +0000 (14:37 -0700)]
Remove references to `bv-div-zero-const` in docs (#6672)

The bv-div-zero-const option has been removed and is now always
enabled, so this commit updates the documentation of the kinds to
reflect that. It also makes the language to describe the special cases a
bit more uniform.

3 years agoFixes for printing define-fun-rec (#6673)
Andrew Reynolds [Wed, 2 Jun 2021 21:16:40 +0000 (16:16 -0500)]
Fixes for printing define-fun-rec (#6673)

3 years agoRemove option to ignore negative memberships (#6665)
Andres Noetzli [Wed, 2 Jun 2021 19:41:14 +0000 (12:41 -0700)]
Remove option to ignore negative memberships (#6665)

Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.

3 years agoAdding getters to the python API and testing them (#6652)
yoni206 [Wed, 2 Jun 2021 19:30:46 +0000 (12:30 -0700)]
Adding getters to the python API and testing them (#6652)

This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.

3 years agoRemove redundant logic ALL_SUPPORTED. (#6664)
Aina Niemetz [Wed, 2 Jun 2021 17:16:26 +0000 (10:16 -0700)]
Remove redundant logic ALL_SUPPORTED. (#6664)

3 years agoMove `toPythonObj` tests to the new API unit test directory (#6656)
yoni206 [Wed, 2 Jun 2021 16:47:09 +0000 (09:47 -0700)]
Move `toPythonObj` tests to the new API unit test directory (#6656)

This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.

3 years agoUse proper variable name (#6670)
Gereon Kremer [Wed, 2 Jun 2021 16:01:08 +0000 (18:01 +0200)]
Use proper variable name (#6670)

This PR fixes the driver which used an incorrect variable name in competition mode.

3 years agoFix unsat core proofs (#6655)
Andrew Reynolds [Wed, 2 Jun 2021 15:28:36 +0000 (10:28 -0500)]
Fix unsat core proofs (#6655)

Fixes cases of satisfiable unsat cores when proofs are enabled.

Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.

3 years agoMake `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)
Andres Noetzli [Wed, 2 Jun 2021 13:50:51 +0000 (06:50 -0700)]
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict  (#6663)

Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.

3 years agoRemove `Options::operator[]` (#6649)
Gereon Kremer [Wed, 2 Jun 2021 13:21:22 +0000 (15:21 +0200)]
Remove `Options::operator[]` (#6649)

This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.

3 years agoMove public wrapper functions out of options class (#6600)
Gereon Kremer [Wed, 2 Jun 2021 12:11:05 +0000 (14:11 +0200)]
Move public wrapper functions out of options class (#6600)

This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.

3 years agoFix issues with double negation in circuit propagator (#6669)
Gereon Kremer [Wed, 2 Jun 2021 11:55:40 +0000 (13:55 +0200)]
Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.

3 years agoFix issues when poly is disabled (#6668)
Gereon Kremer [Wed, 2 Jun 2021 10:11:13 +0000 (12:11 +0200)]
Fix issues when poly is disabled (#6668)

Recent changes introduced issues when libpoly is disabled.

3 years agoMake `Options::assign()` specializations free functions (#6648)
Gereon Kremer [Wed, 2 Jun 2021 06:55:24 +0000 (08:55 +0200)]
Make `Options::assign()` specializations free functions (#6648)

This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.

3 years agoDo manual squash cleanup for docs (#6646)
Gereon Kremer [Wed, 2 Jun 2021 06:29:02 +0000 (08:29 +0200)]
Do manual squash cleanup for docs (#6646)

This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):

- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch

3 years agodocs: Migrate input languages page. (#6659)
Aina Niemetz [Wed, 2 Jun 2021 00:21:56 +0000 (17:21 -0700)]
docs: Migrate input languages page. (#6659)

This migrates page https://cvc4.github.io/input-languages.

3 years agodocs: Restructure index page, fix style issue. (#6657)
Aina Niemetz [Wed, 2 Jun 2021 00:05:52 +0000 (17:05 -0700)]
docs: Restructure index page, fix style issue. (#6657)

3 years agoSome additions to the datatypes python API (#6640)
yoni206 [Tue, 1 Jun 2021 21:24:43 +0000 (14:24 -0700)]
Some additions to the datatypes python API (#6640)

This commit makes the following additions, in order to sync the python API with the cpp API.

1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.

3 years agoUse top-level substitutions in ITE simp (#6651)
Andrew Reynolds [Tue, 1 Jun 2021 18:58:49 +0000 (13:58 -0500)]
Use top-level substitutions in ITE simp (#6651)

With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.

Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.

This is required for SMT-COMP.

3 years agoDisable timeout regressions (#6650)
Andrew Reynolds [Tue, 1 Jun 2021 14:59:41 +0000 (09:59 -0500)]
Disable timeout regressions (#6650)

Disables two regressions that have been timing out causing nightlies to fail.

3 years agoFP value support in python API (#6644)
yoni206 [Tue, 1 Jun 2021 09:40:54 +0000 (02:40 -0700)]
FP value support in python API (#6644)

This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.

getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.

3 years agoRemove Options::ref() (#6647)
Gereon Kremer [Mon, 31 May 2021 14:05:39 +0000 (16:05 +0200)]
Remove Options::ref() (#6647)

This PR gets rid of the templated Options::ref() method (and all its specializations for every option).

3 years agoRemove invalid options from run scripts (#6645)
Andres Noetzli [Mon, 31 May 2021 04:13:37 +0000 (21:13 -0700)]
Remove invalid options from run scripts (#6645)

This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.

3 years agoUpdate `toPythonObj` to use new getters -- part 1 (#6623)
yoni206 [Mon, 31 May 2021 00:56:14 +0000 (17:56 -0700)]
Update `toPythonObj` to use new getters -- part 1 (#6623)

Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.

A future PR will add more getters to the python API.

Co-authored-by: Gereon Kremer nafur42@gmail.com
3 years agoCompute model values for nested sequences in order (#6631)
Andres Noetzli [Mon, 31 May 2021 00:35:08 +0000 (17:35 -0700)]
Compute model values for nested sequences in order (#6631)

Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.

While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.

This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.

cc @yoni206

3 years agoRemove `Options::set()` method (#6556)
Gereon Kremer [Sat, 29 May 2021 07:09:34 +0000 (09:09 +0200)]
Remove `Options::set()` method (#6556)

This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.

3 years ago(Optimization) remove popObjective, add resetObjectives, rename pushObjective =>...
Ouyancheng [Fri, 28 May 2021 21:00:16 +0000 (14:00 -0700)]
(Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634)

In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:

optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.

3 years agoPython API: bugfix + translating tests from cpp unit tests (#6559)
yoni206 [Fri, 28 May 2021 20:28:56 +0000 (13:28 -0700)]
Python API: bugfix + translating tests from cpp unit tests (#6559)

This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp

The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.

3 years agoAdd non-templated method to set option defaults (#6540)
Gereon Kremer [Fri, 28 May 2021 19:46:54 +0000 (21:46 +0200)]
Add non-templated method to set option defaults (#6540)

This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.

3 years agoDisable `--jh-rlv-order` for slow regressions (#6633)
Andres Noetzli [Fri, 28 May 2021 14:10:15 +0000 (07:10 -0700)]
Disable `--jh-rlv-order` for slow regressions (#6633)

This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.

3 years ago`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)
Andres Noetzli [Fri, 28 May 2021 03:28:20 +0000 (20:28 -0700)]
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)

Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.

3 years agoFix regular expression aggressive elim (#6627)
Andrew Reynolds [Thu, 27 May 2021 23:22:28 +0000 (18:22 -0500)]
Fix regular expression aggressive elim (#6627)

Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.

The benchmarks from the 2 issues timeout, a regression is added for the projects issue.

3 years agoFix `str.replace_re` and `str.replace_re_all` (#6615)
Andres Noetzli [Thu, 27 May 2021 22:42:10 +0000 (15:42 -0700)]
Fix `str.replace_re` and `str.replace_re_all` (#6615)

Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.

3 years agoAdd Lexicographic + Pareto Optimizations (#6626)
Ouyancheng [Thu, 27 May 2021 22:02:48 +0000 (15:02 -0700)]
Add Lexicographic + Pareto Optimizations (#6626)

Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.

Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.

3 years agoUpdate proof namespaces (#6614)
Andrew Reynolds [Thu, 27 May 2021 21:28:58 +0000 (16:28 -0500)]
Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

3 years agoFix CEGQI for datatypes with Boolean subfields (#6630)
Andrew Reynolds [Thu, 27 May 2021 21:18:28 +0000 (16:18 -0500)]
Fix CEGQI for datatypes with Boolean subfields (#6630)

Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.

This also corrects the expected solution on a benchmark that had an incorrect status.

Fixes #6603.

3 years agoFix spurious assertion for trivial abduction (#6629)
Andrew Reynolds [Thu, 27 May 2021 20:02:43 +0000 (15:02 -0500)]
Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.

3 years agoFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)
Aina Niemetz [Thu, 27 May 2021 19:08:24 +0000 (12:08 -0700)]
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)

This is to make it consistent with the name of the SMT-LIB operator
(fp.add).

3 years agoReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624)
Andres Noetzli [Thu, 27 May 2021 17:11:57 +0000 (10:11 -0700)]
Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)

This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.

3 years agoAdd support for Box optimization (#6599)
Ouyancheng [Thu, 27 May 2021 07:53:58 +0000 (00:53 -0700)]
Add support for Box optimization (#6599)

Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.

3 years agoAvoid uploading docs if they did not change (#6621)
Gereon Kremer [Thu, 27 May 2021 07:38:12 +0000 (09:38 +0200)]
Avoid uploading docs if they did not change (#6621)

Fixes an oversight from #6601.

3 years agoEnable new justification heuristic by default (#6613)
Andrew Reynolds [Thu, 27 May 2021 06:44:55 +0000 (01:44 -0500)]
Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

3 years agoUse references instead of getter functions (#6597)
Gereon Kremer [Wed, 26 May 2021 20:30:19 +0000 (22:30 +0200)]
Use references instead of getter functions (#6597)

This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules.

3 years ago More precise includes of `Node` constants (#6617)
Andres Noetzli [Wed, 26 May 2021 14:30:17 +0000 (07:30 -0700)]
 More precise includes of `Node` constants (#6617)

We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).

The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.

3 years agoAdd more examples to the documentation (#6569)
Gereon Kremer [Wed, 26 May 2021 06:30:45 +0000 (08:30 +0200)]
Add more examples to the documentation (#6569)

This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)

3 years agoEnsure proper types in unit tests (#6598)
Gereon Kremer [Wed, 26 May 2021 06:20:03 +0000 (08:20 +0200)]
Ensure proper types in unit tests (#6598)

This PR fixes a type mixup (the usual long vs long long mixup on macos systems) in the unit tests for the new api::Term getters.
Fixes #6594.

3 years agoReduce size of sphinx-gh output (#6601)
Gereon Kremer [Wed, 26 May 2021 06:10:51 +0000 (08:10 +0200)]
Reduce size of sphinx-gh output (#6601)

This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)

3 years agoapi docs: Fix and tweak style for home and top links. (#6618)
Aina Niemetz [Tue, 25 May 2021 21:05:40 +0000 (14:05 -0700)]
api docs: Fix and tweak style for home and top links. (#6618)

3 years agoReplace deprecated calls to `std::allocator` (#6606)
Andres Noetzli [Tue, 25 May 2021 13:51:56 +0000 (06:51 -0700)]
Replace deprecated calls to `std::allocator` (#6606)

Fixes #6453. This commit replaces all calls to std::allocator with calls to
std::allocator_traits. Strictly speaking, allocate() and deallocate() are
not deprecated but the commit replaces them for uniformity.

3 years ago[Unit tests] Fix path of Java bindings (#6616)
Andres Noetzli [Tue, 25 May 2021 03:21:16 +0000 (20:21 -0700)]
[Unit tests] Fix path of Java bindings (#6616)

Currently, when configuring cvc5 with Java bindings, CMake complains
about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)`
not using the correct number of arguments in the Java unit tests. The
issue is that `${CVC5_JAR_PATH}` is empty. The value of
`${CVC5_JAR_PATH}` was computed in the Java API bindings but then not
shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is
not used anywhere else, this commit moves the computation of
`${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the
API subdirectories are processed before the test subdirectories.

3 years agoFix non-fixed length case in re-elim (#6612)
Andrew Reynolds [Mon, 24 May 2021 23:59:28 +0000 (18:59 -0500)]
Fix non-fixed length case in re-elim (#6612)

Fixes followup issues from #6604.

3 years agoImplementation of the new justification heuristic (#6465)
Andrew Reynolds [Mon, 24 May 2021 19:32:48 +0000 (14:32 -0500)]
Implementation of the new justification heuristic (#6465)

This adds the new implementation of the justification heuristic. It does not enable this strategy yet.

A followup PR will activate this strategy within DecisionEngine.

3 years agoMove proof utilities to src/proof/ (#6611)
Andrew Reynolds [Mon, 24 May 2021 18:51:09 +0000 (13:51 -0500)]
Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

3 years agoFix re-elim length requirement for symbolic RE memberships (#6609)
Andrew Reynolds [Mon, 24 May 2021 16:15:12 +0000 (11:15 -0500)]
Fix re-elim length requirement for symbolic RE memberships (#6609)

Fixes #6604.

Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.

3 years agoFix instance of no rewrite in extended rewriter (#6610)
Andrew Reynolds [Mon, 24 May 2021 15:55:17 +0000 (10:55 -0500)]
Fix instance of no rewrite in extended rewriter (#6610)

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.

3 years agoBetter formalization of regular expression unfolding skolems (#6602)
Andrew Reynolds [Mon, 24 May 2021 14:39:56 +0000 (09:39 -0500)]
Better formalization of regular expression unfolding skolems (#6602)

This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.

It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.

3 years agoFix tests of unsat cores (#6593)
Andrew Reynolds [Fri, 21 May 2021 21:46:48 +0000 (16:46 -0500)]
Fix tests of unsat cores (#6593)

This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.

It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.

It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).

3 years agoFix and refactor relevant domain (#6528)
Andrew Reynolds [Fri, 21 May 2021 21:27:19 +0000 (16:27 -0500)]
Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.

3 years agoFormalize shared selectors as skolem functions (#6591)
Andrew Reynolds [Fri, 21 May 2021 21:07:50 +0000 (16:07 -0500)]
Formalize shared selectors as skolem functions (#6591)

This is work towards properly printing shared selectors in external proofs.

3 years agoMinor simplification to boolean proof checker (#6590)
Andrew Reynolds [Fri, 21 May 2021 20:48:39 +0000 (15:48 -0500)]
Minor simplification to boolean proof checker (#6590)

3 years ago(proof-new) Minor documentation sync (#6592)
Andrew Reynolds [Fri, 21 May 2021 20:16:20 +0000 (15:16 -0500)]
(proof-new) Minor documentation sync (#6592)

3 years agoAdd utility to get all types occurring in a term (#6588)
Andrew Reynolds [Fri, 21 May 2021 18:04:49 +0000 (13:04 -0500)]
Add utility to get all types occurring in a term (#6588)

Required for external proof conversions.

3 years agoUpdate to sygus standard output for check-synth responses (#6521)
Andrew Reynolds [Fri, 21 May 2021 17:15:28 +0000 (12:15 -0500)]
Update to sygus standard output for check-synth responses (#6521)

This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.

It also removes the unused command GetSynthSolutionCommand.