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

Age	Commit message (Collapse)	Author
2021-01-20	SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)	Aina Niemetz
	This enables more strict handling of operators div, mod and abs for Integer arithmetic logics. More strict handling for '/' for Real arithmetic logics is more involved and should be done in the parser -- instead at solving time, like is currently done for checking that the application * is in the linear fragment. The latter should be checked in the parser, too. This is postponed to a later PR.
2020-05-22	Refactor operator elimination in arithmetic (#4519)	Andrew Reynolds
	This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong: (1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers. (2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental. The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way. As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR. This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts. Also notice that --rewrite-divk is effectively now enabled by default always. Fixes #4484, fixes #4486, fixes #4481.
2014-03-19	Minor usability fixes related to SMT-LIB compliance.	Morgan Deters

2014-03-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.