summaryrefslogtreecommitdiff
path: root/src/expr/node_builder.h
AgeCommit message (Expand)Author
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2014-07-01Update copyrights.Morgan Deters
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-06-27Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don'...Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-02-05Fix a compiler warning in NodeBuilderMorgan Deters
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan Deters
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
2011-10-28* ability to output NodeBuilders without first converting them to Nodes---use...Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's m...Morgan Deters
2011-06-30some things I had laying around in a directory but never got committed; minor...Morgan Deters
2011-06-06Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on...Morgan Deters
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan Deters
2010-10-28Changing NodeBuilder::debugCheckType() to maybeCheckType()Christopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-09-21Rm'ing automatic type check in NodeBuilder for vars/constantsChristopher L. Conway
2010-09-21Moving automatic type check to NodeBuilder (Fixes: #199)Christopher L. Conway
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-09-02"Leftist NodeBuilders" are now supported.Morgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
2010-07-02* Added white-box TheoryEngine test that tests the rewriterMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-06-03* Added NodeBuilder<>::getChild() to make interface more consistentMorgan Deters
2010-06-01Fixed a bug in partial_model.cpp where the data was immediately deallocated b...Tim King
2010-04-26Adding the intermediary TypeNode to represent (and separate) the Types at the...Dejan Jovanović
2010-04-15Implementing missing NodeBuilder::constructNodeChristopher L. Conway
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-14* Better dependency tracking for unit test building and linking, andMorgan Deters
2010-04-04* Addressed issues brought up in Chris's review of Morgan'sMorgan Deters
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-03-30Highlights of this commit are:Morgan Deters
2010-03-12* src/context/cdmap.h: rename orderedIterator to iterator, do awayMorgan Deters
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
2010-03-08Fixing Debug("prop") => Debug("node") typoDejan Jovanović
2010-03-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback