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

Age	Commit message (Collapse)	Author
2016-09-12	Refactor prenex modes.	ajreynol

2016-09-12	Remove old implementation of cbqi	ajreynol

2016-09-12	Prefer non-cardinality constants in term models for sep logic.	ajreynol

2016-09-12	Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵	ajreynol
	breaking in theory sep.
2016-09-09	Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.	ajreynol

2016-09-09	Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵	ajreynol
	allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
2016-09-08	Refactor seplog preprocess. Handle case where sep data type cannot be inferred.	ajreynol

2016-09-03	Miniscope top level conjunctions for prenex normal form, allow one level ↵	ajreynol
	miniscoping in prenex normal form.
2016-09-03	Option for prenex normal form	ajreynol

2016-09-01	Merge pull request #91 from timothy-king/no-throw	Tim King
	Relaxing the throw specifiers for the destructors for Node, TypeNode,…
2016-09-01	Fix boolean term issue in invariants from sygus. Minor default options ↵	ajreynol
	changes for cbqi.
2016-09-01	Cleanup quantifier elimination in smt engine.	ajreynol

2016-09-01	Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested ↵	ajreynol
	quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
2016-09-01	Relaxing the throw specifiers for the destructors for Node, TypeNode, the ↵	Tim King
	context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.
2016-08-31	Removing the forward declaration of QuantInfo from rewrite_engine.h.	Tim King

2016-08-31	Cleaning up the dead FORIT macros.	Tim King

2016-08-31	Removing the usage of typeof from theory_sets_private.	Tim King

2016-08-31	Beautifying theory_model.h.	Tim King

2016-08-31	Removing BOOST_FOREACH from theory/sets/scrutinize.h.	Tim King

2016-08-31	Removing typeof from sets normal form and beautifying the file.	Tim King

2016-08-31	Removing typeof from command_executor_portfolio.cpp.	Tim King

2016-08-31	Removing typeof from didyoumean.cpp.	Tim King

2016-08-26	Basic support for EPR+CBQI. Minor cleanup.	ajreynol

2016-08-25	Minor cleanup preprocessing, add ppNotifyAssertions.	ajreynol

2016-08-25	Options for counterexample guided instantiation.	ajreynol

2016-08-19	Fixed two bugs	Clark Barrett

2016-08-19	Added fitsSignedLong and fitsUnsignedLong	Clark Barrett

2016-08-16	Initial infrastructure for ExtTheory, generalize extended term handling in ↵	ajreynol
	TheoryStrings to use this.
2016-08-15	Enable bounded set membership with --fmf-bound. Map to term models for ↵	ajreynol
	bounded set membership.
2016-08-12	Minor fixes to model construction to take singleton equivalence classes into ↵	ajreynol
	account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
2016-08-12	Merge pull request #90 from 4tXJ7f/fewer_preproc_holes	guykatzz
	Add support for fewer preprocessing holes
2016-08-11	Add support for fewer preprocessing holes	Andres Notzli
	This commit adds support for the --fewer-preprocessing-holes flag. This flag changes the preprocessing part in proofs in two ways: it (1) removes assertions that are just restating inputs and uses the inputs directly instead and it (2) changes the form of the preprocessed assertions to contain the input that they originate from. The code in this commit is mostly taken from the proofs branch in Guy's fork.
2016-08-11	Minor change to strings, introduce proxy vars only when necessary.	ajreynol

2016-08-10	Improvements to strings: work on propagations for reverse normal form ↵	ajreynol
	processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
2016-08-09	Merge pull request #89 from 4tXJ7f/fix_proof_spaces	guykatzz
	Fix missing/redundant spaces in proofs
2016-08-09	Fixes for sep star rewrite.	ajreynol

2016-08-09	Fix missing/redundant spaces in proofsfix_proof_spaces	Andres Notzli
	Before, in some cases, e.g. when printing sorts and in resolution proofs, the proofs contained redundant and/or missing spaces. With this commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10 let12)` instead of `(trust_f (= (Array Index Element )let10 let12))`.
2016-08-05	Minor: add/fix comments, remove redundant includes	Andres Notzli

2016-08-03	Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.	Guy

2016-08-03	Merge pull request #87 from 4tXJ7f/fix_oob_access	barrettcw
	Fix out-of-bounds access in ExprManager
2016-07-30	Prioritize inferences when processing normal forms in strings.	ajreynol

2016-07-28	The "aggressive" optimizer for lemma L now returns the conjunction of all ↵	Guy
	lemmas L' that originated from L and were used in the unsat core
2016-07-28	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-07-28	Bug fix involving negated lemmas	Guy

2016-07-28	Fix bug 749.	ajreynol

2016-07-28	Add the negative conjunction case	Guy

2016-07-27	Fix out-of-bounds access in ExprManager	Andres Notzli
	The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough because the INC_STAT macro tries to access `d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an out-of-bounds access. Found bug with UBSan.
2016-07-27	Proper instrumentation of the preprocessing phase	Guy

2016-07-27	proper handling of ITEs	Guy

2016-07-27	Proper handling of IFF lemmas in the unsat core.	Guy
	Don't return duplicates in the unsat core