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

Age	Commit message (Collapse)	Author
2011-08-27	Removing Theory::registerTerm() as discussed in the meeting. Now ↵	Dejan Jovanović
	pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).
2011-08-24	Simplification of the preregister and register throught a NodeVisitor class. ↵	Dejan Jovanović
	The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.