This command will eventually take a mode; for now it assumes a default implementation. I've opened cvc5/cvc5-wishues#104 to track this.
This is a feature requested by Certora.
There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option.
This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).
This commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a declare-const command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in NodeManager::mkAbstractValue())
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.
This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.
Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an @ are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.
Adds support for incremental abduction, adds regression for using push/pop in combination with get-abduct, and a use of get-abduct-next.
Adds this method to C++, java API.
Interpolation/abduction not yet supported in Python API, I'm waiting for @yoni206 to add this; getAbductNext will be added to Python API in followup PR.
This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next.
By default, the SyGuS subsolver will generate a new solution for each successive check-synth.
This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case.
This completes our support for incremental SyGuS.
This adds a function to create unresolved sorts for mutually recursive
datatpes. This function creates an uninterpreted sort if the arity of
the unresolved sort is 0, and a sort constructor sort otherwise.
This PR removes the possibility to have void options. While there are (very) few options that may legitimately be considered void (they do not actually hold a value, but merely trigger a handler or predicate), the type being void introduces a number of special cases in the options setup. Their only real benefit was to avoid having data members that would never be used.
As it turns out, though, the same can be achieved by not specifying a name, which already supported as well.
For mode options, getOptionInfo would hold the name of the enum values for the default value and the available modes. This PR changes this to hold the string values instead, which is what users can actually use via the API.
This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to
REGEXP_ALLCHAR to match their SMT-LIB representation (re.none,
re.allchar). It further renames api::Solver::mkRegexpEmpty() to
mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar.
This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.
This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.
This renames Solver::getSeparationHeap to Solver::getValueSepHeap,
Solver::getSeparationNilTerm to Solver::getSepNil and
Solver::declareSeparationHeap to Solver::declareSepHeap.
@mudathirmahgoub @alex-ozdemir @yoni206
This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.
