summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2017-09-28Cegqi refactor prep bv (#1155)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-27Minor fixes for partial quantifier elimination. (#1147)Andrew Reynolds
2017-09-27CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)Aina Niemetz
2017-09-26Fix type checking of to_real (#1127)Martin Brain
2017-09-26Improve FP rewriter: const folding, other (#1126)Martin Brain
2017-09-26Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)Tim King
2017-09-25Cegqi refactor substitutions (#1129)Andrew Reynolds
2017-09-25Fix bug related to sort inference + subtypes. (#1125)Andrew Reynolds
2017-09-25Fixing CID 1362917: There was a branch where d_issup was not initialized. Swi...Tim King
2017-09-25Fixing CID 1362895: Initializing d_bvp to nullptr. (#1137)Tim King
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-20Extend quantifier-free UF solver to higher-order. This includes an ex… (#1100)Andrew Reynolds
2017-09-19Add FP type enumerator and cardinality computer (#1104)Martin
2017-09-19Refactor cegqi instantiation infrastructure so that it is more independent of...Andrew Reynolds
2017-09-14Make floating-point comparison operators chainable (#1101)Martin
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
2017-09-13Floating point symfpu support (#1093)Martin
2017-09-13Add new kinds required for higher-order. (#1083)Andrew Reynolds
2017-09-13Add isConst check for lambda expressions. (#1084)Andrew Reynolds
2017-09-13Modify equality engine to allow operators to be marked as external terms (#1082)Andrew Reynolds
2017-09-12Initial infrastructure for BV instantiation via word-level inversions. (#1056)Andrew Reynolds
2017-09-11Adding reasonable breaks in switch statement in TheoryStrings::normalizeRegex...Tim King
2017-09-11Addressing a coverity scan complaint in theory_strings.cpp. I believe the roo...Tim King
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-09-07Properly handle user cardinality constraints for uf-ss=none. (#1068)Andrew Reynolds
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
2017-08-31Replace CVC4_THREADLOCAL in interactive_shell (#1065)Andres Noetzli
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
2017-08-30Fix model construction for parametric types (#1059)Andrew Reynolds
2017-08-24Merge pull request #191 from timothy-king/cleanup-regexpAndrew Reynolds
2017-08-23Fix typosAndres Noetzli
2017-08-23Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)Tim King
2017-08-21Cleanup: use Assert rather than C assert. (#1052)Aina Niemetz
2017-08-17Remove unused SubrangeBound(s) classes (#221)Andres Noetzli
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-08-14Move function defns from smt_engine_scope.h to cpp (#216)Andres Noetzli
2017-08-11Fix compiler warnings in theory/arith/nonlinear_extension.cppAina Niemetz
2017-08-11Maintain frontier for tangent planes.ajreynol
2017-08-09Remove AigBitblaster implementation if ABC is not compiled (#212)Mathias Preiner
2017-08-09Fix Assertion (compiler warning) in theory/bv/theory_bv.cppAina Niemetz
2017-08-08Use cache for datatypes cycle check, add regression.ajreynol
2017-08-07Fix compiler warning in theory/quantifiers/term_database_sygus.cppAina Niemetz
2017-08-07Change sygus output for failed reconstruction case.ajreynol
2017-07-31Minor improvement for enumerative instantiation.ajreynol
2017-07-29Change remaining hash_set -> unordered_set (#208)Andres Noetzli
2017-07-29Add support for charat in native language, minor cleanup.ajreynol
2017-07-28Fix cache issues for cyclic string equations.ajreynol
2017-07-22Deprecating the unused convenience_node_builders.h (#203)Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback