summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/skolemize.cpp
AgeCommit message (Collapse)Author
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
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").
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14Add internal API methods for pool-based instantiation (#6350)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions. This PR also eliminates some unused code in TheoryArithPrivate. Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
Currently, NodeBuilder takes a single template argument: An integer that determines the expected number of arguments. This argument is used to determine the size of the d_inlineNvChildSpace array. This array is used to construct nodes inline. The advantage of this is that we don't have to allocate a NodeValue on the heap for the node under construction until we are sure that the node is new. While templating the array size may save some stack space (or avoid a heap allocation if we statically know that we a fixed number of children and that number is greater than 10), it complicates the code and leads to longer compile times. Thus, this commit removes the template argument and moves some of the NodeBuilder code to a source file for faster compilation. CPU build time before change (debug build): 2429.68s CPU build time after change (debug build): 2228.44s Signed-off-by: Andres Noetzli noetzli@amazon.com
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate dependencies on quantifiers engine in internal quantifiers code ↵Andrew Reynolds
(#6240) This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned. Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2021-02-23Add interface to TheoryState for sort inference and facts (#5967)Andrew Reynolds
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality. This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
In particular, theory_engine.h is included many places spuriously. A few blocks of code changed indentation, updated to guidelines.
2021-01-27(proof-new) Improvements to quantifiers engine and instantiate interfaces ↵Andrew Reynolds
(#5814) This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure). Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
This is a step towards breaking up the quantifiers engine. The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed. This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
2020-11-12(proof-new) Proofs for skolemization (#5339)Andrew Reynolds
This adds support for proofs in the quantifiers module that performs skolemization. Also fixes a bug in the proof checker for skolemization.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-06-16Update copyright headers.Aina Niemetz
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
* Fix some documentation. * Move model basis out of term db. * Moving * Finished moving. * Document Skolemize and term enumeration. * Minor * Model basis to first order model. * Change function name. * Minor * Clang format. * Minor * Format * Minor * Format * Address review.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback