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

Age	Commit message (Collapse)	Author
2017-08-17	Add mbqi interleave option, change option fs-inst to fs-interleave.	ajreynol

2017-08-10	Fix line numbers in options_template	Andres Noetzli

2017-08-04	Set default language to smt lib 2.6 (including as a base language for ↵	ajreynol
	sygus), update regressions.
2017-07-14	Removing BOOST_FOREACH usage.	Tim King

2017-07-10	Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵	ajreynol
	of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
2017-07-10	Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵	ajreynol
	decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-07	Update copyright headers.	Mathias Preiner

2017-06-28	Enable non-linear solve by default, update regressions.	ajreynol

2017-05-30	print only labeled assertions as part of the unsat core	guykatzz
	added the option dump-unsat-cores-full for printing the entire core, as before
2017-05-12	Adding VPATH back in	makaimann

2017-05-12	Conditional coverage build	makaimann

2017-05-05	Do not eliminate extended arithmetic symbols when finite model finding is ↵	ajreynol
	on, add regression.
2017-04-21	Handle subtypes in sets. Bug fixes for tuples with subtypes.	ajreynol

2017-04-20	Minor fixes.	ajreynol

2017-04-18	Coverage fix	makaimann
	Forcing some make variables to be absolute paths lcov does not (officially) support relative paths src/expr and src/options in particular were breaking it
2017-04-07	Change option names for nl.	ajreynol

2017-04-05	Merge pull request #143 from FabianWolff/master	Clark Barrett
	Fix several spelling errors
2017-04-05	Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵	ajreynol
	NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
2017-04-05	Fix several spelling errors	Fabian Wolff

2017-04-04	Enable multi-trigger-linear by default, add option.	ajreynol

2017-04-02	Adding a model based axiom instantiation scheme for multiplication. Merge ↵	Tim King
	commit for nlAlgMaster.
2017-03-31	Add option multi-trigger-linear, minor optimization to E-matching.	ajreynol

2017-03-29	Add quantifiers options related to model and master equality engine.	ajreynol

2017-03-24	Refactor model building for quantifiers to be a single pass, simplification. ↵	ajreynol
	Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2017-03-22	Work on new approach for sygus involving conditional solutions. Refactoring ↵	ajreynol
	of sygus solver. Bug fix for sygus solution reconstruction.
2017-03-16	Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵	ajreynol
	mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2017-03-06	Adding support for bool-to-bv	Clark Barrett
	Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass.
2017-03-02	Minor cleanup and reorganization related to last commit.	ajreynol

2017-03-02	Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵	ajreynol
	Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
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