This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/.
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
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
Fixes https://github.com/cvc5/cvc5-projects/issues/445. Fixes
https://github.com/cvc5/cvc5-projects/issues/446. The issue is related
to the preprocessing pass for doing rewrite rule synthesis based on the
input. It was removing duplicate arguments from both chaining operators
and non-chaining operators when constructing the corresponding
datatypes. In the case of non-chaining operators, it could happen that
the constructor of the datatype did not have the correct number of
arguments for a given kind if there was a term where multiple arguments
were the same. This commit fixes the issue by doing the duplicate
elimination only for chaining operators.
Fixescvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.
Fixescvc5/cvc5-projects#397. Fixes
cvc5/cvc5-projects#399. After performing the
substitution on the child node, the result was not added as a child to
the node under construction, resulting in nodes with too few children.
This commit fixes that issue.
This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.
Tests are updated and added, as well as other minor changes.
Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345cvc5/cvc5-projects#344cvc5/cvc5-projects#343
@mpreiner FYI
This PR consolidates SetLanguage, ExprSetDepth and ExprDag into a single consistent utility. Also, it makes it play more nicely with users setting these options and removes some obsolete code.
