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

Age	Commit message (Collapse)	Author
2017-02-15	Minimization modes for fmf bound.	ajreynol

2017-02-07	Generalize finite bound inference to unifiable variables in set membership ↵	ajreynol
	literals.
2016-12-29	Changing getTearDownIncremental() to return the type of ↵	Tim King
	options::tearDownIncremental.
2016-12-07	Refactoring, generalization of bounded inference module. Simplification of ↵	ajreynol
	rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
2016-11-21	Refactoring related to track instantiation option.	ajreynol

2016-11-11	Add simple inferences for extended bitvector functions, add a few related ↵	ajreynol
	options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-10	Add option for enabling/disabling lazy extended function reduction in ↵	ajreynol
	bitvectors.
2016-11-08	Add a few options to separation logic and sets. Minor changes to separation ↵	ajreynol
	logic, change syntax for empty heap constraint.
2016-10-26	New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵	ajreynol
	as extension of sets solver, add regressions.
2016-10-05	Added an option that allow empty dependencies when attempting to minimize ↵	guykatzz
	preprocessing holes
2016-09-20	More refactoring of cbqi. Add a few regressions. Add option for qcf.	ajreynol

2016-09-16	Use matching heuristics for EPR instantiation.	ajreynol

2016-09-15	Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵	ajreynol
	default in EPR mode.
2016-09-12	Refactor prenex modes.	ajreynol

2016-09-12	Remove old implementation of cbqi	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-03	Option for prenex normal form	ajreynol

2016-09-01	Fix boolean term issue in invariants from sygus. Minor default options ↵	ajreynol
	changes for cbqi.
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-08-31	Removing typeof from didyoumean.cpp.	Tim King

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

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

2016-08-15	Enable bounded set membership with --fmf-bound. Map to term models for ↵	ajreynol
	bounded set membership.
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-07-27	Added an option for a more aggressive weakest implicant optimization	Guy

2016-07-26	Add option to minimize sygus solutions based on using weakest implicants of ↵	ajreynol
	instantiations in unsat cores.
2016-07-26	Minor improvements to strings related to constant splitting, including a few ↵	ajreynol
	options (disabled by default).
2016-07-20	Print only instantiations that are in the unsat core when --proof is ↵	ajreynol
	enabled. Add option to minimize sygus solutions based on unsat core (disabled by default).
2016-07-19	Add infrastructure for tracking instantiation lemmas (for proofs, and ↵	ajreynol
	minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-16	Refactor strings extf evaluation info. Ensure strings eager preprocess ↵	ajreynol
	eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
2016-07-06	Add comment field for model, resolves hack for printing sep logic models.	ajreynol

2016-07-05	Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵	ajreynol
	not drop patterns from merged prenex (fixes bug 743).
2016-06-23	Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,	Clark Barrett
	re-enabled cdmap_black.
2016-06-17	Support for separation logic. Enable cbqi by default for pure BV.	ajreynol

2016-06-08	Merge branch 'master' of https://github.com/CVC4/CVC4	Guy

2016-06-08	LFSC letification is true by default	Guy

2016-06-08	Support for printing a global let map in LFSC proofs.	Guy
	Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-06-06	Merge pull request #85 from CVC4/master_for_proof_merge	guykatzz
	Merge from proof branch
2016-06-03	Remove NodeListMap from datatypes and equality inference. Add option ↵	ajreynol
	--dt-blast-splits.
2016-06-01	Merge from proof branch	Guy

2016-06-01	Revert "Merging proof branch"	Guy
	This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01	Merging proof branch	Guy

2016-05-24	Merged cryptominisat from experimental branch.	Liana Hadarean

2016-05-24	Improvements to symmetry breaking in sygus search. Minor fix for getting ↵	ajreynol
	instantiations of non-registered quantifiers in sygus.
2016-05-18	Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. ↵	ajreynol
	Minor fixes for inst max level.
2016-05-16	Enable --sygus-direct-eval by default, limit to terms that do not induce ↵	ajreynol
	Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
2016-05-15	Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. ↵	ajreynol
	Enable e-matching when --strings-exp is enabled.
2016-05-12	Add casc scripts. Improvements to qcf related to nested quantifiers and ↵	ajreynol
	variable ordering.
2016-05-10	Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor ↵	ajreynol
	optimizations to sygus and qcf.
2016-05-05	Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵	ajreynol
	irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.