summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2014-10-16Fix clang warningsMorgan Deters
2014-10-16Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch...ajreynol
2014-10-16Use n-ary splits instead of binary splits in theory datatypes.ajreynol
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by CE...ajreynol
2014-10-14fix for memory leak in BVQuickChecklianah
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, a...Morgan Deters
2014-10-14amend prvs commitKshitij Bansal
2014-10-14trace decision-nodeKshitij Bansal
2014-10-13CEGQI uses model. Enforce fairness in CEGQI natively.ajreynol
2014-10-13Model building into quantifiers engine. Simplify axiom-inst mode.ajreynol
2014-10-13Refactor model builder from model engine to quant engine. Work on fairness s...ajreynol
2014-10-11Merge branch '1.4.x'Morgan Deters
2014-10-11Some defensive programming at destruction time, and fix a latent dangling poi...Morgan Deters
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti...Kshitij Bansal
2014-10-10CleanupMorgan Deters
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
2014-10-09Refactor quantifier prenex option. By default, do not pull quantifiers with ...ajreynol
2014-10-08Merge branch '1.4.x'Morgan Deters
2014-10-08Add unsat cores support to CVC native language.Morgan Deters
2014-10-08Some minor cleanup.Morgan Deters
2014-10-08Remove private header from public driver.Morgan Deters
2014-10-07Fix portoflio issues (debugging code was being called even when tag was off)Kshitij Bansal
2014-10-07Merge remote-tracking branch 'upstream/master' into sets-mergableKshitij Bansal
2014-10-07update default Sets optionsKshitij Bansal
2014-10-07whitespace fixesKshitij Bansal
2014-10-08Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep...ajreynol
2014-10-07add couple of statsKshitij Bansal
2014-10-07sets stronger equality propagatorKshitij Bansal
2014-10-07Refactor quantifiers attributes.ajreynol
2014-10-07define-const is an extended command, not permitted in strict mode.Morgan Deters
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. Than...Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.Morgan Deters
2014-10-06Some minor cleanup.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-06Print array constants in SMT-LIB models with new syntax.Morgan Deters
2014-10-06Clear out decls/defs with RESET command.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ...Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-10-03Support exporting array-store-all expressions to other ExprManagers (fixes po...Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks Christo...Morgan Deters
2014-10-03Improve error in CVC parser in presence of unrecognized command name.Morgan Deters
2014-10-03More array constants and parsing: better error messages, extend to CVC presen...Morgan Deters
2014-10-03Minor fixes to CVC printer.Morgan Deters
2014-10-03SMT-LIB parser support for array constants (Z3 syntax).Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback