| Age | Commit message (Collapse) | Author |
|---|
|
sensitive (#4972)
This will be used by TermFormulaRemoval.
|
|
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
|
|
Callbacks for term-context-sensitive terms.
It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.
These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.
|
|
Towards removing the Expr-level datatype.
Moves DatatypeIndex to its own file, which is the only thing that is necessary remaining from expr/datatype.h.
Also updates the datatype kinds file in preparation for the removal.
|
|
Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().
|
|
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
|
|
Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.
Requires #4617.
|
|
Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.
|
|
This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.
|
|
Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.
|
|
Also adds a commonly used proof generator: the proof reference proof generator.
|
|
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
|
|
This class is used for delaying proof node creation until it is necessary.
|
|
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
|
|
This class is the Node-level representation of a sequence. It is analogous to CVC4::String.
|
|
This is required for dag-ifying ProofNode output.
|
|
This adds the general utility for maintaining mappings from Skolems to their witness form via attributes.
I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs.
|
|
A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag.
Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent.
|
|
Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.
ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).
ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.
This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.
|
|
This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).
|
|
Towards disentangling Options / NodeManager / SmtEngine.
This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.
The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.
The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.
It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
|
|
Implement an iterator for pre- and post-order traversals.
I believe that this will be useful in pre-processing passes, many of
which do postorder traversals that they implement by hand.
Right now this iterator does not support modification of the traversal
pattern, but we could add this later on, if we want it.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
|
|
Done by:
Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.
|
|
|
|
This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.
Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.
|
|
|
|
|
|
|
|
|
|
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
|
|
|
|
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
|
