projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2012-06-06 Dejan JovanovićChanges to the combination mechanism, lots of details... commit | commitdiff | tree
2012-06-06 Clark BarrettFixed problem causing crash at destruction time commit | commitdiff | tree
2012-06-05 Clark BarrettMore clean-up commit | commitdiff | tree
2012-06-05 Clark BarrettFixed a performance issue with unconstrained simplifier commit | commitdiff | tree
2012-06-05 Clark BarrettAdding missing files... commit | commitdiff | tree
2012-06-04 Clark BarrettAdded preprocessing pass that propagates unconstrained... commit | commitdiff | tree
2012-06-01 Morgan Detersadd a global user-context push/pop in smt engine, just... commit | commitdiff | tree
2012-05-31 Clark BarrettFixed bug in bv: one more case where non-shared equalit... commit | commitdiff | tree
2012-05-31 Morgan Deterssvn:ignore a parallel-tests driver file that automake... commit | commitdiff | tree
2012-05-31 Morgan Deterspass JAVA_CPPFLAGS properly commit | commitdiff | tree
2012-05-30 Clark BarrettAdded BitwiseEq bitvector rewrite commit | commitdiff | tree
2012-05-30 Clark BarrettFixed problem with array queue growing too large commit | commitdiff | tree
2012-05-30 Morgan Detersremove unused/broken check build target commit | commitdiff | tree
2012-05-29 Morgan Detersremoving now-unused TheoryEngine::setLogic() interface... commit | commitdiff | tree
2012-05-29 Clark BarrettEnabled SolveEq bv rewrite commit | commitdiff | tree
2012-05-28 Clark BarrettAdded some BV rewrites, fixed bugs in array theory... commit | commitdiff | tree
2012-05-27 Dejan Jovanovićsome reordering to keep invariants commit | commitdiff | tree
2012-05-27 Dejan JovanovićCommitting the work on equality engine, I need to see... commit | commitdiff | tree
2012-05-27 Clark BarrettAnother expensive function call in a Debug trace commit | commitdiff | tree
2012-05-27 Clark BarrettAnother expensive function call in a Debug line commit | commitdiff | tree
2012-05-25 Kshitij Bansalinit bug fix commit | commitdiff | tree
2012-05-25 Clark BarrettChecking 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 KingThis 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 Detersmain() no longer catches non-CVC4 exceptions. This... commit | commitdiff | tree
2012-05-19 Tim KingAdding 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 KingThis commit adds TypeNode::leastCommonTypeNode(). ... commit | commitdiff | tree
2012-05-18 Tim KingThis commit removes the dead psuedoboolean code. commit | commitdiff | tree
2012-05-18 Tim KingRemoving long unsigned operator+ from CDList's const_it... commit | commitdiff | tree
next