| 2012-05-27 |
Dejan Jovanović | Committing the work on equality engine, I need to see... |
commit | commitdiff | tree |
| 2012-05-27 |
Clark Barrett | Another expensive function call in a Debug trace |
commit | commitdiff | tree |
| 2012-05-27 |
Clark Barrett | Another expensive function call in a Debug line |
commit | commitdiff | tree |
| 2012-05-25 |
Kshitij Bansal | init bug fix |
commit | commitdiff | tree |
| 2012-05-25 |
Clark Barrett | Checking in fix for bug 340 - somehow didn't get checke... |
commit | commitdiff | tree |
| 2012-05-24 |
Dejan Jovanović | Separating the subtheory implementations in the bitvect... |
commit | commitdiff | tree |
| 2012-05-24 |
Dejan Jovanović | Significant changes to the internals of the equality... |
commit | commitdiff | tree |
| 2012-05-22 |
Tim King | This commit merges in the branch arithmetic/cprop. |
commit | commitdiff | tree |
| 2012-05-21 |
Dejan Jovanović | Updating equality manager to handle tagged trigger... |
commit | commitdiff | tree |
| 2012-05-21 |
Morgan Deters | main() no longer catches non-CVC4 exceptions. This... |
commit | commitdiff | tree |
| 2012-05-19 |
Tim King | Adding regress test for bug 341. |
commit | commitdiff | tree |
| 2012-05-19 |
Tim King | - The array type rules were fixed to use isSubtypeOf. |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | Removing long unsigned operator+ from CDList's const_it... |
commit | commitdiff | tree |
| 2012-05-18 |
Dejan Jovanović | removing failing regression |
commit | commitdiff | tree |
| 2012-05-17 |
Tim King | This fixes a fascinating segfault. This is the sequenc... |
commit | commitdiff | tree |
| 2012-05-17 |
Morgan Deters | Fixing an issue with LogicInfo::isPure() that turned... |
commit | commitdiff | tree |
| 2012-05-17 |
Liana Hadarean | Fixed bug 338: |
commit | commitdiff | tree |
| 2012-05-17 |
Tim King | Adding failing regression for ite type computation. |
commit | commitdiff | tree |
| 2012-05-17 |
Dejan Jovanović | Queueing up asserted literals in the proxy instead... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | adding simple-minded handling of (dis-)equalities where... |
commit | commitdiff | tree |
| 2012-05-16 |
Morgan Deters | Fixing C compatibility library (it still had a referenc... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | testcase for bug 337 |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | Changes to SAT solver: |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | equality status for bitvectors can now look into the... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | removing duplicate literals in explanations of propagations |
commit | commitdiff | tree |
| 2012-05-16 |
Liana Hadarean | refactored TheoryBV bitblaster and equality engine... |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | fixed QF_BV performance problem due to using CDList... |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | test cases |
commit | commitdiff | tree |
| 2012-05-15 |
Tim King | Fix to shared terms visitor. |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Implement TypeNode::isComparableTo() and add a unit... |
commit | commitdiff | tree |
| 2012-05-15 |
Clark Barrett | Fixed several bugs in shared terms database |
commit | commitdiff | tree |
| 2012-05-15 |
Tim King | This commit removes the CONST_INTEGER kind from nodes... |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaste... |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | removing all extended commands (as inspired by the... |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Fix QF_AUFLIA (resolves bug #331). |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | fixing warnings, grr |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | several bug fixes: in TheoryBV::NotifyClass missing... |
commit | commitdiff | tree |
| 2012-05-14 |
Dejan Jovanović | fixes for shared term registration. previously the... |
commit | commitdiff | tree |
| 2012-05-14 |
Clark Barrett | Fixed assertion failures in array theory |
commit | commitdiff | tree |
| 2012-05-14 |
Morgan Deters | in debug builds, -d can be used for trace tags that... |
commit | commitdiff | tree |
| 2012-05-14 |
Dejan Jovanović | fixing up preregistration again |
commit | commitdiff | tree |
| 2012-05-13 |
Dejan Jovanović | fixing build warnings |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix regex in Debug_tags and Trace_tags generation for... |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | fix typo in sed line |
commit | commitdiff | tree |
| 2012-05-11 |
Morgan Deters | output a warning message when a function type (or datat... |
commit | commitdiff | tree |
| 2012-05-11 |
Clark Barrett | Disabled arith-rewrite-equalities by default unless... |
commit | commitdiff | tree |
| 2012-05-11 |
Clark Barrett | Added some ITE rewrites, |
commit | commitdiff | tree |
| 2012-05-11 |
Tim King | Partially fixes something-like-a-problem with TheoryAri... |
commit | commitdiff | tree |
| 2012-05-10 |
Tim King | Removing now unneeded (as of r3425) typenames from... |
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | fix an issue which breaks language bindings (so this... |
commit | commitdiff | tree |
| 2012-05-09 |
Morgan Deters | --disable-tracing at configure time now disables Trace... |
commit | commitdiff | tree |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
commit | commitdiff | tree |
| 2012-05-09 |
Kshitij Bansal | rm something for a future merge that sneaked in |
commit | commitdiff | tree |
| 2012-05-09 |
Kshitij Bansal | Merge from decision branch (ITE support) |
commit | commitdiff | tree |
| 2012-05-09 |
Dejan Jovanović | Fixing the debug tags generation and related methods... |
commit | commitdiff | tree |
| 2012-05-08 |
Liana Hadarean | Merging in bvprop branch, with proper bit-vector propag... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixing a bug with TheoryArith::ppAssert() and shared... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixes a sign bug in the DioSolver. |
commit | commitdiff | tree |
| 2012-05-04 |
Clark Barrett | Guard for expensive Debug trace |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | options: fail if the debug or trace tag specified doesn... |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | fix: getNumTraceTags, getNumDebugTags |
commit | commitdiff | tree |
| 2012-05-04 |
Tim King | - This fixes a problem where simplex produced the same... |
commit | commitdiff | tree |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
commit | commitdiff | tree |
| 2012-05-02 |
Clark Barrett | Changing d_sharedTermsExist to logicInfo.isSharingEnabled() |
commit | commitdiff | tree |
| 2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | New LogicInfo functionality. |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | require boost library (but not the threading support... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | undo, again |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | undo previous commit (as it will break a number of... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | fix parser logic-handling oversights: QF_UFBV should... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | break dependence on zlib-dev for now |
commit | commitdiff | tree |
| 2012-04-27 |
Clark Barrett | Fixed warning in decision_engine.h, minor tweak to... |
commit | commitdiff | tree |
| 2012-04-27 |
Tim King | This merges in the branch cvc4/branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | portfolio driver: respect parseOnly option |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | fix for de+lemmas |
commit | commitdiff | tree |
| 2012-04-24 |
Tim King | This commit merges in the branch branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-23 |
Kshitij Bansal | Merge from decision branch -- partially working justifi... |
commit | commitdiff | tree |
| 2012-04-20 |
Clark Barrett | Updates to array theory - much more lazy about introduc... |
commit | commitdiff | tree |
| 2012-04-19 |
Tim King | In the constructor of DecisionEngine, there were 2... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | add the missing BINARY variable in some test/regress... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | cout -> warning. Happening in portfolio |
commit | commitdiff | tree |
| 2012-04-18 |
Dejan Jovanović | disabling the problematic pragma in node_manager.h... |
commit | commitdiff | tree |
| 2012-04-17 |
Dejan Jovanović | Fix for thos annoying "array index" warnings in product... |
commit | commitdiff | tree |
| 2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
commit | commitdiff | tree |
| 2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
commit | commitdiff | tree |
| 2012-04-14 |
Clark Barrett | Fixed bug in sharing with arrays of different types |
commit | commitdiff | tree |
| 2012-04-13 |
Morgan Deters | Fix SExpr name qualification for swig, and #include... |
commit | commitdiff | tree |
| 2012-04-12 |
Morgan Deters | svn ignore Makefile.in for aufbv regression directory |
commit | commitdiff | tree |
| 2012-04-12 |
Tim King | Adds an operator<< to SExpr::SexprTypes. This fixes... |
commit | commitdiff | tree |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
commit | commitdiff | tree |
| 2012-04-06 |
François Bobot | * Smt2 printer for datatypes |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | fix distributed builds (and therefore the Debian nightl... |
commit | commitdiff | tree |
| 2012-04-06 |
Dejan Jovanović | processing assertions in bit-vectors even when in fullc... |
commit | commitdiff | tree |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog