cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2019-12-02	OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ ↵	makaimann
	API (#3355) * Treat uninterpreted functions as a child in Term iteration * Remove unnecessary const_iterator constructor * Add parameter comments to const_iterator constructor * Use operator[] instead of storing a vector of Expr children * Switch pos member variable from int to uint32_t * Add comment about how UFs are treated in iteration * Allow OpTerm to contain a single Kind, update OpTerm construction * Update mkTerm to use only an OpTerm (and not also a Kind) * Remove unnecessary function checkMkOpTerm * Update mkOpTerm comments to not use _OP Kinds * Update examples to use new mkTerm * First pass on fixing unit test * Override kind for Constructor and Selector Terms * More fixes to unit tests * Updates to parser * Remove old assert (for Kind, OpTerm pattern which was removed) * Remove _OP kinds from public API Add hasOpTerm and getOpTerm methods to Term * Add test for UF iteration * Add unit test for getOpTerm * Move OpTerm implementation above Term implemenation to match header file Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than forward declaring within the same file that it's declared. * Fix mkTerm in datatypes-new.cpp example * Use helper function for creating term from Kind to avoid nested API calls * Rename: OpTerm->Op in API * Update OpTerm->Op in examples/tests/parser * Add case for APPLY_TESTER * operator term -> operator * Update src/api/cvc4cpp.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Comment comment suggestion Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Add not-null checks and implement Op from a single Kind constructor * Undo sed mistake for OpTerm replacement * Add 'd_' prefix to member vars * Fix comment and remove old commented-out code * Formatting * Revert "Formatting" This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9. * More fixes for sed mistakes * Minor formatting * Undo changes in CVC parser * Add isIndexed and prefix with d_ * Create helper function for isIndexed to avoid calling API functions in other API functions
2019-10-08	Make ackermannization generally applicable rather than just BV (#3315)	Ying Sheng
	The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.