summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2015-11-26Update to new implementation of single invocation partition by default.ajreynol
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-11-25Infrastructure for partially single invocation properties. Bug fix for uncons...ajreynol
2015-11-23Adding a missing delete to InstStrategyCegqi destructor.Tim King
2015-11-23Isolating the dependencies on CVC4_ANTLR3_OLD_INPUT_STREAM. Also freeing more...Tim King
2015-11-23Freeing memory allocated for signal handling.Tim King
2015-11-18Option for midpoints in cbqi.ajreynol
2015-11-17Improve relevant domain computation for arithmetic, full saturation strategy....ajreynol
2015-11-12Minor fixes and improvements to purify quant, relational triggers.ajreynol
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...ajreynol
2015-11-09Replacing an inefficient use of std::find(...) to use std::set's find() instead.Tim King
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-05Merging the google branch back into master.Tim King
2015-11-05Fixes some initialization and desctruction problems in quantifiers. Also rest...Tim King
2015-11-05This commit slightly generalizes the scripts for generating the _tags files.Tim King
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-11-03Fixing typo.Tim King
2015-11-03Adding a test to ensure the <build>/src/theory directory is available to the ...Tim King
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-29Removes an extra dollar sign from src/options/mktagheaders. The extra dollar ...Tim King
2015-10-27Adding the new mkdirs script to EXTRA_DIST. This should fix the failing night...Tim King
2015-10-26This commit fixes a bug related to a public header depending on a compiler fl...Tim King
2015-10-26This commit removes using absolute paths in the generation of the .subdirs fi...Tim King
2015-10-26This commit moves the scripts for building the Debug_tags, Traces_tags, Debug...Tim King
2015-10-26This fixes a one definition rule violation for reduceDB_lt in Solver.cc in mi...Tim King
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, mi...ajreynol
2015-10-24Fixes related to string contains.ajreynol
2015-10-23This removes a bug for reading data that has been popped from the back of a v...Tim King
2015-10-23Specify that the default initialization must always be done for CDOhash_map's...Tim King
2015-10-23Switching Options::current() to return a pointer. This helps avoid undefined ...Tim King
2015-10-23This patch slightly generalizes how the std::isfinite function in <cmath> is ...Tim King
2015-10-22Enable counterexample-guided quantifier instantiation by default for quantifi...ajreynol
2015-10-21Minor refactoring in strings related to length.ajreynol
2015-10-20Refactor strings, remove old cycle checks in normalize eqc.ajreynol
2015-10-20Clean up explanations involving string length. Add regression.ajreynol
2015-10-19Improve stratification of strings extended function reductions, add regressio...ajreynol
2015-10-19Improve regexp rewriter, simplify regexp preprocess, add basic trans closure ...ajreynol
2015-10-18Fix for no condense func values.ajreynol
2015-10-16Add option to interleave enumerative instantiation with other strategies.ajreynol
2015-10-16Throw error for recursively defined types involving Boolean.ajreynol
2015-10-16Fix for codatatype constant rewrite, add regression.ajreynol
2015-10-15Fix congruence check in strings, fixes bug 686.ajreynol
2015-10-15Change semantics of str.substr to allow endpoint out of bounds, and return em...ajreynol
2015-10-15Decompose string contains, minor refactoring.ajreynol
2015-10-13remove options infrastructure code which depended on undefined behaviorKshitij Bansal
2015-10-11fix regression tests, support fallback mode for proofsKshitij Bansal
2015-10-11Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastru...ajreynol
2015-10-08Minor improvements to strings. Refactor rewriter. Enable fairness for multipl...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback