summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-06-27Fix minor warnings found by recent clang/gcc.Morgan Deters
2013-06-27Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don'...Morgan Deters
2013-06-27Better user documentation for mkVar() and mkBoundVar().Morgan Deters
2013-06-07Fix for bug 517.Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-29Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unkno...Morgan Deters
2013-05-20Fix destruction issue in GetValueCommand leading to crash.Morgan Deters
2013-05-20A couple of fixes to the get-option command for compliance with SMT-LIB.Morgan Deters
2013-05-20minor changes to language bindingsMorgan Deters
2013-05-01Comment out some debug-related things in attribute code, no longer neededMorgan Deters
2013-04-23Theory "alternates" supportMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
2013-03-27some Java bindings fixes (fixes Debian build problems)Morgan Deters
2013-03-27Merge branch 'master' into bv-corelianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21Add the ability to "mute" commands, needed for SMT-LIB compliance.Morgan Deters
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14Fix warning (line annotation)Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-03-13post failed attempts at getting the incremental solver to worklianah
2013-03-06more slicer changes for incrementallianah
2013-02-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
2013-02-07Make --default-dag-thresh apply to stringstreamsMorgan Deters
2013-02-05Merge branch '1.0.x'Morgan Deters
2013-02-05Fix a compiler warning in NodeBuilderMorgan Deters
2013-02-05remove now-unnecessary wrappers from Type interfaceMorgan Deters
2013-02-04Merge branch '1.0.x'Morgan Deters
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan Deters
2013-02-01Merge branch '1.0.x'Morgan Deters
2013-02-01Fix a tuple attribute bug that was causing model-generation problems for tuplesMorgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2012-12-01fix to TNode assertion (which is too strict, given lax ordering requirements ...Morgan Deters
2012-12-01remove instantiator frameworkMorgan Deters
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
2012-12-01fix memory corruption issue in debug builds that led to unhelpful outputMorgan Deters
2012-12-01fix #line annotation warningMorgan Deters
2012-11-30Updating the combination.cpp example.Tim King
2012-11-30change detection/handling of output language more reasonably; fixes a nagging...Morgan Deters
2012-11-29minor documentation fixMorgan Deters
2012-11-29Hack to support global variables for CVC language extended to export mechanism.Kshitij Bansal
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback