cvc5.git
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.

2 years agoAdding some missing python API methods and tests (#8441)
yoni206 [Wed, 30 Mar 2022 06:05:49 +0000 (09:05 +0300)]
Adding some missing python API methods and tests (#8441)

This PR adds methods to the python API, as well as tests for the new methods and other tests for existing methods, translated from solver_black.cpp.

2 years agoChange tuple tokens and update datatypes theory ref (#8420)
Andrew Reynolds [Wed, 30 Mar 2022 04:39:29 +0000 (23:39 -0500)]
Change tuple tokens and update datatypes theory ref (#8420)

Changes tuple_ to tuple. for consistency.

Also fixes the lexer list for smt2 and updates the datatypes theory reference with missing content.

2 years agoAdd LFSC to internal proof checker (#8442)
Andrew Reynolds [Wed, 30 Mar 2022 03:57:41 +0000 (22:57 -0500)]
Add LFSC to internal proof checker (#8442)

Similar to ALETHE, this was forgotten. Was not causing issues since --proof-check=eager is not used by default.

2 years agoFix some documentation warnings (#8453)
mudathirmahgoub [Wed, 30 Mar 2022 03:15:58 +0000 (22:15 -0500)]
Fix some documentation warnings  (#8453)

2 years agoRename master branch to main. (#8452)
Mathias Preiner [Wed, 30 Mar 2022 02:55:15 +0000 (19:55 -0700)]
Rename master branch to main. (#8452)

2 years agoShow the code for utilities in the docs. (#8387)
Abdalrhman Mohamed [Wed, 30 Mar 2022 02:11:08 +0000 (21:11 -0500)]
Show the code for utilities in the docs. (#8387)

This PR adds the code for printing synthesis solutions to the docs. Various other changes are made to increase the consistency between the different bindings.

Signed-off-by: Abdalrhman M Mohamed <abdalrhman-mohamed@uiowa.edu>
2 years agoTypeNode: Rename isSort() and getSortConstructorArity(). (#8446)
Aina Niemetz [Wed, 30 Mar 2022 00:22:40 +0000 (17:22 -0700)]
TypeNode: Rename isSort() and getSortConstructorArity(). (#8446)

Names of these two functions were slightly confusing with respect to API
terminology. This renames isSort() to isUninterpretedSort() and
getSortConstructorArity() to getUninterpretedSortConstructorArity() for
more consistency and clarity.

2 years agoIntroduce internal namespace and remove api namespace. (#8443)
Mathias Preiner [Tue, 29 Mar 2022 23:23:01 +0000 (16:23 -0700)]
Introduce internal namespace and remove api namespace. (#8443)

The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:

cvc5
  ~~ public API
  ::context
  ::internal
  ::parser
  ::main

After this PR it will be:

cvc5
  ~~ public API
  ::internal
      ::context
      ::main
  ::parser

2 years agoapi: Add Sort::getInstantiatedParameters(). (#8445)
Aina Niemetz [Tue, 29 Mar 2022 21:36:12 +0000 (14:36 -0700)]
api: Add Sort::getInstantiatedParameters(). (#8445)

This adds a function to retrieve the sort arguments an instantiated
sort has been instantiated with. It further deletes
Sort::getDatatypeParamSorts() and
Sort::getUninterpretedSortParamSorts().

2 years agobv-to-int: fix translation of bvneg (#8437)
yoni206 [Tue, 29 Mar 2022 20:00:32 +0000 (23:00 +0300)]
bv-to-int: fix translation of bvneg  (#8437)

The translation of bvneg to integers did not match the comment documenting it, causing #8413 .
This PR fixes the issue and includes the test from #8413 as well as a simpler test.
Fixes #8413 .

2 years agoMake ensureTermSort private (#8436)
Andrew Reynolds [Tue, 29 Mar 2022 19:37:22 +0000 (14:37 -0500)]
Make ensureTermSort private (#8436)

This method was used to correct a limitation in the old API regarding parsing decimals. It should not be a public API method.

2 years agoAdd information for cardinality constraint to the API (#8422)
Andrew Reynolds [Tue, 29 Mar 2022 18:57:07 +0000 (13:57 -0500)]
Add information for cardinality constraint to the API (#8422)

Python API is not implemented yet, as it requires new infrastructure for returning pairs.

2 years agoMake ProofNodeManager mkScope more robust (#8435)
Andrew Reynolds [Tue, 29 Mar 2022 18:17:29 +0000 (13:17 -0500)]
Make ProofNodeManager mkScope more robust (#8435)

This make mkScope more robust in two ways:

- Literals rewritten to true can be justified by MACRO_SR_PRED_INTRO.
- Literals that are rewritten to other non-rewritable free assumptions can also be linked.

This is enough to ensure that current issues with (= t false) vs (not f) are fixed for Boolean arrays.

2 years agoAdd bags.rst (#8432)
mudathirmahgoub [Tue, 29 Mar 2022 17:32:37 +0000 (12:32 -0500)]
Add bags.rst (#8432)

2 years agoFix issue related to use of Boolean term variable for set/bag choose (#8423)
Andrew Reynolds [Tue, 29 Mar 2022 16:46:14 +0000 (11:46 -0500)]
Fix issue related to use of Boolean term variable for set/bag choose (#8423)

Fixes cvc5/cvc5-projects#501.

I am considering making this detail internal to SkolemManager to avoid similar issues in the future. However, there are some subtle performance implications in doing so, so this will be addressed later.

2 years ago[API] Add `{is,get}RoundingModeValue()` (#8429)
Andres Noetzli [Tue, 29 Mar 2022 14:43:02 +0000 (07:43 -0700)]
[API] Add `{is,get}RoundingModeValue()` (#8429)

It also fixes a wrong entry in s_rmodes_internal.

2 years agoTypeNode: Refactor get param types handling. (#8428)
Aina Niemetz [Tue, 29 Mar 2022 08:33:05 +0000 (01:33 -0700)]
TypeNode: Refactor get param types handling. (#8428)

This introduces TypeNode::getInstantiatedParamTypes() and deletes
TypeNode::getParamTypes(). This is in preparation for adding
api::Sort::getInstantiatedParameters().

2 years agoFix for issue 5925: constant arrays should be nonlinear. (#8430)
Clark Barrett [Tue, 29 Mar 2022 06:50:55 +0000 (23:50 -0700)]
Fix for issue 5925: constant arrays should be nonlinear. (#8430)

Fixes #5925. The "nonlinear" optimization did not take constant arrays into account.

2 years agoapi: Add Sort::isInstantiated(). (#8425)
Aina Niemetz [Tue, 29 Mar 2022 01:37:13 +0000 (18:37 -0700)]
api: Add Sort::isInstantiated(). (#8425)

This further removes Sort::isUinterpretedSortParameterized().

2 years agoMove `RoundingMode` to `cvc5_types.h` (#8427)
Andres Noetzli [Tue, 29 Mar 2022 01:13:46 +0000 (18:13 -0700)]
Move `RoundingMode` to `cvc5_types.h` (#8427)

This moves RoundingMode to cvc5_types.h and switches to using the
auto-generated enum bindings. It also fixes the Java-bindings generator
for enums (certain parts were previously hardcoded for Kind) and
extends the unit tests for Solver::mkRoundingMode() to actually check
the value being created.

2 years agoMark more methods as experimental (#8426)
Andrew Reynolds [Mon, 28 Mar 2022 23:09:43 +0000 (18:09 -0500)]
Mark more methods as experimental (#8426)

2 years agoRename get-interpol to get-interpolant. (#8424)
Mathias Preiner [Mon, 28 Mar 2022 22:30:19 +0000 (15:30 -0700)]
Rename get-interpol to get-interpolant. (#8424)

2 years ago[API] Mark methods as experimental (#8249)
Andres Noetzli [Mon, 28 Mar 2022 21:23:21 +0000 (14:23 -0700)]
[API] Mark methods as experimental (#8249)

2 years agoci: Enable all language bindings for debug build. (#8419)
Mathias Preiner [Mon, 28 Mar 2022 20:48:07 +0000 (13:48 -0700)]
ci: Enable all language bindings for debug build. (#8419)

2 years agoapi: Remove left-over Sort::getUninterpretedSortName from header. (#8421)
Aina Niemetz [Mon, 28 Mar 2022 19:25:19 +0000 (12:25 -0700)]
api: Remove left-over Sort::getUninterpretedSortName from header. (#8421)

2 years ago[proofs] Alethe: Call Printer (#8408)
Lachnitt [Mon, 28 Mar 2022 19:05:26 +0000 (12:05 -0700)]
[proofs] Alethe: Call Printer (#8408)

The alethe printer was not called on Master.

2 years ago[proofs] Alethe: Add ALETHE_RULE to builtin proof checker (#8409)
Lachnitt [Mon, 28 Mar 2022 18:44:44 +0000 (11:44 -0700)]
[proofs] Alethe: Add ALETHE_RULE to builtin proof checker (#8409)

Proofs would fail because the internal proof checker would return null and the alethe check is not trusted.

2 years agoFix synth result python unit test (#8418)
Andrew Reynolds [Mon, 28 Mar 2022 17:31:34 +0000 (12:31 -0500)]
Fix synth result python unit test (#8418)

2 years agoMark solve-bv-as-int as expert. (#8417)
Mathias Preiner [Mon, 28 Mar 2022 16:49:32 +0000 (09:49 -0700)]
Mark solve-bv-as-int as expert. (#8417)

Option not yet stable.

2 years agoSeparating produce-interpols from the mode of interpolant generation (#8326)
yoni206 [Sat, 26 Mar 2022 17:10:06 +0000 (20:10 +0300)]
Separating produce-interpols from the mode of interpolant generation (#8326)

In current master, --produce-interpols takes a mode, where "none" is the default mode, in which interpolant generation is not enabled.
This PR makes --produce-interpols a Boolean, and adds a interpols-mode option to determine the mode, similarly to unsat cores.

2 years agobuiltin: Move type rules implementation to .cpp file. (#8407)
Aina Niemetz [Sat, 26 Mar 2022 07:27:11 +0000 (00:27 -0700)]
builtin: Move type rules implementation to .cpp file. (#8407)

2 years agoapi: Rename *SortConstructor* to *UninterpretedSortConstructor*. (#8406)
Aina Niemetz [Sat, 26 Mar 2022 05:40:42 +0000 (22:40 -0700)]
api: Rename *SortConstructor* to *UninterpretedSortConstructor*. (#8406)

2 years agoFix spurious assertion failure (#8404)
Andrew Reynolds [Sat, 26 Mar 2022 03:46:31 +0000 (22:46 -0500)]
Fix spurious assertion failure (#8404)

This was wrong when doing sequences of reals and a seq.nth merges with a seq.len.

Fixes cvc5/cvc5-projects#502.

2 years agoThrow logic exception for set.map (#8403)
Andrew Reynolds [Sat, 26 Mar 2022 02:51:29 +0000 (21:51 -0500)]
Throw logic exception for set.map (#8403)

Support parsing/rewriting, but not solving currently.

2 years agoMore minor cleaning of options (#8401)
Andrew Reynolds [Sat, 26 Mar 2022 01:53:51 +0000 (20:53 -0500)]
More minor cleaning of options (#8401)

Removes a few more unnecessary options and moves the location of one.

2 years agoFixes for API kind documentation (#8397)
Andrew Reynolds [Sat, 26 Mar 2022 01:07:05 +0000 (20:07 -0500)]
Fixes for API kind documentation (#8397)

Also renames str.tolower -> str.to_lower, str.toupper -> str.to_upper.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
2 years agoAdd API unit tests for options (#8339)
Gereon Kremer [Sat, 26 Mar 2022 00:42:26 +0000 (01:42 +0100)]
Add API unit tests for options (#8339)

This PR adds some unit tests that cover some remaining cases of getOptionInfo() and getDriverOptions().
It also adds some fixes to the java bindings of these methods.

2 years agoapi: Unify mkOp variants. (#8369)
Mathias Preiner [Fri, 25 Mar 2022 23:57:10 +0000 (16:57 -0700)]
api: Unify mkOp variants. (#8369)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2 years agoapi: More comprehensive documentation of INTERNAL_KIND. (#8400)
Aina Niemetz [Fri, 25 Mar 2022 23:33:17 +0000 (16:33 -0700)]
api: More comprehensive documentation of INTERNAL_KIND. (#8400)

2 years ago[Parser] Fix resolution of indexed symbols (#8383)
Andres Noetzli [Fri, 25 Mar 2022 23:09:13 +0000 (16:09 -0700)]
[Parser] Fix resolution of indexed symbols (#8383)

Fixes #8377. Commit 3a97480ffab492f8272ad9c7c192d04b43eeea60 changed how
we handle indexed symbols. In particular, it added the option to resolve
them later when the arguments are known. However, the condition for when
to do this resolution was incorrect: It was applied to _all_ known
indexed symbols and not only the ones that can't immediately be resolved
to a kind. This commit fixes the condition.

2 years agoapi: Remove Sort::isParametricDatatype(). (#8405)
Aina Niemetz [Fri, 25 Mar 2022 22:43:35 +0000 (15:43 -0700)]
api: Remove Sort::isParametricDatatype(). (#8405)

Previously, Sort::isParametricDatatype() returned true for both
instantiated and non-instantiated parametric datatypes.

This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated.

Co-authored-by: ajreynol <andrew.j.reynolds@gmail.com>
2 years ago[proofs] [sat] Have SAT solver communicate whether it has optimized the assertion...
Haniel Barbosa [Fri, 25 Mar 2022 21:25:04 +0000 (18:25 -0300)]
[proofs] [sat] Have SAT solver communicate whether it has optimized the assertion level of a clause (#8399)

This way both the SAT proof manager and the Proof Cnf Stream can properly track
proofs for clauses added at assertion levels below their original user level.

This commit, besides some minor tweaks, adds the hooks in the places where
a clause can be created with an optimized level and we need to track:

when the explanation of a propagation is requested
when a clause/lemma is added
when a lemma is added (from the backlog of lemmas added when Minisat was busy)
For clauses derived via resolution, this information is computed directly in the SAT proof manager.

This commit also reverts a change from #7790 where whether to optimize clauses was computed only once for the SAT solver. This cannot be the case because between different check-sat calls the state can change.

Finally, this commit enables proofs for several regressions that were previously incompatible with proofs. Since now proofs are compatible with optimizing the level of clauses during incremental solving, this commit should lead to performance improvements.

Fixes cvc5/cvc5-projects#314

2 years agoapi: Rename kind NULL_EXPR to NULL_TERM. (#8402)
Aina Niemetz [Fri, 25 Mar 2022 20:50:34 +0000 (13:50 -0700)]
api: Rename kind NULL_EXPR to NULL_TERM. (#8402)

2 years agoGenerate `enum` bindings for Python and Java (#8393)
Andres Noetzli [Fri, 25 Mar 2022 20:28:12 +0000 (13:28 -0700)]
Generate `enum` bindings for Python and Java (#8393)

This commit generalizes the generation of bindings for enums to include
enums in cvc5_types.h. The commit only generates the bindings, but
does not use them yet (e.g., do add an argument to
Solver::blockModels()). The generated Java bindings already respect
the C++ namespace whereas the Python bindings require a minor
restructuring to make the namespaces work (i.e., instead of cvc5kinds,
we should have cvc5.api.kinds).

2 years agoUpdate checkSynth and checkSynthNext to return SynthResult (#8382)
Andrew Reynolds [Fri, 25 Mar 2022 20:00:14 +0000 (15:00 -0500)]
Update checkSynth and checkSynthNext to return SynthResult (#8382)

Also extends to non-trivial unit test of SynthResult.

Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.

2 years agoChange output of abduction/interpolation for failed inputs (#8396)
Andrew Reynolds [Fri, 25 Mar 2022 19:19:35 +0000 (14:19 -0500)]
Change output of abduction/interpolation for failed inputs (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.

2 years ago[proofs] Alethe: Bug Fix in Cong Rule (#8391)
Lachnitt [Fri, 25 Mar 2022 18:59:26 +0000 (11:59 -0700)]
[proofs] Alethe: Bug Fix in Cong Rule (#8391)

cvc5 suffered a segfault in the CONG rule because the refl step, e.g. (= v0 v0), was added without the cl connector, e.g. (cl (= v0 v0))

2 years agoapi: Remove blocks in kinds header. (#8398)
Aina Niemetz [Fri, 25 Mar 2022 18:00:27 +0000 (11:00 -0700)]
api: Remove  blocks in kinds header. (#8398)

2 years ago[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the...
Haniel Barbosa [Fri, 25 Mar 2022 17:41:56 +0000 (14:41 -0300)]
[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the ProofCnfStream (#8388)

Adds functionality for the TheoryProxy and ProofCnfStream modules to be notified of clauses that were asserted in lower levels than the current one. These clauses have their proofs tracked in the ProofCnfStream via an OptimizedClausesManager object.

Since the SAT solver may optimize the assertion level of propagation
explanations and of added clauses, we need to be able to maintain proofs across
context-popping. Not doing this can lead to open proofs. To do this the Proof
cnf stream uses an OptClausesManager to re-add proofs of facts inserted at
optimized levels.

Future PRs will change the SAT solver to use these notifications.

2 years agoFixes related to set defaults for sygus/proofs (#8395)
Andrew Reynolds [Fri, 25 Mar 2022 17:02:23 +0000 (12:02 -0500)]
Fixes related to set defaults for sygus/proofs (#8395)

This ensures we always report that SyGuS is incompatible with proofs. As a result, we require disabling sygus in 2 contexts where it should have been disabled before.

2 years agoFix Python API tests (#8392)
Andres Noetzli [Fri, 25 Mar 2022 13:08:01 +0000 (06:08 -0700)]
Fix Python API tests (#8392)

Note that we are currently not running API tests on the CI due to the
changes in 23dd064.

2 years agoapi: Refactor kinds documentation. (#8384)
Aina Niemetz [Fri, 25 Mar 2022 03:13:06 +0000 (20:13 -0700)]
api: Refactor kinds documentation. (#8384)