This PR moves the public API headers into a top-level include directory. This makes it easier to find the public API of cvc5 and makes the install headers script obsolete.
Fixes#9553Fixes#9556
This corrects issues in our parser related to when symbols should be added to our symbol table.
In particular, symbols should be bound only when commands are executed and not as they are parsed. Binding during parsing leads to errors in interactive mode where those symbols are bound more than once, say if a command is partially parsed and then re-parsed based on our line buffering. This required further modifications to the interactive shell to execute commands immediately as they are parsed, since executing them may impact parsing (say if a declare-fun was on the same line as the subsequent command).
This adds new methods for accessing the binding methods of the underlying symbol table of symbol manager.
There are further issues of this form to correct, e.g. for define-fun-rec, which will be addressed in a separate PR.
Organizing the PR a bit:
we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.
This renames Smt2 and Tptp to Smt2State and TptpState, and decouples their implementation from ANTLR specific parsing. The Smt2State will be reused in the new flex parser.
It introduces ANTLR-specific wrappers of these classes (called by their previous names Smt2 and Tptp to avoid propagating further name changes), having the same functionality for parsing.
Followup PRs will clean Smt2State / TptpState and move them to smt2_state.h / tptp_state.h.
This experimental option causes cvc5 to synthesize rewrite rules based on the input. The code for this is a preprocessing pass which used to rewrite the input to a sygus conjecture. This is confusing since it changes the semantics of the input. We now call a separate subsolver.
This also cleans up set defaults. The options required for synthesizing rewrite rules are now applied locally to the subsolver spawned by the preprocessing pass.
We now terminate with an exception in the rare case when rewrite rule synthesis terminates.
This is required for further enhancements to the sygus solver for answering infeasible.
This commit moves the `Command` infrastructure to the parser (to
`src/parser/api/cpp`) and moves it to the `cvc5::parser` namespace. The
`Command`-related files are compiled with `-D__BUILDING_CVC5LIB`,
because they need access to the internal printers. The commit refactors
the internal code to not depend on `Command` anymore. To do this, the
commit refactors printing derived classes of `CommandStatus` to follow a
similar structure to printing commands (so that we can also print
command statuses internally without creating instances of
`Commandstatus`). This is a step towards a parser API.
This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR.
It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default).
This is work towards efficient support for `to_lower`/`to_upper`.
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.
