| Age | Commit message (Collapse) | Author |
|---|
|
This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.
This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.
This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.
The other dumping tags are deleted for now, and will be reimplemented as needed.
|
|
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 properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.
Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.
|
|
Includes miscellaneous improvements and fixes to the LFSC proof conversion from proof-new in preparation for CI on master.
|
|
|
|
This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder.
It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.
|
|
This makes cardinality constraints nullary operators. This eliminates hacks for supporting these previously.
It also removes an unimplemented kind CARDINALITY_VALUE.
Notice that the parser and printer now do not use a common syntax for cardinality constraints, this will be resolved on followup PRs.
|
|
Work towards a new internal fuzzing technique.
The new fuzzing technique leverages elements of the IJCAR 2020 paper on abduction, this moves https://github.com/cvc5/cvc5/blob/master/src/theory/quantifiers/sygus/cegis_core_connective.h#L44 to its own file. A followup PR will break this and further utility methods out of this file.
|
|
Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts.
|
|
|
|
When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;
difference_type Iter::difference_type
value_type Iter::value_type
pointer Iter::pointer
reference Iter::reference
iterator_category Iter::iterator_category
```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.
This pull request performs the fix, and the program is semantically equivalent before and after the fix.
References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator
|
|
This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.
This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.
|
|
This PR performs a first refactoring on the NlModel class. It improves model value computation, comparison and stores the model substitutions in a map (instead of two vectors).
|
|
This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.
It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.
|
|
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.
|
|
This utility converts from terms used in the internal calculus to terms that capture how they should be printed in LFSC.
|
|
This ensures we don't try to apply e.g. enumerative instantiation to quantified formulas over regular expressions, since no type enumerator exists for RE.
Fixes #6750.
|
|
Towards rewrite rule reconstruction
|
|
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 splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
|
|
It was not robust to cases where a function-to-synthesize occurred in a higher-order context.
Also does general clean up of the single invocation utility.
|
|
Initial work towards rewrite rule reconstruction.
|
|
|
|
Initial work towards rewrite rule reconstruction
|
|
Adds a utility for converting nodes. This is the first step towards the LFSC proof conversion.
|
|
Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.
|
|
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*`.
|
|
There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.
|
|
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.
|
|
|
|
|
|
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.
It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.
|
|
This is work towards properly printing shared selectors in external proofs.
|
|
|
|
Required for external proof conversions.
|
|
This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
|
|
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.
|
|
|
|
reflects that it is a macro, which we will eliminate
|
|
|
|
Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:
Cannot name a term in a binder (e.g., quantifiers, definitions)
To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.
The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
|
|
|
