summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-10-27Refactor theory model (#1236)Andrew Reynolds
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
2017-10-20SyGuS term size limit (#1262)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-02Unify hash functions for pairs (#1161)Andres Noetzli
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
2017-09-13Add new kinds required for higher-order. (#1083)Andrew Reynolds
2017-09-13Modify equality engine to allow operators to be marked as external terms (#1082)Andrew Reynolds
2017-09-07Properly handle user cardinality constraints for uf-ss=none. (#1068)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, cbqi...ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-03-21Improve computeCareGraph functions to check shared term equality status once ...ajreynol
2017-03-03Fix for collectModelInfo related to finite types + preregistration. Generaliz...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-01-04Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor chan...ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + un...ajreynol
2016-10-02Removing the throw specifiers from theory_uf_type_rules.h.Tim King
2016-09-25Deleting optional members of StrongSolverTheoryUF.Tim King
2016-09-16Handling a corner case where a ROW's guard is a constant disequality.Guy
2016-09-01Relaxing the throw specifiers for the destructors for Node, TypeNode, the con...Tim King
2016-07-06A few proof bugs fixedGuy
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in...ajreynol
2016-05-20Improvements to theory combination + strings: do not return trivial care grap...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-04-03Removed the theory-specific merge reason types. Instead, added a mechanism fo...Guy
2016-03-28Minor cleanup from last commit (quant util, equality infer). Do not set fmfBo...ajreynol
2016-03-24Refactored the equality engine in order to remove theory-specific logic from ...Guy
2016-03-23squash-merge from proof branchGuy
2016-03-23Fixing two garbage collection issues in Region and SortModel.Tim King
2016-03-07Minor change to F-Length inference in strings. No internal tracking of cardin...ajreynol
2016-02-26Refactoring of inferences in strings. Add several options.ajreynol
2016-02-24Add entailment checks between length terms to reduce splitting in strings sol...ajreynol
2016-02-09Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to...ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-05Changing the way the equality engine explains disequalities.guykatzz
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Add SmtGlobals ClassTim King
2016-01-01Added propagation rule for array ext lemmas to aid proofsClark Barrett
2015-12-22Bug fix uf-ss-totality.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback