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

Age	Commit message (Collapse)	Author
2021-04-14	Rename public and private headers in src/include. (#6352)	Aina Niemetz

2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-09	Rename CVC4__ header guards to CVC5__. (#6326)	Aina Niemetz

2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-16	cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)	Mathias Preiner
	The build system (cmake) will automatically generate an export header cvc4_export.h, which makes sure that the correct export features are defined depending on the compiler and target platform. The macro CVC4_EXPORT replaces CVC4_PUBLIC and its usage is reduced by 2/3. Co-authored-by: Gereon Kremer <nafur42@gmail.com>
2021-03-09	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-09-22	Add skeleton for theory of bags (multisets) (#5100)	mudathirmahgoub
	This PR adds initial headers and mostly empty source files for the theory of bags (multisets). It acts as a basis for future commits. It includes straightforward implementation for typing rules an enumerator for bags.
2020-09-22	Update 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-08-28	Replace Theory::Set with TheoryIdSet (#4959)	Andrew Reynolds
	This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine. This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h. It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h. This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.
2020-06-16	Update copyright headers.	Aina Niemetz

2019-10-10	Make order of theories explicit in the source code. (#3379)	Aina Niemetz
	Fixes #2517. This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future. This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used. I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993