summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
AgeCommit message (Expand)Author
2017-10-27Refactor theory model (#1236)Andrew Reynolds
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-02Add 5 FP kinds for partial to total fn conversion (#1128)Martin
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-18Floating point symfpu support (#1103)Martin
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
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-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-06-21Properly handle subtypes in smt2 printer.ajreynol
2017-05-30print only labeled assertions as part of the unsat coreguykatzz
2017-05-25Quote unsat core names if applicable, fixes bug 816.ajreynol
2017-04-20Minor fixes.ajreynol
2017-04-14Fix nullary operator printers, minor.ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-03-16Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ...ajreynol
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...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-22Fix smt2 and cvc printers for testers when output and input languages are dif...ajreynol
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-20Infrastructure for storing and printing heap models for separation logic. Ens...ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-04-20update from the masterPaulMeng
2016-04-15change transitive closure operator name to TCLOUSREPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
2016-02-15Merge remote-tracking branch 'origin/master'PaulMeng
2016-02-15extended smt parser for the finite relationsPaulMeng
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-10-15Change semantics of str.substr to allow endpoint out of bounds, and return em...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-30fix smt2 parameterized sort printingKshitij Bansal
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-03-28printer change for string smtlib2Tianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback