cvc5.git
2 years agoVarious improvements and fixes in the documentation (#8551)
Gereon Kremer [Mon, 4 Apr 2022 19:09:47 +0000 (12:09 -0700)]
Various improvements and fixes in the documentation (#8551)

This PR contains a variety of fixed and improvements to the documentation.

2 years agoRename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)
Andrew Reynolds [Mon, 4 Apr 2022 18:35:38 +0000 (13:35 -0500)]
Rename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)

This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).

Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.

2 years agoUse raw symbols in proofs (#8550)
Andrew Reynolds [Mon, 4 Apr 2022 17:41:40 +0000 (12:41 -0500)]
Use raw symbols in proofs (#8550)

This ensures we don't quote symbols that should not be quoted, fixing two issues:
(1) Proofs in the internal calculus don't convert `:args` to `|:args|`.
(2) LFSC identifiers for terms are not quoted based on SMT-LIB restrictions.

Work towards https://github.com/cvc5/cvc5-projects/issues/466, quoted TypeNode names still need to be addressed.

2 years ago[proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)
Haniel Barbosa [Mon, 4 Apr 2022 14:12:39 +0000 (11:12 -0300)]
[proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)

Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof).

This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set.

There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do
not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases.

2 years agoFix for get-value with empty uninterpreted sort domain (#8547)
Andrew Reynolds [Mon, 4 Apr 2022 10:31:27 +0000 (05:31 -0500)]
Fix for get-value with empty uninterpreted sort domain (#8547)

Alternative for https://github.com/cvc5/cvc5/pull/8546.

We were mistakenly using `mkGroundTerm` instead of `mkGroundValue` to make the domain of an uninterpreted sort non-empty.

This ensures that get-value calls do not throw a spurious exception when there is a declared uninterpreted sort and there are no terms of that sort.

As a result, this also required fixing a few further issues regarding how uninterpreted sort constants are printed in models, and fixing the expected results on 2 more regressions.

2 years agoStart post-release for 0.0.11
Mathias Preiner [Sun, 3 Apr 2022 04:32:04 +0000 (21:32 -0700)]
Start post-release for 0.0.11

2 years agoBump version to 0.0.11
Mathias Preiner [Sun, 3 Apr 2022 04:32:04 +0000 (21:32 -0700)]
Bump version to 0.0.11

2 years agouse one process more than we have cores (#8545)
Gereon Kremer [Sat, 2 Apr 2022 20:03:56 +0000 (22:03 +0200)]
use one process more than we have cores (#8545)

This PR uses one process more than we have cores in the CI. This speeds up the CI jobs when time is spent waiting on IO instead of actually using the CPU.

2 years agoRename mkSygusGrammar to mkGrammar (#8544)
Andrew Reynolds [Sat, 2 Apr 2022 19:40:41 +0000 (14:40 -0500)]
Rename mkSygusGrammar to mkGrammar (#8544)

2 years agoRemove variant of mkDatatypeDecl with one sort parameter (#8543)
Andrew Reynolds [Sat, 2 Apr 2022 19:21:46 +0000 (14:21 -0500)]
Remove variant of mkDatatypeDecl with one sort parameter (#8543)

Subsumed by the vector version.

Also marks more methods as experimetnal.

2 years agoapi: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)
Aina Niemetz [Sat, 2 Apr 2022 18:57:50 +0000 (11:57 -0700)]
api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)

2 years agoFollow renaming within pythonic API (#8532)
Gereon Kremer [Sat, 2 Apr 2022 18:31:32 +0000 (20:31 +0200)]
Follow renaming within pythonic API (#8532)

We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.

2 years agoAlways cancel already running CI runs on forks (#8542)
Gereon Kremer [Sat, 2 Apr 2022 18:08:36 +0000 (20:08 +0200)]
Always cancel already running CI runs on forks (#8542)

One effect of our changed concurrency policy is that we never cancel runs on forks. This PR changes this, always allowing the concurrency mechanism to cancel on repositories that are not the main repository.

2 years agoMinor edits in docs. (#8540)
Cesare Tinelli [Sat, 2 Apr 2022 03:09:22 +0000 (22:09 -0500)]
Minor edits in docs. (#8540)

2 years agoIgnore irrelevant exponential terms (#8534)
Andrew Reynolds [Sat, 2 Apr 2022 02:48:35 +0000 (21:48 -0500)]
Ignore irrelevant exponential terms (#8534)

Fixes #8517.

2 years agodocs: Add Python installation instructions for pip. (#8538)
Mathias Preiner [Sat, 2 Apr 2022 02:26:33 +0000 (19:26 -0700)]
docs: Add Python installation instructions for pip. (#8538)

2 years agoapi: Remove DatatypeConstructor::getSelectorTerm(). (#8535)
Aina Niemetz [Sat, 2 Apr 2022 01:53:15 +0000 (18:53 -0700)]
api: Remove DatatypeConstructor::getSelectorTerm(). (#8535)

2 years agoRequire that used model values are constant in CEGQI (#8528)
Andrew Reynolds [Sat, 2 Apr 2022 01:27:01 +0000 (20:27 -0500)]
Require that used model values are constant in CEGQI (#8528)

Fixes #8520.

2 years agoAdd a few miscellaneous pieces of documentation (#8533)
Andrew Reynolds [Sat, 2 Apr 2022 01:02:47 +0000 (20:02 -0500)]
Add a few miscellaneous pieces of documentation (#8533)

2 years agoRemove java API methods that accepts lists as arguments (#8541)
mudathirmahgoub [Sat, 2 Apr 2022 00:40:47 +0000 (19:40 -0500)]
Remove java API methods that accepts lists as arguments (#8541)

This PR removes some unnecessary methods in the Java API that were added to simplify several unit tests that use dynamic arrays. The goal is to make the java API consistent and as small as possible.
Users could use asList, toArray methods to use generic lists if they wish.

2 years agoAdd more explanations in the API (#8493)
Andrew Reynolds [Sat, 2 Apr 2022 00:12:37 +0000 (19:12 -0500)]
Add more explanations in the API (#8493)

This also removes a few references to "first-order constants" (using "free constant" instead) since mkConst can be used to construct higher-order free constants.

2 years agoSimplify the python base API in a few places (#8514)
Gereon Kremer [Fri, 1 Apr 2022 23:53:33 +0000 (01:53 +0200)]
Simplify the python base API in a few places (#8514)

This PR simplifies a few methods in the python base API.

2 years agoSimplifications to the datatypes API (#8511)
Andrew Reynolds [Fri, 1 Apr 2022 23:23:18 +0000 (18:23 -0500)]
Simplifications to the datatypes API (#8511)

This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes.

API Changes:
(1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors.
(2) adds to unit test examples that use this variant instead of using unresolved sorts.
(3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental.

Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet.

Followup PR will add to documentation on elaborate further on how to use the datatypes API.

2 years agodocs: Document UnknownExplanation. (#8508)
Mathias Preiner [Fri, 1 Apr 2022 22:53:53 +0000 (15:53 -0700)]
docs: Document UnknownExplanation. (#8508)

2 years agoPrevent using the coverings solver with extended operators (#8523)
Gereon Kremer [Fri, 1 Apr 2022 22:24:16 +0000 (00:24 +0200)]
Prevent using the coverings solver with extended operators (#8523)

The way we construct the model within the nonlinear extension makes using multiple subsolvers that contribute to the model potentially unsound. This PR prevent the coverings solver from being used if extended operators are present, unless --nl-cov-force is given.
Fixes #8515. Fixes #8516.

2 years agoapi kinds: Refactor docs for kinds to properly render in Python. (#8510)
Aina Niemetz [Fri, 1 Apr 2022 22:03:58 +0000 (15:03 -0700)]
api kinds: Refactor docs for kinds to properly render in Python. (#8510)

2 years agoapi: Remove Datatype::getConstructorTerm(). (#8529)
Aina Niemetz [Fri, 1 Apr 2022 21:36:07 +0000 (14:36 -0700)]
api: Remove Datatype::getConstructorTerm(). (#8529)

2 years agoReplace regression by minimized one via ddSMT (#8531)
Haniel Barbosa [Fri, 1 Apr 2022 20:29:41 +0000 (17:29 -0300)]
Replace regression by minimized one via ddSMT (#8531)

2 years agoOnly run pypi packaging when release is published (#8526)
Gereon Kremer [Fri, 1 Apr 2022 20:29:24 +0000 (22:29 +0200)]
Only run pypi packaging when release is published (#8526)

We incorrectly triggered pypi packaging when a release was created or published, i.e. it would run twice.

2 years agomake-release: Clarify instructions for pushing commits and tag. (#8524)
Mathias Preiner [Fri, 1 Apr 2022 20:28:31 +0000 (13:28 -0700)]
make-release: Clarify instructions for pushing commits and tag. (#8524)

2 years ago[proofs] [doc] Document string rules (#8498)
Haniel Barbosa [Fri, 1 Apr 2022 20:27:47 +0000 (17:27 -0300)]
[proofs] [doc] Document string rules (#8498)

Also replaces negation of equality literals by disequality literals.

2 years agoChange CI concurrency policy to not queue on main (#8530)
Gereon Kremer [Fri, 1 Apr 2022 20:26:52 +0000 (22:26 +0200)]
Change CI concurrency policy to not queue on main (#8530)

Previously, we would only allow one job per branch/PR and only cancel old jobs on PRs.
This PR changes this policy to allow multiple jobs at once on main.
The way this is done basically follows https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#example-using-a-fallback-value.

2 years agoDocument special member functions in python API (#8513)
Gereon Kremer [Fri, 1 Apr 2022 20:12:10 +0000 (22:12 +0200)]
Document special member functions in python API (#8513)

This PR documents relevant special member functions __getitem__ and __iter__ for some classes in the base python API.

2 years agoPython API: Do not rename enumerators. (#8507)
Aina Niemetz [Fri, 1 Apr 2022 19:45:36 +0000 (12:45 -0700)]
Python API: Do not rename enumerators. (#8507)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
Co-authored-by: Gereon Kremer <gkremer@stanford.edu>
2 years ago[proofs] [alethe] Fix Alethe post-processor (#8525)
Haniel Barbosa [Fri, 1 Apr 2022 19:22:42 +0000 (16:22 -0300)]
[proofs] [alethe] Fix Alethe post-processor (#8525)

Previously the Alethe post-processor was merging subproofs, which should not be done at this stage. As a consequence some post-processed proofs were becoming open.

2 years agoStart post-release for 0.0.10
Mathias Preiner [Fri, 1 Apr 2022 18:18:09 +0000 (11:18 -0700)]
Start post-release for 0.0.10

2 years agoBump version to 0.0.10
Mathias Preiner [Fri, 1 Apr 2022 18:18:09 +0000 (11:18 -0700)]
Bump version to 0.0.10

2 years agoInternal simplifications to constructing datatypes (#8519)
Andrew Reynolds [Fri, 1 Apr 2022 18:16:43 +0000 (13:16 -0500)]
Internal simplifications to constructing datatypes (#8519)

In preparation for #8511.

This makes it so that unresolved sorts are automatically inferred when constructing datatypes at the NodeManager level. This is in preparation for simplifying the API.

Changes:
(1) NodeManager is cleaned so that unresolved types are automatically inferred and are not a part of its public interface. Internal code generating datatypes is simplified as a result.
(2) Adds necessary utilities to TypeNode and cleans an unused flag
(3) The parser is cleaned to not track unresolved sorts in an ad-hoc manner.
(4) The API is patched to use the simpler interface.

2 years agoFix pypi packaging trigger again (#8512)
Gereon Kremer [Fri, 1 Apr 2022 17:33:03 +0000 (19:33 +0200)]
Fix pypi packaging trigger again (#8512)

Further workflows are not triggered when the GITHUB_TOKEN is used. This PR creates new releases using the ACTION_USER_TOKEN instead.

2 years ago[proofs] [doc] Minor changes to general proofs page, some changes to Alethe page...
Haniel Barbosa [Fri, 1 Apr 2022 17:27:05 +0000 (14:27 -0300)]
[proofs] [doc] Minor changes to general proofs page, some changes to Alethe page, added DOT page (#8501)

2 years agoRemove decorator from python API (#8505)
Gereon Kremer [Fri, 1 Apr 2022 16:58:00 +0000 (18:58 +0200)]
Remove decorator from python API (#8505)

This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.

2 years ago[API] Add mode argument for `Solver::blockModel()` (#8521)
Andres Noetzli [Fri, 1 Apr 2022 16:26:14 +0000 (09:26 -0700)]
[API] Add mode argument for `Solver::blockModel()` (#8521)

This commit changes Solver::blockModel() to take a mode as an argument
instead of relying on an option.

2 years agoRemove `UnknownExplanation::NO_STATUS` (#8518)
Andres Noetzli [Fri, 1 Apr 2022 12:36:48 +0000 (05:36 -0700)]
Remove `UnknownExplanation::NO_STATUS` (#8518)

Result already supports storing a NONE result, so
UnknownExplanation::NO_STATUS seems redundant. This removes that
explanation, which was only being used in the optimization solver.

2 years agoFix javadoc custom tag warning (#8502)
mudathirmahgoub [Fri, 1 Apr 2022 09:33:14 +0000 (04:33 -0500)]
Fix javadoc custom tag warning (#8502)

Fix this warning
Note: Custom tags that could override future standard tags:  @apiNote. To avoid potential overrides, use at least one period character (.) in custom tag names.

2 years agodocs: Add documentation for modes. (#8509)
Mathias Preiner [Fri, 1 Apr 2022 06:09:38 +0000 (23:09 -0700)]
docs: Add documentation for modes. (#8509)

2 years agoPython api: Various fixes in docs. (#8480)
Aina Niemetz [Fri, 1 Apr 2022 05:45:33 +0000 (22:45 -0700)]
Python api: Various fixes in docs. (#8480)

2 years ago[API] Remove redundant version of `mkFunctionSort` (#8503)
Andres Noetzli [Fri, 1 Apr 2022 04:50:25 +0000 (21:50 -0700)]
[API] Remove redundant version of `mkFunctionSort` (#8503)

mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.

2 years agoFix sygus-inst when combined with bounded string quantifiers (#8500)
Andrew Reynolds [Fri, 1 Apr 2022 04:25:05 +0000 (23:25 -0500)]
Fix sygus-inst when combined with bounded string quantifiers (#8500)

Strings introduces bounded quantified formulas for reasoning about extended functions. We should not process these with sygus-inst.

Fixes #8497.

2 years agoapi: Swap arguments of declareSygusVar. (#8499)
Mathias Preiner [Fri, 1 Apr 2022 01:32:44 +0000 (18:32 -0700)]
api: Swap arguments of declareSygusVar. (#8499)

Make it consistent with other declare*/define* functions.

2 years agoapi: Use std::optional for symbols in mk* functions. (#8495)
Mathias Preiner [Fri, 1 Apr 2022 01:10:29 +0000 (18:10 -0700)]
api: Use std::optional for symbols in mk* functions. (#8495)

Makes all symbols in mk* functions optional.

2 years agomake-release: Change instructions for pushing tag.
Mathias Preiner [Fri, 1 Apr 2022 00:49:35 +0000 (17:49 -0700)]
make-release: Change instructions for pushing tag.

2 years agoStart post-release for 0.0.9
Mathias Preiner [Fri, 1 Apr 2022 00:45:49 +0000 (17:45 -0700)]
Start post-release for 0.0.9

2 years agoBump version to 0.0.9
Mathias Preiner [Fri, 1 Apr 2022 00:45:49 +0000 (17:45 -0700)]
Bump version to 0.0.9

2 years agoAlso run on created. (#8506)
Gereon Kremer [Fri, 1 Apr 2022 00:44:49 +0000 (02:44 +0200)]
Also run on created. (#8506)

The way we now create releases apparently does not trigger the release::published event. It should trigger the release::created event, though.

2 years agoAdd documentation for sequences (#8496)
Ying Sheng [Thu, 31 Mar 2022 23:37:49 +0000 (16:37 -0700)]
Add documentation for sequences (#8496)

Added documentation for sequences.

2 years agoFix bag example links (#8504)
mudathirmahgoub [Thu, 31 Mar 2022 22:48:55 +0000 (17:48 -0500)]
Fix bag example links (#8504)

2 years agoHandled quoted symbols in indexed operators (#8491)
Andrew Reynolds [Thu, 31 Mar 2022 22:09:38 +0000 (17:09 -0500)]
Handled quoted symbols in indexed operators (#8491)

Fixes https://github.com/cvc5/cvc5/issues/8489.

The SMT-LIB standard says that symbols and quoted symbols are identical page 24: `This means for instance that abc and |abc| are the same symbol.`.  We did not parse quoted symbols in indexed operators, this fixes the issue.

2 years agoVarious fixes related to isDatatypeXXX checks. (#8473)
Aina Niemetz [Thu, 31 Mar 2022 21:27:39 +0000 (14:27 -0700)]
Various fixes related to isDatatypeXXX checks. (#8473)

2 years agoSort, TypeNode: Rename functions related to datatypes. (#8472)
Aina Niemetz [Thu, 31 Mar 2022 20:50:45 +0000 (13:50 -0700)]
Sort, TypeNode: Rename functions related to datatypes. (#8472)

2 years agoDisable minisat variable elimination when a parametric theory is present (#8487)
Andrew Reynolds [Thu, 31 Mar 2022 19:34:31 +0000 (14:34 -0500)]
Disable minisat variable elimination when a parametric theory is present (#8487)

Fixes cvc5/cvc5-projects#506.

It seems there are extremely few cases where it is safe to use this option.

2 years agoRemove examples that use the old API (#8486)
Andres Noetzli [Thu, 31 Mar 2022 19:11:41 +0000 (12:11 -0700)]
Remove examples that use the old API (#8486)

This removes examples that use the old API and the parser. They were not
currently being compiled and we can reintroduce them if we need
them/have a new parser API.

2 years agoapi: Remove warning for Sort::instantiate(). (#8475)
Aina Niemetz [Thu, 31 Mar 2022 18:48:17 +0000 (11:48 -0700)]
api: Remove warning for Sort::instantiate(). (#8475)

2 years agoDo not export dt.size (#8483)
Andrew Reynolds [Thu, 31 Mar 2022 18:28:16 +0000 (13:28 -0500)]
Do not export dt.size (#8483)

This kind is hardcoded only to work for sygus. I am not sure we want to support general constraints over it, or even if the token dt.size is the appropriate one.

Also adds a missing experimental warning that I had missed.

Fixes cvc5/cvc5-projects#504.

2 years agoFix check for whether PI is reduced (#8485)
Andrew Reynolds [Thu, 31 Mar 2022 18:05:53 +0000 (13:05 -0500)]
Fix check for whether PI is reduced (#8485)

Fixes cvc5/cvc5-projects#505.

Also fixes a counter-intuitive behavior where 0 was not considered reduced and does minor cleanup.

2 years agoci: Fix typo in update-pr job. (#8492)
Mathias Preiner [Thu, 31 Mar 2022 17:31:16 +0000 (10:31 -0700)]
ci: Fix typo in update-pr job. (#8492)

2 years agoImprove documentation for Statistics in C++ API (#8476)
Gereon Kremer [Thu, 31 Mar 2022 17:30:33 +0000 (19:30 +0200)]
Improve documentation for Statistics in C++ API (#8476)

This PR improves the documentation of the Statistics and the Stat class in the C++ API.

2 years ago[proofs] Adding post-visit processing to proof node updater (#8431)
Haniel Barbosa [Thu, 31 Mar 2022 16:56:20 +0000 (13:56 -0300)]
[proofs] Adding post-visit processing to proof node updater (#8431)

Previously in the proof node updater only structural reasoning was done at post-visit time (merging subproofs, checking free assumptions). This commit adds a virtual method to allow updating the proof node at post-visit time.

In particular this commit is important to functionality in the alethe post processing that is deactivated in master.

CC @Lachnitt

2 years agoRemove support for Python 2.x (#8488)
Andres Noetzli [Thu, 31 Mar 2022 16:24:33 +0000 (09:24 -0700)]
Remove support for Python 2.x (#8488)

This removes support for Python 2.x. We haven't been testing it and
there isn't a good reason to support it.

2 years agoAdd examples/bags.cpp (#8463)
mudathirmahgoub [Thu, 31 Mar 2022 15:17:22 +0000 (10:17 -0500)]
Add examples/bags.cpp (#8463)

2 years agoFix Java examples (#8484)
Andres Noetzli [Thu, 31 Mar 2022 14:38:11 +0000 (07:38 -0700)]
Fix Java examples (#8484)

This fixes the Java examples. The examples were not able the find the
`cvc5::cvc5jar` target because the namespace had accidentally been
changed to `cvc5::internal::` in commit
bbcd471ed40c813c48957ced5596471cc0ccebe9. This reverts that change.

2 years agoFix lower vs upper bound issue for eager RE conflicts (#8482)
Andrew Reynolds [Thu, 31 Mar 2022 14:06:28 +0000 (09:06 -0500)]
Fix lower vs upper bound issue for eager RE conflicts (#8482)

Fixes #8481.

2 years agoInstall necessary packages (#8479)
Gereon Kremer [Thu, 31 Mar 2022 07:01:57 +0000 (09:01 +0200)]
Install necessary packages (#8479)

We use beautifulsoup to generate the version selector of the release documentation. This PR makes sure all necessary dependencies for this script are installed.

2 years agoOnly run update-pr for normal commits on main (#8478)
Gereon Kremer [Thu, 31 Mar 2022 05:59:41 +0000 (07:59 +0200)]
Only run update-pr for normal commits on main (#8478)

Doing a release (or generally pushing two commits at the same time) can trigger a race condition in the update-pr action that technically fails the CI workflow. This PR only runs this action for normal commits, in particular it does not run it for releases (which is the common case where we push multiple commits at once). To be sure, it also puts all update-pr jobs into a concurrency group that enforces sequential execution.

2 years agoImprove documentation for OptionInfo (#8474)
Gereon Kremer [Thu, 31 Mar 2022 04:40:10 +0000 (06:40 +0200)]
Improve documentation for OptionInfo (#8474)

This PR improves the documentation for OptionInfo and adds documentation for the DriverOptions class.

2 years agoMove Java package to `io.github.cvc5` (#8469)
Andres Noetzli [Thu, 31 Mar 2022 04:09:03 +0000 (21:09 -0700)]
Move Java package to `io.github.cvc5` (#8469)

Previously, we were using io.github.cvc5.api to mirror the C++
namespace that the API was in. The namespace of the C++ API changed to
simply cvc5 and so this commit updates the Java package accordingly.

2 years ago[proofs] [doc] Documenting arrays, bit-vectors, datatypes and quantifiers rules ...
Haniel Barbosa [Thu, 31 Mar 2022 03:35:40 +0000 (00:35 -0300)]
[proofs] [doc] Documenting arrays, bit-vectors, datatypes and quantifiers rules (#8465)

2 years ago[proofs] [doc] Document equality rules (#8462)
Haniel Barbosa [Thu, 31 Mar 2022 02:53:26 +0000 (23:53 -0300)]
[proofs] [doc] Document equality rules (#8462)

2 years agodocs: Remove api namespace. (#8455)
Mathias Preiner [Thu, 31 Mar 2022 02:30:21 +0000 (19:30 -0700)]
docs: Remove api namespace. (#8455)

2 years agoFix non-termination in the strings rewriter (#8438)
Andrew Reynolds [Thu, 31 Mar 2022 02:08:18 +0000 (21:08 -0500)]
Fix non-termination in the strings rewriter (#8438)

Fixes #8434.

This makes our component containment utility less aggressive. This impacts (seldom used) rewrites for indexof and replace only.

2 years agoapi: Mark experimental kinds. (#8464)
Aina Niemetz [Thu, 31 Mar 2022 01:47:05 +0000 (18:47 -0700)]
api: Mark experimental kinds. (#8464)

2 years agoStart post-release for 0.0.8
Mathias Preiner [Thu, 31 Mar 2022 00:53:18 +0000 (17:53 -0700)]
Start post-release for 0.0.8

2 years agoBump version to 0.0.8
Mathias Preiner [Thu, 31 Mar 2022 00:53:18 +0000 (17:53 -0700)]
Bump version to 0.0.8

2 years agoci: Do not cancel jobs on main branch. (#8471)
Mathias Preiner [Thu, 31 Mar 2022 00:50:04 +0000 (17:50 -0700)]
ci: Do not cancel jobs on main branch. (#8471)

This will prevent that jobs on the main branch get cancelled when new PRs are merged in before the previous ones finished on main.

2 years agoFix case of Boolean skolem for ground term E-matching (#8447)
Andrew Reynolds [Thu, 31 Mar 2022 00:49:33 +0000 (19:49 -0500)]
Fix case of Boolean skolem for ground term E-matching (#8447)

Work towards fixing the second issue on cvc5/cvc5-projects#487, which now gives the same error as #8347.

2 years agoci: Update older PRs first. (#8477)
Mathias Preiner [Thu, 31 Mar 2022 00:25:23 +0000 (17:25 -0700)]
ci: Update older PRs first. (#8477)

2 years agoapi: Remove isUninterpretedSortParameterized from header file. (#8470)
Mathias Preiner [Thu, 31 Mar 2022 00:17:20 +0000 (17:17 -0700)]
api: Remove isUninterpretedSortParameterized from header file. (#8470)

Method was removed in #8425.

2 years agoAllow for multiple (equal) base model values (#8467)
Gereon Kremer [Wed, 30 Mar 2022 23:44:49 +0000 (01:44 +0200)]
Allow for multiple (equal) base model values (#8467)

This PR weakens an assertion about multiple model values in the same equivalence class. We now accept multiple base model values in the same equivalence class, as long as they compare equal. This allows to gracefully handle cases where real algebraic numbers fail to realize that they are rational.
Fixes #8414.

2 years agoExclude competition build for issue8377-resolve-indexed.smt2. (#8468)
Mathias Preiner [Wed, 30 Mar 2022 23:04:16 +0000 (16:04 -0700)]
Exclude competition build for issue8377-resolve-indexed.smt2. (#8468)

Fixes the nightly competition builds.

2 years agoMove cvc5::internal::context to cvc5::context. (#8451)
Mathias Preiner [Wed, 30 Mar 2022 22:16:46 +0000 (15:16 -0700)]
Move cvc5::internal::context to cvc5::context. (#8451)

2 years agoPatch cross reference in Kind.java documentation (#8458)
mudathirmahgoub [Wed, 30 Mar 2022 21:58:08 +0000 (16:58 -0500)]
Patch cross reference in Kind.java documentation (#8458)

This PR patches cross reference links in Kind.java comments for now until a proper way is implemented that handles documentation for cpp, python and Java API.

2 years agodocs: Add bags to list of theory references. (#8461)
Aina Niemetz [Wed, 30 Mar 2022 20:39:28 +0000 (13:39 -0700)]
docs: Add bags to list of theory references. (#8461)

2 years agoapi: Add Sort::getUninterpretedSortConstructor(). (#8459)
Aina Niemetz [Wed, 30 Mar 2022 19:39:52 +0000 (12:39 -0700)]
api: Add Sort::getUninterpretedSortConstructor(). (#8459)

This further introduces TypeNode::isInstantiatedUninterpretedSort().

2 years agoFix policy for purifying arguments of exp (#8416)
Andrew Reynolds [Wed, 30 Mar 2022 19:17:09 +0000 (14:17 -0500)]
Fix policy for purifying arguments of exp (#8416)

This corrects the policy for when to purify exp. It ensures we purify exp whenever the kind is not a variable or constant, instead of when the kind is a transcendental function app. The latter permits problematic terms like (exp (* (exp 1.0) (exp 1.0)).

This also corrects an issue where information for ordering on variables would be skipped if we failed to produce a model value for a single variable, which was the original source of the error on #8415.

It furthermore fixes the PfRule ARITH_TRANS_EXP_APPROX_BELOW, which did not handle non-constant arguments of exp.

Fixes #8415.

2 years agoFixes for sygus-inst (#8448)
Andrew Reynolds [Wed, 30 Mar 2022 18:55:21 +0000 (13:55 -0500)]
Fixes for sygus-inst (#8448)

Fixes two issues:

Symmetry breaking was disabled after latest refactoring of sygus options. This meant that the terms considered by sygus-inst were often redundant.
The instantiation constant attribute is set on evaluation variables. This avoids model-unsoundness issues with sygus-inst, which are caused by using the evaluation variable (itself) in instantiations.
The latter issue was discovered by trying the second issue from cvc5/cvc5-projects#487 with --sygus-inst, where it incorrectly says "sat" after the fix from #8447.

Fixed #8456. Fixes #8457.

2 years agoFix subtype issue in cegqi arithmetic (#8440)
Andrew Reynolds [Wed, 30 Mar 2022 18:06:34 +0000 (13:06 -0500)]
Fix subtype issue in cegqi arithmetic (#8440)

Fixes #8410.

Was not properly checking for cases where an Integer variable had a Real term as its solution.

2 years agoTypeNode: Unify functions to instantiate parametric sorts. (#8449)
Aina Niemetz [Wed, 30 Mar 2022 15:07:13 +0000 (08:07 -0700)]
TypeNode: Unify functions to instantiate parametric sorts. (#8449)

This unifies `instantiateParametricDatatype()` and
`instantiateSortConstructor()` into `instantiate()`. It further fixes
how the API calls TypeNode instantation.

2 years ago[API] Move `UnknownExplanation` to `cvc5_types.h` (#8450)
Andres Noetzli [Wed, 30 Mar 2022 14:30:11 +0000 (07:30 -0700)]
[API] Move `UnknownExplanation` to `cvc5_types.h` (#8450)

This also fixes some minor issues in the `parseenums.py` script.

2 years ago[proof] [doc] Document external proof rules (#8439)
Haniel Barbosa [Wed, 30 Mar 2022 13:53:57 +0000 (10:53 -0300)]
[proof] [doc] Document external proof rules (#8439)

2 years agoMove cvc5::internal::main to cvc5::main. (#8454)
Mathias Preiner [Wed, 30 Mar 2022 08:51:42 +0000 (01:51 -0700)]
Move cvc5::internal::main to cvc5::main. (#8454)

2 years agoAdd information for cardinality constraint to the Python API (#8444)
yoni206 [Wed, 30 Mar 2022 06:55:56 +0000 (09:55 +0300)]
Add information for cardinality constraint to the Python API (#8444)

This PR complements #8422 by adding a tester and a getter for cardinality constraints to the python API. The corresponding test from solver_black is translated and included.