summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2016-09-29Minor cleanup and additions to quantifiers statistics.ajreynol
2016-09-28Fix the merge of kbansal/card branch (2039eab).Kshitij Bansal
A bug was introduced in the cleanup process as preparation for the merge (theory_sets_private.cpp, lines 2502-2508 in this commit).
2016-09-27Reverting part of the previous changes to unconstrained simplifier.Tim King
2016-09-26Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.Tim King
2016-09-25Deleting the eager bitblasting solver if present in TheoryBV.Tim King
2016-09-25Adding a destructor to QuantAntiSkolem.Tim King
2016-09-25Adding a destructor to TermDb.Tim King
2016-09-25Adding a destructor to CegqiOutputSingleInv.Tim King
2016-09-25Deleting optional members of StrongSolverTheoryUF.Tim King
2016-09-25Disambiguating a vector insert warning coming from coverity scan.Tim King
2016-09-25Deleting a temporary in theory sets enumerator.Tim King
2016-09-25Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.Tim King
2016-09-25Removing an unused iterator.Tim King
2016-09-25Fixing a potential use after free coming from a pop_back() call invalidating ↵Tim King
strictly earlier entries.
2016-09-21Remove duplicate code from my last commitajreynol
2016-09-20Refactor, separate theory-specific counterexample-guided instantiation.ajreynol
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-18Minor fix for stringsajreynol
2016-09-16In a ROW guard proof, if the transitivity proof does not have a disequality, ↵guykatzz
we can deduce that it is a constant-disequality proof and process it accordingly
2016-09-16Merge branch 'master' of https://github.com/CVC4/CVC4guykatzz
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-16Handling a corner case where a ROW's guard is a constant disequality.Guy
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
2016-09-16More refactoring of cbqi, start developing new interface.ajreynol
2016-09-15Further refactor cbqi.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by ↵ajreynol
default in EPR mode.
2016-09-15Make sep pto a trigger kind, track in equality engines and term database.ajreynol
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 ↵ajreynol
to EPR
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 ↵ajreynol
breaking in theory sep.
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 ↵ajreynol
allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
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 ↵ajreynol
miniscoping in prenex normal form.
2016-09-03Option for prenex normal formajreynol
2016-09-01Merge pull request #91 from timothy-king/no-throwTim King
Relaxing the throw specifiers for the destructors for Node, TypeNode,…
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options ↵ajreynol
changes for cbqi.
2016-09-01Cleanup quantifier elimination in smt engine.ajreynol
2016-09-01Updates 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-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the ↵Tim King
context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback