summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2018-06-01Formatajreynol
2018-05-31More simplifyajreynol
2018-05-31Simplify beta reduction.ajreynol
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-04-30Remove subsort symmetry breaking (#1807)Andrew Reynolds
2018-04-10Properly implement function extensionality based on cardinality (#1765)Andrew Reynolds
2018-04-09Fix higher-order term indexing. (#1754)Andrew Reynolds
2018-03-25Cleanup various exit calls (#1692)Andrew Reynolds
2018-03-23Remove unused code (#1700)Andrew Reynolds
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-13Initializes TriggerInfo::polarity. Resolves CID 1172054. (#1358)Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback