summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-09-15Refactor setIncomplete in quantifiers.ajreynol
2016-09-14Support for unique variable generation in node manager.ajreynol
2016-09-14Lemma cache in theory sep. Minor optimization for sets. Minor improvements to...ajreynol
2016-09-13Minor changes to sep logic, epr, quantifier splitting.ajreynol
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-12Prefer non-cardinality constants in term models for sep logic.ajreynol
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry b...ajreynol
2016-09-09Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.ajreynol
2016-09-09Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a...ajreynol
2016-09-08Refactor seplog preprocess. Handle case where sep data type cannot be inferred.ajreynol
2016-09-03Miniscope top level conjunctions for prenex normal form, allow one level mini...ajreynol
2016-09-03Option for prenex normal formajreynol
2016-09-01Merge pull request #91 from timothy-king/no-throwTim King
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options change...ajreynol
2016-09-01Cleanup quantifier elimination in smt engine.ajreynol
2016-09-01Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier...ajreynol
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-08-31Removing the forward declaration of QuantInfo from rewrite_engine.h.Tim King
2016-08-31Cleaning up the dead FORIT macros.Tim King
2016-08-31Removing the usage of typeof from theory_sets_private.Tim King
2016-08-31Beautifying theory_model.h.Tim King
2016-08-31Removing BOOST_FOREACH from theory/sets/scrutinize.h.Tim King
2016-08-31Removing typeof from sets normal form and beautifying the file.Tim King
2016-08-31Removing typeof from command_executor_portfolio.cpp.Tim King
2016-08-31Removing typeof from didyoumean.cpp.Tim King
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
2016-08-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-08-25Options for counterexample guided instantiation.ajreynol
2016-08-19Fixed two bugsClark Barrett
2016-08-19Added fitsSignedLong and fitsUnsignedLongClark Barrett
2016-08-16Initial infrastructure for ExtTheory, generalize extended term handling in Th...ajreynol
2016-08-15Expression sharing on demand in LFSC (replace definitionally equivalent child...ajreynol
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for bounde...ajreynol
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ...ajreynol
2016-08-12Merge pull request #90 from 4tXJ7f/fewer_preproc_holesguykatzz
2016-08-11Add support for fewer preprocessing holesAndres Notzli
2016-08-11Minor change to strings, introduce proxy vars only when necessary.ajreynol
2016-08-10Improvements to strings: work on propagations for reverse normal form process...ajreynol
2016-08-09Merge pull request #89 from 4tXJ7f/fix_proof_spacesguykatzz
2016-08-09Fixes for sep star rewrite.ajreynol
2016-08-09Fix missing/redundant spaces in proofsfix_proof_spacesAndres Notzli
2016-08-05Merge pull request #88 from 4tXJ7f/fix_commentsguykatzz
2016-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
2016-08-03Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.Guy
2016-08-03Merge pull request #87 from 4tXJ7f/fix_oob_accessbarrettcw
2016-07-30Prioritize inferences when processing normal forms in strings.ajreynol
2016-07-28The "aggressive" optimizer for lemma L now returns the conjunction of all lem...Guy
2016-07-28Merge branch 'master' of https://github.com/CVC4/CVC4Guy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback