Also makes another method statically available in NodeManager
(mkDummySkolem).
---------
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
This distinguishes a new kind of internal skolem DUMMY_SKOLEM for all skolems that are not formalized internally.
We now have the invariant that terms with internal kind cvc5::internal::Kind::SKOLEM are (exportable) skolems in our API.
Thus, calls in the SkolemManager e.g. isSkolemFunction now are simply a Kind check.
Moreover, cvc5::internal::Kind::SKOLEM is now mapped to a new cvc5::Kind::SKOLEM kind.
Note that #10559 should go in first, since INPUT_VARIABLE is an exception to the invariant introduced here.
FYI @HanielB
This makes printing kinds depend on the output language, which enables us to print nicer error messages with the SMT-LIB symbol instead of the internal kind.
With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.
This does not make this change yet, so CONST_RATIONAL is still used throughout.
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.
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
This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.
This makes all methods for constructing skolems local to SkolemManager.
It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.
This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
