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

Age	Commit message (Collapse)	Author
2014-03-07	Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into ↵	Tim King
	master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
2014-02-17	type conversion	Tianyi Liang

2013-09-13	Documentation fixes, some code typo fixes, file perms, other minor things.	Morgan Deters

2013-06-24	Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵	Morgan Deters
	allows linearization of div,mod,/ by a constant.
2013-05-03	Code cleanup. Reducing misc. warnings in arithmetic.	Tim King

2013-05-03	Merging branch 'soiquickexplain'.	Tim King

2013-05-02	Adding quick explain for soi simplex.	Tim King

2013-05-01	Working on the new explanation system.	Tim King

2013-04-30	Draft of the new propagation code.	Tim King

2013-04-26	FCSimplex branch merge	Tim King

2013-04-02	Making arithmetic model reversion on unsat checks an option.	Tim King

2013-04-01	Adding a restart test strategy to integers.	Tim King

2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-04	Some fixes for the miplib preprocessing pass.	Morgan Deters
	* TNode violation bug fix (thanks to Tim King for discovery & fix) * change Boolean miplib-trick substitution option into a threshold * ppAssert() the generated miplib constraints to arithmetic
2013-02-03	Some cleanup of miplib regressions and options	Morgan Deters

2013-02-03	new option for doing top-level miplib substitutions (or not)	Morgan Deters

2013-02-03	new miplib pass, works for 1 or 2 vars	Morgan Deters

2013-01-31	Adding a heuristic to more eagerly split bounded integer variables.	Tim King

2013-01-23	Adding miplibtrick option.	Tim King

2012-10-06	* Clean up some options documentation	Morgan Deters
	* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
2012-07-31	Options merge. This commit:	Morgan Deters
	1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options) 2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace. 3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..) The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options: * to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp. * to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser(). * ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options) * this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file * Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true). Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h). Benefits of the new options system include: 1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed). 2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.) 3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc. 4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.) 5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose I've taken lots of care not to break anything. Hopefully, I've succeeded in that.