projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2012-06-14 Kshitij Bansaladd passing regression commit | commitdiff | tree
2012-06-14 Dejan Jovanovićchanging to a more natural propagation order in uf... commit | commitdiff | tree
2012-06-14 Dejan Jovanovićsome changes to the uf engine commit | commitdiff | tree
2012-06-14 Tim KingBrings the tuning branch into trunk. This includes... commit | commitdiff | tree
2012-06-14 Morgan Detersbug 346 resolved commit | commitdiff | tree
2012-06-14 Dejan Jovanović* removing rewriteEquality from the rewriter commit | commitdiff | tree
2012-06-13 Dejan Jovanovićremoving bug233 until morgan commits the actual file commit | commitdiff | tree
2012-06-13 Morgan Detersadding some regressions to the usual regressions runs... commit | commitdiff | tree
2012-06-13 Tim KingAdded witnesses to Constraints. commit | commitdiff | tree
2012-06-13 Tim King- Added a loop to internally assert constraints that... commit | commitdiff | tree
2012-06-13 Tim KingFixed whitespace warning on Makefile. commit | commitdiff | tree
2012-06-13 Tim KingAdds debugging output to theory_engine.cpp. commit | commitdiff | tree
2012-06-13 Morgan Detersrevisions to the "make submission" target commit | commitdiff | tree
2012-06-13 Morgan DetersDon't use the "inlined" feature of ANTLR 3.2, which... commit | commitdiff | tree
2012-06-13 Kshitij Bansaladd passing regression commit | commitdiff | tree
2012-06-13 Dejan Jovanovićfix for bug 354 commit | commitdiff | tree
2012-06-13 Clark BarrettFixed failing assertion when EqualityEngine is in conflict commit | commitdiff | tree
2012-06-13 Dejan Jovanovićenabling regressions from last night, all fixed commit | commitdiff | tree
2012-06-13 Kshitij Bansalenable some decision regressions commit | commitdiff | tree
2012-06-13 Kshitij BansalMake d_result in DE context dependent commit | commitdiff | tree
2012-06-13 Clark BarrettFixed definition of bvsmod commit | commitdiff | tree
2012-06-13 Kshitij Bansaldecision regressions, all but one fail commit | commitdiff | tree
2012-06-13 Clark BarrettFixes more problems in bv rewrites commit | commitdiff | tree
2012-06-13 Dejan Jovanović!(*child_it).isConst() assertion fail commit | commitdiff | tree
2012-06-13 Dejan Jovanovićr2.node == response.node failure commit | commitdiff | tree
2012-06-13 Dejan Jovanovićr2.node == response.node failure commit | commitdiff | tree
2012-06-13 Dejan Jovanović!current[0].isConst() failure commit | commitdiff | tree
2012-06-13 Clark BarrettFixes lots of problems in bv rewrite rules and adds... commit | commitdiff | tree
2012-06-13 Dejan Jovanovićbenchmark to show that we don't rewrite bvsmod correctly commit | commitdiff | tree
2012-06-12 Morgan DetersFix some compile warnings (but they never showed up... commit | commitdiff | tree
2012-06-12 Morgan DetersFix to SMT-LIBv1 parser: QF_UF declares sort "U", but... commit | commitdiff | tree
2012-06-12 Dejan Jovanovićmissing problems commit | commitdiff | tree
2012-06-12 Dejan Jovanovićwrong answer for bv commit | commitdiff | tree
2012-06-12 Clark BarrettMoved some things around in the preprocessor. Now... commit | commitdiff | tree
2012-06-12 Clark BarrettFixed fuzzing bug commit | commitdiff | tree
2012-06-12 Tim KingFix to yesterday's change in arithmetic. commit | commitdiff | tree
2012-06-12 Kshitij Bansalbv reduced with decision: sat instead of unsat commit | commitdiff | tree
2012-06-12 Kshitij BansalAssert fail equaility_engine.cpp: hasTerm(node) with... commit | commitdiff | tree
2012-06-12 Dejan Jovanovićbufixes and the bugs commit | commitdiff | tree
2012-06-12 Dejan Jovanovićconflicts from theories are removable commit | commitdiff | tree
2012-06-12 Clark BarrettChanged bitvector theory rewriter so that equalities... commit | commitdiff | tree
2012-06-12 Kshitij Bansalcleanup of exit mechanism when decisionEngine is on... commit | commitdiff | tree
2012-06-12 Clark BarrettFixed bug causing QF_LIA/solver_cvc4/incorrect1.smt... commit | commitdiff | tree
2012-06-12 Clark BarrettFixed failing assertion in arrays for bug 347 commit | commitdiff | tree
2012-06-12 Dejan Jovanovićmore breakage in aufbv commit | commitdiff | tree
2012-06-12 Morgan Detersminor cleanup, and replace a "private:" in equality... commit | commitdiff | tree
2012-06-12 Clark BarrettFixed compile error commit | commitdiff | tree
2012-06-12 Clark BarrettEnabling constant propagation commit | commitdiff | tree
2012-06-12 Morgan Detersfix a few compatibility bindings issues commit | commitdiff | tree
2012-06-12 Dejan Jovanovićwrong answer benchmarks commit | commitdiff | tree
2012-06-12 Dejan Jovanovićwrong result benchmark commit | commitdiff | tree
2012-06-12 Dejan Jovanovićtests for the commit | commitdiff | tree
2012-06-12 Dejan Jovanovićtest cases for the commit | commitdiff | tree
2012-06-12 Clark BarrettAdding constant propagation code - needs more testing... commit | commitdiff | tree
2012-06-12 Tim KingAdding incorrect qf_lia result. commit | commitdiff | tree
2012-06-12 Morgan Detersfix ordering issue of --dump-to and --default-dag-thres... commit | commitdiff | tree
2012-06-11 Tim KingFix to term normalization of integer equalities. Adds... commit | commitdiff | tree
2012-06-11 Tim KingFixing type comparision assertion in getEqualityStatus(). commit | commitdiff | tree
2012-06-11 Dejan Jovanovićanother benchmark that used to fail commit | commitdiff | tree
2012-06-11 Dejan Jovanovićfixing bitvector bugs commit | commitdiff | tree
2012-06-11 Morgan Detersmark a quantifiers global var as "static" so we can... commit | commitdiff | tree
2012-06-11 Clark BarrettOK, now the rewrite issues are fixed commit | commitdiff | tree
2012-06-11 Morgan Detersdistribute an .expect file. fixes a "make check" failu... commit | commitdiff | tree
2012-06-11 Morgan DetersMerge from quantifiers2-trunkmerge branch. commit | commitdiff | tree
2012-06-11 Clark BarrettFix for array bug with decision heuristic commit | commitdiff | tree
2012-06-11 Morgan Detersfix issue referred to in bug 352 regarding infinite... commit | commitdiff | tree
2012-06-11 Dejan Jovanovićfailing bv examples commit | commitdiff | tree
2012-06-11 Clark BarrettFixed bug 352 commit | commitdiff | tree
2012-06-11 Dejan Jovanovićsome failing examples commit | commitdiff | tree
2012-06-10 Clark BarrettFixed one more bug in rewriter commit | commitdiff | tree
2012-06-10 Clark BarrettAdded a very fruitful assertion to the rewriter: checks... commit | commitdiff | tree
2012-06-10 Dejan Jovanovićadding an assertion to trigger the problem of bug349... commit | commitdiff | tree
2012-06-10 Dejan Jovanovićfixes for bug347 commit | commitdiff | tree
2012-06-09 Clark BarrettTurning on unconstrained simp for QF_AUFBV commit | commitdiff | tree
2012-06-09 Morgan DetersCleanup and comments for the dag-ifier. Also some... commit | commitdiff | tree
2012-06-09 Morgan DetersDagification of output expressions. commit | commitdiff | tree
2012-06-08 Morgan DetersThe option --arith-presolve-lemmas had previously been... commit | commitdiff | tree
2012-06-08 Morgan DetersExtend Printer infrastructure also to the "Result"... commit | commitdiff | tree
2012-06-08 Morgan Detersminor fixes, for Mac OS commit | commitdiff | tree
2012-06-08 Dejan Jovanovićvery small fast example for the bv fail commit | commitdiff | tree
2012-06-08 Morgan DetersFix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri... commit | commitdiff | tree
2012-06-08 Kshitij Bansalhandle BitVectorSignExtend in pickler commit | commitdiff | tree
2012-06-08 Kshitij Bansalthreadlocal commit | commitdiff | tree
2012-06-08 Kshitij BansalMerge from decision branch (till r3663) commit | commitdiff | tree
2012-06-08 Dejan Jovanovićsmall fuzz examples where bv fails commit | commitdiff | tree
2012-06-07 Dejan Jovanovićfixing the wrong results. arrays equality adaptor had... commit | commitdiff | tree
2012-06-07 Morgan DetersLogicInfo locking implemented, and some initialization... commit | commitdiff | tree
2012-06-07 Clark BarrettFixed performance issue with ite_simplifier on some... commit | commitdiff | tree
2012-06-07 Morgan DetersAdding EchoCommand and associated printer and parser... commit | commitdiff | tree
2012-06-07 Dejan Jovanovićcleaning up the expample for the future commit | commitdiff | tree
2012-06-07 Clark BarrettAdded small test case for diseq propagation commit | commitdiff | tree
2012-06-07 Dejan Jovanovićfixing some bugs in propagation of disequalities commit | commitdiff | tree
2012-06-06 Clark BarrettDon't ever call nonclausalSimplify if simplificationMod... commit | commitdiff | tree
2012-06-06 Clark BarrettFixed assertion failures commit | commitdiff | tree
2012-06-06 Morgan Detersremoving std::cout from trunk commit | commitdiff | tree
2012-06-06 Morgan Detersalso remove now-incorrect comment from makefile commit | commitdiff | tree
2012-06-06 Clark BarrettFixed broken test case, removed one that is a mistake commit | commitdiff | tree
2012-06-06 Morgan Detersunconstrained regressions are now run with "make check... commit | commitdiff | tree
2012-06-06 Morgan DetersFixing numerous issues with tests and "make dist": commit | commitdiff | tree
2012-06-06 Dejan Jovanovićdisabling a super-expensive assertions to speed up... commit | commitdiff | tree
next