summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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
2017-07-20Merge branch 'master' into cleanup-regexpTim King
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-17Merge branch 'master' into cleanup-regexpTim King
2017-07-17Use is_sorted, merge, copy from std (#199)Andres Noetzli
2017-07-14Removing BOOST_FOREACH usage.Tim King
2017-07-13Cleaning up the CVC4::String class.Tim King
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ...ajreynol
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-07-07Use new copyright header format.Mathias Preiner
2017-07-05Fix for logic info, update regressions. Update casc tfa script.ajreynol
2017-07-05Non-linear supported in ALL logics. Minor fixes for set logic with sygus.ajreynol
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, cbqi...ajreynol
2017-06-21Merge pull request #175 from CVC4/fix_uninitAndrew Reynolds
2017-06-18Fix assertionajreynol
2017-06-18Minor change to ensureTheoryAtoms for bug 828.ajreynol
2017-06-15Fix for bug 639.Clark Barrett
2017-06-15Fix for issue related to cbqi + E-matching.ajreynol
2017-06-15Fix relevant domain for datatypes, fixes bug 824.ajreynol
2017-06-15Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cb...ajreynol
2017-06-14Remove UdivSelf rewrite, add UdivZero rewriteAndres Noetzli
2017-06-14Fix uninitialized valueAndres Noetzli
2017-06-03Fix compile errorClark Barrett
2017-06-01Minor optimizations related to cbqi.ajreynol
2017-05-31Fix model construction for BV with cbqi. Minor change to defaults.ajreynol
2017-05-31Minor fix to last commit.ajreynol
2017-05-31Change to-int, div, int-div skolems from CDAttribute to stored in CDHashMap. ...ajreynol
2017-05-26Checking that equalities belong to the arithmetic theory in the solve() routine.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback