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

Age	Commit message (Collapse)	Author
2021-10-07	Make the cardinality of the alphabet of strings configurable (#7298)	Andrew Reynolds
	This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.
2021-10-04	Eliminating static calls to rewriter from strings (#7302)	Andrew Reynolds

2021-09-01	Lazy proof reconstruction for strings theory solver (#7096)	Andrew Reynolds
	This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule. This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs). Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
2021-08-24	Uniform treatment of trusted theory inferences in proofs (#7044)	Andrew Reynolds
	Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
2021-04-12	Refactor and update copyright headers. (#6316)	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-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-11-30	(proof-new) Proofs for regular expression elimination (#5361)	Andrew Reynolds
	Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM. This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE.
2020-10-13	(proof-new) Simplifications for proof rule checker interface (#5244)	Andrew Reynolds
	Some of the interfaces in the proof rule checker are unnecessary now and can be deleted. This also updates STRING_TRUST to have pedantic level 2.
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-16	Add non-emptiness to conclusion of positive RE star unfolding. (#4899)	Andrew Reynolds
	A recent commit (77e9881) simplified the form of the conclusion in regular expression star unfolding for the sake of uniformity in our internal proof calculus. However, this led to a noticeable drop in performance on a few specific RE benchmarks (the Norn set). This preserves the old behavior by extending the core rule for RE unfolding. It also makes one minor change to the strings proof checker carried over from the proof-new branch.
2020-08-15	(proof-new) Add the strings proof checker (#4858)	Andrew Reynolds
	It also adds enumeration for two new rules that have been recently added.