summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-03-19inequality reasoning works on small examples added to regressions (not ↵Liana Hadarean
incremental); currently disabled though
2013-03-19added the cpp file for the inequality graphLiana Hadarean
2013-03-19implementing more inequality graph stuff; work in progress doesn't compileLiana Hadarean
2013-03-18more work on inequality reasoning for bvlianah
2013-03-16started work on the inequality bv subtheorylianah
2013-03-13post failed attempts at getting the incremental solver to worklianah
2013-03-06more slicer changes for incrementallianah
2013-03-06Best heuristics for handling decision requests from arraysClark Barrett
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive ↵Andrew Reynolds
miniscoping option --ag-miniscope-quant, minor cleanup
2013-03-05Merge branch '1.0.x'Morgan Deters
Conflicts: src/smt/smt_engine.cpp
2013-03-05Bugfix for SmtEngine: proper unsubscribing for NodeManager eventsMorgan Deters
2013-03-01Merge branch '1.0.x'Morgan Deters
2013-02-26Bug fix for rep-set.Morgan Deters
(Cherry-picked from commit c71ec27 in master.)
2013-02-26Fix for quantifiers containing Boolean terms.Morgan Deters
2013-02-26Merge branch '1.0.x'lianah
2013-02-26Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.xlianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as ↵Andrew Reynolds
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-02-20Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.Morgan Deters
2013-02-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-02-18Fix for gitinfo (resolves bug 399).Morgan Deters
2013-02-16Merge branch '1.0.x'Kshitij Bansal
2013-02-16gitinfo modifications fixKshitij Bansal
2013-02-16Merge pull request #6 from kbansal/decNewoptionsKshitij Bansal
decision/ code refactoring
2013-02-16decision: jh: more refactoring (.h->.cpp, xor/iff)Kshitij Bansal
2013-02-16decision/ : jh: refactor embedded ITE, other minorKshitij Bansal
other minor: cleanup some remaning fragments of GiveUpException(), hopefully all is gone now.
2013-02-16decision/: justification: refactor ITE outKshitij Bansal
2013-02-16refactoring justification_heuristic codeKshitij Bansal
2013-02-16rm decision jh GiveUp related codeKshitij Bansal
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-16Merge branch '1.0.x'Morgan Deters
2013-02-16Fix version identification for new git repository.Morgan Deters
2013-02-16Fix typo in error messageMorgan Deters
2013-02-15Merge branch '1.0.x'Kshitij Bansal
2013-02-15prvs commit: lower warning to noticeKshitij Bansal
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
2013-02-15Merge branch '1.0.x'Kshitij Bansal
2013-02-15make incremental+portfolio experimentalKshitij Bansal
2013-02-15Merge pull request #5 from kbansal/1.0.xKshitij Bansal
make incremental+portfolio experimental
2013-02-15make incremental+portfolio experimentalKshitij Bansal
2013-02-15Merge branch '1.0.x'Morgan Deters
2013-02-15Fix builds/ links to survive configuring twice with different prefixesMorgan Deters
2013-02-15Fix ECHO command in CVC language parser to not output quotation marksMorgan Deters
2013-02-15Merge branch '1.0.x'Tim King
2013-02-15repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-02-14Merge pull request #4 from tiliang/masterDejan Jovanović
a bugfix in rewriting rules
2013-02-14Removing BVDebug and replacing with Debug.Tim King
2013-02-13repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
2013-02-13started working on incremental slicer - not compilinglianah
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-11undid the caching that actually hurt performancelianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback