| Age | Commit message (Collapse) | Author |
|---|
|
This PR ensures that the possible modes returned in getOptionInfo() are always sorted. Their order would depend on the python dictionary ordering, which changed with a somewhat recent python version and thereby breaks our tests.
|
|
This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.
|
|
This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
|
|
This PR adds kind BAG_MAP to bags.
|
|
This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.
|
|
This adds the last two remaining API methods required for implementing the text output of get-model on the API side.
A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.
This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
|
|
While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.
|
|
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
|
|
This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.
Here we focus on the translation of nodes without children.
Unit tests are included.
|
|
This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions.
|
|
This removes support for creating bit-vectors from a string without a
size argument. We further also now require that the base argument is
always given (it has no default value).
|
|
This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.
This is a special case of term annotations that occur as the body of a quantified formula.
If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.
|
|
This commit adds `Term.java`, `TermTest.java`, and `cvc5_Term.cpp` to the Java API.
|
|
This PR refactors the nonlinear extension(s) to access options only via the environment class.
|
|
This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
|
|
This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.
|
|
Fixes cpp API's mkBitVector(val_str, base) constructor.
|
|
For some configurations, the unit test `solver_black` was unable to find
the correct variant `std::find()`. This commit adds an explicit include
of `<algorithm>`, which declares the `std::find()` as required by the
unit test.
|
|
This PR removes calls to the Solver constructor with an Options object, and instead uses the setOption() method.
|
|
This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.
|
|
This PR adds a new API function api::Solver::getOptionNames() that exposes a list of all option names as strings. This PR will be followed by another that adds a method to further inspect a particular option by name, and thereby allows to inspect the solver options in a sensible way.
|
|
Also adds a call to get proof in a unit test.
|
|
This is work towards eliminating circular dependencies on SmtEngine.
This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine.
It is also work towards eliminating the output manager, which is now subsumed by Env.
|
|
This ensures that e.g. COMBINATION_SPLIT shows up under theory::builtin::inferencesLemmas, and -t im. It also removes outdated interfaces from OutputChannel, and makes the feature TheoryEngine::ensureLemmaAtoms more modular, which was required for making these interfaces more consistent.
It also ensures that TheoryBuiltin has an inference manager, which will simplify special casing in #6956.
|
|
This PR improves the check when we use libedit: only when the input is an interactive terminal.
This is motivated by a change to the unit test for the interactive mode that now properly redirects standard input (and output).
|
|
Note the change to the unit test makes it so the test is not dependent on Node ID order.
|
|
This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.
|
|
|
|
Fixes #6866. The `theory_airth_cad_white` unit test has been failing on
some platforms (e.g., macOS) due to statically linking libpoly in
libcvc5 and then separately linking it in the unit tests. This resulted
in issues with `static` variables. This commit fixes the issue by
avoiding linking libpoly in the unit tests and instead relying solely on
libcvc5.
Co-authored-by: Ouyancheng <1024842937@qq.com>
|
|
Fixes #6047. The test was disabled because ASan found a use-after-free
due to an object allocated in the top scope being destroyed after the
scope (see #2607 for a detailed explanation). At first, the plan was to
add support for this use case. However, we have decided that we
currently don't need support for this feature and added a guard against
it (#6082). This commit reenables the test but changes it to destroy the
object allocated in the top level scope before the corresponding level
is popped. It additionally adds a test of the guard from #6082.
|
|
|
|
|
|
This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.
|
|
This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.
|
|
This commit replaces (old) internal string kind names to match the API / smt2 standard names.
|
|
|
|
After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.
|
|
This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.
|
|
|
|
OptimizationResult now contains:
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded
This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API.
Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)...
|
|
Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.
|
|
The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().
|
|
This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests.
|
|
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.
Fixes #3958, #5396, #5736, #5743, #5947.
|
|
|
|
This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.
|
|
pushObjective => addObjective (#6634)
In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:
optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.
|
|
Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.
Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.
|
|
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
|
|
This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.
|
